From 302de6266e60716f3452e6364bde82198c10c9cc Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sat, 25 Feb 2023 15:24:45 +0100 Subject: [PATCH] nicer constructors for ASTs --- lib/Quox/Syntax/Term/Base.idr | 38 ++++++++-- tests/Tests/Equal.idr | 16 +++-- tests/Tests/Typechecker.idr | 127 +++++++++++++++------------------- 3 files changed, 98 insertions(+), 83 deletions(-) diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr index fb18f95..4e50f88 100644 --- a/lib/Quox/Syntax/Term/Base.idr +++ b/lib/Quox/Syntax/Term/Base.idr @@ -152,20 +152,48 @@ mutual %name Scoped body %name ScopedBody body +||| scope which ignores all its binders +public export %inline +SN : {s : Nat} -> f n -> Scoped s f n +SN = S (replicate s "_") . N + +||| scope which uses its binders +public export %inline +SY : Vect s BaseName -> f (s + n) -> Scoped s f n +SY ns = S ns . Y + +||| more convenient Pi +public export %inline +Pi_ : (qty : q) -> (x : BaseName) -> + (arg : Term q d n) -> (res : Term q d (S n)) -> Term q d n +Pi_ {qty, x, arg, res} = Pi {qty, arg, res = S [x] $ Y res} + ||| non dependent function type public export %inline Arr : (qty : q) -> (arg, res : Term q d n) -> Term q d n -Arr {qty, arg, res} = Pi {qty, arg, res = S ["_"] $ N res} +Arr {qty, arg, res} = Pi {qty, arg, res = SN res} -||| non dependent equality type +||| more convenient Sig public export %inline -Eq0 : (ty, l, r : Term q d n) -> Term q d n -Eq0 {ty, l, r} = Eq {ty = S ["_"] $ N ty, l, r} +Sig_ : (x : BaseName) -> (fst : Term q d n) -> + (snd : Term q d (S n)) -> Term q d n +Sig_ {x, fst, snd} = Sig {fst, snd = S [x] $ Y snd} ||| non dependent pair type public export %inline And : (fst, snd : Term q d n) -> Term q d n -And {fst, snd} = Sig {fst, snd = S ["_"] $ N snd} +And {fst, snd} = Sig {fst, snd = SN snd} + +||| more convenient Eq +public export %inline +Eq_ : (i : BaseName) -> (ty : Term q (S d) n) -> + (l, r : Term q d n) -> Term q d n +Eq_ {i, ty, l, r} = Eq {ty = S [i] $ Y ty, l, r} + +||| non dependent equality type +public export %inline +Eq0 : (ty, l, r : Term q d n) -> Term q d n +Eq0 {ty, l, r} = Eq {ty = SN ty, l, r} ||| same as `F` but as a term public export %inline diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr index 0fb43b9..0ce5908 100644 --- a/tests/Tests/Equal.idr +++ b/tests/Tests/Equal.idr @@ -12,10 +12,10 @@ defGlobals : Definitions Three defGlobals = fromList [("A", mkAbstract Zero $ TYPE 0), ("B", mkAbstract Zero $ TYPE 0), - ("a", mkAbstract Any $ FT "A"), - ("a'", mkAbstract Any $ FT "A"), - ("b", mkAbstract Any $ FT "B"), - ("f", mkAbstract Any $ Arr One (FT "A") (FT "A")), + ("a", mkAbstract Any $ FT "A"), + ("a'", mkAbstract Any $ FT "A"), + ("b", mkAbstract Any $ FT "B"), + ("f", mkAbstract Any $ Arr One (FT "A") (FT "A")), ("id", mkDef Any (Arr One (FT "A") (FT "A")) (["x"] :\\ BVT 0)), ("eq-ab", mkAbstract Zero $ Eq0 (TYPE 0) (FT "A") (FT "B"))] @@ -117,6 +117,7 @@ tests = "equality & subtyping" :- [ let tm1 = Arr Zero (FT "A") (FT "B") tm2 = Arr One (FT "A") (FT "B") in equalT (MkTyContext ZeroIsOne [<]) (TYPE 0) tm1 tm2, + todo "dependent function types", note "[todo] should π ≤ ρ ⊢ (ρ·A) → B <: (π·A) → B?" ], @@ -143,8 +144,8 @@ tests = "equality & subtyping" :- [ (["x", "y"] :\\ BVT 0), testEq "λ x ⇒ [a] = λ x ⇒ [a] (Y vs N)" $ equalT empty (Arr Zero (FT "B") (FT "A")) - (Lam $ S ["x"] $ Y $ FT "a") - (Lam $ S ["x"] $ N $ FT "a"), + (Lam $ SY ["x"] $ FT "a") + (Lam $ SN $ FT "a"), testEq "λ x ⇒ [f [x]] = [f] (η)" $ equalT empty (Arr One (FT "A") (FT "A")) (["x"] :\\ E (F "f" :@ BVT 0)) @@ -159,7 +160,8 @@ tests = "equality & subtyping" :- [ {globals = fromList [("A", mkDef zero (TYPE 2) (TYPE 1))]} $ equalT empty (TYPE 2) (Eq0 (TYPE 1) (TYPE 0) (TYPE 0)) - (Eq0 (FT "A") (TYPE 0) (TYPE 0)) + (Eq0 (FT "A") (TYPE 0) (TYPE 0)), + todo "dependent equality types" ], "equalities and uip" :- diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr index 84d4d86..c19e51b 100644 --- a/tests/Tests/Typechecker.idr +++ b/tests/Tests/Typechecker.idr @@ -36,8 +36,8 @@ inj act = do reflTy : IsQty q => Term q d n reflTy = - Pi zero (TYPE 0) $ S ["A"] $ Y $ - Pi one (BVT 0) $ S ["x"] $ Y $ + Pi_ zero "A" (TYPE 0) $ + Pi_ one "x" (BVT 0) $ Eq0 (BVT 1) (BVT 0) (BVT 0) reflDef : IsQty q => Term q d n @@ -46,30 +46,28 @@ reflDef = ["A","x"] :\\ ["i"] :\\% BVT 0 fstTy : Term Three d n fstTy = - (Pi Zero (TYPE 1) $ S ["A"] $ Y $ - Pi Zero (Arr Any (BVT 0) (TYPE 1)) $ S ["B"] $ Y $ - Arr Any (Sig (BVT 1) $ S ["x"] $ Y $ E $ BV 1 :@ BVT 0) - (BVT 1)) + (Pi_ Zero "A" (TYPE 1) $ + Pi_ Zero "B" (Arr Any (BVT 0) (TYPE 1)) $ + Arr Any (Sig_ "x" (BVT 1) $ E $ BV 1 :@ BVT 0) (BVT 1)) fstDef : Term Three d n fstDef = (["A","B","p"] :\\ - E (CasePair Any (BV 0) (S ["_"] $ N $ BVT 2) - (S ["x","y"] $ Y $ BVT 1))) + E (CasePair Any (BV 0) (SN $ BVT 2) (SY ["x","y"] $ BVT 1))) sndTy : Term Three d n sndTy = - (Pi Zero (TYPE 1) $ S ["A"] $ Y $ - Pi Zero (Arr Any (BVT 0) (TYPE 1)) $ S ["B"] $ Y $ - Pi Any (Sig (BVT 1) $ S ["x"] $ Y $ E $ BV 1 :@ BVT 0) $ S ["p"] $ Y $ + (Pi_ Zero "A" (TYPE 1) $ + Pi_ Zero "B" (Arr Any (BVT 0) (TYPE 1)) $ + Pi_ Any "p" (Sig_ "x" (BVT 1) $ E $ BV 1 :@ BVT 0) $ E (BV 1 :@ E (F "fst" :@@ [BVT 2, BVT 1, BVT 0]))) sndDef : Term Three d n sndDef = (["A","B","p"] :\\ E (CasePair Any (BV 0) - (S ["p"] $ Y $ E $ BV 2 :@ E (F "fst" :@@ [BVT 3, BVT 2, BVT 0])) - (S ["x","y"] $ Y $ BVT 0))) + (SY ["p"] $ E $ BV 2 :@ E (F "fst" :@@ [BVT 3, BVT 2, BVT 0])) + (SY ["x","y"] $ BVT 0))) defGlobals : Definitions Three @@ -85,8 +83,8 @@ defGlobals = fromList ("f", mkAbstract Any $ Arr One (FT "A") (FT "A")), ("g", mkAbstract Any $ Arr One (FT "A") (FT "B")), ("f2", mkAbstract Any $ Arr One (FT "A") $ Arr One (FT "A") (FT "B")), - ("p", mkAbstract Any $ Pi One (FT "A") $ S ["x"] $ Y $ E $ F "P" :@ BVT 0), - ("q", mkAbstract Any $ Pi One (FT "A") $ S ["x"] $ Y $ E $ F "P" :@ BVT 0), + ("p", mkAbstract Any $ Pi_ One "x" (FT "A") $ E $ F "P" :@ BVT 0), + ("q", mkAbstract Any $ Pi_ One "x" (FT "A") $ E $ F "P" :@ BVT 0), ("refl", mkDef Any reflTy reflDef), ("fst", mkDef Any fstTy fstDef), ("snd", mkDef Any sndTy sndDef)] @@ -180,7 +178,7 @@ tests = "typechecker" :- [ check_ (ctx [<]) szero (Arr One (FT "C") (FT "D")) (TYPE 0), testTC "0 · (1·x : A) → P x ⇐ ★₀" $ check_ (ctx [<]) szero - (Pi One (FT "A") $ S ["x"] $ Y $ E $ F "P" :@ BVT 0) + (Pi_ One "x" (FT "A") $ E $ F "P" :@ BVT 0) (TYPE 0), testTCFail "0 · A ⊸ P ⇍ ★₀" $ check_ (ctx [<]) szero (Arr One (FT "A") $ FT "P") (TYPE 0), @@ -196,14 +194,14 @@ tests = "typechecker" :- [ check_ (ctx [<]) szero (FT "A" `And` FT "P") (TYPE 0), testTC "0 · (x : A) × P x ⇐ ★₀" $ check_ (ctx [<]) szero - (Sig (FT "A") $ S ["x"] $ Y $ E $ F "P" :@ BVT 0) (TYPE 0), + (Sig_ "x" (FT "A") $ E $ F "P" :@ BVT 0) (TYPE 0), testTC "0 · (x : A) × P x ⇐ ★₁" $ check_ (ctx [<]) szero - (Sig (FT "A") $ S ["x"] $ Y $ E $ F "P" :@ BVT 0) (TYPE 1), + (Sig_ "x" (FT "A") $ E $ F "P" :@ BVT 0) (TYPE 1), testTC "0 · (A : ★₀) × A ⇐ ★₁" $ - check_ (ctx [<]) szero (Sig (TYPE 0) $ S ["A"] $ Y $ BVT 0) (TYPE 1), + check_ (ctx [<]) szero (Sig_ "A" (TYPE 0) $ BVT 0) (TYPE 1), testTCFail "0 · (A : ★₀) × A ⇍ ★₀" $ - check_ (ctx [<]) szero (Sig (TYPE 0) $ S ["A"] $ Y $ BVT 0) (TYPE 0), + check_ (ctx [<]) szero (Sig_ "A" (TYPE 0) $ BVT 0) (TYPE 0), testTCFail "1 · A × A ⇍ ★₀" $ check_ (ctx [<]) sone (FT "A" `And` FT "A") (TYPE 0) ], @@ -214,15 +212,13 @@ tests = "typechecker" :- [ testTC "0 · {a,b,c} ⇐ ★₀" $ check_ (ctx [<]) szero (enum ["a", "b", "c"]) (TYPE 0), testTC "0 · {a,b,c} ⇐ ★₃" $ - check_ (ctx [<]) szero - (Sig (FT "A") $ S ["x"] $ Y $ E $ F "P" :@ BVT 0) (TYPE 0), + check_ (ctx [<]) szero (Sig_ "x" (FT "A") $ E $ F "P" :@ BVT 0) (TYPE 0), testTC "0 · (x : A) × P x ⇐ ★₁" $ - check_ (ctx [<]) szero - (Sig (FT "A") $ S ["x"] $ Y $ E $ F "P" :@ BVT 0) (TYPE 1), + check_ (ctx [<]) szero (Sig_ "x" (FT "A") $ E $ F "P" :@ BVT 0) (TYPE 1), testTC "0 · (A : ★₀) × A ⇐ ★₁" $ - check_ (ctx [<]) szero (Sig (TYPE 0) $ S ["A"] $ Y $ BVT 0) (TYPE 1), + check_ (ctx [<]) szero (Sig_ "A" (TYPE 0) $ BVT 0) (TYPE 1), testTCFail "0 · (A : ★₀) × A ⇍ ★₀" $ - check_ (ctx [<]) szero (Sig (TYPE 0) $ S ["A"] $ Y $ BVT 0) (TYPE 0), + check_ (ctx [<]) szero (Sig_ "A" (TYPE 0) $ BVT 0) (TYPE 0), testTCFail "1 · A × A ⇍ ★₀" $ check_ (ctx [<]) sone (FT "A" `And` FT "A") (TYPE 0) ], @@ -251,7 +247,7 @@ tests = "typechecker" :- [ testTCFail "1 · A ⇏ ★₀" $ infer_ (ctx [<]) sone (F "A"), note "refl : (0·A : ★₀) → (1·x : A) → (x ≡ x : A) ≔ (λ A x ⇒ λᴰ _ ⇒ x)", - testTC "1 · refl ⇒ ⋯" $ inferAs (ctx [<]) sone (F "refl") reflTy, + testTC "1 · refl ⇒ ⋯" $ inferAs (ctx [<]) sone (F "refl") reflTy, testTC "1 · [refl] ⇐ ⋯" $ check_ (ctx [<]) sone (FT "refl") reflTy ], @@ -296,51 +292,43 @@ tests = "typechecker" :- [ testTC "1 · (a, λᴰ i ⇒ a) ⇐ (x : A) × (x ≡ a)" $ check_ (ctx [<]) sone (Pair (FT "a") (["i"] :\\% FT "a")) - (Sig (FT "A") $ S ["x"] $ Y $ - Eq0 (FT "A") (BVT 0) (FT "a")) + (Sig_ "x" (FT "A") $ Eq0 (FT "A") (BVT 0) (FT "a")) ], "unpairing" :- [ testTC "x : A × A ⊢ 1 · (case1 x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 1·x" $ inferAsQ (ctx [< FT "A" `And` FT "A"]) sone - (CasePair One (BV 0) - (S ["_"] $ N $ FT "B") - (S ["l", "r"] $ Y $ E $ F "f2" :@@ [BVT 1, BVT 0])) + (CasePair One (BV 0) (SN $ FT "B") + (SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])) (FT "B") [< One], testTC "x : A × A ⊢ 1 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ ω·x" $ inferAsQ (ctx [< FT "A" `And` FT "A"]) sone - (CasePair Any (BV 0) - (S ["_"] $ N $ FT "B") - (S ["l", "r"] $ Y $ E $ F "f2" :@@ [BVT 1, BVT 0])) + (CasePair Any (BV 0) (SN $ FT "B") + (SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])) (FT "B") [< Any], testTC "x : A × A ⊢ 0 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 0·x" $ inferAsQ (ctx [< FT "A" `And` FT "A"]) szero - (CasePair Any (BV 0) - (S ["_"] $ N $ FT "B") - (S ["l", "r"] $ Y $ E $ F "f2" :@@ [BVT 1, BVT 0])) + (CasePair Any (BV 0) (SN $ FT "B") + (SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])) (FT "B") [< Zero], testTCFail "x : A × A ⊢ 1 · (case0 x return B of (l,r) ⇒ f2 l r) ⇏" $ infer_ (ctx [< FT "A" `And` FT "A"]) sone - (CasePair Zero (BV 0) - (S ["_"] $ N $ FT "B") - (S ["l", "r"] $ Y $ E $ F "f2" :@@ [BVT 1, BVT 0])), + (CasePair Zero (BV 0) (SN $ FT "B") + (SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])), testTC "x : A × B ⊢ 1 · (caseω x return A of (l,r) ⇒ l) ⇒ A ⊳ ω·x" $ inferAsQ (ctx [< FT "A" `And` FT "B"]) sone - (CasePair Any (BV 0) - (S ["_"] $ N $ FT "A") - (S ["l", "r"] $ Y $ BVT 1)) + (CasePair Any (BV 0) (SN $ FT "A") + (SY ["l", "r"] $ BVT 1)) (FT "A") [< Any], testTC "x : A × B ⊢ 0 · (case1 x return A of (l,r) ⇒ l) ⇒ A ⊳ 0·x" $ inferAsQ (ctx [< FT "A" `And` FT "B"]) szero - (CasePair One (BV 0) - (S ["_"] $ N $ FT "A") - (S ["l", "r"] $ Y $ BVT 1)) + (CasePair One (BV 0) (SN $ FT "A") + (SY ["l", "r"] $ BVT 1)) (FT "A") [< Zero], testTCFail "x : A × B ⊢ 1 · (case1 x return A of (l,r) ⇒ l) ⇏" $ infer_ (ctx [< FT "A" `And` FT "B"]) sone - (CasePair One (BV 0) - (S ["_"] $ N $ FT "A") - (S ["l", "r"] $ Y $ BVT 1)), + (CasePair One (BV 0) (SN $ FT "A") + (SY ["l", "r"] $ BVT 1)), note "fst : (0·A : ★₁) → (0·B : A ↠ ★₁) → ((x : A) × B x) ↠ A", note " ≔ (λ A B p ⇒ caseω p return A of (x, y) ⇒ x)", testTC "0 · ‹type of fst› ⇐ ★₂" $ @@ -356,7 +344,7 @@ tests = "typechecker" :- [ testTC "0 · snd ★₀ (λ x ⇒ x) ⇒ (ω·p : (A : ★₀) × A) → fst ★₀ (λ x ⇒ x) p" $ inferAs (ctx [<]) szero (F "snd" :@@ [TYPE 0, ["x"] :\\ BVT 0]) - (Pi Any (Sig (TYPE 0) $ S ["A"] $ Y $ BVT 0) $ S ["p"] $ Y $ + (Pi_ Any "A" (Sig_ "A" (TYPE 0) $ BVT 0) $ (E $ F "fst" :@@ [TYPE 0, ["x"] :\\ BVT 0, BVT 0])) ], @@ -373,20 +361,19 @@ tests = "typechecker" :- [ "equalities" :- [ testTC "1 · (λᴰ i ⇒ a) ⇐ a ≡ a" $ - check_ (ctx [<]) sone (DLam $ S ["i"] $ N $ FT "a") + check_ (ctx [<]) sone (DLam $ SN $ FT "a") (Eq0 (FT "A") (FT "a") (FT "a")), testTC "0 · (λ p q ⇒ λᴰ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q" $ check_ (ctx [<]) szero - (Lam $ S ["p"] $ Y $ Lam $ S ["q"] $ N $ DLam $ S ["i"] $ N $ BVT 0) - (Pi Any (Eq0 (FT "A") (FT "a") (FT "a")) $ S ["p"] $ Y $ - Pi Any (Eq0 (FT "A") (FT "a") (FT "a")) $ S ["q"] $ Y $ + (["p","q"] :\\ ["i"] :\\% BVT 1) + (Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $ + Pi_ Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $ Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0)), testTC "0 · (λ p q ⇒ λᴰ i ⇒ q) ⇐ (ω·p q : a ≡ a') → p ≡ q" $ check_ (ctx [<]) szero - (Lam $ S ["p"] $ N $ Lam $ S ["q"] $ Y $ - DLam $ S ["i"] $ N $ BVT 0) - (Pi Any (Eq0 (FT "A") (FT "a") (FT "a")) $ S ["p"] $ Y $ - Pi Any (Eq0 (FT "A") (FT "a") (FT "a")) $ S ["q"] $ Y $ + (["p","q"] :\\ ["i"] :\\% BVT 0) + (Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $ + Pi_ Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $ Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0)) ], @@ -398,11 +385,11 @@ tests = "typechecker" :- [ testTC "cong" $ check_ (ctx [<]) sone (["x", "y", "xy"] :\\ ["i"] :\\% E (F "p" :@ E (BV 0 :% BV 0))) - (Pi Zero (FT "A") $ S ["x"] $ Y $ - Pi Zero (FT "A") $ S ["y"] $ Y $ - Pi One (Eq0 (FT "A") (BVT 1) (BVT 0)) $ S ["xy"] $ Y $ - Eq (S ["i"] $ Y $ E $ F "P" :@ E (BV 0 :% BV 0)) - (E $ F "p" :@ BVT 2) (E $ F "p" :@ BVT 1)), + (Pi_ Zero "x" (FT "A") $ + Pi_ Zero "y" (FT "A") $ + Pi_ One "xy" (Eq0 (FT "A") (BVT 1) (BVT 0)) $ + Eq_ "i" (E $ F "P" :@ E (BV 0 :% BV 0)) + (E $ F "p" :@ BVT 2) (E $ F "p" :@ BVT 1)), note "0·A : Type, 0·P : ω·A → Type,", note "ω·p q : (1·x : A) → P x", note "⊢", @@ -411,12 +398,10 @@ tests = "typechecker" :- [ testTC "funext" $ check_ (ctx [<]) sone (["eq"] :\\ ["i"] :\\% ["x"] :\\ E (BV 1 :@ BVT 0 :% BV 0)) - (Pi One - (Pi One (FT "A") $ S ["x"] $ Y $ - Eq0 (E $ F "P" :@ BVT 0) - (E $ F "p" :@ BVT 0) (E $ F "q" :@ BVT 0)) $ - S ["eq"] $ Y $ - Eq0 (Pi Any (FT "A") $ S ["x"] $ Y $ E $ F "P" :@ BVT 0) - (FT "p") (FT "q")) + (Pi_ One "eq" + (Pi_ One "x" (FT "A") + (Eq0 (E $ F "P" :@ BVT 0) + (E $ F "p" :@ BVT 0) (E $ F "q" :@ BVT 0))) + (Eq0 (Pi_ Any "x" (FT "A") $ E $ F "P" :@ BVT 0) (FT "p") (FT "q"))) ] ]