quox/tests/Tests/Typechecker.idr

419 lines
16 KiB
Idris
Raw Normal View History

2023-02-11 12:15:50 -05:00
module Tests.Typechecker
import Quox.Syntax
import Quox.Syntax.Qty.Three
import Quox.Typechecker as Lib
import public TypingImpls
import TAP
2023-02-13 16:06:53 -05:00
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)]
2023-02-11 12:15:50 -05:00
0 M : Type -> Type
2023-02-13 16:06:53 -05:00
M = ReaderT (Definitions Three) $ Either Error'
2023-02-11 12:15:50 -05:00
2023-02-13 16:06:53 -05:00
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
2023-02-11 12:15:50 -05:00
reflTy : IsQty q => Term q d n
reflTy =
2023-02-25 09:24:45 -05:00
Pi_ zero "A" (TYPE 0) $
Pi_ one "x" (BVT 0) $
2023-02-11 12:15:50 -05:00
Eq0 (BVT 1) (BVT 0) (BVT 0)
reflDef : IsQty q => Term q d n
reflDef = [< "A","x"] :\\ [< "i"] :\\% BVT 0
2023-02-11 12:15:50 -05:00
2023-02-23 04:04:16 -05:00
fstTy : Term Three d n
fstTy =
2023-02-25 09:24:45 -05:00
(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))
2023-02-23 04:04:16 -05:00
fstDef : Term Three d n
fstDef =
([< "A","B","p"] :\\
E (CasePair Any (BV 0) (SN $ BVT 2) (SY [< "x","y"] $ BVT 1)))
2023-02-23 04:04:16 -05:00
sndTy : Term Three d n
sndTy =
2023-02-25 09:24:45 -05:00
(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) $
2023-02-23 04:04:16 -05:00
E (BV 1 :@ E (F "fst" :@@ [BVT 2, BVT 1, BVT 0])))
sndDef : Term Three d n
sndDef =
([< "A","B","p"] :\\
2023-02-23 04:04:16 -05:00
E (CasePair Any (BV 0)
(SY [< "p"] $ E $ BV 2 :@ E (F "fst" :@@ [BVT 3, BVT 2, BVT 0]))
(SY [< "x","y"] $ BVT 0)))
2023-02-23 04:04:16 -05:00
2023-02-11 12:15:50 -05:00
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),
2023-02-23 04:04:16 -05:00
("refl", mkDef Any reflTy reflDef),
("fst", mkDef Any fstTy fstDef),
("snd", mkDef Any sndTy sndDef)]
2023-02-11 12:15:50 -05:00
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
2023-03-15 10:54:51 -04:00
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
2023-02-11 12:15:50 -05:00
2023-02-13 16:06:53 -05:00
inferredTypeEq : TyContext Three d n -> (exp, got : Term Three d n) -> M ()
inferredTypeEq ctx exp got =
catchError
(inj $ equalType ctx exp got)
2023-02-13 16:06:53 -05:00
(\_ : Error' => throwError $ WrongInfer exp got)
qoutEq : (exp, got : QOutput Three n) -> M ()
qoutEq qout res = unless (qout == res) $ throwError $ WrongQOut qout res
2023-02-11 12:15:50 -05:00
inferAs : TyContext Three d n -> (sg : SQty Three) ->
Elim Three d n -> Term Three d n -> M ()
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
inferAsQ : TyContext Three d n -> (sg : SQty Three) ->
Elim Three d n -> Term Three d n -> QOutput Three n -> M ()
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
infer_ : TyContext Three d n -> (sg : SQty Three) -> Elim Three d n -> M ()
2023-02-13 16:06:53 -05:00
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 ()
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
check_ : TyContext Three d n -> SQty Three ->
Term Three d n -> Term Three d n -> M ()
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
checkType_ : TyContext Three d n -> Term Three d n -> Maybe Universe -> M ()
checkType_ ctx s u = inj $ checkType ctx s u
2023-02-23 04:04:16 -05:00
-- ω 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
2023-02-11 12:15:50 -05:00
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)
2023-02-11 12:15:50 -05:00
],
"function types" :- [
2023-02-13 16:06:53 -05:00
note "A, B : ★₀; C, D : ★₁; P : A ⇾ ★₀",
2023-02-12 15:30:08 -05:00
testTC "0 · A ⊸ B ⇐ ★₀" $
check_ empty szero (Arr One (FT "A") (FT "B")) (TYPE 0),
2023-02-12 15:30:08 -05:00
note "subtyping",
testTC "0 · A ⊸ B ⇐ ★₁" $
check_ empty szero (Arr One (FT "A") (FT "B")) (TYPE 1),
2023-02-12 15:30:08 -05:00
testTC "0 · C ⊸ D ⇐ ★₁" $
check_ empty szero (Arr One (FT "C") (FT "D")) (TYPE 1),
2023-02-12 15:30:08 -05:00
testTCFail "0 · C ⊸ D ⇍ ★₀" $
check_ empty szero (Arr One (FT "C") (FT "D")) (TYPE 0),
2023-02-13 16:06:53 -05:00
testTC "0 · (1·x : A) → P x ⇐ ★₀" $
check_ empty szero
2023-02-25 09:24:45 -05:00
(Pi_ One "x" (FT "A") $ E $ F "P" :@ BVT 0)
2023-02-13 16:06:53 -05:00
(TYPE 0),
testTCFail "0 · A ⊸ P ⇍ ★₀" $
check_ empty szero (Arr One (FT "A") $ FT "P") (TYPE 0),
2023-02-19 11:51:44 -05:00
testTC "0=1 ⊢ 0 · A ⊸ P ⇐ ★₀" $
check_ empty01 szero (Arr One (FT "A") $ FT "P") (TYPE 0)
2023-02-13 16:06:53 -05:00
],
"pair types" :- [
note #""A × B" for "(_ : A) × B""#,
testTC "0 · A × A ⇐ ★₀" $
check_ empty szero (FT "A" `And` FT "A") (TYPE 0),
2023-02-23 04:04:16 -05:00
testTCFail "0 · A × P ⇍ ★₀" $
check_ empty szero (FT "A" `And` FT "P") (TYPE 0),
2023-02-23 04:04:16 -05:00
testTC "0 · (x : A) × P x ⇐ ★₀" $
check_ empty szero
2023-02-25 09:24:45 -05:00
(Sig_ "x" (FT "A") $ E $ F "P" :@ BVT 0) (TYPE 0),
2023-02-23 04:04:16 -05:00
testTC "0 · (x : A) × P x ⇐ ★₁" $
check_ empty szero
2023-02-25 09:24:45 -05:00
(Sig_ "x" (FT "A") $ E $ F "P" :@ BVT 0) (TYPE 1),
2023-02-23 04:04:16 -05:00
testTC "0 · (A : ★₀) × A ⇐ ★₁" $
check_ empty szero (Sig_ "A" (TYPE 0) $ BVT 0) (TYPE 1),
2023-02-23 04:04:16 -05:00
testTCFail "0 · (A : ★₀) × A ⇍ ★₀" $
check_ empty szero (Sig_ "A" (TYPE 0) $ BVT 0) (TYPE 0),
2023-02-13 16:06:53 -05:00
testTCFail "1 · A × A ⇍ ★₀" $
check_ empty sone (FT "A" `And` FT "A") (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") (TYPE 0),
2023-02-13 16:06:53 -05:00
testTC "0 · [A] ⇐ ★₀" $
check_ empty szero (FT "A") (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") (TYPE 1),
2023-02-12 15:30:08 -05:00
note "(fail) runtime-relevant type",
testTCFail "1 · A ⇏ ★₀" $
infer_ empty sone (F "A"),
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") reflTy,
testTC "1 · [refl] ⇐ ⋯" $ check_ empty sone (FT "refl") 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 {n = 1} (ctx [< ("x", FT "A")]) sone
2023-02-13 16:06:53 -05:00
(BV 0) (FT "A") [< one],
2023-02-14 15:14:47 -05:00
testTC "x : A ⊢ 1 · [x] ⇐ A ⊳ 1·x" $
checkQ {n = 1} (ctx [< ("x", FT "A")]) sone (BVT 0) (FT "A") [< one],
2023-02-23 04:04:16 -05:00
note "f2 : A ⊸ A ⊸ B",
testTC "x : A ⊢ 1 · f2 [x] [x] ⇒ B ⊳ ω·x" $
inferAsQ {n = 1} (ctx [< ("x", FT "A")]) sone
2023-02-23 04:04:16 -05:00
(F "f2" :@@ [BVT 0, BVT 0]) (FT "B") [< 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 ([< "x"] :\\ BVT 0) (Arr One (FT "A") (FT "A")),
2023-03-04 15:02:51 -05:00
testTC "1 · (λ x ⇒ x) ⇐ A → A" $
check_ empty sone ([< "x"] :\\ BVT 0) (Arr Any (FT "A") (FT "A")),
2023-02-12 15:30:08 -05:00
note "(fail) zero binding used relevantly",
2023-03-04 15:02:51 -05:00
testTCFail "1 · (λ x ⇒ x) ⇍ A ⇾ A" $
check_ empty sone ([< "x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")),
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 ([< "x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")),
2023-03-04 15:02:51 -05:00
testTC "1 · (λ A x ⇒ refl A x) ⇐ ⋯ # (type of refl)" $
check_ empty sone
([< "A", "x"] :\\ E (F "refl" :@@ [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 (Pair (FT "a") (FT "a")) (FT "A" `And` FT "A"),
2023-02-23 04:04:16 -05:00
testTC "x : A ⊢ 1 · (x, x) ⇐ A × A ⊳ ω·x" $
checkQ (ctx [< ("x", FT "A")]) sone
2023-02-23 04:04:16 -05:00
(Pair (BVT 0) (BVT 0)) (FT "A" `And` FT "A") [< Any],
2023-03-04 15:02:51 -05:00
testTC "1 · (a, δ i ⇒ a) ⇐ (x : A) × (x ≡ a)" $
check_ empty sone
(Pair (FT "a") ([< "i"] :\\% FT "a"))
2023-02-25 09:24:45 -05:00
(Sig_ "x" (FT "A") $ Eq0 (FT "A") (BVT 0) (FT "a"))
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", FT "A" `And` FT "A")]) sone
2023-02-25 09:24:45 -05:00
(CasePair One (BV 0) (SN $ FT "B")
(SY [< "l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0]))
2023-02-23 04:04:16 -05:00
(FT "B") [< 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", FT "A" `And` FT "A")]) sone
2023-02-25 09:24:45 -05:00
(CasePair Any (BV 0) (SN $ FT "B")
(SY [< "l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0]))
2023-02-23 04:04:16 -05:00
(FT "B") [< 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", FT "A" `And` FT "A")]) szero
2023-02-25 09:24:45 -05:00
(CasePair Any (BV 0) (SN $ FT "B")
(SY [< "l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0]))
2023-02-23 04:04:16 -05:00
(FT "B") [< 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", FT "A" `And` FT "A")]) sone
2023-02-25 09:24:45 -05:00
(CasePair Zero (BV 0) (SN $ FT "B")
(SY [< "l", "r"] $ E $ F "f2" :@@ [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", FT "A" `And` FT "B")]) sone
2023-02-25 09:24:45 -05:00
(CasePair Any (BV 0) (SN $ FT "A")
(SY [< "l", "r"] $ BVT 1))
2023-02-23 04:04:16 -05:00
(FT "A") [< 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", FT "A" `And` FT "B")]) szero
2023-02-25 09:24:45 -05:00
(CasePair One (BV 0) (SN $ FT "A")
(SY [< "l", "r"] $ BVT 1))
2023-02-23 04:04:16 -05:00
(FT "A") [< 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", FT "A" `And` FT "B")]) sone
2023-02-25 09:24:45 -05:00
(CasePair One (BV 0) (SN $ FT "A")
(SY [< "l", "r"] $ BVT 1)),
2023-02-23 04:04:16 -05: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-02-23 04:04:16 -05:00
testTC "0 · type of fst ⇐ ★₂" $
check_ empty szero fstTy (TYPE 2),
2023-02-23 04:04:16 -05:00
testTC "1 · def of fsttype of fst" $
check_ empty sone fstDef fstTy,
2023-02-23 04:04:16 -05: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-02-23 04:04:16 -05:00
testTC "0 · type of snd ⇐ ★₂" $
check_ empty szero sndTy (TYPE 2),
2023-02-23 04:04:16 -05:00
testTC "1 · def of sndtype of snd" $
check_ empty sone sndDef sndTy,
2023-03-04 15:02:51 -05:00
testTC "0 · snd ★₀ (λ x ⇒ x) ⇒ (ω·p : (A : ★₀) × A) → fst ★₀ (λ x ⇒ x) p" $
inferAs empty szero
(F "snd" :@@ [TYPE 0, [< "x"] :\\ BVT 0])
2023-02-25 09:24:45 -05:00
(Pi_ Any "A" (Sig_ "A" (TYPE 0) $ BVT 0) $
(E $ F "fst" :@@ [TYPE 0, [< "x"] :\\ BVT 0, BVT 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-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 (DLam $ SN $ FT "a")
2023-02-13 16:06:53 -05:00
(Eq0 (FT "A") (FT "a") (FT "a")),
2023-03-04 15:02:51 -05:00
testTC "0 · (λ p q ⇒ δ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
check_ empty szero
([< "p","q"] :\\ [< "i"] :\\% BVT 1)
2023-02-25 09:24:45 -05:00
(Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $
Pi_ Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $
2023-02-13 16:06:53 -05:00
Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0)),
2023-03-04 15:02:51 -05:00
testTC "0 · (λ p q ⇒ δ i ⇒ q) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
check_ empty szero
([< "p","q"] :\\ [< "i"] :\\% BVT 0)
2023-02-25 09:24:45 -05:00
(Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $
Pi_ Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $
2023-02-13 16:06:53 -05:00
Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0))
],
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)))
2023-02-25 09:24:45 -05:00
(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)),
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))
2023-02-25 09:24:45 -05:00
(Pi_ One "eq"
(Pi_ One "x" (FT "A")
(Eq0 (E $ F "P" :@ BVT 0)
(E $ F "p" :@ BVT 0) (E $ F "q" :@ BVT 0)))
2023-03-10 15:52:29 -05:00
(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 { }
2023-02-11 12:15:50 -05:00
]
]