unfold definitions in equality checking, plus cleanup

lib/Quox/Context.idr

@@ -15,7 +15,7 @@ import Control.Monad.Identity
 infixl 5 :<
 ||| a sequence of bindings under an existing context. each successive element
 ||| has one more bound variable, which correspond to all previous elements
-||| as well as the global context.
+||| as well as the surrounding context.
 public export
 data Telescope : (tm : Nat -> Type) -> (from, to : Nat) -> Type where
   Lin  : Telescope tm from from
@@ -26,7 +26,7 @@ public export
 Telescope' : (a : Type) -> (from, to : Nat) -> Type
 Telescope' a = Telescope (\_ => a)
 
-||| a global context is actually just a telescope over no existing bindings
+||| a top level context is actually just a telescope over no existing bindings
 public export
 Context : (tm : Nat -> Type) -> (len : Nat) -> Type
 Context tm len = Telescope tm 0 len

lib/Quox/Definition.idr

@@ -0,0 +1,52 @@
+module Quox.Definition
+
+import public Quox.Syntax
+import public Data.SortedMap
+import public Control.Monad.State
+
+
+public export
+record AnyTerm where
+  constructor T
+  def : forall d, n. Term d n
+
+public export
+record Definition where
+  constructor MkDef'
+  qty         : Qty
+  0 qtyGlobal : IsGlobal qty
+  type        : AnyTerm
+  term        : Maybe AnyTerm
+
+public export %inline
+MkDef : (qty : Qty) -> (0 qtyGlobal : IsGlobal qty) =>
+           (type, term : forall d, n. Term d n) -> Definition
+MkDef {qty, type, term} =
+  MkDef' {qty, qtyGlobal = %search, type = T type, term = Just (T term)}
+
+public export %inline
+MkAbstract : (qty : Qty) -> (0 qtyGlobal : IsGlobal qty) =>
+             (type : forall d, n. Term d n) -> Definition
+MkAbstract {qty, type} =
+  MkDef' {qty, qtyGlobal = %search, type = T type, term = Nothing}
+
+
+public export %inline
+(.type0) : Definition -> Term 0 0
+g.type0 = g.type.def
+
+public export %inline
+(.term0) : Definition -> Maybe (Term 0 0)
+g.term0 = map (\t => t.def) g.term
+
+public export %inline
+(.qtyP) : Definition -> Subset Qty IsGlobal
+g.qtyP = Element g.qty g.qtyGlobal
+
+public export %inline
+isZero : Definition -> Bool
+isZero g = g.qty == Zero
+
+public export
+Definitions : Type
+Definitions = SortedMap Name Definition

lib/Quox/Equal.idr

@@ -1,52 +1,72 @@
 module Quox.Equal
 
 import public Quox.Syntax
-import Control.Monad.Either
-import Generics.Derive
+import public Quox.Definition
+import public Quox.Typing
+import public Control.Monad.Either
+import public Control.Monad.Reader
+import Data.Maybe
 
-%default total
-%language ElabReflection
-
-
-public export
-data Mode = Equal | Sub
-%runElab derive "Mode" [Generic, Meta, Eq, Ord, DecEq, Show]
-
-public export
-data Error
-= ClashT Mode (Term d n) (Term d n)
-| ClashU Mode Universe Universe
-| ClashQ      Qty      Qty
 
 private %inline
-ClashE : Mode -> Elim d n -> Elim d n -> Error
+ClashE : EqMode -> Elim d n -> Elim d n -> Error
 ClashE mode = ClashT mode `on` E
 
-parameters {auto _ : MonadError Error m}
+public export
+CanEq : (Type -> Type) -> Type
+CanEq m = (MonadError Error m, MonadReader Definitions m)
+
+
+parameters {auto _ : CanEq m}
   private %inline
-  clashT : Mode -> Term d n -> Term d n -> m a
+  clashT : EqMode -> Term d n -> Term d n -> m a
   clashT mode = throwError .: ClashT mode
 
   private %inline
-  clashE : Mode -> Elim d n -> Elim d n -> m a
+  clashE : EqMode -> Elim d n -> Elim d n -> m a
   clashE mode = throwError .: ClashE mode
 
+  private %inline
+  defE : Name -> m (Maybe (Elim d n))
+  defE x = asks $ \defs => do
+    g <- lookup x defs
+    pure $ (!g.term).def :# g.type.def
+
+  private %inline
+  defT : Name -> m (Maybe (Term d n))
+  defT x = map E <$> defE x
+
+  export %inline
+  compareU' : EqMode -> Universe -> Universe -> Bool
+  compareU' = \case Equal => (==); Sub => (<=)
+
+  export %inline
+  compareU : EqMode -> Universe -> Universe -> m ()
+  compareU mode k l = unless (compareU' mode k l) $
+    throwError $ ClashU mode k l
+
   mutual
     private covering
-    compareTN' : Mode ->
+    compareTN' : EqMode ->
                  (s, t : Term 0 n) ->
                  (0 _ : NotRedexT s) -> (0 _ : NotRedexT t) -> m ()
 
-    compareTN' mode (TYPE k) (TYPE l) _ _ =
-      case mode of
-           Equal => unless (k == l) $ throwError $ ClashU Equal k l
-           Sub   => unless (k <= l) $ throwError $ ClashU Sub   k l
+    compareTN' mode (E e) (E f) ps pt = compareE0 mode e f
+    -- if either term is a def, try to unfold it
+    compareTN' mode s@(E (F x)) t ps pt = do
+      Just s' <- defT x  | Nothing => clashT mode s t
+      compareT0 mode s' t
+    compareTN' mode s t@(E (F y)) ps pt = do
+      Just t' <- defT y  | Nothing => clashT mode s t
+      compareT0 mode s t'
+    compareTN' mode s@(E _) t _ _ = clashT mode s t
+
+    compareTN' mode (TYPE k) (TYPE l) _ _ = compareU mode k l
     compareTN' mode s@(TYPE _) t _ _ = clashT mode s t
 
     compareTN' mode (Pi qty1 _ arg1 res1) (Pi qty2 _ arg2 res2) _ _ = do
-      -- [todo] this should probably always be ==, right..?
       unless (qty1 == qty2) $ throwError $ ClashQ qty1 qty2
-      compareT0  mode arg2 arg1 -- reversed for contravariant Sub
+      compareT0  mode arg2 arg1 -- reversed for contravariant domain
       compareTS0 mode res1 res2
     compareTN' mode s@(Pi {}) t _ _ = clashT mode s t
 
@@ -55,20 +75,25 @@ parameters {auto _ : MonadError Error m}
       compareTS0 Equal body1 body2
     compareTN' mode s@(Lam {}) t _ _ = clashT mode s t
 
-    compareTN' mode (E e) (E f) ps pt = compareE0 mode e f
-    compareTN' mode s@(E _) t _ _ = clashT mode s t
-
     compareTN' _ (CloT  {}) _ ps _ = void $ ps IsCloT
     compareTN' _ (DCloT {}) _ ps _ = void $ ps IsDCloT
 
     private covering
-    compareEN' : Mode ->
+    compareEN' : EqMode ->
                  (e, f : Elim 0 n) ->
                  (0 _ : NotRedexE e) -> (0 _ : NotRedexE f) -> m ()
 
     compareEN' mode e@(F x) f@(F y) _ _ =
-      unless (x == y) $ clashE mode e f
-    compareEN' mode e@(F _) f _ _ = clashE mode e f
+      if x == y then pure () else
+      case (!(defE x), !(defE y)) of
+           (Nothing, Nothing) => clashE mode e f
+           (s', t') => compareE0 mode (fromMaybe e s') (fromMaybe f t')
+    compareEN' mode e@(F x) f _ _ = do
+      Just e' <- defE x  | Nothing => clashE mode e f
+      compareE0 mode e' f
+    compareEN' mode e f@(F y) _ _ = do
+      Just f' <- defE y  | Nothing => clashE mode e f
+      compareE0 mode e f'
 
     compareEN' mode e@(B i) f@(B j) _ _ =
       unless (i == j) $ clashE mode e f
@@ -92,35 +117,35 @@ parameters {auto _ : MonadError Error m}
 
 
     private covering %inline
-    compareTN : Mode -> NonRedexTerm 0 n -> NonRedexTerm 0 n -> m ()
+    compareTN : EqMode -> NonRedexTerm 0 n -> NonRedexTerm 0 n -> m ()
     compareTN mode s t = compareTN' mode s.fst t.fst s.snd t.snd
 
     private covering %inline
-    compareEN : Mode -> NonRedexElim 0 n -> NonRedexElim 0 n -> m ()
+    compareEN : EqMode -> NonRedexElim 0 n -> NonRedexElim 0 n -> m ()
     compareEN mode e f = compareEN' mode e.fst f.fst e.snd f.snd
 
 
     export covering %inline
-    compareT : Mode -> DimEq d -> Term d n -> Term d n -> m ()
+    compareT : EqMode -> DimEq d -> Term d n -> Term d n -> m ()
     compareT mode eqs s t =
       for_ (splits eqs) $ \th => compareT0 mode (s /// th) (t /// th)
 
     export covering %inline
-    compareE : Mode -> DimEq d -> Elim d n -> Elim d n -> m ()
+    compareE : EqMode -> DimEq d -> Elim d n -> Elim d n -> m ()
     compareE mode eqs e f =
       for_ (splits eqs) $ \th => compareE0 mode (e /// th) (f /// th)
 
 
     export covering %inline
-    compareT0 : Mode -> Term 0 n -> Term 0 n -> m ()
+    compareT0 : EqMode -> Term 0 n -> Term 0 n -> m ()
     compareT0 mode s t = compareTN mode (whnfT s) (whnfT t)
 
     export covering %inline
-    compareE0 : Mode -> Elim 0 n -> Elim 0 n -> m ()
+    compareE0 : EqMode -> Elim 0 n -> Elim 0 n -> m ()
     compareE0 mode e f = compareEN mode (whnfE e) (whnfE f)
 
     export covering %inline
-    compareTS0 : Mode -> ScopeTerm 0 n -> ScopeTerm 0 n -> m ()
+    compareTS0 : EqMode -> ScopeTerm 0 n -> ScopeTerm 0 n -> m ()
     compareTS0 mode (TUnused body1) (TUnused body2) =
       compareT0 mode body1 body2
     compareTS0 mode body1 body2 =

lib/Quox/Syntax/Qty.idr

@@ -74,7 +74,11 @@ data IsSubj : Qty -> Type where
   SZero : IsSubj Zero
   SOne  : IsSubj One
 
+export Uninhabited (IsSubj Any) where uninhabited _ impossible
+
 public export
 data IsGlobal : Qty -> Type where
   GZero : IsGlobal Zero
   GAny  : IsGlobal Any
+
+export Uninhabited (IsGlobal One) where uninhabited _ impossible

lib/Quox/Syntax/Term/Pretty.idr

@@ -40,7 +40,7 @@ mutual
         sep [!lamD, hl TVar !(prettyM x), !arrowD]
           <//> !(under T x $ prettyM t)
     prettyM (E e) =
-      prettyM e
+      pure $ hl Delim "[" <+> !(prettyM e) <+> hl Delim "]"
     prettyM (CloT s th) =
       parensIfM SApp . hang 2 =<<
         [|withPrec SApp (prettyM s) </> prettyTSubst th|]

lib/Quox/Typechecker.idr

@@ -2,9 +2,9 @@ module Quox.Typechecker
 
 import public Quox.Syntax
 import public Quox.Typing
-import Control.Monad.Either
+import public Quox.Equal
+import public Control.Monad.Either
 
-%hide Equal.Error
 %default total
 
 
@@ -27,7 +27,7 @@ private %inline
 expectEqualQ : MonadError Error m =>
                (expect, actual : Qty) -> m ()
 expectEqualQ pi rh =
-  unless (pi == rh) $ throwError $ EqualError $ ClashQ pi rh
+  unless (pi == rh) $ throwError $ ClashQ pi rh
 
 
 private %inline
@@ -40,12 +40,6 @@ tail : TyContext d (S n) -> TyContext d n
 tail = {tctx $= tail, qctx $= tail}
 
 
-private %inline
-globalSubjQty : Global -> Qty
-globalSubjQty (MkGlobal {qty = Zero, _}) = Zero
-globalSubjQty (MkGlobal {qty = Any,  _}) = One
-
-
 private %inline
 weakI : InferResult d n -> InferResult d (S n)
 weakI = {type $= weakT, qout $= (:< zero)}
@@ -66,30 +60,35 @@ subjMult sg qty =
      else Element One  %search
 
 
-mutual
+public export
+CanTC : (Type -> Type) -> Type
+CanTC m = (MonadError Error m, MonadReader Definitions m)
+
+parameters {auto _ : CanTC m}
+ mutual
   -- [todo] it seems like the options here for dealing with substitutions are
   -- to either push them or parametrise the whole typechecker over ambient
   -- substitutions. both of them seem like the same amount of work for the
   -- computer but pushing is less work for the me
 
   export covering %inline
-  check : MonadError Error m => {d, n : Nat} ->
-          (ctx : TyContext d n) -> (sg : Qty) -> {auto 0 sgs : IsSubj sg} ->
+  check : {d, n : Nat} ->
+          (ctx : TyContext d n) -> (sg : Qty) -> (0 _ : IsSubj sg) =>
           (subj : Term d n) -> (ty : Term d n) ->
           m (CheckResult n)
   check ctx sg subj ty = check' ctx sg (pushSubstsT subj) ty
 
   export covering %inline
-  infer : MonadError Error m => {d, n : Nat} ->
-          (ctx : TyContext d n) -> (sg : Qty) -> {auto 0 sgs : IsSubj sg} ->
+  infer : {d, n : Nat} ->
+          (ctx : TyContext d n) -> (sg : Qty) -> (0 _ : IsSubj sg) =>
           (subj : Elim d n) ->
           m (InferResult d n)
   infer ctx sg subj = infer' ctx sg (pushSubstsE subj)
 
 
   export covering
-  check' : MonadError Error m => {d, n : Nat} ->
-           (ctx : TyContext d n) -> (sg : Qty) -> {auto 0 sgs : IsSubj sg} ->
+  check' : {d, n : Nat} ->
+           (ctx : TyContext d n) -> (sg : Qty) -> (0 _ : IsSubj sg) =>
            (subj : NotCloTerm d n) -> (ty : Term d n) ->
            m (CheckResult n)
 
@@ -99,7 +98,6 @@ mutual
     unless (l < l') $ throwError $ BadUniverse l l'
     pure zero
 
-  -- [todo] factor this stuff out
   check' ctx sg (Element (Pi qty x arg res) _) ty = do
     l <- expectTYPE ty
     expectEqualQ zero sg
@@ -119,21 +117,19 @@ mutual
   check' ctx sg (Element (E e) _) ty = do
     infres <- infer ctx sg e
     ignore $ check ctx zero ty (TYPE UAny)
-    either (throwError . EqualError) pure $ infres.type `subT` ty
+    subT infres.type ty
     pure infres.qout
 
   export covering
-  infer' : MonadError Error m => {d, n : Nat} ->
-           (ctx : TyContext d n) -> (sg : Qty) -> {auto 0 sgs : IsSubj sg} ->
+  infer' : {d, n : Nat} ->
+           (ctx : TyContext d n) -> (sg : Qty) -> (0 _ : IsSubj sg) =>
            (subj : NotCloElim d n) ->
            m (InferResult d n)
 
-  infer' ctx sg (Element (F x) _) =
-    case lookup x ctx.globals of
-         Just g => do
-           expectEqualQ (globalSubjQty g) sg
-           pure $ InfRes {type = g.type, qout = zero}
-         Nothing => throwError $ NotInScope x
+  infer' ctx sg (Element (F x) _) = do
+    Just g <- asks $ lookup x  | Nothing => throwError $ NotInScope x
+    when (isZero g) $ expectEqualQ sg Zero
+    pure $ InfRes {type = g.type.def, qout = zero}
 
   infer' ctx sg (Element (B i) _) =
     pure $ lookupBound sg i ctx

lib/Quox/Typing.idr

@@ -2,12 +2,17 @@ module Quox.Typing
 
 import public Quox.Syntax
 import public Quox.Context
-import public Quox.Equal
+import public Quox.Definition
 
 import Data.Nat
 import public Data.SortedMap
 import Control.Monad.Reader
 import Control.Monad.State
+import Generics.Derive
+
+%hide TT.Name
+%default total
+%language ElabReflection
 
 %default total
 
@@ -31,22 +36,9 @@ QOutput : Nat -> Type
 QOutput = QContext
 
 
-public export
-record Global where
-  constructor MkGlobal
-  qty         : Qty
-  0 qtyGlobal : IsGlobal qty
-  type, term  : forall d, n. Term d n
-
-public export
-Globals : Type
-Globals = SortedMap Name Global
-
-
 public export
 record TyContext (d, n : Nat) where
   constructor MkTyContext
-  globals : Globals
   dctx : DContext d
   tctx : TContext d n
   qctx : QContext n
@@ -99,11 +91,18 @@ record InferResult d n where
   qout : QOutput n
 
 
+public export
+data EqMode = Equal | Sub
+%runElab derive "EqMode" [Generic, Meta, Eq, Ord, DecEq, Show]
+
+
 public export
 data Error
-= NotInScope   Name
-| ExpectedTYPE (Term d n)
+= ExpectedTYPE (Term d n)
 | ExpectedPi   (Term d n)
 | BadUniverse  Universe Universe
-| EqualError   (Equal.Error)
-%hide Equal.Error
+
+| ClashT EqMode (Term d n) (Term d n)
+| ClashU EqMode Universe Universe
+| ClashQ        Qty      Qty
+| NotInScope    Name

lib/quox-lib.ipkg

@@ -26,6 +26,7 @@ modules =
   Quox.Syntax.Term.Subst,
   Quox.Syntax.Universe,
   Quox.Syntax.Var,
+  Quox.Definition,
   Quox.Token,
   Quox.Lexer,
   Quox.Parser,

tests/Tests/Equal.idr

@@ -5,30 +5,45 @@ import Quox.Pretty
 import TAP
 
 export
-ToInfo Equal.Error where
+ToInfo Error where
+  toInfo (NotInScope x) =
+    [("type", "NotInScope"),
+     ("name", show x)]
+  toInfo (ExpectedTYPE t) =
+    [("type", "ExpectedTYPE"),
+     ("got", prettyStr True t)]
+  toInfo (ExpectedPi t) =
+    [("type", "ExpectedPi"),
+     ("got", prettyStr True t)]
+  toInfo (BadUniverse k l) =
+    [("type", "BadUniverse"),
+     ("low",  show k),
+     ("high", show l)]
   toInfo (ClashT mode s t) =
-    [("clash", "term"),
+    [("type", "ClashT"),
      ("mode",  show mode),
      ("left",  prettyStr True s),
      ("right", prettyStr True t)]
   toInfo (ClashU mode k l) =
-    [("clash", "universe"),
+    [("type", "ClashU"),
      ("mode",  show mode),
      ("left",  prettyStr True k),
      ("right", prettyStr True l)]
   toInfo (ClashQ pi rh) =
-    [("clash", "quantity"),
+    [("type", "ClashQ"),
      ("left",  prettyStr True pi),
      ("right", prettyStr True rh)]
 
 
-M = Either Equal.Error
+M = ReaderT Definitions (Either Error)
 
-testEq : String -> Lazy (M ()) -> Test
-testEq = test
+parameters (label : String) (act : Lazy (M ()))
+           {default empty globals : Definitions}
+  testEq : Test
+  testEq = test label $ runReaderT globals act
 
-testNeq : String -> Lazy (M ()) -> Test
-testNeq label = testThrows label $ const True
+  testNeq : Test
+  testNeq = testThrows label (const True) $ runReaderT globals act
 
 
 subT : {default 0 d, n : Nat} -> Term d n -> Term d n -> M ()
@@ -144,11 +159,22 @@ tests = "equality & subtyping" :- [
 
     todo "term d-closure",
 
-    "free var" :- [
+    "free var" :-
+    let au_bu = fromList
+          [("A", MkDef Any (TYPE (U 1)) (TYPE (U 0))),
+           ("B", MkDef Any (TYPE (U 1)) (TYPE (U 0)))]
+        au_ba = fromList
+          [("A", MkDef Any (TYPE (U 1)) (TYPE (U 0))),
+           ("B", MkDef Any (TYPE (U 1)) (FT "A"))]
+    in [
       testEq "A ≡ A" $
         equalE (F "A") (F "A"),
       testNeq "A ≢ B" $
         equalE (F "A") (F "B"),
+      testEq "A ≔ ★₀, B ≔ ★₀ ⊢ A ≡ B" {globals = au_bu} $
+        equalE (F "A") (F "B"),
+      testEq "A ≔ ★₀, B ≔ A ⊢ A ≡ B" {globals = au_ba} $
+        equalE (F "A") (F "B"),
       testEq "A <: A" $
         subE (F "A") (F "A"),
       testNeq "A ≮: B" $