η for box

fixes #27

examples/all.quox

@@ -5,3 +5,4 @@ load "maybe.quox"
 load "nat.quox"
 load "pair.quox"
 load "list.quox"
+load "eta.quox"

examples/eta.quox

@@ -0,0 +1,13 @@
+namespace eta {
+
+def0 Π : (A : ★) → (A → ★) → ★ = λ A B ⇒ (x : A) → B x
+
+def0 function : (A : ★) → (B : A → Type) → (P : Π A B → ★) → (f : Π A B) →
+                P (λ x ⇒ f x) → P f =
+  λ A B P f p ⇒ p
+
+def0 box : (A : ★) → (P : [ω.A] → ★) → (e : [ω.A]) →
+           P [case1 e return A of {[x] ⇒ x}] → P e =
+  λ A P e p ⇒ p
+
+}

lib/Quox/Equal.idr

@@ -140,12 +140,6 @@ compareType : Definitions -> EqContext n -> (s, t : Term 0 n) ->
               Eff EqualInner ()
 
 
-||| converts an elim "Γ ⊢ e" to "Γ, x ⊢ e x", for comparing with
-||| a lambda "Γ ⊢ λx ⇒ t" that has been converted to "Γ, x ⊢ t".
-private %inline
-toLamBody : Elim d n -> Term d (S n)
-toLamBody e = E $ App (weakE 1 e) (BVT 0 e.loc) e.loc
-
 namespace Term
   private covering
   compare0' : (defs : Definitions) -> EqContext n ->
@@ -174,13 +168,16 @@ namespace Term
       (Lam {}, t) => wrongType t.loc ctx ty t
       (E _,    t) => wrongType t.loc ctx ty t
       (s,      _) => wrongType s.loc ctx ty s
-    where
+  where
-      ctx' : EqContext (S n)
+    ctx' : EqContext (S n)
-      ctx' = extendTy qty res.name arg ctx
+    ctx' = extendTy qty res.name arg ctx
 
-      eta : Loc -> Elim 0 n -> ScopeTerm 0 n -> Eff EqualInner ()
+    toLamBody : Elim d n -> Term d (S n)
-      eta _   e (S _ (Y b)) = compare0 defs ctx' res.term (toLamBody e) b
+    toLamBody e = E $ App (weakE 1 e) (BVT 0 e.loc) e.loc
-      eta loc e (S _ (N _)) = clashT loc ctx ty s t
+
+    eta : Loc -> Elim 0 n -> ScopeTerm 0 n -> Eff EqualInner ()
+    eta loc e (S _ (N _)) = clashT loc ctx ty s t
+    eta _   e (S _ (Y b)) = compare0 defs ctx' res.term (toLamBody e) b
 
   compare0' defs ctx ty@(Sig {fst, snd, _}) s t = local_ Equal $
     case (s, t) of
@@ -251,18 +248,30 @@ namespace Term
       (E _,     t) => wrongType t.loc ctx nat t
       (s,       _) => wrongType s.loc ctx nat s
 
-  compare0' defs ctx ty@(BOX q ty' {}) s t = local_ Equal $
+  compare0' defs ctx bty@(BOX q ty {}) s t = local_ Equal $
     case (s, t) of
       --     Γ ⊢ s = t : A
       -- -----------------------
       --  Γ ⊢ [s] = [t] : [π.A]
-      (Box s' {}, Box t' {}) => compare0 defs ctx ty' s' t'
+      (Box s _, Box t _) => compare0 defs ctx ty s t
+
+      --   Γ ⊢ 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
 
       (E e, E f) => ignore $ Elim.compare0 defs ctx e f
 
-      (Box {}, t) => wrongType t.loc ctx ty t
+      (Box {}, _) => wrongType t.loc ctx bty t
-      (E   _,  t) => wrongType t.loc ctx ty t
+      (E   _,  _) => wrongType t.loc ctx bty t
-      (s,      _) => wrongType s.loc ctx ty s
+      _           => wrongType s.loc ctx bty s
+  where
+    eta : Term 0 n -> Elim 0 n -> Eff EqualInner ()
+    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 ty s (E e)
 
   compare0' defs ctx ty@(E _) s t = do
     -- a neutral type can only be inhabited by neutral values

tests/Tests/Equal.idr

@@ -48,6 +48,7 @@ tests : Test
 tests = "equality & subtyping" :- [
   note #""s{t,…}" for term substs; "s‹p,…›" for dim substs"#,
   note #""0=1 ⊢ 𝒥" means that 𝒥 holds in an inconsistent dim context"#,
+  note "binds before ∥ are globals, after it are BVs",
 
   "universes" :- [
     testEq "★₀ = ★₀" $
@@ -165,7 +166,6 @@ tests = "equality & subtyping" :- [
       refl a x = ^Ann (^DLam (SN x)) (^Eq0 a x x)
   in
   [
-    note "binds before ∥ are globals, after it are BVs",
     note #"refl A x is an abbreviation for "(δ i ⇒ x) ∷ (x ≡ x : A)""#,
     testEq "refl A a = refl A a" $
       equalE empty
@@ -523,9 +523,51 @@ tests = "equality & subtyping" :- [
   todo "enum",
   todo "enum elim",
 
-  todo "box types",
+  "box types" :- [
-  todo "boxes",
+    testEq "[1.A] = [1.A] : ★" $
-  todo "box elim",
+      equalT empty
+        (^TYPE 0)
+        (^BOX One (^FT "A" 0))
+        (^BOX One (^FT "A" 0)),
+    testNeq "[1.A] ≠ [ω.A] : ★" $
+      equalT empty
+        (^TYPE 0)
+        (^BOX One (^FT "A" 0))
+        (^BOX Any (^FT "A" 0)),
+    testNeq "[1.A] ≠ [1.B] : ★" $
+      equalT empty
+        (^TYPE 0)
+        (^BOX One (^FT "A" 0))
+        (^BOX One (^FT "B" 0)),
+    testNeq "[1.A] ≠ A : ★" $
+      equalT empty
+        (^TYPE 0)
+        (^BOX One (^FT "A" 0))
+        (^FT "A" 0),
+    testEq "0=1 ⊢ [1.A] = [1.B] : ★" $
+      equalT empty01
+        (^TYPE 0)
+        (^BOX One (^FT "A" 0))
+        (^BOX One (^FT "B" 0))
+  ],
+
+  "boxes" :- [
+    testEq "[a] = [a] : [ω.A]" $
+      equalT empty
+        (^BOX Any (^FT "A" 0))
+        (^Box (^FT "a" 0))
+        (^Box (^FT "a" 0)),
+    testNeq "[a] ≠ [a'] : [ω.A]" $
+      equalT empty
+        (^BOX Any (^FT "A" 0))
+        (^Box (^FT "a" 0))
+        (^Box (^FT "a'" 0)),
+    testEq "ω.x : [ω.A] ⊢ x = [case1 b return A of {[y] ⇒ y}] : [ω.A]" $
+      equalT (ctx [< ("x", ^BOX Any (^FT "A" 0))])
+        (^BOX Any (^FT "A" 0))
+        (^BVT 0)
+        (^Box (E $ ^CaseBox One (^BV 0) (SN $ ^FT "A" 0) (SY [< "y"] (^BVT 0))))
+  ],
 
   "elim closure" :- [
     note "bold numbers for de bruijn indices",