more tc tests
This commit is contained in:
parent
534e0d2270
commit
846bbc9ca3
1 changed files with 119 additions and 28 deletions
|
|
@ -7,9 +7,31 @@ import public TypingImpls
|
||||||
import TAP
|
import TAP
|
||||||
|
|
||||||
|
|
||||||
0 M : Type -> Type
|
data Error'
|
||||||
M = ReaderT (Definitions Three) $ Either (Error Three)
|
= 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 : IsQty q => Term q d n
|
||||||
|
|
@ -23,17 +45,19 @@ reflDef = ["A","x"] :\\ ["i"] :\\% BVT 0
|
||||||
|
|
||||||
defGlobals : Definitions Three
|
defGlobals : Definitions Three
|
||||||
defGlobals = fromList
|
defGlobals = fromList
|
||||||
[("A", mkAbstract Zero $ TYPE 0),
|
[("A", mkAbstract Zero $ TYPE 0),
|
||||||
("B", mkAbstract Zero $ TYPE 0),
|
("B", mkAbstract Zero $ TYPE 0),
|
||||||
("C", mkAbstract Zero $ TYPE 1),
|
("C", mkAbstract Zero $ TYPE 1),
|
||||||
("D", mkAbstract Zero $ TYPE 1),
|
("D", mkAbstract Zero $ TYPE 1),
|
||||||
("P", mkAbstract Zero $ Arr Any (FT "A") (TYPE 0)),
|
("P", mkAbstract Zero $ Arr Any (FT "A") (TYPE 0)),
|
||||||
("a", mkAbstract Any $ FT "A"),
|
("a", mkAbstract Any $ FT "A"),
|
||||||
("b", mkAbstract Any $ FT "B"),
|
("a'", mkAbstract Any $ FT "A"),
|
||||||
("f", mkAbstract Any $ Arr One (FT "A") (FT "A")),
|
("b", mkAbstract Any $ FT "B"),
|
||||||
("g", mkAbstract Any $ Arr One (FT "A") (FT "B")),
|
("f", mkAbstract Any $ Arr One (FT "A") (FT "A")),
|
||||||
("p", mkAbstract Any $ Pi One "x" (FT "A") $ TUsed $ E $ F "P" :@ BVT 0),
|
("g", mkAbstract Any $ Arr One (FT "A") (FT "B")),
|
||||||
("q", mkAbstract Any $ Pi One "x" (FT "A") $ TUsed $ E $ F "P" :@ BVT 0),
|
("f2", mkAbstract Any $ Arr One (FT "A") $ Arr One (FT "A") (FT "A")),
|
||||||
|
("p", mkAbstract Any $ Pi One "x" (FT "A") $ TUsed $ E $ F "P" :@ BVT 0),
|
||||||
|
("q", mkAbstract Any $ Pi One "x" (FT "A") $ TUsed $ E $ F "P" :@ BVT 0),
|
||||||
("refl", mkDef Any reflTy reflDef)]
|
("refl", mkDef Any reflTy reflDef)]
|
||||||
|
|
||||||
parameters (label : String) (act : Lazy (M ()))
|
parameters (label : String) (act : Lazy (M ()))
|
||||||
|
|
@ -53,20 +77,40 @@ ctxWith dctx tqctx =
|
||||||
ctx : Context (\i => (Term Three 0 i, Three)) n -> TyContext Three 0 n
|
ctx : Context (\i => (Term Three 0 i, Three)) n -> TyContext Three 0 n
|
||||||
ctx = ctxWith DNil
|
ctx = ctxWith DNil
|
||||||
|
|
||||||
|
inferredTypeEq : TyContext Three d n -> (exp, got : Term Three d n) -> M ()
|
||||||
|
inferredTypeEq ctx exp got =
|
||||||
|
catchError
|
||||||
|
(inj $ equalType (makeDimEq ctx.dctx) ctx.tctx 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) ->
|
inferAs : TyContext Three d n -> (sg : SQty Three) ->
|
||||||
Elim Three d n -> Term Three d n -> M ()
|
Elim Three d n -> Term Three d n -> M ()
|
||||||
inferAs ctx sg e ty = do
|
inferAs ctx sg e ty = do
|
||||||
ty' <- infer ctx sg e
|
res <- inj $ infer ctx sg e
|
||||||
catchError
|
inferredTypeEq ctx ty res.type
|
||||||
(equalType (makeDimEq ctx.dctx) ctx.tctx ty ty'.type)
|
|
||||||
(\_ : Error Three => throwError $ ClashT Equal (TYPE UAny) ty ty'.type)
|
inferAsQ : TyContext Three d n -> (sg : SQty Three) ->
|
||||||
|
Elim Three d n -> Term Three d n -> QOutput Three n -> M ()
|
||||||
|
inferAsQ ctx sg e ty qout = do
|
||||||
|
res <- inj $ infer ctx sg e
|
||||||
|
inferredTypeEq ctx ty res.type
|
||||||
|
qoutEq qout res.qout
|
||||||
|
|
||||||
infer_ : TyContext Three d n -> (sg : SQty Three) -> Elim Three d n -> M ()
|
infer_ : TyContext Three d n -> (sg : SQty Three) -> Elim Three d n -> M ()
|
||||||
infer_ ctx sg e = ignore $ infer ctx sg e
|
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 sg s ty qout = do
|
||||||
|
res <- inj $ check ctx sg s ty
|
||||||
|
qoutEq qout res
|
||||||
|
|
||||||
check_ : TyContext Three d n -> SQty Three ->
|
check_ : TyContext Three d n -> SQty Three ->
|
||||||
Term Three d n -> Term Three d n -> M ()
|
Term Three d n -> Term Three d n -> M ()
|
||||||
check_ ctx sg s ty = ignore $ check ctx sg s ty
|
check_ ctx sg s ty = ignore $ inj $ check ctx sg s ty
|
||||||
|
|
||||||
export
|
export
|
||||||
tests : Test
|
tests : Test
|
||||||
|
|
@ -82,7 +126,7 @@ tests = "typechecker" :- [
|
||||||
],
|
],
|
||||||
|
|
||||||
"function types" :- [
|
"function types" :- [
|
||||||
note "A, B : ★₀; C, D : ★₁",
|
note "A, B : ★₀; C, D : ★₁; P : A ⇾ ★₀",
|
||||||
testTC "0 · A ⊸ B ⇐ ★₀" $
|
testTC "0 · A ⊸ B ⇐ ★₀" $
|
||||||
check_ (ctx [<]) szero (Arr One (FT "A") (FT "B")) (TYPE 0),
|
check_ (ctx [<]) szero (Arr One (FT "A") (FT "B")) (TYPE 0),
|
||||||
note "subtyping",
|
note "subtyping",
|
||||||
|
|
@ -91,25 +135,52 @@ tests = "typechecker" :- [
|
||||||
testTC "0 · C ⊸ D ⇐ ★₁" $
|
testTC "0 · C ⊸ D ⇐ ★₁" $
|
||||||
check_ (ctx [<]) szero (Arr One (FT "C") (FT "D")) (TYPE 1),
|
check_ (ctx [<]) szero (Arr One (FT "C") (FT "D")) (TYPE 1),
|
||||||
testTCFail "0 · C ⊸ D ⇍ ★₀" $
|
testTCFail "0 · C ⊸ D ⇍ ★₀" $
|
||||||
check_ (ctx [<]) szero (Arr One (FT "C") (FT "D")) (TYPE 0)
|
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") $ TUsed $ E $ F "P" :@ BVT 0)
|
||||||
|
(TYPE 0),
|
||||||
|
testTCFail "0 · A ⊸ P ⇍ ★₀" $
|
||||||
|
check_ (ctx [<]) 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 "1 · A × A ⇍ ★₀" $
|
||||||
|
check_ (ctx [<]) sone (FT "A" `And` FT "A") (TYPE 0)
|
||||||
],
|
],
|
||||||
|
|
||||||
"free vars" :- [
|
"free vars" :- [
|
||||||
note "A : ★₀",
|
note "A : ★₀",
|
||||||
testTC "0 · A ⇒ ★₀" $
|
testTC "0 · A ⇒ ★₀" $
|
||||||
inferAs (ctx [<]) szero (F "A") (TYPE 0),
|
inferAs (ctx [<]) szero (F "A") (TYPE 0),
|
||||||
note "check",
|
testTC "0 · [A] ⇐ ★₀" $
|
||||||
testTC "0 · A ⇐ ★₀" $
|
|
||||||
check_ (ctx [<]) szero (FT "A") (TYPE 0),
|
check_ (ctx [<]) szero (FT "A") (TYPE 0),
|
||||||
note "subtyping",
|
note "subtyping",
|
||||||
testTC "0 · A ⇐ ★₁" $
|
testTC "0 · [A] ⇐ ★₁" $
|
||||||
check_ (ctx [<]) szero (FT "A") (TYPE 1),
|
check_ (ctx [<]) szero (FT "A") (TYPE 1),
|
||||||
note "(fail) runtime-relevant type",
|
note "(fail) runtime-relevant type",
|
||||||
testTCFail "1 · A ⇏ ★₀" $
|
testTCFail "1 · A ⇏ ★₀" $
|
||||||
infer_ (ctx [<]) sone (F "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 ⇒ ⋯" $ inferAs (ctx [<]) sone (F "refl") reflTy,
|
||||||
testTC "1 · refl ⇐ ⋯" $ check_ (ctx [<]) sone (FT "refl") reflTy
|
testTC "1 · [refl] ⇐ ⋯" $ check_ (ctx [<]) sone (FT "refl") reflTy
|
||||||
|
],
|
||||||
|
|
||||||
|
"bound vars" :- [
|
||||||
|
testTC "1·x : A ⊢ 1 · x ⇒ A ⊳ 1·x" $
|
||||||
|
inferAsQ {n = 1} (ctx [< (FT "A", one)]) sone
|
||||||
|
(BV 0) (FT "A") [< one],
|
||||||
|
testTC "1·x : A ⊢ 1 · [x] ⇐ A ⊳ 1·x" $
|
||||||
|
checkQ {n = 1} (ctx [< (FT "A", one)]) sone (BVT 0) (FT "A") [< one],
|
||||||
|
note "f2 : A ⊸ A ⊸ A",
|
||||||
|
testTC "ω·x : A ⊢ 1 · f2 [x] [x] ⇒ A ⊳ ω·x" $
|
||||||
|
inferAsQ {n = 1} (ctx [< (FT "A", Any)]) sone
|
||||||
|
(F "f2" :@@ [BVT 0, BVT 0]) (FT "A") [< Any],
|
||||||
|
note #"("0·x : A ⊢ 1 · x ⇒ A" won't fail because"#,
|
||||||
|
note " a var's quantity is only checked once it leaves scope)"
|
||||||
],
|
],
|
||||||
|
|
||||||
"lambda" :- [
|
"lambda" :- [
|
||||||
|
|
@ -132,11 +203,31 @@ tests = "typechecker" :- [
|
||||||
check_ (ctx [<]) sone reflDef reflTy
|
check_ (ctx [<]) sone reflDef reflTy
|
||||||
],
|
],
|
||||||
|
|
||||||
|
"equalities" :- [
|
||||||
|
testTC "1 · (λᴰ i ⇒ a) ⇐ a ≡ a" $
|
||||||
|
check_ (ctx [<]) sone (DLam "i" $ DUnused $ FT "a")
|
||||||
|
(Eq0 (FT "A") (FT "a") (FT "a")),
|
||||||
|
testTC "0 · (λ p q ⇒ λᴰ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
|
||||||
|
check_ (ctx [<]) szero
|
||||||
|
(Lam "p" $ TUsed $ Lam "q" $ TUnused $
|
||||||
|
DLam "i" $ DUnused $ BVT 0)
|
||||||
|
(Pi Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $ TUsed $
|
||||||
|
Pi Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $ TUsed $
|
||||||
|
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
|
||||||
|
(Lam "p" $ TUnused $ Lam "q" $ TUsed $
|
||||||
|
DLam "i" $ DUnused $ BVT 0)
|
||||||
|
(Pi Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $ TUsed $
|
||||||
|
Pi Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $ TUsed $
|
||||||
|
Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0))
|
||||||
|
],
|
||||||
|
|
||||||
"misc" :- [
|
"misc" :- [
|
||||||
note "0·A : Type, 0·P : A → Type, ω·p : (1·x : A) → P x",
|
note "0·A : Type, 0·P : A → Type, ω·p : (1·x : A) → P x",
|
||||||
note "⊢",
|
note "⊢",
|
||||||
note "1 · λ x y xy ⇒ λᴰ i ⇒ p (xy i)",
|
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 " ⇐ (0·x y : A) → (1·xy : x ≡ y) → Eq [i ⇒ P (xy i)] (p x) (p y)",
|
||||||
testTC "cong" $
|
testTC "cong" $
|
||||||
check_ (ctx [<]) sone
|
check_ (ctx [<]) sone
|
||||||
(["x", "y", "xy"] :\\ ["i"] :\\% E (F "p" :@ E (BV 0 :% BV 0)))
|
(["x", "y", "xy"] :\\ ["i"] :\\% E (F "p" :@ E (BV 0 :% BV 0)))
|
||||||
|
|
@ -146,10 +237,10 @@ tests = "typechecker" :- [
|
||||||
Eq "i" (DUsed $ E $ F "P" :@ E (BV 0 :% BV 0))
|
Eq "i" (DUsed $ E $ F "P" :@ E (BV 0 :% BV 0))
|
||||||
(E $ F "p" :@ BVT 2) (E $ F "p" :@ BVT 1)),
|
(E $ F "p" :@ BVT 2) (E $ F "p" :@ BVT 1)),
|
||||||
note "0·A : Type, 0·P : ω·A → Type,",
|
note "0·A : Type, 0·P : ω·A → Type,",
|
||||||
note "ω·p, q : (1·x : A) → P x",
|
note "ω·p q : (1·x : A) → P x",
|
||||||
note "⊢",
|
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",
|
note " ⇐ (1·eq : (1·x : A) → p x ≡ q x) → p ≡ q",
|
||||||
testTC "funext" $
|
testTC "funext" $
|
||||||
check_ (ctx [<]) sone
|
check_ (ctx [<]) sone
|
||||||
(["eq"] :\\ ["i"] :\\% ["x"] :\\ E (BV 1 :@ BVT 0 :% BV 0))
|
(["eq"] :\\ ["i"] :\\% ["x"] :\\ E (BV 1 :@ BVT 0 :% BV 0))
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue