quox/tests/Tests/Typechecker.idr

587 lines
23 KiB
Idris
Raw Normal View History

2023-02-11 12:15:50 -05:00
module Tests.Typechecker
import Quox.Syntax
import Quox.Typechecker as Lib
import Control.Monad.ST
2023-02-11 12:15:50 -05:00
import public TypingImpls
import TAP
2023-03-31 17:43:25 -04:00
import Quox.EffExtra
2023-05-01 21:06:25 -04:00
import AstExtra
2023-05-14 13:58:46 -04:00
import PrettyExtra
2023-05-01 21:06:25 -04:00
%hide Prelude.App
%hide Pretty.App
2023-02-11 12:15:50 -05:00
2023-02-13 16:06:53 -05:00
data Error'
2023-04-01 13:16:43 -04:00
= TCError Typing.Error
2023-05-14 13:58:46 -04:00
| WrongInfer (BContext d) (BContext n) (Term d n) (Term d n)
2023-04-01 13:16:43 -04:00
| WrongQOut (QOutput n) (QOutput n)
2023-02-13 16:06:53 -05:00
export
ToInfo Error' where
toInfo (TCError e) = toInfo e
2023-05-14 13:58:46 -04:00
toInfo (WrongInfer dnames tnames good bad) =
2023-02-13 16:06:53 -05:00
[("type", "WrongInfer"),
2023-05-14 13:58:46 -04:00
("wanted", prettyStr $ prettyTerm dnames tnames good),
("got", prettyStr $ prettyTerm dnames tnames bad)]
2023-02-13 16:06:53 -05:00
toInfo (WrongQOut good bad) =
[("type", "WrongQOut"),
2023-05-14 13:58:46 -04:00
("wanted", show good),
("wanted", show bad)]
2023-02-13 16:06:53 -05:00
2023-08-24 13:55:57 -04:00
0 Test : List (Type -> Type)
Test = [Except Error', DefsReader]
2023-02-11 12:15:50 -05:00
2023-08-24 13:55:57 -04:00
inj : Eff TC a -> Eff Test a
2023-06-23 12:32:05 -04:00
inj act = rethrow $ mapFst TCError $ runTC !(askAt DEFS) act
2023-02-11 12:15:50 -05:00
2023-04-01 13:16:43 -04:00
reflTy : Term d n
2023-02-11 12:15:50 -05:00
reflTy =
2023-05-01 21:06:25 -04:00
^PiY Zero "A" (^TYPE 0)
(^PiY One "x" (^BVT 0)
(^Eq0 (^BVT 1) (^BVT 0) (^BVT 0)))
2023-02-11 12:15:50 -05:00
2023-04-01 13:16:43 -04:00
reflDef : Term d n
2023-05-01 21:06:25 -04:00
reflDef = ^LamY "A" (^LamY "x" (^DLamY "i" (^BVT 0)))
2023-02-11 12:15:50 -05:00
2023-02-23 04:04:16 -05:00
2023-04-01 13:16:43 -04:00
fstTy : Term d n
2023-02-23 04:04:16 -05:00
fstTy =
2023-05-21 14:09:34 -04:00
^PiY Zero "A" (^TYPE 0)
(^PiY Zero "B" (^Arr Any (^BVT 0) (^TYPE 0))
2023-05-01 21:06:25 -04:00
(^Arr Any (^SigY "x" (^BVT 1) (E $ ^App (^BV 1) (^BVT 0))) (^BVT 1)))
2023-02-23 04:04:16 -05:00
2023-04-01 13:16:43 -04:00
fstDef : Term d n
2023-02-23 04:04:16 -05:00
fstDef =
2023-05-01 21:06:25 -04:00
^LamY "A" (^LamY "B" (^LamY "p"
(E $ ^CasePair Any (^BV 0) (SN $ ^BVT 2)
(SY [< "x", "y"] $ ^BVT 1))))
2023-02-23 04:04:16 -05:00
2023-04-01 13:16:43 -04:00
sndTy : Term d n
2023-02-23 04:04:16 -05:00
sndTy =
2023-05-21 14:09:34 -04:00
^PiY Zero "A" (^TYPE 0)
(^PiY Zero "B" (^Arr Any (^BVT 0) (^TYPE 0))
2023-05-01 21:06:25 -04:00
(^PiY Any "p" (^SigY "x" (^BVT 1) (E $ ^App (^BV 1) (^BVT 0)))
(E $ ^App (^BV 1)
2023-05-21 14:09:34 -04:00
(E $ ^App (^App (^App (^F "fst" 0) (^BVT 2)) (^BVT 1)) (^BVT 0)))))
2023-02-23 04:04:16 -05:00
2023-04-01 13:16:43 -04:00
sndDef : Term d n
2023-02-23 04:04:16 -05:00
sndDef =
2023-05-01 21:06:25 -04:00
-- λ A B p ⇒ caseω p return p' ⇒ B (fst A B p') of { (x, y) ⇒ y }
^LamY "A" (^LamY "B" (^LamY "p"
(E $ ^CasePair Any (^BV 0)
(SY [< "p"] $ E $
^App (^BV 2)
2023-05-21 14:09:34 -04:00
(E $ ^App (^App (^App (^F "fst" 0) (^BVT 3)) (^BVT 2)) (^BVT 0)))
2023-05-01 21:06:25 -04:00
(SY [< "x", "y"] $ ^BVT 0))))
nat : Term d n
2023-11-02 13:14:22 -04:00
nat = ^NAT
2023-02-23 04:04:16 -05:00
2023-05-21 14:09:34 -04:00
apps : Elim d n -> List (Term d n) -> Elim d n
apps = foldl (\f, s => ^App f s)
2023-02-23 04:04:16 -05:00
2023-04-01 13:16:43 -04:00
defGlobals : Definitions
2023-02-11 12:15:50 -05:00
defGlobals = fromList
[("A", mkPostulate GZero (^TYPE 0)),
("B", mkPostulate GZero (^TYPE 0)),
("C", mkPostulate GZero (^TYPE 1)),
("D", mkPostulate GZero (^TYPE 1)),
("P", mkPostulate GZero (^Arr Any (^FT "A" 0) (^TYPE 0))),
("a", mkPostulate GAny (^FT "A" 0)),
("a'", mkPostulate GAny (^FT "A" 0)),
("b", mkPostulate GAny (^FT "B" 0)),
("c", mkPostulate GAny (^FT "C" 0)),
("d", mkPostulate GAny (^FT "D" 0)),
("f", mkPostulate GAny (^Arr One (^FT "A" 0) (^FT "A" 0))),
("", mkPostulate GAny (^Arr Any (^FT "A" 0) (^FT "A" 0))),
("g", mkPostulate GAny (^Arr One (^FT "A" 0) (^FT "B" 0))),
("f2", mkPostulate GAny
2023-05-21 14:09:34 -04:00
(^Arr One (^FT "A" 0) (^Arr One (^FT "A" 0) (^FT "B" 0)))),
("p", mkPostulate GAny
2023-05-21 14:09:34 -04:00
(^PiY One "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))),
("q", mkPostulate GAny
2023-05-21 14:09:34 -04:00
(^PiY One "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))),
("refl", mkDef GAny reflTy reflDef),
("fst", mkDef GAny fstTy fstDef),
("snd", mkDef GAny sndTy sndDef)]
2023-02-11 12:15:50 -05:00
2023-08-24 13:55:57 -04:00
parameters (label : String) (act : Lazy (Eff Test ()))
2023-04-01 13:16:43 -04:00
{default defGlobals globals : Definitions}
2023-02-11 12:15:50 -05:00
testTC : Test
2023-03-31 17:43:25 -04:00
testTC = test label {e = Error', a = ()} $
2023-04-17 17:58:24 -04:00
extract $ runExcept $ runReaderAt DEFS globals act
2023-02-11 12:15:50 -05:00
testTCFail : Test
2023-03-31 17:43:25 -04:00
testTCFail = testThrows label (const True) $
2023-04-17 17:58:24 -04:00
(extract $ runExcept $ runReaderAt DEFS globals act) $> "()"
2023-02-11 12:15:50 -05:00
2023-08-24 13:55:57 -04:00
inferredTypeEq : TyContext d n -> (exp, got : Term d n) -> Eff Test ()
2023-02-13 16:06:53 -05:00
inferredTypeEq ctx exp got =
2023-05-14 13:58:46 -04:00
wrapErr (const $ WrongInfer ctx.dnames ctx.tnames exp got) $ inj $ lift $
2023-05-01 21:06:25 -04:00
equalType noLoc ctx exp got
2023-02-13 16:06:53 -05:00
2023-08-24 13:55:57 -04:00
qoutEq : (exp, got : QOutput n) -> Eff Test ()
2023-03-31 17:43:25 -04:00
qoutEq qout res = unless (qout == res) $ throw $ WrongQOut qout res
2023-02-13 16:06:53 -05:00
2023-08-24 13:55:57 -04:00
inferAs : TyContext d n -> (sg : SQty) -> Elim d n -> Term d n -> Eff Test ()
2023-02-19 11:51:44 -05:00
inferAs ctx@(MkTyContext {dctx, _}) sg e ty = do
case !(inj $ infer ctx sg e) of
Just res => inferredTypeEq ctx ty res.type
Nothing => pure ()
2023-02-13 16:06:53 -05:00
2023-04-01 13:16:43 -04:00
inferAsQ : TyContext d n -> (sg : SQty) ->
2023-08-24 13:55:57 -04:00
Elim d n -> Term d n -> QOutput n -> Eff Test ()
2023-02-19 11:51:44 -05:00
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 ()
2023-02-11 12:15:50 -05:00
2023-08-24 13:55:57 -04:00
infer_ : TyContext d n -> (sg : SQty) -> Elim d n -> Eff Test ()
2023-02-13 16:06:53 -05:00
infer_ ctx sg e = ignore $ inj $ infer ctx sg e
2023-04-01 13:16:43 -04:00
checkQ : TyContext d n -> SQty ->
2023-08-24 13:55:57 -04:00
Term d n -> Term d n -> QOutput n -> Eff Test ()
2023-02-19 11:51:44 -05:00
checkQ ctx@(MkTyContext {dctx, _}) sg s ty qout = do
case !(inj $ check ctx sg s ty) of
Just res => qoutEq qout res
Nothing => pure ()
2023-02-11 12:15:50 -05:00
2023-08-24 13:55:57 -04:00
check_ : TyContext d n -> SQty -> Term d n -> Term d n -> Eff Test ()
2023-02-13 16:06:53 -05:00
check_ ctx sg s ty = ignore $ inj $ check ctx sg s ty
2023-02-11 12:15:50 -05:00
2023-08-24 13:55:57 -04:00
checkType_ : TyContext d n -> Term d n -> Maybe Universe -> Eff Test ()
checkType_ ctx s u = inj $ checkType ctx s u
2023-02-23 04:04:16 -05:00
2023-02-11 12:15:50 -05:00
export
tests : Test
tests = "typechecker" :- [
"universes" :- [
testTC "0 · ★₀ ⇐ ★₁ # by checkType" $
2023-05-01 21:06:25 -04:00
checkType_ empty (^TYPE 0) (Just 1),
testTC "0 · ★₀ ⇐ ★₁ # by check" $
check_ empty SZero (^TYPE 0) (^TYPE 1),
testTC "0 · ★₀ ⇐ ★₂" $
2023-05-01 21:06:25 -04:00
checkType_ empty (^TYPE 0) (Just 2),
testTC "0 · ★₀ ⇐ ★_" $
2023-05-01 21:06:25 -04:00
checkType_ empty (^TYPE 0) Nothing,
testTCFail "0 · ★₁ ⇍ ★₀" $
2023-05-01 21:06:25 -04:00
checkType_ empty (^TYPE 1) (Just 0),
testTCFail "0 · ★₀ ⇍ ★₀" $
2023-05-01 21:06:25 -04:00
checkType_ empty (^TYPE 0) (Just 0),
testTC "0=1 ⊢ 0 · ★₁ ⇐ ★₀" $
2023-05-01 21:06:25 -04:00
checkType_ empty01 (^TYPE 1) (Just 0),
testTCFail "1 · ★₀ ⇍ ★₁ # by check" $
check_ empty SOne (^TYPE 0) (^TYPE 1)
2023-02-11 12:15:50 -05:00
],
"function types" :- [
2023-05-01 21:06:25 -04:00
note "A, B : ★₀; C, D : ★₁; P : 0.A → ★₀",
testTC "0 · 1.A → B ⇐ ★₀" $
check_ empty SZero (^Arr One (^FT "A" 0) (^FT "B" 0)) (^TYPE 0),
2023-02-12 15:30:08 -05:00
note "subtyping",
2023-05-01 21:06:25 -04:00
testTC "0 · 1.A → B ⇐ ★₁" $
check_ empty SZero (^Arr One (^FT "A" 0) (^FT "B" 0)) (^TYPE 1),
2023-05-01 21:06:25 -04:00
testTC "0 · 1.C → D ⇐ ★₁" $
check_ empty SZero (^Arr One (^FT "C" 0) (^FT "D" 0)) (^TYPE 1),
2023-05-01 21:06:25 -04:00
testTCFail "0 · 1.C → D ⇍ ★₀" $
check_ empty SZero (^Arr One (^FT "C" 0) (^FT "D" 0)) (^TYPE 0),
2023-05-01 21:06:25 -04:00
testTC "0 · 1.(x : A) → P x ⇐ ★₀" $
check_ empty SZero
2023-05-21 14:09:34 -04:00
(^PiY One "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))
2023-05-01 21:06:25 -04:00
(^TYPE 0),
testTCFail "0 · 1.A → P ⇍ ★₀" $
check_ empty SZero (^Arr One (^FT "A" 0) (^FT "P" 0)) (^TYPE 0),
2023-05-01 21:06:25 -04:00
testTC "0=1 ⊢ 0 · 1.A → P ⇐ ★₀" $
check_ empty01 SZero (^Arr One (^FT "A" 0) (^FT "P" 0)) (^TYPE 0)
2023-02-13 16:06:53 -05:00
],
"pair types" :- [
testTC "0 · A × A ⇐ ★₀" $
check_ empty SZero (^And (^FT "A" 0) (^FT "A" 0)) (^TYPE 0),
2023-02-23 04:04:16 -05:00
testTCFail "0 · A × P ⇍ ★₀" $
check_ empty SZero (^And (^FT "A" 0) (^FT "P" 0)) (^TYPE 0),
2023-02-23 04:04:16 -05:00
testTC "0 · (x : A) × P x ⇐ ★₀" $
check_ empty SZero
2023-05-21 14:09:34 -04:00
(^SigY "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))
2023-05-01 21:06:25 -04:00
(^TYPE 0),
2023-02-23 04:04:16 -05:00
testTC "0 · (x : A) × P x ⇐ ★₁" $
check_ empty SZero
2023-05-21 14:09:34 -04:00
(^SigY "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))
2023-05-01 21:06:25 -04:00
(^TYPE 1),
2023-02-23 04:04:16 -05:00
testTC "0 · (A : ★₀) × A ⇐ ★₁" $
check_ empty SZero
2023-05-01 21:06:25 -04:00
(^SigY "A" (^TYPE 0) (^BVT 0))
(^TYPE 1),
2023-02-23 04:04:16 -05:00
testTCFail "0 · (A : ★₀) × A ⇍ ★₀" $
check_ empty SZero
2023-05-01 21:06:25 -04:00
(^SigY "A" (^TYPE 0) (^BVT 0))
(^TYPE 0),
2023-02-13 16:06:53 -05:00
testTCFail "1 · A × A ⇍ ★₀" $
check_ empty SOne
2023-05-21 14:09:34 -04:00
(^And (^FT "A" 0) (^FT "A" 0))
2023-05-01 21:06:25 -04:00
(^TYPE 0)
2023-02-11 12:15:50 -05:00
],
2023-02-23 04:04:16 -05:00
"enum types" :- [
testTC "0 · {} ⇐ ★₀" $ check_ empty SZero (^enum []) (^TYPE 0),
testTC "0 · {} ⇐ ★₃" $ check_ empty SZero (^enum []) (^TYPE 3),
2023-03-04 15:02:51 -05:00
testTC "0 · {a,b,c} ⇐ ★₀" $
check_ empty SZero (^enum ["a", "b", "c"]) (^TYPE 0),
2023-03-04 15:02:51 -05:00
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)
2023-02-23 04:04:16 -05:00
],
2023-02-11 12:15:50 -05:00
"free vars" :- [
2023-02-12 15:30:08 -05:00
note "A : ★₀",
2023-02-11 12:15:50 -05:00
testTC "0 · A ⇒ ★₀" $
inferAs empty SZero (^F "A" 0) (^TYPE 0),
2023-02-13 16:06:53 -05:00
testTC "0 · [A] ⇐ ★₀" $
check_ empty SZero (^FT "A" 0) (^TYPE 0),
2023-02-12 15:30:08 -05:00
note "subtyping",
2023-02-13 16:06:53 -05:00
testTC "0 · [A] ⇐ ★₁" $
check_ empty SZero (^FT "A" 0) (^TYPE 1),
2023-02-12 15:30:08 -05:00
note "(fail) runtime-relevant type",
testTCFail "1 · A ⇏ ★₀" $
infer_ empty SOne (^F "A" 0),
testTC "1 . f ⇒ 1.A → A" $
inferAs empty SOne (^F "f" 0) (^Arr One (^FT "A" 0) (^FT "A" 0)),
testTC "1 . f ⇐ 1.A → A" $
check_ empty SOne (^FT "f" 0) (^Arr One (^FT "A" 0) (^FT "A" 0)),
testTCFail "1 . f ⇍ 0.A → A" $
check_ empty SOne (^FT "f" 0) (^Arr Zero (^FT "A" 0) (^FT "A" 0)),
testTCFail "1 . f ⇍ ω.A → A" $
check_ empty SOne (^FT "f" 0) (^Arr Any (^FT "A" 0) (^FT "A" 0)),
testTC "1 . (λ x ⇒ f x) ⇐ 1.A → A" $
check_ empty SOne
2023-05-21 14:09:34 -04:00
(^LamY "x" (E $ ^App (^F "f" 0) (^BVT 0)))
(^Arr One (^FT "A" 0) (^FT "A" 0)),
testTC "1 . (λ x ⇒ f x) ⇐ ω.A → A" $
check_ empty SOne
2023-05-21 14:09:34 -04:00
(^LamY "x" (E $ ^App (^F "f" 0) (^BVT 0)))
(^Arr Any (^FT "A" 0) (^FT "A" 0)),
testTCFail "1 . (λ x ⇒ f x) ⇍ 0.A → A" $
check_ empty SOne
2023-05-21 14:09:34 -04:00
(^LamY "x" (E $ ^App (^F "f" 0) (^BVT 0)))
(^Arr Zero (^FT "A" 0) (^FT "A" 0)),
testTC "1 . fω ⇒ ω.A → A" $
inferAs empty SOne (^F "" 0) (^Arr Any (^FT "A" 0) (^FT "A" 0)),
testTC "1 . (λ x ⇒ fω x) ⇐ ω.A → A" $
check_ empty SOne
2023-05-21 14:09:34 -04:00
(^LamY "x" (E $ ^App (^F "" 0) (^BVT 0)))
(^Arr Any (^FT "A" 0) (^FT "A" 0)),
testTCFail "1 . (λ x ⇒ fω x) ⇍ 0.A → A" $
check_ empty SOne
2023-05-21 14:09:34 -04:00
(^LamY "x" (E $ ^App (^F "" 0) (^BVT 0)))
(^Arr Zero (^FT "A" 0) (^FT "A" 0)),
testTCFail "1 . (λ x ⇒ fω x) ⇍ 1.A → A" $
check_ empty SOne
2023-05-21 14:09:34 -04:00
(^LamY "x" (E $ ^App (^F "" 0) (^BVT 0)))
(^Arr One (^FT "A" 0) (^FT "A" 0)),
2023-03-04 15:02:51 -05:00
note "refl : (0·A : ★₀) → (1·x : A) → (x ≡ x : A) ≔ (λ A x ⇒ δ _ ⇒ x)",
testTC "1 · refl ⇒ ⋯" $ inferAs empty SOne (^F "refl" 0) reflTy,
testTC "1 · [refl] ⇐ ⋯" $ check_ empty SOne (^FT "refl" 0) reflTy
2023-02-13 16:06:53 -05:00
],
"bound vars" :- [
2023-02-14 15:14:47 -05:00
testTC "x : A ⊢ 1 · x ⇒ A ⊳ 1·x" $
inferAsQ (ctx [< ("x", ^FT "A" 0)]) SOne
2023-05-21 14:09:34 -04:00
(^BV 0) (^FT "A" 0) [< One],
2023-05-01 21:06:25 -04:00
testTC "x : A ⊢ 1 · x ⇐ A ⊳ 1·x" $
checkQ (ctx [< ("x", ^FT "A" 0)]) SOne (^BVT 0) (^FT "A" 0) [< One],
2023-05-01 21:06:25 -04:00
note "f2 : 1.A → 1.A → B",
testTC "x : A ⊢ 1 · f2 x x ⇒ B ⊳ ω·x" $
inferAsQ (ctx [< ("x", ^FT "A" 0)]) SOne
2023-05-21 14:09:34 -04:00
(^App (^App (^F "f2" 0) (^BVT 0)) (^BVT 0)) (^FT "B" 0) [< Any]
2023-02-11 12:15:50 -05:00
],
"lambda" :- [
2023-02-12 15:30:08 -05:00
note "linear & unrestricted identity",
2023-03-04 15:02:51 -05:00
testTC "1 · (λ x ⇒ x) ⇐ A → A" $
check_ empty SOne
2023-05-01 21:06:25 -04:00
(^LamY "x" (^BVT 0))
2023-05-21 14:09:34 -04:00
(^Arr One (^FT "A" 0) (^FT "A" 0)),
2023-05-01 21:06:25 -04:00
testTC "1 · (λ x ⇒ x) ⇐ ω.A → A" $
check_ empty SOne
2023-05-01 21:06:25 -04:00
(^LamY "x" (^BVT 0))
2023-05-21 14:09:34 -04:00
(^Arr Any (^FT "A" 0) (^FT "A" 0)),
2023-02-12 15:30:08 -05:00
note "(fail) zero binding used relevantly",
2023-05-01 21:06:25 -04:00
testTCFail "1 · (λ x ⇒ x) ⇍ 0.A → A" $
check_ empty SOne
2023-05-01 21:06:25 -04:00
(^LamY "x" (^BVT 0))
2023-05-21 14:09:34 -04:00
(^Arr Zero (^FT "A" 0) (^FT "A" 0)),
2023-02-12 15:30:08 -05:00
note "(but ok in overall erased context)",
2023-03-04 15:02:51 -05:00
testTC "0 · (λ x ⇒ x) ⇐ A ⇾ A" $
check_ empty SZero
2023-05-01 21:06:25 -04:00
(^LamY "x" (^BVT 0))
2023-05-21 14:09:34 -04:00
(^Arr Zero (^FT "A" 0) (^FT "A" 0)),
2023-03-04 15:02:51 -05:00
testTC "1 · (λ A x ⇒ refl A x) ⇐ ⋯ # (type of refl)" $
check_ empty SOne
2023-05-21 14:09:34 -04:00
(^LamY "A" (^LamY "x"
(E $ ^App (^App (^F "refl" 0) (^BVT 1)) (^BVT 0))))
2023-02-12 15:30:08 -05:00
reflTy,
2023-03-04 15:02:51 -05:00
testTC "1 · (λ A x ⇒ δ i ⇒ x) ⇐ ⋯ # (def. and type of refl)" $
check_ empty SOne reflDef reflTy
2023-02-11 12:15:50 -05:00
],
2023-02-23 04:04:16 -05:00
"pairs" :- [
testTC "1 · (a, a) ⇐ A × A" $
check_ empty SOne
2023-05-21 14:09:34 -04:00
(^Pair (^FT "a" 0) (^FT "a" 0)) (^And (^FT "A" 0) (^FT "A" 0)),
2023-02-23 04:04:16 -05:00
testTC "x : A ⊢ 1 · (x, x) ⇐ A × A ⊳ ω·x" $
checkQ (ctx [< ("x", ^FT "A" 0)]) SOne
2023-05-21 14:09:34 -04:00
(^Pair (^BVT 0) (^BVT 0)) (^And (^FT "A" 0) (^FT "A" 0)) [< Any],
2023-03-04 15:02:51 -05:00
testTC "1 · (a, δ i ⇒ a) ⇐ (x : A) × (x ≡ a)" $
check_ empty SOne
2023-05-21 14:09:34 -04:00
(^Pair (^FT "a" 0) (^DLamN (^FT "a" 0)))
(^SigY "x" (^FT "A" 0) (^Eq0 (^FT "A" 0) (^BVT 0) (^FT "a" 0)))
2023-02-23 04:04:16 -05:00
],
"unpairing" :- [
2023-03-04 15:02:51 -05:00
testTC "x : A × A ⊢ 1 · (case1 x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 1·x" $
inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "A" 0))]) SOne
2023-05-21 14:09:34 -04:00
(^CasePair One (^BV 0) (SN $ ^FT "B" 0)
(SY [< "l", "r"] $ E $ ^App (^App (^F "f2" 0) (^BVT 1)) (^BVT 0)))
(^FT "B" 0) [< One],
2023-03-04 15:02:51 -05:00
testTC "x : A × A ⊢ 1 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ ω·x" $
inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "A" 0))]) SOne
2023-05-21 14:09:34 -04:00
(^CasePair Any (^BV 0) (SN $ ^FT "B" 0)
(SY [< "l", "r"] $ E $ ^App (^App (^F "f2" 0) (^BVT 1)) (^BVT 0)))
(^FT "B" 0) [< Any],
2023-03-04 15:02:51 -05:00
testTC "x : A × A ⊢ 0 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 0·x" $
inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "A" 0))]) SZero
2023-05-21 14:09:34 -04:00
(^CasePair Any (^BV 0) (SN $ ^FT "B" 0)
(SY [< "l", "r"] $ E $ ^App (^App (^F "f2" 0) (^BVT 1)) (^BVT 0)))
(^FT "B" 0) [< Zero],
2023-03-04 15:02:51 -05:00
testTCFail "x : A × A ⊢ 1 · (case0 x return B of (l,r) ⇒ f2 l r) ⇏" $
infer_ (ctx [< ("x", ^And (^FT "A" 0) (^FT "A" 0))]) SOne
2023-05-21 14:09:34 -04:00
(^CasePair Zero (^BV 0) (SN $ ^FT "B" 0)
(SY [< "l", "r"] $ E $ ^App (^App (^F "f2" 0) (^BVT 1)) (^BVT 0))),
2023-03-04 15:02:51 -05:00
testTC "x : A × B ⊢ 1 · (caseω x return A of (l,r) ⇒ l) ⇒ A ⊳ ω·x" $
inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "B" 0))]) SOne
2023-05-21 14:09:34 -04:00
(^CasePair Any (^BV 0) (SN $ ^FT "A" 0)
2023-05-01 21:06:25 -04:00
(SY [< "l", "r"] $ ^BVT 1))
2023-05-21 14:09:34 -04:00
(^FT "A" 0) [< Any],
2023-03-04 15:02:51 -05:00
testTC "x : A × B ⊢ 0 · (case1 x return A of (l,r) ⇒ l) ⇒ A ⊳ 0·x" $
inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "B" 0))]) SZero
2023-05-21 14:09:34 -04:00
(^CasePair One (^BV 0) (SN $ ^FT "A" 0)
2023-05-01 21:06:25 -04:00
(SY [< "l", "r"] $ ^BVT 1))
2023-05-21 14:09:34 -04:00
(^FT "A" 0) [< Zero],
2023-03-04 15:02:51 -05:00
testTCFail "x : A × B ⊢ 1 · (case1 x return A of (l,r) ⇒ l) ⇏" $
infer_ (ctx [< ("x", ^And (^FT "A" 0) (^FT "B" 0))]) SOne
2023-05-21 14:09:34 -04:00
(^CasePair One (^BV 0) (SN $ ^FT "A" 0)
2023-05-01 21:06:25 -04:00
(SY [< "l", "r"] $ ^BVT 1)),
2023-05-21 14:09:34 -04:00
note "fst : 0.(A : ★₀) → 0.(B : ω.A → ★₀) → ω.((x : A) × B x) → A",
2023-03-04 15:02:51 -05:00
note " ≔ (λ A B p ⇒ caseω p return A of (x, y) ⇒ x)",
2023-05-21 14:09:34 -04:00
testTC "0 · type of fst ⇐ ★₁" $
check_ empty SZero fstTy (^TYPE 1),
2023-02-23 04:04:16 -05:00
testTC "1 · def of fsttype of fst" $
check_ empty SOne fstDef fstTy,
2023-05-21 14:09:34 -04:00
note "snd : 0.(A : ★₀) → 0.(B : A ↠ ★₀) → ω.(p : (x : A) × B x) → B (fst A B p)",
2023-03-04 15:02:51 -05:00
note " ≔ (λ A B p ⇒ caseω p return p ⇒ B (fst A B p) of (x, y) ⇒ y)",
2023-05-21 14:09:34 -04:00
testTC "0 · type of snd ⇐ ★₁" $
check_ empty SZero sndTy (^TYPE 1),
2023-02-23 04:04:16 -05:00
testTC "1 · def of sndtype of snd" $
check_ empty SOne sndDef sndTy,
2023-05-21 14:09:34 -04:00
testTC "0 · snd A P ⇒ ω.(p : (x : A) × P x) → P (fst A P p)" $
inferAs empty SZero
2023-05-21 14:09:34 -04:00
(^App (^App (^F "snd" 0) (^FT "A" 0)) (^FT "P" 0))
(^PiY Any "p" (^SigY "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))
(E $ ^App (^F "P" 0)
(E $ apps (^F "fst" 0) [^FT "A" 0, ^FT "P" 0, ^BVT 0]))),
testTC "1 · fst A (λ _ ⇒ B) (a, b) ⇒ A" $
inferAs empty SOne
2023-05-21 14:09:34 -04:00
(apps (^F "fst" 0)
[^FT "A" 0, ^LamN (^FT "B" 0), ^Pair (^FT "a" 0) (^FT "b" 0)])
(^FT "A" 0),
testTC "1 · fst¹ A (λ _ ⇒ B) (a, b) ⇒ A" $
inferAs empty SOne
2023-05-21 14:09:34 -04:00
(apps (^F "fst" 1)
[^FT "A" 0, ^LamN (^FT "B" 0), ^Pair (^FT "a" 0) (^FT "b" 0)])
(^FT "A" 0),
testTCFail "1 · fst ★⁰ (λ _ ⇒ ★⁰) (A, B) ⇏" $
infer_ empty SOne
2023-05-21 14:09:34 -04:00
(apps (^F "fst" 0)
[^TYPE 0, ^LamN (^TYPE 0), ^Pair (^FT "A" 0) (^FT "B" 0)]),
testTC "0 · fst¹ ★⁰ (λ _ ⇒ ★⁰) (A, B) ⇒ ★⁰" $
inferAs empty SZero
2023-05-21 14:09:34 -04:00
(apps (^F "fst" 1)
[^TYPE 0, ^LamN (^TYPE 0), ^Pair (^FT "A" 0) (^FT "B" 0)])
(^TYPE 0)
2023-02-23 04:04:16 -05:00
],
"enums" :- [
2023-03-05 07:17:46 -05:00
testTC "1 · 'a ⇐ {a}" $
check_ empty SOne (^Tag "a") (^enum ["a"]),
2023-03-05 07:17:46 -05:00
testTC "1 · 'a ⇐ {a, b, c}" $
check_ empty SOne (^Tag "a") (^enum ["a", "b", "c"]),
2023-03-05 07:17:46 -05:00
testTCFail "1 · 'a ⇍ {b, c}" $
check_ empty SOne (^Tag "a") (^enum ["b", "c"]),
2023-03-05 07:17:46 -05:00
testTC "0=1 ⊢ 1 · 'a ⇐ {b, c}" $
check_ empty01 SOne (^Tag "a") (^enum ["b", "c"])
2023-02-23 04:04:16 -05:00
],
2023-03-26 08:40:54 -04:00
"enum matching" :- [
testTC "ω.x : {tt} ⊢ 1 · case1 x return {tt} of { 'tt ⇒ 'tt } ⇒ {tt}" $
inferAs (ctx [< ("x", ^enum ["tt"])]) SOne
2023-05-01 21:06:25 -04:00
(^CaseEnum One (^BV 0) (SN (^enum ["tt"]))
(singleton "tt" (^Tag "tt")))
(^enum ["tt"]),
2023-03-26 08:40:54 -04:00
testTCFail "ω.x : {tt} ⊢ 1 · case1 x return {tt} of { 'ff ⇒ 'tt } ⇏" $
infer_ (ctx [< ("x", ^enum ["tt"])]) SOne
2023-05-01 21:06:25 -04:00
(^CaseEnum One (^BV 0) (SN (^enum ["tt"]))
(singleton "ff" (^Tag "tt")))
2023-03-26 08:40:54 -04:00
],
2023-04-01 10:02:02 -04:00
"equality types" :- [
2023-04-01 13:16:43 -04:00
testTC "0 · : ★₀ ⇐ Type" $
2023-05-01 21:06:25 -04:00
checkType_ empty (^Eq0 (^TYPE 0) nat nat) Nothing,
2023-04-01 13:16:43 -04:00
testTC "0 · : ★₀ ⇐ ★₁" $
check_ empty SZero (^Eq0 (^TYPE 0) nat nat) (^TYPE 1),
2023-04-01 13:16:43 -04:00
testTCFail "1 · : ★₀ ⇍ ★₁" $
check_ empty SOne (^Eq0 (^TYPE 0) nat nat) (^TYPE 1),
2023-04-01 13:16:43 -04:00
testTC "0 · : ★₀ ⇐ ★₂" $
check_ empty SZero (^Eq0 (^TYPE 0) nat nat) (^TYPE 2),
2023-04-01 13:16:43 -04:00
testTC "0 · : ★₁ ⇐ ★₂" $
check_ empty SZero (^Eq0 (^TYPE 1) nat nat) (^TYPE 2),
2023-04-01 13:16:43 -04:00
testTCFail "0 · : ★₁ ⇍ ★₁" $
check_ empty SZero (^Eq0 (^TYPE 1) nat nat) (^TYPE 1),
2023-04-01 13:16:43 -04:00
testTCFail "0 ≡ 'beep : {beep} ⇍ Type" $
2023-05-01 21:06:25 -04:00
checkType_ empty
(^Eq0 (^enum ["beep"]) (^Zero) (^Tag "beep"))
Nothing,
2023-04-01 13:16:43 -04:00
testTC "ab : A ≡ B : ★₀, x : A, y : B ⊢ 0 · Eq [i ⇒ ab i] x y ⇐ ★₀" $
2023-05-21 14:09:34 -04:00
check_ (ctx [< ("ab", ^Eq0 (^TYPE 0) (^FT "A" 0) (^FT "B" 0)),
("x", ^FT "A" 0), ("y", ^FT "B" 0)]) SZero
2023-05-01 21:06:25 -04:00
(^EqY "i" (E $ ^DApp (^BV 2) (^BV 0)) (^BVT 1) (^BVT 0))
(^TYPE 0),
2023-04-01 13:16:43 -04:00
testTCFail "ab : A ≡ B : ★₀, x : A, y : B ⊢ Eq [i ⇒ ab i] y x ⇍ Type" $
2023-05-21 14:09:34 -04:00
check_ (ctx [< ("ab", ^Eq0 (^TYPE 0) (^FT "A" 0) (^FT "B" 0)),
("x", ^FT "A" 0), ("y", ^FT "B" 0)]) SZero
2023-05-01 21:06:25 -04:00
(^EqY "i" (E $ ^DApp (^BV 2) (^BV 0)) (^BVT 0) (^BVT 1))
(^TYPE 0)
2023-04-01 10:02:02 -04:00
],
2023-02-13 16:06:53 -05:00
"equalities" :- [
2023-03-04 15:02:51 -05:00
testTC "1 · (δ i ⇒ a) ⇐ a ≡ a" $
check_ empty SOne (^DLamN (^FT "a" 0))
2023-05-21 14:09:34 -04:00
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0)),
2023-05-01 21:06:25 -04:00
testTC "0 · (λ p q ⇒ δ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q # uip" $
check_ empty SZero
2023-05-01 21:06:25 -04:00
(^LamY "p" (^LamY "q" (^DLamN (^BVT 1))))
2023-05-21 14:09:34 -04:00
(^PiY Any "p" (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0))
(^PiY Any "q" (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0))
(^Eq0 (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0))
(^BVT 1) (^BVT 0)))),
2023-05-01 21:06:25 -04:00
testTC "0 · (λ p q ⇒ δ i ⇒ q) ⇐ (ω·p q : a ≡ a') → p ≡ q # uip(2)" $
check_ empty SZero
2023-05-01 21:06:25 -04:00
(^LamY "p" (^LamY "q" (^DLamN (^BVT 0))))
2023-05-21 14:09:34 -04:00
(^PiY Any "p" (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0))
(^PiY Any "q" (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0))
(^Eq0 (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0))
(^BVT 1) (^BVT 0))))
2023-02-13 16:06:53 -05:00
],
2023-03-31 13:11:35 -04:00
"natural numbers" :- [
testTC "0 · ⇐ ★₀" $ check_ empty SZero nat (^TYPE 0),
testTC "0 · ⇐ ★₇" $ check_ empty SZero nat (^TYPE 7),
testTCFail "1 · ⇍ ★₀" $ check_ empty SOne nat (^TYPE 0),
testTC "1 · zero ⇐ " $ check_ empty SOne (^Zero) nat,
testTCFail "1 · zero ⇍ ×" $ check_ empty SOne (^Zero) (^And nat nat),
2023-03-31 13:11:35 -04:00
testTC "ω·n : ⊢ 1 · succ n ⇐ " $
check_ (ctx [< ("n", nat)]) SOne (^Succ (^BVT 0)) nat,
2023-03-31 13:11:35 -04:00
testTC "1 · λ n ⇒ succ n ⇐ 1." $
check_ empty SOne
2023-05-01 21:06:25 -04:00
(^LamY "n" (^Succ (^BVT 0)))
(^Arr One nat nat)
2023-03-31 13:11:35 -04:00
],
2023-04-01 10:01:53 -04:00
"natural elim" :- [
note "1 · λ n ⇒ case1 n return of { zero ⇒ 0; succ n ⇒ n }",
note " ⇐ 1.",
testTC "pred" $
check_ empty SOne
2023-05-01 21:06:25 -04:00
(^LamY "n" (E $
^CaseNat One Zero (^BV 0) (SN nat)
(^Zero) (SY [< "n", ^BN Unused] $ ^BVT 1)))
(^Arr One nat nat),
2023-04-01 10:01:53 -04:00
note "1 · λ m n ⇒ case1 m return of { zero ⇒ n; succ _, 1.p ⇒ succ p }",
note " ⇐ 1. → 1. → 1.",
testTC "plus" $
check_ empty SOne
2023-05-01 21:06:25 -04:00
(^LamY "m" (^LamY "n" (E $
^CaseNat One One (^BV 1) (SN nat)
(^BVT 0)
(SY [< ^BN Unused, "p"] $ ^Succ (^BVT 0)))))
(^Arr One nat (^Arr One nat nat))
2023-04-01 10:01:53 -04:00
],
2023-03-31 13:11:35 -04:00
"box types" :- [
testTC "0 · [0.] ⇐ ★₀" $
check_ empty SZero (^BOX Zero nat) (^TYPE 0),
2023-03-31 13:11:35 -04:00
testTC "0 · [0.★₀] ⇐ ★₁" $
check_ empty SZero (^BOX Zero (^TYPE 0)) (^TYPE 1),
2023-03-31 13:11:35 -04:00
testTCFail "0 · [0.★₀] ⇍ ★₀" $
check_ empty SZero (^BOX Zero (^TYPE 0)) (^TYPE 0)
2023-03-31 13:11:35 -04:00
],
todo "box values",
todo "box elim",
2023-04-03 11:46:23 -04:00
"type-case" :- [
testTC "0 · type-case ∷ ★₀ return ★₀ of { _ ⇒ } ⇒ ★₀" $
inferAs empty SZero
2023-05-01 21:06:25 -04:00
(^TypeCase (^Ann nat (^TYPE 0)) (^TYPE 0) empty nat)
(^TYPE 0)
2023-04-03 11:46:23 -04:00
],
2023-05-01 21:06:25 -04:00
todo "add the examples dir to the tests"
]
{-
2023-02-11 12:15:50 -05:00
"misc" :- [
2023-02-12 15:30:08 -05:00
note "0·A : Type, 0·P : A → Type, ω·p : (1·x : A) → P x",
note "",
2023-03-04 15:02:51 -05:00
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)",
2023-02-12 15:30:08 -05:00
testTC "cong" $
check_ empty SOne
([< "x", "y", "xy"] :\\ [< "i"] :\\% E (F "p" :@ E (BV 0 :% BV 0)))
(PiY Zero "x" (FT "A") $
PiY Zero "y" (FT "A") $
PiY One "xy" (Eq0 (FT "A") (BVT 1) (BVT 0)) $
EqY "i" (E $ F "P" :@ E (BV 0 :% BV 0))
2023-02-25 09:24:45 -05:00
(E $ F "p" :@ BVT 2) (E $ F "p" :@ BVT 1)),
2023-02-12 15:30:08 -05:00
note "0·A : Type, 0·P : ω·A → Type,",
2023-02-13 16:06:53 -05:00
note "ω·p q : (1·x : A) → P x",
2023-02-12 15:30:08 -05:00
note "",
2023-03-04 15:02:51 -05:00
note "1 · λ eq ⇒ δ i ⇒ λ x ⇒ eq x i",
2023-02-13 16:06:53 -05:00
note " ⇐ (1·eq : (1·x : A) → p x ≡ q x) → p ≡ q",
2023-02-12 15:30:08 -05:00
testTC "funext" $
check_ empty SOne
([< "eq"] :\\ [< "i"] :\\% [< "x"] :\\ E (BV 1 :@ BVT 0 :% BV 0))
(PiY One "eq"
(PiY One "x" (FT "A")
2023-02-25 09:24:45 -05:00
(Eq0 (E $ F "P" :@ BVT 0)
(E $ F "p" :@ BVT 0) (E $ F "q" :@ BVT 0)))
(Eq0 (PiY Any "x" (FT "A") $ E $ F "P" :@ BVT 0) (FT "p") (FT "q"))),
2023-03-10 15:52:29 -05:00
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 { }
2023-02-11 12:15:50 -05:00
]
2023-05-01 21:06:25 -04:00
-}