wip

closes #38, again

lib/Quox/Equal.idr

@@ -280,8 +280,6 @@ namespace Term
       --  Γ ⊢ s₁ = t₁ ⇐ A     Γ ⊢ s₂ = t₂ ⇐ B{s₁/x}
       -- --------------------------------------------
       --     Γ ⊢ (s₁, t₁) = (s₂,t₂) ⇐ (x : A) × B
-      --
-      -- [todo] η for π ≥ 0 maybe
       (Pair sFst sSnd {}, Pair tFst tSnd {}) => do
         compare0 defs ctx sg fst sFst tFst
         compare0 defs ctx sg (sub1 snd (Ann sFst fst fst.loc)) sSnd tSnd
@@ -303,15 +301,16 @@ namespace Term
           compare0 defs ctx sg (sub1 snd (Ann s fst s.loc)) (E $ Snd e e.loc) t
         SOne => clashT loc ctx ty s t
 
-  compare0' defs ctx sg ty@(Enum {}) s t = local_ Equal $
+  compare0' defs ctx sg ty@(Enum cases _) s t = local_ Equal $
+    -- η for empty & singleton enums
+    if length (SortedSet.toList cases) <= 1 then pure () else
     case (s, t) of
       -- --------------------
-      --  Γ ⊢ `t = `t ⇐ {ts}
+      --  Γ ⊢ 't = 't ⇐ {ts}
       --
       -- t ∈ ts is in the typechecker, not here, ofc
