some more typechecker tests
This commit is contained in:
parent
4b814d7502
commit
3d9b730803
1 changed files with 176 additions and 10 deletions
|
|
@ -43,6 +43,35 @@ reflTy =
|
||||||
reflDef : IsQty q => Term q d n
|
reflDef : IsQty q => Term q d n
|
||||||
reflDef = ["A","x"] :\\ ["i"] :\\% BVT 0
|
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 : Definitions Three
|
||||||
defGlobals = fromList
|
defGlobals = fromList
|
||||||
[("A", mkAbstract Zero $ TYPE 0),
|
[("A", mkAbstract Zero $ TYPE 0),
|
||||||
|
|
@ -55,10 +84,12 @@ defGlobals = fromList
|
||||||
("b", mkAbstract Any $ FT "B"),
|
("b", mkAbstract Any $ FT "B"),
|
||||||
("f", mkAbstract Any $ Arr One (FT "A") (FT "A")),
|
("f", mkAbstract Any $ Arr One (FT "A") (FT "A")),
|
||||||
("g", mkAbstract Any $ Arr One (FT "A") (FT "B")),
|
("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),
|
("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),
|
("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 ()))
|
parameters (label : String) (act : Lazy (M ()))
|
||||||
{default defGlobals globals : Definitions Three}
|
{default defGlobals globals : Definitions Three}
|
||||||
|
|
@ -69,8 +100,9 @@ parameters (label : String) (act : Lazy (M ()))
|
||||||
testTCFail = testThrows label (const True) $ runReaderT globals act
|
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
|
ctx = MkTyContext new
|
||||||
|
ctx01 = MkTyContext ZeroIsOne
|
||||||
|
|
||||||
inferredTypeEq : TyContext Three d n -> (exp, got : Term Three d n) -> M ()
|
inferredTypeEq : TyContext Three d n -> (exp, got : Term Three d n) -> M ()
|
||||||
inferredTypeEq ctx exp got =
|
inferredTypeEq ctx exp got =
|
||||||
|
|
@ -111,6 +143,16 @@ check_ : TyContext Three d n -> SQty Three ->
|
||||||
Term Three d n -> Term Three d n -> M ()
|
Term Three d n -> Term Three d n -> M ()
|
||||||
check_ ctx sg s ty = ignore $ inj $ check ctx sg s ty
|
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
|
export
|
||||||
tests : Test
|
tests : Test
|
||||||
tests = "typechecker" :- [
|
tests = "typechecker" :- [
|
||||||
|
|
@ -122,8 +164,7 @@ tests = "typechecker" :- [
|
||||||
testTCFail "0 · ★₀ ⇍ ★₀" $ check_ (ctx [<]) szero (TYPE 0) (TYPE 0),
|
testTCFail "0 · ★₀ ⇍ ★₀" $ check_ (ctx [<]) szero (TYPE 0) (TYPE 0),
|
||||||
testTCFail "0 · ★_ ⇍ ★_" $ check_ (ctx [<]) szero (TYPE UAny) (TYPE UAny),
|
testTCFail "0 · ★_ ⇍ ★_" $ check_ (ctx [<]) szero (TYPE UAny) (TYPE UAny),
|
||||||
testTCFail "1 · ★₀ ⇍ ★₁" $ check_ (ctx [<]) sone (TYPE 0) (TYPE 1),
|
testTCFail "1 · ★₀ ⇍ ★₁" $ check_ (ctx [<]) sone (TYPE 0) (TYPE 1),
|
||||||
testTC "0=1 ⊢ 0 · ★₁ ⇐ ★₀" $
|
testTC "0=1 ⊢ 0 · ★₁ ⇐ ★₀" $ check_ (ctx01 [<]) szero (TYPE 1) (TYPE 0)
|
||||||
check_ (MkTyContext (ZeroIsOne {d = 0}) [<]) szero (TYPE 1) (TYPE 0)
|
|
||||||
],
|
],
|
||||||
|
|
||||||
"function types" :- [
|
"function types" :- [
|
||||||
|
|
@ -144,18 +185,59 @@ tests = "typechecker" :- [
|
||||||
testTCFail "0 · A ⊸ P ⇍ ★₀" $
|
testTCFail "0 · A ⊸ P ⇍ ★₀" $
|
||||||
check_ (ctx [<]) szero (Arr One (FT "A") $ FT "P") (TYPE 0),
|
check_ (ctx [<]) szero (Arr One (FT "A") $ FT "P") (TYPE 0),
|
||||||
testTC "0=1 ⊢ 0 · A ⊸ P ⇐ ★₀" $
|
testTC "0=1 ⊢ 0 · A ⊸ P ⇐ ★₀" $
|
||||||
check_ (MkTyContext (ZeroIsOne {d = 0}) [<]) szero
|
check_ (ctx01 [<]) szero (Arr One (FT "A") $ FT "P") (TYPE 0)
|
||||||
(Arr One (FT "A") $ FT "P") (TYPE 0)
|
|
||||||
],
|
],
|
||||||
|
|
||||||
"pair types" :- [
|
"pair types" :- [
|
||||||
note #""A × B" for "(_ : A) × B""#,
|
note #""A × B" for "(_ : A) × B""#,
|
||||||
testTC "0 · A × A ⇐ ★₀" $
|
testTC "0 · A × A ⇐ ★₀" $
|
||||||
check_ (ctx [<]) szero (FT "A" `And` FT "A") (TYPE 0),
|
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 ⇍ ★₀" $
|
testTCFail "1 · A × A ⇍ ★₀" $
|
||||||
check_ (ctx [<]) sone (FT "A" `And` FT "A") (TYPE 0)
|
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" :- [
|
"free vars" :- [
|
||||||
note "A : ★₀",
|
note "A : ★₀",
|
||||||
testTC "0 · A ⇒ ★₀" $
|
testTC "0 · A ⇒ ★₀" $
|
||||||
|
|
@ -179,10 +261,10 @@ tests = "typechecker" :- [
|
||||||
(BV 0) (FT "A") [< one],
|
(BV 0) (FT "A") [< one],
|
||||||
testTC "x : A ⊢ 1 · [x] ⇐ A ⊳ 1·x" $
|
testTC "x : A ⊢ 1 · [x] ⇐ A ⊳ 1·x" $
|
||||||
checkQ {n = 1} (ctx [< FT "A"]) sone (BVT 0) (FT "A") [< one],
|
checkQ {n = 1} (ctx [< FT "A"]) sone (BVT 0) (FT "A") [< one],
|
||||||
note "f2 : A ⊸ A ⊸ A",
|
note "f2 : A ⊸ A ⊸ B",
|
||||||
testTC "x : A ⊢ 1 · f2 [x] [x] ⇒ A ⊳ ω·x" $
|
testTC "x : A ⊢ 1 · f2 [x] [x] ⇒ B ⊳ ω·x" $
|
||||||
inferAsQ {n = 1} (ctx [< FT "A"]) sone
|
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" :- [
|
"lambda" :- [
|
||||||
|
|
@ -205,6 +287,90 @@ tests = "typechecker" :- [
|
||||||
check_ (ctx [<]) sone reflDef reflTy
|
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" :- [
|
"equalities" :- [
|
||||||
testTC "1 · (λᴰ i ⇒ a) ⇐ a ≡ a" $
|
testTC "1 · (λᴰ i ⇒ a) ⇐ a ≡ a" $
|
||||||
check_ (ctx [<]) sone (DLam $ S ["i"] $ N $ FT "a")
|
check_ (ctx [<]) sone (DLam $ S ["i"] $ N $ FT "a")
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue