From b85dcb5402c9699e8cd8a9c7fa3ef5fd4370fd3e Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sun, 17 Sep 2023 19:10:46 +0200 Subject: [PATCH] =?UTF-8?q?=CE=B7=20for=20box?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit fixes #27 --- examples/all.quox | 1 + examples/eta.quox | 13 +++++++++++ lib/Quox/Equal.idr | 43 ++++++++++++++++++++++--------------- tests/Tests/Equal.idr | 50 +++++++++++++++++++++++++++++++++++++++---- 4 files changed, 86 insertions(+), 21 deletions(-) create mode 100644 examples/eta.quox diff --git a/examples/all.quox b/examples/all.quox index b24ebcf..e95a025 100644 --- a/examples/all.quox +++ b/examples/all.quox @@ -5,3 +5,4 @@ load "maybe.quox" load "nat.quox" load "pair.quox" load "list.quox" +load "eta.quox" diff --git a/examples/eta.quox b/examples/eta.quox new file mode 100644 index 0000000..1e9dadd --- /dev/null +++ b/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 + +} diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr index 82e7b22..7b47ae4 100644 --- a/lib/Quox/Equal.idr +++ b/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 - ctx' : EqContext (S n) - ctx' = extendTy qty res.name arg ctx + where + ctx' : EqContext (S n) + ctx' = extendTy qty res.name arg ctx - eta : Loc -> Elim 0 n -> ScopeTerm 0 n -> Eff EqualInner () - eta _ e (S _ (Y b)) = compare0 defs ctx' res.term (toLamBody e) b - eta loc e (S _ (N _)) = clashT loc ctx ty s t + toLamBody : Elim d n -> Term d (S n) + toLamBody e = E $ App (weakE 1 e) (BVT 0 e.loc) e.loc + + 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 - (E _, t) => wrongType t.loc ctx ty t - (s, _) => wrongType s.loc ctx ty s + (Box {}, _) => wrongType t.loc ctx bty t + (E _, _) => wrongType t.loc ctx bty t + _ => 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 diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr index a263a2b..128131c 100644 --- a/tests/Tests/Equal.idr +++ b/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", - todo "boxes", - todo "box elim", + "box types" :- [ + testEq "[1.A] = [1.A] : ★" $ + 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",