quox/tests/Tests/Typechecker.idr

418 lines
16 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", mkPostulate Zero $ TYPE 0),
("B", mkPostulate Zero $ TYPE 0),
("C", mkPostulate Zero $ TYPE 1),
("D", mkPostulate Zero $ TYPE 1),
("P", mkPostulate Zero $ Arr Any (FT "A") (TYPE 0)),
("a", mkPostulate Any $ FT "A"),
("a'", mkPostulate Any $ FT "A"),
("b", mkPostulate Any $ FT "B"),
("f", mkPostulate Any $ Arr One (FT "A") (FT "A")),
("g", mkPostulate Any $ Arr One (FT "A") (FT "B")),
("f2", mkPostulate Any $ Arr One (FT "A") $ Arr One (FT "A") (FT "B")),
("p", mkPostulate Any $ Pi_ One "x" (FT "A") $ E $ F "P" :@ BVT 0),
("q", mkPostulate 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 $> "()"
anys : {n : Nat} -> QContext Three n
anys {n = 0} = [<]
anys {n = S n} = anys :< Any
ctx, ctx01 : {n : Nat} -> Context (\n => (BaseName, Term Three 0 n)) n ->
TyContext Three 0 n
ctx tel = let (ns, ts) = unzip tel in
MkTyContext new [<] ts ns anys
ctx01 tel = let (ns, ts) = unzip tel in
MkTyContext ZeroIsOne [<] ts ns anys
empty01 : TyContext Three 0 0
empty01 = {dctx := ZeroIsOne} empty
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_ empty (TYPE 0) (Just 1),
testTC "0 · ★₀ ⇐ ★₁ # by check" $
check_ empty szero (TYPE 0) (TYPE 1),
testTC "0 · ★₀ ⇐ ★₂" $
checkType_ empty (TYPE 0) (Just 2),
testTC "0 · ★₀ ⇐ ★_" $
checkType_ empty (TYPE 0) Nothing,
testTCFail "0 · ★₁ ⇍ ★₀" $
checkType_ empty (TYPE 1) (Just 0),
testTCFail "0 · ★₀ ⇍ ★₀" $
checkType_ empty (TYPE 0) (Just 0),
testTC "0=1 ⊢ 0 · ★₁ ⇐ ★₀" $
checkType_ empty01 (TYPE 1) (Just 0),
testTCFail "1 · ★₀ ⇍ ★₁ # by check" $
check_ empty sone (TYPE 0) (TYPE 1)
],
"function types" :- [
note "A, B : ★₀; C, D : ★₁; P : A ⇾ ★₀",
testTC "0 · A ⊸ B ⇐ ★₀" $
check_ empty szero (Arr One (FT "A") (FT "B")) (TYPE 0),
note "subtyping",
testTC "0 · A ⊸ B ⇐ ★₁" $
check_ empty szero (Arr One (FT "A") (FT "B")) (TYPE 1),
testTC "0 · C ⊸ D ⇐ ★₁" $
check_ empty szero (Arr One (FT "C") (FT "D")) (TYPE 1),
testTCFail "0 · C ⊸ D ⇍ ★₀" $
check_ empty szero (Arr One (FT "C") (FT "D")) (TYPE 0),
testTC "0 · (1·x : A) → P x ⇐ ★₀" $
check_ empty szero
(Pi_ One "x" (FT "A") $ E $ F "P" :@ BVT 0)
(TYPE 0),
testTCFail "0 · A ⊸ P ⇍ ★₀" $
check_ empty szero (Arr One (FT "A") $ FT "P") (TYPE 0),
testTC "0=1 ⊢ 0 · A ⊸ P ⇐ ★₀" $
check_ empty01 szero (Arr One (FT "A") $ FT "P") (TYPE 0)
],
"pair types" :- [
note #""A × B" for "(_ : A) × B""#,
testTC "0 · A × A ⇐ ★₀" $
check_ empty szero (FT "A" `And` FT "A") (TYPE 0),
testTCFail "0 · A × P ⇍ ★₀" $
check_ empty szero (FT "A" `And` FT "P") (TYPE 0),
testTC "0 · (x : A) × P x ⇐ ★₀" $
check_ empty szero
(Sig_ "x" (FT "A") $ E $ F "P" :@ BVT 0) (TYPE 0),
testTC "0 · (x : A) × P x ⇐ ★₁" $
check_ empty szero
(Sig_ "x" (FT "A") $ E $ F "P" :@ BVT 0) (TYPE 1),
testTC "0 · (A : ★₀) × A ⇐ ★₁" $
check_ empty szero (Sig_ "A" (TYPE 0) $ BVT 0) (TYPE 1),
testTCFail "0 · (A : ★₀) × A ⇍ ★₀" $
check_ empty szero (Sig_ "A" (TYPE 0) $ BVT 0) (TYPE 0),
testTCFail "1 · A × A ⇍ ★₀" $
check_ empty sone (FT "A" `And` FT "A") (TYPE 0)
],
"enum types" :- [
testTC "0 · {} ⇐ ★₀" $ check_ empty szero (enum []) (TYPE 0),
testTC "0 · {} ⇐ ★₃" $ check_ empty szero (enum []) (TYPE 3),
testTC "0 · {a,b,c} ⇐ ★₀" $
check_ empty szero (enum ["a", "b", "c"]) (TYPE 0),
testTC "0 · {a,b,c} ⇐ ★₃" $
check_ empty szero (enum ["a", "b", "c"]) (TYPE 3),
testTCFail "1 · {} ⇍ ★₀" $ check_ empty sone (enum []) (TYPE 0),
testTC "0=1 ⊢ 1 · {} ⇐ ★₀" $ check_ empty01 sone (enum []) (TYPE 0)
],
"free vars" :- [
note "A : ★₀",
testTC "0 · A ⇒ ★₀" $
inferAs empty szero (F "A") (TYPE 0),
testTC "0 · [A] ⇐ ★₀" $
check_ empty szero (FT "A") (TYPE 0),
note "subtyping",
testTC "0 · [A] ⇐ ★₁" $
check_ empty szero (FT "A") (TYPE 1),
note "(fail) runtime-relevant type",
testTCFail "1 · A ⇏ ★₀" $
infer_ empty sone (F "A"),
note "refl : (0·A : ★₀) → (1·x : A) → (x ≡ x : A) ≔ (λ A x ⇒ δ _ ⇒ x)",
testTC "1 · refl ⇒ ⋯" $ inferAs empty sone (F "refl") reflTy,
testTC "1 · [refl] ⇐ ⋯" $ check_ empty sone (FT "refl") reflTy
],
"bound vars" :- [
testTC "x : A ⊢ 1 · x ⇒ A ⊳ 1·x" $
inferAsQ {n = 1} (ctx [< ("x", FT "A")]) sone
(BV 0) (FT "A") [< one],
testTC "x : A ⊢ 1 · [x] ⇐ A ⊳ 1·x" $
checkQ {n = 1} (ctx [< ("x", 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 [< ("x", FT "A")]) sone
(F "f2" :@@ [BVT 0, BVT 0]) (FT "B") [< Any]
],
"lambda" :- [
note "linear & unrestricted identity",
testTC "1 · (λ x ⇒ x) ⇐ A ⊸ A" $
check_ empty sone ([< "x"] :\\ BVT 0) (Arr One (FT "A") (FT "A")),
testTC "1 · (λ x ⇒ x) ⇐ A → A" $
check_ empty sone ([< "x"] :\\ BVT 0) (Arr Any (FT "A") (FT "A")),
note "(fail) zero binding used relevantly",
testTCFail "1 · (λ x ⇒ x) ⇍ A ⇾ A" $
check_ empty sone ([< "x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")),
note "(but ok in overall erased context)",
testTC "0 · (λ x ⇒ x) ⇐ A ⇾ A" $
check_ empty szero ([< "x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")),
testTC "1 · (λ A x ⇒ refl A x) ⇐ ⋯ # (type of refl)" $
check_ empty sone
([< "A", "x"] :\\ E (F "refl" :@@ [BVT 1, BVT 0]))
reflTy,
testTC "1 · (λ A x ⇒ δ i ⇒ x) ⇐ ⋯ # (def. and type of refl)" $
check_ empty sone reflDef reflTy
],
"pairs" :- [
testTC "1 · (a, a) ⇐ A × A" $
check_ empty sone (Pair (FT "a") (FT "a")) (FT "A" `And` FT "A"),
testTC "x : A ⊢ 1 · (x, x) ⇐ A × A ⊳ ω·x" $
checkQ (ctx [< ("x", FT "A")]) sone
(Pair (BVT 0) (BVT 0)) (FT "A" `And` FT "A") [< Any],
testTC "1 · (a, δ i ⇒ a) ⇐ (x : A) × (x ≡ a)" $
check_ empty 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 [< ("x", 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 [< ("x", 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 [< ("x", 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 [< ("x", 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 [< ("x", 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 [< ("x", 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 [< ("x", 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_ empty szero fstTy (TYPE 2),
testTC "1 · def of fsttype of fst" $
check_ empty 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_ empty szero sndTy (TYPE 2),
testTC "1 · def of sndtype of snd" $
check_ empty sone sndDef sndTy,
testTC "0 · snd ★₀ (λ x ⇒ x) ⇒ (ω·p : (A : ★₀) × A) → fst ★₀ (λ x ⇒ x) p" $
inferAs empty 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_ empty sone (Tag "a") (enum ["a"]),
testTC "1 · 'a ⇐ {a, b, c}" $
check_ empty sone (Tag "a") (enum ["a", "b", "c"]),
testTCFail "1 · 'a ⇍ {b, c}" $
check_ empty sone (Tag "a") (enum ["b", "c"]),
testTC "0=1 ⊢ 1 · 'a ⇐ {b, c}" $
check_ empty01 sone (Tag "a") (enum ["b", "c"])
],
"equalities" :- [
testTC "1 · (δ i ⇒ a) ⇐ a ≡ a" $
check_ empty 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_ empty 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_ empty 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_ empty 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_ empty 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"))),
todo "absurd (when coerce is in)"
-- absurd : (`true ≡ `false : {true, false}) ⇾ (0·A : ★₀) → A ≔
-- λ e ⇒
-- case coerce [i ⇒ case e @i return ★₀ of {`true ⇒ {tt}; `false ⇒ {}}]
-- @0 @1 `tt
-- return A
-- of { }
]
]