-      (Tag t1 {}, Tag t2 {}) =>
-        unless (t1 == t2) $ clashT s.loc ctx ty s t
-      (E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
+      (Tag t1 {}, Tag t2 {}) => unless (t1 == t2) $ clashT s.loc ctx ty s t
+      (E e,       E f)       => ignore $ Elim.compare0 defs ctx sg e f
 
       (Tag {}, E _)    => clashT s.loc ctx ty s t
       (E _,    Tag {}) => clashT s.loc ctx ty s t
@@ -374,9 +373,9 @@ namespace Term
       --  Γ ⊢ [s] = [t] ⇐ [π.A]
       (Box s _, Box t _) => compare0 defs ctx sg ty s t
 
-      --   Γ ⊢ s = (case1 e return A of {[x] ⇒ x}) ⇐ A
-      -- -----------------------------------------------
-      --            Γ ⊢ [s] = e ⇐ [ρ.A]
+      --   Γ ⊢ σ⨴ρ · s = (case1 e return A of {[x] ⇒ x}) ⇐ A
+      -- -----------------------------------------------------
+      --               Γ ⊢ σ · [s] = e ⇐ [ρ.A]
       (Box s loc, E f)       => eta s f
       (E e,       Box t loc) => eta t e
 
@@ -390,7 +389,7 @@ namespace Term
     eta s e = do
       nm <- mnb "inner" e.loc
       let e = CaseBox One e (SN ty) (SY [< nm] (BVT 0 nm.loc)) e.loc
-      compare0 defs ctx sg ty s (E e)
+      compare0 defs ctx (sg `subjMult` q) ty s (E e)
 
   compare0' defs ctx sg ty@(E _) s t = do
     -- a neutral type can only be inhabited by neutral values

lib/Quox/Syntax/Term/Subst.idr

@@ -134,6 +134,15 @@ public export %inline
 dweakT : (by : Nat) -> Term d n -> Term (by + d) n
 dweakT by t = t // shift by
 
+public export %inline
+dweakS : (by : Nat) -> ScopeTermN s d n -> ScopeTermN s (by + d) n
+dweakS by t = t // shift by
+
+public export %inline
+dweakDS : {s : Nat} -> (by : Nat) ->
+          DScopeTermN s d n -> DScopeTermN s (by + d) n
+dweakDS by t = t // shift by
+
 public export %inline
 dweakE : (by : Nat) -> Elim d n -> Elim (by + d) n
 dweakE by t = t // shift by
@@ -143,6 +152,15 @@ public export %inline
 weakT : (by : Nat) -> Term d n -> Term d (by + n)
 weakT by t = t // shift by
 
+public export %inline
+weakS : {s : Nat} -> (by : Nat) -> ScopeTermN s d n -> ScopeTermN s d (by + n)
+weakS by t = t // shift by
+
+public export %inline
+weakDS : {s : Nat} -> (by : Nat) ->
+         DScopeTermN s d n -> DScopeTermN s d (by + n)
+weakDS by t = t // shift by
+
 public export %inline
 weakE : (by : Nat) -> Elim d n -> Elim d (by + n)
 weakE by t = t // shift by

lib/Quox/Typechecker.idr

@@ -510,23 +510,34 @@ mutual
     pure $ InfRes {type = dsub1 ty dim, qout}
 
   infer' ctx sg (Coe ty p q val loc) = do
+    -- if Ψ, 𝑖 | Γ ⊢₀ A ⇐ Type _
     checkType (extendDim ty.name ctx) ty.term Nothing
+    -- if Ψ | Γ ⊢ σ · s ⇐ A‹p/𝑖› ⊳ Σ
     qout <- checkC ctx sg val $ dsub1 ty p
+    -- then Ψ | Γ ⊢ σ · coe (𝑖 ⇒ A) @p @q s ⇒ A‹q/𝑖› ⊳ Σ
     pure $ InfRes {type = dsub1 ty q, qout}
 
   infer' ctx sg (Comp ty p q val r (S [< j0] val0) (S [< j1] val1) loc) = do
+    -- if Ψ | Γ ⊢₀ A ⇐ Type _
     checkType ctx ty Nothing
+    -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ
     qout <- checkC ctx sg val ty
+    -- if Ψ, 𝑗, 𝑖=0      | Γ ⊢ σ · t₀ ⇐ A ⊳ Σ₀
+    --    Ψ, 𝑗, 𝑖=0, 𝑗=p | Γ ⊢ t₀ = s ⇐ A
     let ty'  = dweakT 1 ty; val' = dweakT 1 val; p' = weakD 1 p
         ctx0 = extendDim j0 $ eqDim r (K Zero j0.loc) ctx
         val0 = getTerm val0
     qout0 <- check ctx0 sg val0 ty'
     lift $ equal loc (eqDim (B VZ p.loc) p' ctx0) sg ty' val0 val'
+    -- if Ψ, 𝑗, 𝑖=1      | Γ ⊢ σ · t₁ ⇐ A ⊳ Σ₁
+    --    Ψ, 𝑗, 𝑖=1, 𝑗=p | Γ ⊢ t₁ = s ⇐ A
     let ctx1 = extendDim j1 $ eqDim r (K One j1.loc) ctx
         val1  = getTerm val1
     qout1 <- check ctx1 sg val1 ty'
+    -- if Σ = Σ₀ = Σ₁
     lift $ equal loc (eqDim (B VZ p.loc) p' ctx1) sg ty' val1 val'
     let qouts  = qout :: catMaybes [toMaybe qout0, toMaybe qout1]
+    -- then Ψ | Γ ⊢ comp A @p @q s @r {0 𝑗 ⇒ t₀; 1 𝑗 ⇒ t₁} ⇒ A ⊳ Σ
     pure $ InfRes {type = ty, qout = lubs ctx qouts}
 
   infer' ctx sg (TypeCase ty ret arms def loc) = do

lib/Quox/Typing/Context.idr

@@ -26,6 +26,14 @@ CanShift (LocalVar d) where
   l // by = {type $= (// by), term $= map (// by)} l
 
 namespace LocalVar
+  export %inline
+  letVar : (type, term : Term d n) -> LocalVar d n
+  letVar type term = MkLocal {type, term = Just term}
+
+  export %inline
+  lamVar : (type : Term d n) -> LocalVar d n
+  lamVar type = MkLocal {type, term = Nothing}
+
   subD : DSubst d1 d2 -> LocalVar d1 n -> LocalVar d2 n
   subD th = {type $= (// th), term $= map (// th)}
 
@@ -135,7 +143,7 @@ namespace TyContext
 
   export %inline
   extendTyN : CtxExtension d n1 n2 -> TyContext d n1 -> TyContext d n2
-  extendTyN = extendTyLetN . map (\(q, x, s) => (q, x, MkLocal s Nothing))
+  extendTyN = extendTyLetN . map (\(q, x, s) => (q, x, lamVar s))
 
   export %inline
   extendTyLetN0 : CtxExtensionLet0 d n1 n2 -> TyContext d n1 -> TyContext d n2
@@ -148,7 +156,7 @@ namespace TyContext
   export %inline
   extendTyLet : Qty -> BindName -> Term d n -> Term d n ->
                 TyContext d n -> TyContext d (S n)
-  extendTyLet q x s e = extendTyLetN [< (q, x, MkLocal s (Just e))]
+  extendTyLet q x s e = extendTyLetN [< (q, x, letVar s e)]
 
   export %inline
   extendTy : Qty -> BindName -> Term d n -> TyContext d n -> TyContext d (S n)
@@ -239,7 +247,7 @@ namespace EqContext
 
   export %inline
   extendTyN : CtxExtension 0 n1 n2 -> EqContext n1 -> EqContext n2
-  extendTyN = extendTyLetN . map (\(q, x, s) => (q, x, MkLocal s Nothing))
+  extendTyN = extendTyLetN . map (\(q, x, s) => (q, x, lamVar s))
 
   export %inline
   extendTyLetN0 : CtxExtensionLet0 0 n1 n2 -> EqContext n1 -> EqContext n2
@@ -252,7 +260,7 @@ namespace EqContext
   export %inline
   extendTyLet : Qty -> BindName -> Term 0 n -> Term 0 n ->
                 EqContext n -> EqContext (S n)
-  extendTyLet q x s e = extendTyLetN [< (q, x, MkLocal s (Just e))]
+  extendTyLet q x s e = extendTyLetN [< (q, x, letVar s e)]
 
   export %inline
   extendTy : Qty -> BindName -> Term 0 n -> EqContext n -> EqContext (S n)
@@ -293,6 +301,25 @@ namespace WhnfContext
   empty : WhnfContext 0 0
   empty = MkWhnfContext [<] [<] [<]
 
+  export
+  extendTy' : BindName -> LocalVar d n -> WhnfContext d n -> WhnfContext d (S n)
+  extendTy' x var (MkWhnfContext {termLen, dnames, tnames, tctx}) =
+    MkWhnfContext {
+      dnames,
+      termLen = [|S termLen|],
+      tnames  = tnames :< x,
+      tctx    = tctx   :< var
+    }
+
+  export %inline
+  extendTy : BindName -> Term d n -> WhnfContext d n -> WhnfContext d (S n)
+  extendTy x ty ctx = extendTy' x (lamVar ty) ctx
+
+  export %inline
+  extendTyLet : BindName -> (type, term : Term d n) ->
+                WhnfContext d n -> WhnfContext d (S n)
+  extendTyLet x type term ctx = extendTy' x (letVar {type, term}) ctx
+
   export
   extendDimN : {s : Nat} -> BContext s -> WhnfContext d n ->
                WhnfContext (s + d) n

lib/Quox/Whnf/Coercion.idr

@@ -119,7 +119,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
   eqCoe sty@(S [< j] ty) p q val r loc = do
     -- (coe [j ⇒ Eq [i ⇒ A] L R] @p @q eq) @r
     --   ⇝
-    -- comp [j ⇒ A‹r/i›] @p @q (eq ∷ (Eq [i ⇒ A] L R)‹p/j›)
+    -- comp [j ⇒ A‹r/i›] @p @q ((eq ∷ (Eq [i ⇒ A] L R)‹p/j›) @r)
     --   @r { 0 j ⇒ L; 1 j ⇒ R }
     let ctx1 = extendDim j ctx
     Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
@@ -147,6 +147,10 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
       (ST body.names $ body.term // (a' ::: shift 1)) loc
 
 
+-- new params block to call the above functions at different `n`
+parameters {auto _ : CanWhnf Term Interface.isRedexT}
+           {auto _ : CanWhnf Elim Interface.isRedexE}
+           (defs : Definitions) (ctx : WhnfContext d n) (sg : SQty)
   ||| pushes a coercion inside a whnf-ed term
   export covering
   pushCoe : BindName ->
@@ -163,17 +167,22 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
       IOState tyLoc =>
         whnf defs ctx sg $ Ann s (IOState tyLoc) loc
 
-      -- η expand it so that whnf for App can deal with it
+      -- η expand, then simplify the Coe/App in the body
       --
       -- (coe (𝑖 ⇒ π.(x : A) → B) @p @q s)
       --   ⇝
       -- (λ y ⇒ (coe (𝑖 ⇒ π.(x : A) → B) @p @q s) y) ∷ (π.(x : A) → B)‹q/𝑖›
-      Pi {} =>
-        let inner = Coe (SY [< i] ty) p q s loc in
+      --   ⇝     ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
+      -- (λ y ⇒ ⋯) ∷ (π.(x : A) → B)‹q/𝑖›   -- see `piCoe`
+      --
+      -- do the piCoe step here because otherwise equality checking keeps
+      -- doing the η forever
+      Pi {arg, res = S [< x] _, _} => do
+        let ctx' = extendTy x (arg // one p) ctx
+        body <- piCoe defs ctx' sg
+          (weakDS 1 $ SY [< i] ty) p q (weakT 1 s) (BVT 0 loc) loc
         whnf defs ctx sg $
-          Ann (LamY !(mnb "y" loc)
-                  (E $ App (weakE 1 inner) (BVT 0 loc) loc) loc)
-              (ty // one q) loc
+          Ann (LamY x (E body.fst) loc) (ty // one q) loc
 
       -- no η!!!
       -- push into a pair constructor, otherwise still stuck
@@ -190,7 +199,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
             fstInSnd =
               CoeT !(fresh i)
                    (tfst // (BV 0 loc ::: shift 2))
-                   (weakD 1 p) (BV 0 loc) (dweakT 1 s) fst.loc
+                   (weakD 1 p) (BV 0 loc) (dweakT 1 fst) fst.loc
             snd' = CoeT i (sub1 tsnd fstInSnd) p q snd snd.loc
         whnf defs ctx sg $
           Ann (Pair (E fst') (E snd') sLoc) (ty // one q) loc
@@ -199,17 +208,23 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
       Enum cases tyLoc =>
         whnf defs ctx sg $ Ann s (Enum cases tyLoc) loc
 
-      -- η expand, same as for Π
+      -- η expand/simplify, same as for Π
       --
       -- (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @q s)
       --   ⇝
       -- (δ 𝑘 ⇒ (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @q s) @𝑘) ∷ (Eq (𝑗 ⇒ A) l r)‹q/𝑖›
-      Eq {} =>
-        let inner = Coe (SY [< i] ty) p q s loc in
+      --   ⇝     ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
+      -- (δ 𝑘 ⇒ ⋯) ∷ (Eq (𝑗 ⇒ A) l r)‹q/𝑖›   -- see `eqCoe`
+      --
+      -- do the eqCoe step here because otherwise equality checking keeps
+      -- doing the η forever
+      Eq {ty = S [< j] _, _} => do
+        let ctx' = extendDim j ctx
+        body <- eqCoe defs ctx' sg
+          (dweakDS 1 $ S [< i] $ Y ty) (weakD 1 p) (weakD 1 q)
+          (dweakT 1 s) (BV 0 loc) loc
         whnf defs ctx sg $
-          Ann (DLamY !(mnb "k" loc)
-                  (E $ DApp (dweakE 1 inner) (BV 0 loc) loc) loc)
-              (ty // one q) loc
+          Ann (DLamY i (E body.fst) loc) (ty // one q) loc
 
       -- (coe ℕ @_ @_ s) ⇝ (s ∷ ℕ)
       NAT tyLoc =>
@@ -219,22 +234,19 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
       STRING tyLoc =>
         whnf defs ctx sg $ Ann s (STRING tyLoc) loc
 
-      -- η expand.... kinda
+      -- η expand/simplify
       --
-      -- (coe (𝑖 ⇒ [π. A]) @p @q s)
+      -- (coe (𝑖 ⇒ [π.A]) @p @q s)
       --   ⇝
-      -- [case1 s ∷ [π.A]‹p/𝑖› return A‹q/𝑖›
-      --  of {[x] ⇒ coe (𝑖 ⇒ A) @p @q x}] ∷ [π.A]‹q/𝑖›
+      -- [case coe (𝑖 ⇒ [π.A]) @p @q s return A‹q/𝑖› of {[x] ⇒ x}]
+      --   ⇝
+      -- [case1 s ∷ [π.A]‹p/𝑖› ⋯] ∷ [π.A]‹q/𝑖›   -- see `boxCoe`
       --
-      -- a literal η expansion of `e ⇝ [case e of {[x] ⇒ x}]` causes a loop in
-      -- the equality checker because whnf of `case e ⋯` requires whnf of `e`
+      -- do the eqCoe step here because otherwise equality checking keeps
+      -- doing the η forever
       BOX qty inner tyLoc => do
-        let inner = CaseBox {
-              qty  = One,
-              box  = Ann s (ty // one p) s.loc,
-              ret  = SN $ inner // one q,
-              body = SY [< !(mnb "x" loc)] $ E $
-                     Coe (ST [< i] $ weakT 1 inner) p q (BVT 0 s.loc) s.loc,
-              loc
-            }
-        whnf defs ctx sg $ Ann (Box (E inner) loc) (ty // one q) loc
+        body <- boxCoe defs ctx sg qty
+          (SY [< i] ty) p q s
+          (SN $ inner // one q)
+          (SY [< !(mnb "inner" loc)] (BVT 0 loc)) loc
+        whnf defs ctx sg $ Ann (Box (E body.fst) loc) (ty // one q) loc