quox/tests/Tests/Typechecker.idr

401 lines
15 KiB
Idris
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

module Tests.Typechecker
import Quox.Syntax
import Quox.Syntax.Qty.Three
import Quox.Typechecker as Lib
import public TypingImpls
import TAP
data Error'
= TCError (Typing.Error Three)
| WrongInfer (Term Three d n) (Term Three d n)
| WrongQOut (QOutput Three n) (QOutput Three n)
export
ToInfo Error' where
toInfo (TCError e) = toInfo e
toInfo (WrongInfer good bad) =
[("type", "WrongInfer"),
("wanted", prettyStr True good),
("got", prettyStr True bad)]
toInfo (WrongQOut good bad) =
[("type", "WrongQOut"),
("wanted", prettyStr True good),
("wanted", prettyStr True bad)]
0 M : Type -> Type
M = ReaderT (Definitions Three) $ Either Error'
inj : (forall m. CanTC Three m => m a) -> M a
inj act = do
env <- ask
let res = runReaderT env act {m = Either (Typing.Error Three)}
either (throwError . TCError) pure res
reflTy : IsQty q => Term q d n
reflTy =
Pi_ zero "A" (TYPE 0) $
Pi_ one "x" (BVT 0) $
Eq0 (BVT 1) (BVT 0) (BVT 0)
reflDef : IsQty q => Term q d n
reflDef = ["A","x"] :\\ ["i"] :\\% BVT 0
fstTy : Term Three d n
fstTy =
(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) (SN $ BVT 2) (SY ["x","y"] $ BVT 1)))
sndTy : Term Three d n
sndTy =
(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)
(SY ["p"] $ E $ BV 2 :@ E (F "fst" :@@ [BVT 3, BVT 2, BVT 0]))
(SY ["x","y"] $ BVT 0)))
defGlobals : Definitions Three
defGlobals = fromList
[("A", mkAbstract Zero $ TYPE 0),
("B", mkAbstract Zero $ TYPE 0),
("C", mkAbstract Zero $ TYPE 1),
("D", mkAbstract Zero $ TYPE 1),
("P", mkAbstract Zero $ Arr Any (FT "A") (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")),
("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 "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)]
parameters (label : String) (act : Lazy (M ()))
{default defGlobals globals : Definitions Three}
testTC : Test
testTC = test label $ runReaderT globals act
testTCFail : Test
testTCFail = testThrows label (const True) $ runReaderT globals act
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 =
catchError
(inj $ equalType ctx exp got)
(\_ : Error' => throwError $ WrongInfer exp got)
qoutEq : (exp, got : QOutput Three n) -> M ()
qoutEq qout res = unless (qout == res) $ throwError $ WrongQOut qout res
inferAs : TyContext Three d n -> (sg : SQty Three) ->
Elim Three d n -> Term Three d n -> M ()
inferAs ctx@(MkTyContext {dctx, _}) sg e ty = do
case !(inj $ infer ctx sg e) of
Just res => inferredTypeEq ctx ty res.type
Nothing => pure ()
inferAsQ : TyContext Three d n -> (sg : SQty Three) ->
Elim Three d n -> Term Three d n -> QOutput Three n -> M ()
inferAsQ ctx@(MkTyContext {dctx, _}) sg e ty qout = do
case !(inj $ infer ctx sg e) of
Just res => do
inferredTypeEq ctx ty res.type
qoutEq qout res.qout
Nothing => pure ()
infer_ : TyContext Three d n -> (sg : SQty Three) -> Elim Three d n -> M ()
infer_ ctx sg e = ignore $ inj $ infer ctx sg e
checkQ : TyContext Three d n -> SQty Three ->
Term Three d n -> Term Three d n -> QOutput Three n -> M ()
checkQ ctx@(MkTyContext {dctx, _}) sg s ty qout = do
case !(inj $ check ctx sg s ty) of
Just res => qoutEq qout res
Nothing => pure ()
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
checkType_ : TyContext Three d n -> Term Three d n -> Maybe Universe -> M ()
checkType_ ctx s u = inj $ checkType ctx s u
-- ω 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" :- [
"universes" :- [
testTC "0 · ★₀ ⇐ ★₁ # by checkType" $
checkType_ (ctx [<]) (TYPE 0) (Just 1),
testTC "0 · ★₀ ⇐ ★₁ # by check" $
check_ (ctx [<]) szero (TYPE 0) (TYPE 1),
testTC "0 · ★₀ ⇐ ★₂" $
checkType_ (ctx [<]) (TYPE 0) (Just 2),
testTC "0 · ★₀ ⇐ ★_" $
checkType_ (ctx [<]) (TYPE 0) Nothing,
testTCFail "0 · ★₁ ⇍ ★₀" $
checkType_ (ctx [<]) (TYPE 1) (Just 0),
testTCFail "0 · ★₀ ⇍ ★₀" $
checkType_ (ctx [<]) (TYPE 0) (Just 0),
testTC "0=1 ⊢ 0 · ★₁ ⇐ ★₀" $
checkType_ (ctx01 [<]) (TYPE 1) (Just 0),
testTCFail "1 · ★₀ ⇍ ★₁ # by check" $
check_ (ctx [<]) sone (TYPE 0) (TYPE 1)
],
"function types" :- [
note "A, B : ★₀; C, D : ★₁; P : A ⇾ ★₀",
testTC "0 · A ⊸ B ⇐ ★₀" $
check_ (ctx [<]) szero (Arr One (FT "A") (FT "B")) (TYPE 0),
note "subtyping",
testTC "0 · A ⊸ B ⇐ ★₁" $
check_ (ctx [<]) szero (Arr One (FT "A") (FT "B")) (TYPE 1),
testTC "0 · C ⊸ D ⇐ ★₁" $
check_ (ctx [<]) szero (Arr One (FT "C") (FT "D")) (TYPE 1),
testTCFail "0 · C ⊸ D ⇍ ★₀" $
check_ (ctx [<]) szero (Arr One (FT "C") (FT "D")) (TYPE 0),
testTC "0 · (1·x : A) → P x ⇐ ★₀" $
check_ (ctx [<]) szero
(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),
testTC "0=1 ⊢ 0 · A ⊸ P ⇐ ★₀" $
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_ "x" (FT "A") $ E $ F "P" :@ BVT 0) (TYPE 0),
testTC "0 · (x : A) × P x ⇐ ★₁" $
check_ (ctx [<]) szero
(Sig_ "x" (FT "A") $ E $ F "P" :@ BVT 0) (TYPE 1),
testTC "0 · (A : ★₀) × A ⇐ ★₁" $
check_ (ctx [<]) szero (Sig_ "A" (TYPE 0) $ BVT 0) (TYPE 1),
testTCFail "0 · (A : ★₀) × A ⇍ ★₀" $
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)
],
"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 ⇒ ★₀" $
inferAs (ctx [<]) szero (F "A") (TYPE 0),
testTC "0 · [A] ⇐ ★₀" $
check_ (ctx [<]) szero (FT "A") (TYPE 0),
note "subtyping",
testTC "0 · [A] ⇐ ★₁" $
check_ (ctx [<]) szero (FT "A") (TYPE 1),
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)",
testTC "1 · refl ⇒ ⋯" $ inferAs (ctx [<]) sone (F "refl") reflTy,
testTC "1 · [refl] ⇐ ⋯" $ check_ (ctx [<]) sone (FT "refl") reflTy
],
"bound vars" :- [
testTC "x : A ⊢ 1 · x ⇒ A ⊳ 1·x" $
inferAsQ {n = 1} (ctx [< FT "A"]) sone
(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 ⊸ B",
testTC "x : A ⊢ 1 · f2 [x] [x] ⇒ B ⊳ ω·x" $
inferAsQ {n = 1} (ctx [< FT "A"]) sone
(F "f2" :@@ [BVT 0, BVT 0]) (FT "B") [< Any]
],
"lambda" :- [
note "linear & unrestricted identity",
testTC "1 · (λ x ⇒ x) ⇐ A ⊸ A" $
check_ (ctx [<]) sone (["x"] :\\ BVT 0) (Arr One (FT "A") (FT "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" $
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" $
check_ (ctx [<]) szero (["x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")),
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)" $
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_ "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) (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) (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) (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) (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) (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) (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) (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 ⇐ ★₂" $
check_ (ctx [<]) szero fstTy (TYPE 2),
testTC "1 · def of fsttype 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 sndtype 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 "A" (Sig_ "A" (TYPE 0) $ BVT 0) $
(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 $ 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
(["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
(["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))
],
"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)",
testTC "cong" $
check_ (ctx [<]) sone
(["x", "y", "xy"] :\\ ["i"] :\\% E (F "p" :@ E (BV 0 :% BV 0)))
(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 "",
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
(["eq"] :\\ ["i"] :\\% ["x"] :\\ E (BV 1 :@ BVT 0 :% BV 0))
(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")))
]
]