From bee6eeacdf37eea912a3aeec71ee1205da64ee66 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Tue, 14 Feb 2023 22:28:10 +0100 Subject: [PATCH] pass a `TyContext` into `equal` etc, rather than its components --- lib/Quox/Equal.idr | 16 +-- lib/Quox/Typechecker.idr | 6 +- lib/Quox/Typing.idr | 4 + tests/Tests/Equal.idr | 201 ++++++++++++++++++------------------ tests/Tests/Typechecker.idr | 2 +- 5 files changed, 119 insertions(+), 110 deletions(-) diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr index ea88c5c..c4bcac4 100644 --- a/lib/Quox/Equal.idr +++ b/lib/Quox/Equal.idr @@ -285,8 +285,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} compare0' _ e@(_ :# _) f _ _ = clashE e f -parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)} - (eq : DimEq d) (ctx : TContext q d n) +parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)} (ctx : TyContext q d n) parameters (mode : EqMode) namespace Term export covering @@ -294,16 +293,17 @@ parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)} compare ty s t = do defs <- ask runReaderT {m} (MakeEnv {mode}) $ - for_ (splits eq) $ \th => - compare0 defs (map (/// th) ctx) (ty /// th) (s /// th) (t /// th) + for_ (splits ctx.dctx) $ \th => + compare0 defs (map (/// th) ctx.tctx) + (ty /// th) (s /// th) (t /// th) export covering compareType : (s, t : Term q d n) -> m () compareType s t = do defs <- ask runReaderT {m} (MakeEnv {mode}) $ - for_ (splits eq) $ \th => - compareType defs (map (/// th) ctx) (s /// th) (t /// th) + for_ (splits ctx.dctx) $ \th => + compareType defs (map (/// th) ctx.tctx) (s /// th) (t /// th) namespace Elim ||| you don't have to pass the type in but the arguments must still be @@ -313,8 +313,8 @@ parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)} compare e f = do defs <- ask runReaderT {m} (MakeEnv {mode}) $ - for_ (splits eq) $ \th => - compare0 defs (map (/// th) ctx) (e /// th) (f /// th) + for_ (splits ctx.dctx) $ \th => + compare0 defs (map (/// th) ctx.tctx) (e /// th) (f /// th) namespace Term export covering %inline diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr index 02ce914..067efd8 100644 --- a/lib/Quox/Typechecker.idr +++ b/lib/Quox/Typechecker.idr @@ -168,9 +168,9 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} -- if Ψ, i | Γ ⊢ σ · t ⇐ A ⊳ Σ qout <- check (extendDim ctx) sg body.term ty.term -- if Ψ | Γ ⊢ t‹0› = l : A‹0› - equal ctx.dctx ctx.tctx ty.zero body.zero l + equal ctx ty.zero body.zero l -- if Ψ | Γ ⊢ t‹1› = r : A‹1› - equal ctx.dctx ctx.tctx ty.one body.one r + equal ctx ty.one body.one r -- then Ψ | Γ ⊢ σ · (λᴰi ⇒ t) ⇐ Eq [i ⇒ A] l r ⊳ Σ pure qout @@ -178,7 +178,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} -- if Ψ | Γ ⊢ σ · e ⇒ A' ⊳ Σ infres <- infer ctx sg e -- if Ψ | Γ ⊢ A' <: A - subtype ctx.dctx ctx.tctx infres.type ty + subtype ctx infres.type ty -- then Ψ | Γ ⊢ σ · e ⇐ A ⊳ Σ pure infres.qout diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr index 428f29a..af3afb9 100644 --- a/lib/Quox/Typing.idr +++ b/lib/Quox/Typing.idr @@ -44,6 +44,10 @@ namespace TContext pushD tel = map (/// shift 1) tel namespace TyContext + public export %inline + empty : {d : Nat} -> TyContext q d 0 + empty = MkTyContext {dctx = new, tctx = [<]} + export %inline extendTyN : Telescope (Term q d) from to -> TyContext q d from -> TyContext q d to diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr index 5d6789d..73f9b38 100644 --- a/tests/Tests/Equal.idr +++ b/tests/Tests/Equal.idr @@ -28,20 +28,24 @@ parameters (label : String) (act : Lazy (M ())) testNeq = testThrows label (const True) $ runReaderT globals act -parameters {default 0 d, n : Nat} - {default new eqs : DimEq d} - (ctx : TContext Three d n) - subT : Term Three d n -> Term Three d n -> Term Three d n -> M () - subT ty s t = Term.sub eqs ctx ty s t +parameters (0 d : Nat) (ctx : TyContext Three d n) + subTD, equalTD : Term Three d n -> Term Three d n -> Term Three d n -> M () + subTD ty s t = Term.sub ctx ty s t + equalTD ty s t = Term.equal ctx ty s t - equalT : Term Three d n -> Term Three d n -> Term Three d n -> M () - equalT ty s t = Term.equal eqs ctx ty s t + subED, equalED : Elim Three d n -> Elim Three d n -> M () + subED e f = Elim.sub ctx e f + equalED e f = Elim.equal ctx e f - subE : Elim Three d n -> Elim Three d n -> M () - subE e f = Elim.sub eqs ctx e f +parameters (ctx : TyContext Three 0 n) + subT, equalT : Term Three 0 n -> Term Three 0 n -> Term Three 0 n -> M () + subT = subTD 0 ctx + equalT = equalTD 0 ctx + + subE, equalE : Elim Three 0 n -> Elim Three 0 n -> M () + subE = subED 0 ctx + equalE = equalED 0 ctx - equalE : Elim Three d n -> Elim Three d n -> M () - equalE e f = Elim.equal eqs ctx e f export @@ -52,17 +56,17 @@ tests = "equality & subtyping" :- [ "universes" :- [ testEq "★₀ = ★₀" $ - equalT [<] (TYPE 1) (TYPE 0) (TYPE 0), + equalT empty (TYPE 1) (TYPE 0) (TYPE 0), testNeq "★₀ ≠ ★₁" $ - equalT [<] (TYPE 2) (TYPE 0) (TYPE 1), + equalT empty (TYPE 2) (TYPE 0) (TYPE 1), testNeq "★₁ ≠ ★₀" $ - equalT [<] (TYPE 2) (TYPE 1) (TYPE 0), + equalT empty (TYPE 2) (TYPE 1) (TYPE 0), testEq "★₀ <: ★₀" $ - subT [<] (TYPE 1) (TYPE 0) (TYPE 0), + subT empty (TYPE 1) (TYPE 0) (TYPE 0), testEq "★₀ <: ★₁" $ - subT [<] (TYPE 2) (TYPE 0) (TYPE 1), + subT empty (TYPE 2) (TYPE 0) (TYPE 1), testNeq "★₁ ≮: ★₀" $ - subT [<] (TYPE 2) (TYPE 1) (TYPE 0) + subT empty (TYPE 2) (TYPE 1) (TYPE 0) ], "pi" :- [ @@ -70,79 +74,79 @@ tests = "equality & subtyping" :- [ note #""𝐴 ⇾ 𝐵" for (0·𝐴) → 𝐵"#, testEq "★₀ ⇾ ★₀ = ★₀ ⇾ ★₀" $ let tm = Arr Zero (TYPE 0) (TYPE 0) in - equalT [<] (TYPE 1) tm tm, + equalT empty (TYPE 1) tm tm, testEq "★₀ ⇾ ★₀ <: ★₀ ⇾ ★₀" $ let tm = Arr Zero (TYPE 0) (TYPE 0) in - subT [<] (TYPE 1) tm tm, + subT empty (TYPE 1) tm tm, testNeq "★₁ ⊸ ★₀ ≠ ★₀ ⇾ ★₀" $ let tm1 = Arr Zero (TYPE 1) (TYPE 0) tm2 = Arr Zero (TYPE 0) (TYPE 0) in - equalT [<] (TYPE 2) tm1 tm2, + equalT empty (TYPE 2) tm1 tm2, testEq "★₁ ⊸ ★₀ <: ★₀ ⊸ ★₀" $ let tm1 = Arr One (TYPE 1) (TYPE 0) tm2 = Arr One (TYPE 0) (TYPE 0) in - subT [<] (TYPE 2) tm1 tm2, + subT empty (TYPE 2) tm1 tm2, testEq "★₀ ⊸ ★₀ <: ★₀ ⊸ ★₁" $ let tm1 = Arr One (TYPE 0) (TYPE 0) tm2 = Arr One (TYPE 0) (TYPE 1) in - subT [<] (TYPE 2) tm1 tm2, + subT empty (TYPE 2) tm1 tm2, testEq "★₀ ⊸ ★₀ <: ★₀ ⊸ ★₁" $ let tm1 = Arr One (TYPE 0) (TYPE 0) tm2 = Arr One (TYPE 0) (TYPE 1) in - subT [<] (TYPE 2) tm1 tm2, + subT empty (TYPE 2) tm1 tm2, testEq "A ⊸ B = A ⊸ B" $ let tm = Arr One (FT "A") (FT "B") in - equalT [<] (TYPE 0) tm tm, + equalT empty (TYPE 0) tm tm, testEq "A ⊸ B <: A ⊸ B" $ let tm = Arr One (FT "A") (FT "B") in - subT [<] (TYPE 0) tm tm, + subT empty (TYPE 0) tm tm, note "incompatible quantities", testNeq "★₀ ⊸ ★₀ ≠ ★₀ ⇾ ★₁" $ let tm1 = Arr Zero (TYPE 0) (TYPE 0) tm2 = Arr Zero (TYPE 0) (TYPE 1) in - equalT [<] (TYPE 2) tm1 tm2, + equalT empty (TYPE 2) tm1 tm2, testNeq "A ⇾ B ≠ A ⊸ B" $ let tm1 = Arr Zero (FT "A") (FT "B") tm2 = Arr One (FT "A") (FT "B") in - equalT [<] (TYPE 0) tm1 tm2, + equalT empty (TYPE 0) tm1 tm2, testNeq "A ⇾ B ≮: A ⊸ B" $ let tm1 = Arr Zero (FT "A") (FT "B") tm2 = Arr One (FT "A") (FT "B") in - subT [<] (TYPE 0) tm1 tm2, + subT empty (TYPE 0) tm1 tm2, testEq "0=1 ⊢ A ⇾ B = A ⊸ B" $ let tm1 = Arr Zero (FT "A") (FT "B") tm2 = Arr One (FT "A") (FT "B") in - equalT [<] (TYPE 0) tm1 tm2 {eqs = ZeroIsOne}, + equalT (MkTyContext ZeroIsOne [<]) (TYPE 0) tm1 tm2, note "[todo] should π ≤ ρ ⊢ (ρ·A) → B <: (π·A) → B?" ], "lambda" :- [ testEq "λ x ⇒ [x] = λ x ⇒ [x]" $ - equalT [<] (Arr One (FT "A") (FT "A")) + equalT empty (Arr One (FT "A") (FT "A")) (["x"] :\\ BVT 0) (["x"] :\\ BVT 0), testEq "λ x ⇒ [x] <: λ x ⇒ [x]" $ - subT [<] (Arr One (FT "A") (FT "A")) + subT empty (Arr One (FT "A") (FT "A")) (["x"] :\\ BVT 0) (["x"] :\\ BVT 0), testEq "λ x ⇒ [x] = λ y ⇒ [y]" $ - equalT [<] (Arr One (FT "A") (FT "A")) + equalT empty (Arr One (FT "A") (FT "A")) (["x"] :\\ BVT 0) (["y"] :\\ BVT 0), testEq "λ x ⇒ [x] <: λ y ⇒ [y]" $ - equalT [<] (Arr One (FT "A") (FT "A")) + equalT empty (Arr One (FT "A") (FT "A")) (["x"] :\\ BVT 0) (["y"] :\\ BVT 0), testNeq "λ x y ⇒ [x] ≠ λ x y ⇒ [y]" $ - equalT [<] (Arr One (FT "A") $ Arr One (FT "A") (FT "A")) + equalT empty (Arr One (FT "A") $ Arr One (FT "A") (FT "A")) (["x", "y"] :\\ BVT 1) (["x", "y"] :\\ BVT 0), testEq "λ x ⇒ [a] = λ x ⇒ [a] (TUsed vs TUnused)" $ - equalT [<] (Arr Zero (FT "B") (FT "A")) + equalT empty (Arr Zero (FT "B") (FT "A")) (Lam "x" $ TUsed $ FT "a") (Lam "x" $ TUnused $ FT "a"), testEq "λ x ⇒ [f [x]] = [f] (η)" $ - equalT [<] (Arr One (FT "A") (FT "A")) + equalT empty (Arr One (FT "A") (FT "A")) (["x"] :\\ E (F "f" :@ BVT 0)) (FT "f") ], @@ -150,10 +154,10 @@ tests = "equality & subtyping" :- [ "eq type" :- [ testEq "(★₀ ≡ ★₀ : ★₁) = (★₀ ≡ ★₀ : ★₁)" $ let tm = Eq0 (TYPE 1) (TYPE 0) (TYPE 0) in - equalT [<] (TYPE 2) tm tm, + equalT empty (TYPE 2) tm tm, testEq "A ≔ ★₁ ⊢ (★₀ ≡ ★₀ : ★₁) = (★₀ ≡ ★₀ : A)" {globals = fromList [("A", mkDef zero (TYPE 2) (TYPE 1))]} $ - equalT [<] (TYPE 2) + equalT empty (TYPE 2) (Eq0 (TYPE 1) (TYPE 0) (TYPE 0)) (Eq0 (FT "A") (TYPE 0) (TYPE 0)) ], @@ -166,86 +170,86 @@ tests = "equality & subtyping" :- [ note #""refl [A] x" is an abbreviation for "(λᴰi ⇒ x) ∷ (x ≡ x : A)""#, note "binds before ∥ are globals, after it are BVs", testEq "refl [A] a = refl [A] a" $ - equalE [<] (refl (FT "A") (FT "a")) (refl (FT "A") (FT "a")), + equalE empty (refl (FT "A") (FT "a")) (refl (FT "A") (FT "a")), testEq "p : (a ≡ a' : A), q : (a ≡ a' : A) ∥ ⊢ p = q (free)" {globals = let def = mkAbstract Zero $ Eq0 (FT "A") (FT "a") (FT "a'") in defGlobals `mergeLeft` fromList [("p", def), ("q", def)]} $ - equalE [<] (F "p") (F "q"), + equalE empty (F "p") (F "q"), testEq "∥ x : (a ≡ a' : A), y : (a ≡ a' : A) ⊢ x = y (bound)" $ let ty : forall n. Term Three 0 n := Eq0 (FT "A") (FT "a") (FT "a'") in - equalE [< ty, ty] (BV 0) (BV 1) {n = 2}, + equalE (MkTyContext new [< ty, ty]) (BV 0) (BV 1), testEq "∥ x : [(a ≡ a' : A) ∷ Type 0], y : [ditto] ⊢ x = y" $ let ty : forall n. Term Three 0 n := E (Eq0 (FT "A") (FT "a") (FT "a'") :# TYPE 0) in - equalE [< ty, ty] (BV 0) (BV 1) {n = 2}, + equalE (MkTyContext new [< ty, ty]) (BV 0) (BV 1), testEq "E ≔ a ≡ a' : A, EE ≔ E ∥ x : EE, y : EE ⊢ x = y" {globals = defGlobals `mergeLeft` fromList [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))), ("EE", mkDef zero (TYPE 0) (FT "E"))]} $ - equalE [< FT "EE", FT "EE"] (BV 0) (BV 1) {n = 2}, + equalE (MkTyContext new [< FT "EE", FT "EE"]) (BV 0) (BV 1), testEq "E ≔ a ≡ a' : A, EE ≔ E ∥ x : EE, y : E ⊢ x = y" {globals = defGlobals `mergeLeft` fromList [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))), ("EE", mkDef zero (TYPE 0) (FT "E"))]} $ - equalE [< FT "EE", FT "E"] (BV 0) (BV 1) {n = 2}, + equalE (MkTyContext new [< FT "EE", FT "E"]) (BV 0) (BV 1), testEq "E ≔ a ≡ a' : A ∥ x : E, y : E ⊢ x = y" {globals = defGlobals `mergeLeft` fromList [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'")))]} $ - equalE [< FT "E", FT "E"] (BV 0) (BV 1) {n = 2}, + equalE (MkTyContext new [< FT "E", FT "E"]) (BV 0) (BV 1), testEq "E ≔ a ≡ a' : A ∥ x : (E×E), y : (E×E) ⊢ x = y" {globals = defGlobals `mergeLeft` fromList [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'")))]} $ let ty : forall n. Term Three 0 n := Sig "_" (FT "E") $ TUnused $ FT "E" in - equalE [< ty, ty] (BV 0) (BV 1) {n = 2}, + equalE (MkTyContext new [< ty, ty]) (BV 0) (BV 1), testEq "E ≔ a ≡ a' : A, F ≔ E × E ∥ x : F, y : F ⊢ x = y" {globals = defGlobals `mergeLeft` fromList [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))), ("W", mkDef zero (TYPE 0) (FT "E" `And` FT "E"))]} $ - equalE [< FT "W", FT "W"] (BV 0) (BV 1) {n = 2} + equalE (MkTyContext new [< FT "W", FT "W"]) (BV 0) (BV 1) ], "term closure" :- [ testEq "[#0]{} = [#0] : A" $ - equalT [< FT "A"] (FT "A") {n = 1} + equalT (MkTyContext new [< FT "A"]) (FT "A") (CloT (BVT 0) id) (BVT 0), testEq "[#0]{a} = [a] : A" $ - equalT [<] (FT "A") + equalT empty (FT "A") (CloT (BVT 0) (F "a" ::: id)) (FT "a"), testEq "[#0]{a,b} = [a] : A" $ - equalT [<] (FT "A") + equalT empty (FT "A") (CloT (BVT 0) (F "a" ::: F "b" ::: id)) (FT "a"), testEq "[#1]{a,b} = [b] : A" $ - equalT [<] (FT "A") + equalT empty (FT "A") (CloT (BVT 1) (F "a" ::: F "b" ::: id)) (FT "b"), testEq "(λy. [#1]){a} = λy. [a] : B ⇾ A (TUnused)" $ - equalT [<] (Arr Zero (FT "B") (FT "A")) + equalT empty (Arr Zero (FT "B") (FT "A")) (CloT (Lam "y" $ TUnused $ BVT 0) (F "a" ::: id)) (Lam "y" $ TUnused $ FT "a"), testEq "(λy. [#1]){a} = λy. [a] : B ⇾ A (TUsed)" $ - equalT [<] (Arr Zero (FT "B") (FT "A")) + equalT empty (Arr Zero (FT "B") (FT "A")) (CloT (["y"] :\\ BVT 1) (F "a" ::: id)) (["y"] :\\ FT "a") ], "term d-closure" :- [ testEq "★₀‹𝟎› = ★₀ : ★₁" $ - equalT {d = 1} [<] (TYPE 1) (DCloT (TYPE 0) (K Zero ::: id)) (TYPE 0), + equalTD 1 empty (TYPE 1) (DCloT (TYPE 0) (K Zero ::: id)) (TYPE 0), testEq "(λᴰ i ⇒ a)‹𝟎› = (λᴰ i ⇒ a) : (a ≡ a : A)" $ - equalT {d = 1} [<] + equalTD 1 empty (Eq0 (FT "A") (FT "a") (FT "a")) (DCloT (["i"] :\\% FT "a") (K Zero ::: id)) (["i"] :\\% FT "a"), @@ -261,136 +265,137 @@ tests = "equality & subtyping" :- [ ("B", mkDef Any (TYPE (U 1)) (FT "A"))] in [ testEq "A = A" $ - equalE [<] (F "A") (F "A"), + equalE empty (F "A") (F "A"), testNeq "A ≠ B" $ - equalE [<] (F "A") (F "B"), + equalE empty (F "A") (F "B"), testEq "0=1 ⊢ A = B" $ - equalE {eqs = ZeroIsOne} [<] (F "A") (F "B"), + equalE (MkTyContext ZeroIsOne [<]) (F "A") (F "B"), testEq "A : ★₁ ≔ ★₀ ⊢ A = (★₀ ∷ ★₁)" {globals = au_bu} $ - equalE [<] (F "A") (TYPE 0 :# TYPE 1), + equalE empty (F "A") (TYPE 0 :# TYPE 1), testEq "A : ★₁ ≔ ★₀ ⊢ [A] = ★₀" {globals = au_bu} $ - equalT [<] (TYPE 1) (FT "A") (TYPE 0), + equalT empty (TYPE 1) (FT "A") (TYPE 0), testEq "A ≔ ★₀, B ≔ ★₀ ⊢ A = B" {globals = au_bu} $ - equalE [<] (F "A") (F "B"), + equalE empty (F "A") (F "B"), testEq "A ≔ ★₀, B ≔ A ⊢ A = B" {globals = au_ba} $ - equalE [<] (F "A") (F "B"), + equalE empty (F "A") (F "B"), testEq "A <: A" $ - subE [<] (F "A") (F "A"), + subE empty (F "A") (F "A"), testNeq "A ≮: B" $ - subE [<] (F "A") (F "B"), + subE empty (F "A") (F "B"), testEq "A : ★₃ ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: B" {globals = fromList [("A", mkDef Any (TYPE 3) (TYPE 0)), ("B", mkDef Any (TYPE 3) (TYPE 2))]} $ - subE [<] (F "A") (F "B"), + subE empty (F "A") (F "B"), note "(A and B in different universes)", testEq "A : ★₁ ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: B" {globals = fromList [("A", mkDef Any (TYPE 1) (TYPE 0)), ("B", mkDef Any (TYPE 3) (TYPE 2))]} $ - subE [<] (F "A") (F "B"), + subE empty (F "A") (F "B"), testEq "0=1 ⊢ A <: B" $ - subE [<] (F "A") (F "B") {eqs = ZeroIsOne} + subE (MkTyContext ZeroIsOne [<]) (F "A") (F "B") ], "bound var" :- [ testEq "#0 = #0" $ - equalE [< TYPE 0] (BV 0) (BV 0) {n = 1}, + equalE (MkTyContext new [< TYPE 0]) (BV 0) (BV 0), testEq "#0 <: #0" $ - subE [< TYPE 0] (BV 0) (BV 0) {n = 1}, + subE (MkTyContext new [< TYPE 0]) (BV 0) (BV 0), testNeq "#0 ≠ #1" $ - equalE [< TYPE 0, TYPE 0] (BV 0) (BV 1) {n = 2}, + equalE (MkTyContext new [< TYPE 0, TYPE 0]) (BV 0) (BV 1), testNeq "#0 ≮: #1" $ - subE [< TYPE 0, TYPE 0] (BV 0) (BV 1) {n = 2}, + subE (MkTyContext new [< TYPE 0, TYPE 0]) (BV 0) (BV 1), testEq "0=1 ⊢ #0 = #1" $ - equalE [< TYPE 0, TYPE 0] (BV 0) (BV 1) - {n = 2, eqs = ZeroIsOne} + equalE (MkTyContext ZeroIsOne [< TYPE 0, TYPE 0]) (BV 0) (BV 1) ], "application" :- [ testEq "f [a] = f [a]" $ - equalE [<] (F "f" :@ FT "a") (F "f" :@ FT "a"), + equalE empty (F "f" :@ FT "a") (F "f" :@ FT "a"), testEq "f [a] <: f [a]" $ - subE [<] (F "f" :@ FT "a") (F "f" :@ FT "a"), + subE empty (F "f" :@ FT "a") (F "f" :@ FT "a"), testEq "(λ x ⇒ [x] ∷ A ⊸ A) a = ([a ∷ A] ∷ A) (β)" $ - equalE [<] + equalE empty (((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a") (E (FT "a" :# FT "A") :# FT "A"), testEq "(λ x ⇒ [x] ∷ A ⊸ A) a = a (βυ)" $ - equalE [<] + equalE empty (((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a") (F "a"), testEq "(λ g ⇒ [g [a]] ∷ ⋯)) [f] = (λ y ⇒ [f [y]] ∷ ⋯) [a] (β↘↙)" $ let a = FT "A"; a2a = (Arr One a a) in - equalE [<] + equalE empty (((["g"] :\\ E (BV 0 :@ FT "a")) :# Arr One a2a a) :@ FT "f") (((["y"] :\\ E (F "f" :@ BVT 0)) :# a2a) :@ FT "a"), testEq "(λ x ⇒ [x] ∷ A ⊸ A) a <: a" $ - subE [<] + subE empty (((["x"] :\\ BVT 0) :# (Arr One (FT "A") (FT "A"))) :@ FT "a") (F "a"), note "id : A ⊸ A ≔ λ x ⇒ [x]", - testEq "id [a] = a" $ equalE [<] (F "id" :@ FT "a") (F "a"), - testEq "id [a] <: a" $ subE [<] (F "id" :@ FT "a") (F "a") + testEq "id [a] = a" $ equalE empty (F "id" :@ FT "a") (F "a"), + testEq "id [a] <: a" $ subE empty (F "id" :@ FT "a") (F "a") ], todo "dim application", "annotation" :- [ testEq "(λ x ⇒ f [x]) ∷ A ⊸ A = [f] ∷ A ⊸ A" $ - equalE [<] + equalE empty ((["x"] :\\ E (F "f" :@ BVT 0)) :# Arr One (FT "A") (FT "A")) (FT "f" :# Arr One (FT "A") (FT "A")), testEq "[f] ∷ A ⊸ A = f" $ - equalE [<] (FT "f" :# Arr One (FT "A") (FT "A")) (F "f"), + equalE empty (FT "f" :# Arr One (FT "A") (FT "A")) (F "f"), testEq "(λ x ⇒ f [x]) ∷ A ⊸ A = f" $ - equalE [<] + equalE empty ((["x"] :\\ E (F "f" :@ BVT 0)) :# Arr One (FT "A") (FT "A")) (F "f") ], "elim closure" :- [ testEq "#0{a} = a" $ - equalE [<] (CloE (BV 0) (F "a" ::: id)) (F "a"), + equalE empty (CloE (BV 0) (F "a" ::: id)) (F "a"), testEq "#1{a} = #0" $ - equalE [< FT "A"] (CloE (BV 1) (F "a" ::: id)) (BV 0) {n = 1} + equalE (MkTyContext new [< FT "A"]) + (CloE (BV 1) (F "a" ::: id)) (BV 0) ], "elim d-closure" :- [ note "0·eq-ab : (A ≡ B : ★₀)", testEq "(eq-ab #0)‹𝟎› = eq-ab 𝟎" $ - equalE {d = 1} [<] + equalED 1 empty (DCloE (F "eq-ab" :% BV 0) (K Zero ::: id)) (F "eq-ab" :% K Zero), testEq "(eq-ab #0)‹𝟎› = A" $ - equalE {d = 1} [<] (DCloE (F "eq-ab" :% BV 0) (K Zero ::: id)) (F "A"), + equalED 1 empty (DCloE (F "eq-ab" :% BV 0) (K Zero ::: id)) (F "A"), testEq "(eq-ab #0)‹𝟏› = B" $ - equalE {d = 1} [<] (DCloE (F "eq-ab" :% BV 0) (K One ::: id)) (F "B"), + equalED 1 empty (DCloE (F "eq-ab" :% BV 0) (K One ::: id)) (F "B"), testNeq "(eq-ab #0)‹𝟏› ≠ A" $ - equalE {d = 1} [<] (DCloE (F "eq-ab" :% BV 0) (K One ::: id)) (F "A"), + equalED 1 empty (DCloE (F "eq-ab" :% BV 0) (K One ::: id)) (F "A"), testEq "(eq-ab #0)‹#0,𝟎› = (eq-ab #0)" $ - equalE {d = 2} [<] + equalED 2 empty (DCloE (F "eq-ab" :% BV 0) (BV 0 ::: K Zero ::: id)) (F "eq-ab" :% BV 0), testNeq "(eq-ab #0)‹𝟎› ≠ (eq-ab 𝟎)" $ - equalE {d = 2} [<] + equalED 2 empty (DCloE (F "eq-ab" :% BV 0) (BV 0 ::: K Zero ::: id)) (F "eq-ab" :% K Zero), testEq "#0‹𝟎› = #0 # term and dim vars distinct" $ - equalE {d = 1, n = 1} [< FT "A"] (DCloE (BV 0) (K Zero ::: id)) (BV 0), + equalED 1 (MkTyContext new [< FT "A"]) + (DCloE (BV 0) (K Zero ::: id)) (BV 0), testEq "a‹𝟎› = a" $ - equalE {d = 1} [<] (DCloE (F "a") (K Zero ::: id)) (F "a"), + equalED 1 empty (DCloE (F "a") (K Zero ::: id)) (F "a"), testEq "(f [a])‹𝟎› = f‹𝟎› [a]‹𝟎›" $ let th = (K Zero ::: id) in - equalE {d = 1} [<] + equalED 1 empty (DCloE (F "f" :@ FT "a") th) (DCloE (F "f") th :@ DCloT (FT "a") th) ], "clashes" :- [ testNeq "★₀ ≠ ★₀ ⇾ ★₀" $ - equalT [<] (TYPE 1) (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)), + equalT empty (TYPE 1) (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)), testEq "0=1 ⊢ ★₀ = ★₀ ⇾ ★₀" $ - equalT [<] (TYPE 1) (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)) - {eqs = ZeroIsOne}, + equalT (MkTyContext ZeroIsOne [<]) + (TYPE 1) (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)), todo "others" ] ] diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr index 2126bf3..6d8f931 100644 --- a/tests/Tests/Typechecker.idr +++ b/tests/Tests/Typechecker.idr @@ -75,7 +75,7 @@ ctx = MkTyContext new inferredTypeEq : TyContext Three d n -> (exp, got : Term Three d n) -> M () inferredTypeEq ctx exp got = catchError - (inj $ equalType ctx.dctx ctx.tctx exp got) + (inj $ equalType ctx exp got) (\_ : Error' => throwError $ WrongInfer exp got) qoutEq : (exp, got : QOutput Three n) -> M ()