From 3d9b7308038a04cd80a4701a6c224705978b01db Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Thu, 23 Feb 2023 10:04:16 +0100 Subject: [PATCH] some more typechecker tests --- tests/Tests/Typechecker.idr | 186 ++++++++++++++++++++++++++++++++++-- 1 file changed, 176 insertions(+), 10 deletions(-) diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr index 2f44ef2..84d4d86 100644 --- a/tests/Tests/Typechecker.idr +++ b/tests/Tests/Typechecker.idr @@ -43,6 +43,35 @@ reflTy = reflDef : IsQty q => Term q d n 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)) + +fstDef : Term Three d n +fstDef = + (["A","B","p"] :\\ + E (CasePair Any (BV 0) (S ["_"] $ N $ BVT 2) + (S ["x","y"] $ 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 $ + 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))) + + defGlobals : Definitions Three defGlobals = fromList [("A", mkAbstract Zero $ TYPE 0), @@ -55,10 +84,12 @@ defGlobals = fromList ("b", mkAbstract Any $ FT "B"), ("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 "A")), + ("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), - ("refl", mkDef Any reflTy reflDef)] + ("refl", mkDef Any reflTy reflDef), + ("fst", mkDef Any fstTy fstDef), + ("snd", mkDef Any sndTy sndDef)] parameters (label : String) (act : Lazy (M ())) {default defGlobals globals : Definitions Three} @@ -69,8 +100,9 @@ parameters (label : String) (act : Lazy (M ())) testTCFail = testThrows label (const True) $ runReaderT globals act -ctx : TContext Three 0 n -> TyContext Three 0 n +ctx, ctx01 : TContext Three 0 n -> TyContext Three 0 n ctx = MkTyContext new +ctx01 = MkTyContext ZeroIsOne inferredTypeEq : TyContext Three d n -> (exp, got : Term Three d n) -> M () inferredTypeEq ctx exp got = @@ -111,6 +143,16 @@ check_ : TyContext Three d n -> SQty Three -> Term Three d n -> Term Three d n -> M () check_ ctx sg s ty = ignore $ inj $ check ctx sg s ty + +-- ω is not a subject qty +failing "Can't find an implementation" + sany : SQty Three + sany = Element Any %search + +enum : List TagVal -> Term q d n +enum = Enum . SortedSet.fromList + + export tests : Test tests = "typechecker" :- [ @@ -122,8 +164,7 @@ tests = "typechecker" :- [ testTCFail "0 · ★₀ ⇍ ★₀" $ check_ (ctx [<]) szero (TYPE 0) (TYPE 0), testTCFail "0 · ★_ ⇍ ★_" $ check_ (ctx [<]) szero (TYPE UAny) (TYPE UAny), testTCFail "1 · ★₀ ⇍ ★₁" $ check_ (ctx [<]) sone (TYPE 0) (TYPE 1), - testTC "0=1 ⊢ 0 · ★₁ ⇐ ★₀" $ - check_ (MkTyContext (ZeroIsOne {d = 0}) [<]) szero (TYPE 1) (TYPE 0) + testTC "0=1 ⊢ 0 · ★₁ ⇐ ★₀" $ check_ (ctx01 [<]) szero (TYPE 1) (TYPE 0) ], "function types" :- [ @@ -144,18 +185,59 @@ tests = "typechecker" :- [ testTCFail "0 · A ⊸ P ⇍ ★₀" $ check_ (ctx [<]) szero (Arr One (FT "A") $ FT "P") (TYPE 0), testTC "0=1 ⊢ 0 · A ⊸ P ⇐ ★₀" $ - check_ (MkTyContext (ZeroIsOne {d = 0}) [<]) szero - (Arr One (FT "A") $ FT "P") (TYPE 0) + check_ (ctx01 [<]) szero (Arr One (FT "A") $ FT "P") (TYPE 0) ], "pair types" :- [ note #""A × B" for "(_ : A) × B""#, testTC "0 · A × A ⇐ ★₀" $ check_ (ctx [<]) szero (FT "A" `And` FT "A") (TYPE 0), + testTCFail "0 · A × P ⇍ ★₀" $ + 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), + testTC "0 · (x : A) × P x ⇐ ★₁" $ + check_ (ctx [<]) szero + (Sig (FT "A") $ S ["x"] $ Y $ E $ F "P" :@ BVT 0) (TYPE 1), + testTC "0 · (A : ★₀) × A ⇐ ★₁" $ + check_ (ctx [<]) szero (Sig (TYPE 0) $ S ["A"] $ Y $ BVT 0) (TYPE 1), + testTCFail "0 · (A : ★₀) × A ⇍ ★₀" $ + check_ (ctx [<]) szero (Sig (TYPE 0) $ S ["A"] $ Y $ BVT 0) (TYPE 0), testTCFail "1 · A × A ⇍ ★₀" $ check_ (ctx [<]) sone (FT "A" `And` FT "A") (TYPE 0) ], + "enum types" :- [ + testTC "0 · {} ⇐ ★₀" $ check_ (ctx [<]) szero (enum []) (TYPE 0), + testTC "0 · {} ⇐ ★₃" $ check_ (ctx [<]) szero (enum []) (TYPE 3), + 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), + testTC "0 · (x : A) × P x ⇐ ★₁" $ + check_ (ctx [<]) szero + (Sig (FT "A") $ S ["x"] $ Y $ E $ F "P" :@ BVT 0) (TYPE 1), + testTC "0 · (A : ★₀) × A ⇐ ★₁" $ + check_ (ctx [<]) szero (Sig (TYPE 0) $ S ["A"] $ Y $ BVT 0) (TYPE 1), + testTCFail "0 · (A : ★₀) × A ⇍ ★₀" $ + check_ (ctx [<]) szero (Sig (TYPE 0) $ S ["A"] $ Y $ BVT 0) (TYPE 0), + testTCFail "1 · A × A ⇍ ★₀" $ + check_ (ctx [<]) sone (FT "A" `And` FT "A") (TYPE 0) + ], + + "enum types" :- [ + testTC "0 · {} ⇐ ★₀" $ check_ (ctx [<]) szero (enum []) (TYPE 0), + testTC "0 · {} ⇐ ★₃" $ check_ (ctx [<]) szero (enum []) (TYPE 3), + testTC "0 · {a,b,c} ⇐ ★₀" $ + check_ (ctx [<]) szero (enum ["a", "b", "c"]) (TYPE 0), + testTC "0 · {a,b,c} ⇐ ★₃" $ + check_ (ctx [<]) szero (enum ["a", "b", "c"]) (TYPE 3), + testTCFail "1 · {} ⇍ ★₀" $ check_ (ctx [<]) sone (enum []) (TYPE 0), + testTC "0=1 ⊢ 1 · {} ⇐ ★₀" $ check_ (ctx01 [<]) sone (enum []) (TYPE 0) + ], + "free vars" :- [ note "A : ★₀", testTC "0 · A ⇒ ★₀" $ @@ -179,10 +261,10 @@ tests = "typechecker" :- [ (BV 0) (FT "A") [< one], testTC "x : A ⊢ 1 · [x] ⇐ A ⊳ 1·x" $ checkQ {n = 1} (ctx [< FT "A"]) sone (BVT 0) (FT "A") [< one], - note "f2 : A ⊸ A ⊸ A", - testTC "x : A ⊢ 1 · f2 [x] [x] ⇒ A ⊳ ω·x" $ + note "f2 : A ⊸ A ⊸ B", + testTC "x : A ⊢ 1 · f2 [x] [x] ⇒ B ⊳ ω·x" $ inferAsQ {n = 1} (ctx [< FT "A"]) sone - (F "f2" :@@ [BVT 0, BVT 0]) (FT "A") [< Any] + (F "f2" :@@ [BVT 0, BVT 0]) (FT "B") [< Any] ], "lambda" :- [ @@ -205,6 +287,90 @@ tests = "typechecker" :- [ check_ (ctx [<]) sone reflDef reflTy ], + "pairs" :- [ + testTC "1 · (a, a) ⇐ A × A" $ + check_ (ctx [<]) sone (Pair (FT "a") (FT "a")) (FT "A" `And` FT "A"), + testTC "x : A ⊢ 1 · (x, x) ⇐ A × A ⊳ ω·x" $ + checkQ (ctx [< FT "A"]) sone + (Pair (BVT 0) (BVT 0)) (FT "A" `And` FT "A") [< Any], + 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")) + ], + + "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])) + (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])) + (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])) + (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])), + 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)) + (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)) + (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)), + 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› ⇐ ★₂" $ + check_ (ctx [<]) szero fstTy (TYPE 2), + testTC "1 · ‹def of fst› ⇐ ‹type of fst›" $ + check_ (ctx [<]) sone fstDef fstTy, + note "snd : (0·A : ★₁) → (0·B : A ↠ ★₁) → (ω·p : (x : A) × B x) → B (fst A B p)", + note " ≔ (λ A B p ⇒ caseω p return p ⇒ B (fst A B p) of (x, y) ⇒ y)", + testTC "0 · ‹type of snd› ⇐ ★₂" $ + check_ (ctx [<]) szero sndTy (TYPE 2), + testTC "1 · ‹def of snd› ⇐ ‹type of snd›" $ + check_ (ctx [<]) sone sndDef sndTy, + 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 $ + (E $ F "fst" :@@ [TYPE 0, ["x"] :\\ BVT 0, BVT 0])) + ], + + "enums" :- [ + testTC "1 · `a ⇐ {a}" $ + check_ (ctx [<]) sone (Tag "a") (enum ["a"]), + testTC "1 · `a ⇐ {a, b, c}" $ + check_ (ctx [<]) sone (Tag "a") (enum ["a", "b", "c"]), + testTCFail "1 · `a ⇍ {b, c}" $ + check_ (ctx [<]) sone (Tag "a") (enum ["b", "c"]), + testTC "0=1 ⊢ 1 · `a ⇐ {b, c}" $ + check_ (ctx01 [<]) sone (Tag "a") (enum ["b", "c"]) + ], + "equalities" :- [ testTC "1 · (λᴰ i ⇒ a) ⇐ a ≡ a" $ check_ (ctx [<]) sone (DLam $ S ["i"] $ N $ FT "a")