rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

parser

Browse source
This commit is contained in:
rhiannon morris 2023-03-04 21:02:51 +01:00
parent 95a6644a6c
commit edeee68cb7
11 changed files with 788 additions and 159 deletions
Download patch file Download diff file Expand all files Collapse all files

68
tests/Tests/Typechecker.idr
View file

@ -207,14 +207,14 @@ tests = "typechecker" :- [
],
"enum types" :- [
testTC "0 · `{} ⇐ ★₀" $ check_ (ctx [<]) szero (enum []) (TYPE 0),
testTC "0 · `{} ⇐ ★₃" $ check_ (ctx [<]) szero (enum []) (TYPE 3),
testTC "0 · `{a,b,c} ⇐ ★₀" $
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} ⇐ ★₃" $
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)
testTCFail "1 · {} ⇍ ★₀" $ check_ (ctx [<]) sone (enum []) (TYPE 0),
testTC "0=1 ⊢ 1 · {} ⇐ ★₀" $ check_ (ctx01 [<]) sone (enum []) (TYPE 0)
],
"free vars" :- [
@ -229,7 +229,7 @@ tests = "typechecker" :- [
note "(fail) runtime-relevant type",
testTCFail "1 · A ⇏ ★₀" $
infer_ (ctx [<]) sone (F "A"),
note "refl : (0·A : ★₀) → (1·x : A) → (x ≡ x : A) ≔ (λ A x. δ _. x)",
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] ⇐ ⋯" $ check_ (ctx [<]) sone (FT "refl") reflTy
],
@ -248,21 +248,21 @@ tests = "typechecker" :- [
"lambda" :- [
note "linear & unrestricted identity",
testTC "1 · (λ x. x) ⇐ A ⊸ A" $
testTC "1 · (λ x ⇒ x) ⇐ A ⊸ A" $
check_ (ctx [<]) sone (["x"] :\\ BVT 0) (Arr One (FT "A") (FT "A")),
testTC "1 · (λ x. x) ⇐ A → A" $
testTC "1 · (λ x ⇒ x) ⇐ A → A" $
check_ (ctx [<]) sone (["x"] :\\ BVT 0) (Arr Any (FT "A") (FT "A")),
note "(fail) zero binding used relevantly",
testTCFail "1 · (λ x. x) ⇍ A ⇾ A" $
testTCFail "1 · (λ x ⇒ x) ⇍ A ⇾ A" $
check_ (ctx [<]) sone (["x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")),
note "(but ok in overall erased context)",
testTC "0 · (λ x. x) ⇐ A ⇾ A" $
testTC "0 · (λ x ⇒ x) ⇐ A ⇾ A" $
check_ (ctx [<]) szero (["x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")),
testTC "1 · (λ A x. refl A x) ⇐ ⋯ # (type of refl)" $
testTC "1 · (λ A x ⇒ refl A x) ⇐ ⋯ # (type of refl)" $
check_ (ctx [<]) sone
(["A", "x"] :\\ E (F "refl" :@@ [BVT 1, BVT 0]))
reflTy,
testTC "1 · (λ A x. δ i. x) ⇐ ⋯ # (def. and type of refl)" $
testTC "1 · (λ A x ⇒ δ i ⇒ x) ⇐ ⋯ # (def. and type of refl)" $
check_ (ctx [<]) sone reflDef reflTy
],
@ -272,59 +272,59 @@ tests = "typechecker" :- [
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)" $
testTC "1 · (a, δ i ⇒ a) ⇐ (x : A) × (x ≡ a)" $
check_ (ctx [<]) sone
(Pair (FT "a") (["i"] :\\% 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" $
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) (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" $
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) (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" $
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) (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) ⇏" $
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) (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" $
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) (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" $
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) (SN $ FT "A")
(SY ["l", "r"] $ BVT 1))
(FT "A") [< Zero],
testTCFail "x : A × B ⊢ 1 · (case1 x return A of (l,r). l) ⇏" $
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) (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)",
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)",
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" $
testTC "0 · snd ★₀ (λ x ⇒ x) ⇒ (ω·p : (A : ★₀) × A) → fst ★₀ (λ x ⇒ x) p" $
inferAs (ctx [<]) szero
(F "snd" :@@ [TYPE 0, ["x"] :\\ BVT 0])
(Pi_ Any "A" (Sig_ "A" (TYPE 0) $ BVT 0) $
@ -332,27 +332,27 @@ tests = "typechecker" :- [
],
"enums" :- [
testTC "1 · `a ⇐ `{a}" $
testTC "1 · `a ⇐ {a}" $
check_ (ctx [<]) sone (Tag "a") (enum ["a"]),
testTC "1 · `a ⇐ `{a, b, c}" $
testTC "1 · `a ⇐ {a, b, c}" $
check_ (ctx [<]) sone (Tag "a") (enum ["a", "b", "c"]),
testTCFail "1 · `a ⇍ `{b, c}" $
testTCFail "1 · `a ⇍ {b, c}" $
check_ (ctx [<]) sone (Tag "a") (enum ["b", "c"]),
testTC "0=1 ⊢ 1 · `a ⇐ `{b, c}" $
testTC "0=1 ⊢ 1 · `a ⇐ {b, c}" $
check_ (ctx01 [<]) sone (Tag "a") (enum ["b", "c"])
],
"equalities" :- [
testTC "1 · (δ i. a) ⇐ a ≡ a" $
testTC "1 · (δ i ⇒ a) ⇐ a ≡ 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" $
testTC "0 · (λ p q ⇒ δ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
check_ (ctx [<]) szero
(["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" $
testTC "0 · (λ p q ⇒ δ i ⇒ q) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
check_ (ctx [<]) szero
(["p","q"] :\\ ["i"] :\\% BVT 0)
(Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $
@ -363,8 +363,8 @@ tests = "typechecker" :- [
"misc" :- [
note "0·A : Type, 0·P : A → Type, ω·p : (1·x : A) → P x",
note "⊢",
note "1 · λ x y xy. δ i. p (xy i)",
note " ⇐ (0·x y : A) → (1·xy : x ≡ y) → Eq [i. P (xy i)] (p x) (p y)",
note "1 · λ x y xy ⇒ δ i ⇒ p (xy i)",
note " ⇐ (0·x y : A) → (1·xy : x ≡ y) → Eq [i ⇒ P (xy i)] (p x) (p y)",
testTC "cong" $
check_ (ctx [<]) sone
(["x", "y", "xy"] :\\ ["i"] :\\% E (F "p" :@ E (BV 0 :% BV 0)))
@ -376,7 +376,7 @@ tests = "typechecker" :- [
note "0·A : Type, 0·P : ω·A → Type,",
note "ω·p q : (1·x : A) → P x",
note "⊢",
note "1 · λ eq. δ i. λ x. eq x i",
note "1 · λ eq ⇒ δ i ⇒ λ x ⇒ eq x i",
note " ⇐ (1·eq : (1·x : A) → p x ≡ q x) → p ≡ q",
testTC "funext" $
check_ (ctx [<]) sone