rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

replace ⇒ with . in lambdas, etc

Browse source 
also remove some weird duplication in the tests
This commit is contained in:
rhiannon morris 2023-02-26 11:01:47 +01:00
parent 630832f6c7
commit 55cdb19a4c
3 changed files with 58 additions and 76 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
lib/Quox/Syntax/Term/Pretty.idr
View file

@ -11,22 +11,22 @@ import Data.Vect
private %inline private %inline
typeD, arrowD, timesD, darrowD, lamD, eqndD, dlamD, annD : typeD, arrowD, timesD, lamD, eqndD, dlamD, annD :
Pretty.HasEnv m => m (Doc HL) Pretty.HasEnv m => m (Doc HL)
typeD = hlF Syntax $ ifUnicode "★" "Type" typeD = hlF Syntax $ ifUnicode "★" "Type"
arrowD = hlF Syntax $ ifUnicode "→" "->" arrowD = hlF Syntax $ ifUnicode "→" "->"
timesD = hlF Syntax $ ifUnicode "×" "**" timesD = hlF Syntax $ ifUnicode "×" "**"
darrowD = hlF Syntax $ ifUnicode "⇒" "=>"
lamD = hlF Syntax $ ifUnicode "λ" "fun" lamD = hlF Syntax $ ifUnicode "λ" "fun"
eqndD = hlF Syntax $ ifUnicode "≡" "==" eqndD = hlF Syntax $ ifUnicode "≡" "=="
dlamD = hlF Syntax $ ifUnicode "δ" "dfun" dlamD = hlF Syntax $ ifUnicode "δ" "dfun"
annD = hlF Syntax $ ifUnicode "∷" "::" annD = hlF Syntax $ ifUnicode "∷" "::"
private %inline private %inline
eqD, colonD, commaD, caseD, returnD, ofD : Doc HL eqD, colonD, commaD, dotD, caseD, returnD, ofD : Doc HL
eqD = hl Syntax "Eq" eqD = hl Syntax "Eq"
colonD = hl Syntax ":" colonD = hl Syntax ":"
commaD = hl Syntax "," commaD = hl Syntax ","
dotD = hl Delim "."
caseD = hl Syntax "case" caseD = hl Syntax "case"
ofD = hl Syntax "of" ofD = hl Syntax "of"
returnD = hl Syntax "return" returnD = hl Syntax "return"
@ -46,9 +46,9 @@ prettyLams : Pretty.HasEnv m => PrettyHL a =>
BinderSort -> List BaseName -> a -> m (Doc HL) BinderSort -> List BaseName -> a -> m (Doc HL)
prettyLams sort names body = do prettyLams sort names body = do
lam <- case sort of T => lamD; D => dlamD lam <- case sort of T => lamD; D => dlamD
header <- sequence $ [hl TVar <$> prettyM x | x <- names] ++ [darrowD] header <- sequence $ [hl TVar <$> prettyM x | x <- names]
body <- unders sort names $ prettyM body body <- unders sort names $ prettyM body
parensIfM Outer $ sep (lam :: header) <//> body parensIfM Outer $ (sep (lam :: header) <+> dotD) <//> body
export covering export covering
prettyApps : Pretty.HasEnv m => PrettyHL f => PrettyHL a => prettyApps : Pretty.HasEnv m => PrettyHL f => PrettyHL a =>
@ -66,8 +66,7 @@ prettyArm : Pretty.HasEnv m => PrettyHL a =>
(List BaseName, Doc HL, a) -> m (Doc HL) (List BaseName, Doc HL, a) -> m (Doc HL)
prettyArm (xs, pat, body) = prettyArm (xs, pat, body) =
pure $ hang 2 $ sep pure $ hang 2 $ sep
[hsep [pat, !darrowD], [pat <+> dotD, !(withPrec Outer $ unders T xs $ prettyM body)]
!(withPrec Outer $ unders T xs $ prettyM body)]
export covering export covering
prettyArms : Pretty.HasEnv m => PrettyHL a => prettyArms : Pretty.HasEnv m => PrettyHL a =>
@ -82,7 +81,7 @@ prettyCase : Pretty.HasEnv m =>
prettyCase pi elim r ret arms = prettyCase pi elim r ret arms =
pure $ align $ sep $ pure $ align $ sep $
[hsep [caseD, !(prettyQtyBinds [pi] elim)], [hsep [caseD, !(prettyQtyBinds [pi] elim)],
hsep [returnD, !(prettyM r), !darrowD, !(under T r $ prettyM ret)], hsep [returnD, !(prettyM r) <+> dotD, !(under T r $ prettyM ret)],
hsep [ofD, !(prettyArms arms)]] hsep [ofD, !(prettyArms arms)]]
-- [fixme] put delimiters around tags that aren't simple names -- [fixme] put delimiters around tags that aren't simple names
@ -118,7 +117,7 @@ mutual
parensIfM App $ parensIfM App $
eqD <++> eqD <++>
sep [bracks !(withPrec Outer $ pure $ hang 2 $ sep [bracks !(withPrec Outer $ pure $ hang 2 $
sep [hl DVar !(prettyM i) <++> !darrowD, sep [hl DVar !(prettyM i) <+> dotD,
!(under D i $ prettyM ty)]), !(under D i $ prettyM ty)]),
!(withPrec Arg $ prettyM l), !(withPrec Arg $ prettyM l),
!(withPrec Arg $ prettyM r)] !(withPrec Arg $ prettyM r)]

32
tests/Tests/Equal.idr
View file

@ -122,31 +122,31 @@ tests = "equality & subtyping" :- [
], ],
"lambda" :- [ "lambda" :- [
testEq "λ x ⇒ [x] = λ x ⇒ [x]" $ testEq "λ x. [x] = λ x. [x]" $
equalT empty (Arr One (FT "A") (FT "A")) equalT empty (Arr One (FT "A") (FT "A"))
(["x"] :\\ BVT 0) (["x"] :\\ BVT 0)
(["x"] :\\ BVT 0), (["x"] :\\ BVT 0),
testEq "λ x ⇒ [x] <: λ x ⇒ [x]" $ testEq "λ x. [x] <: λ x. [x]" $
subT empty (Arr One (FT "A") (FT "A")) subT empty (Arr One (FT "A") (FT "A"))
(["x"] :\\ BVT 0) (["x"] :\\ BVT 0)
(["x"] :\\ BVT 0), (["x"] :\\ BVT 0),
testEq "λ x ⇒ [x] = λ y ⇒ [y]" $ testEq "λ x. [x] = λ y. [y]" $
equalT empty (Arr One (FT "A") (FT "A")) equalT empty (Arr One (FT "A") (FT "A"))
(["x"] :\\ BVT 0) (["x"] :\\ BVT 0)
(["y"] :\\ BVT 0), (["y"] :\\ BVT 0),
testEq "λ x ⇒ [x] <: λ y ⇒ [y]" $ testEq "λ x. [x] <: λ y. [y]" $
equalT empty (Arr One (FT "A") (FT "A")) equalT empty (Arr One (FT "A") (FT "A"))
(["x"] :\\ BVT 0) (["x"] :\\ BVT 0)
(["y"] :\\ BVT 0), (["y"] :\\ BVT 0),
testNeq "λ x y ⇒ [x] ≠ λ x y ⇒ [y]" $ testNeq "λ x y. [x] ≠ λ x y. [y]" $
equalT empty (Arr One (FT "A") $ Arr One (FT "A") (FT "A")) equalT empty (Arr One (FT "A") $ Arr One (FT "A") (FT "A"))
(["x", "y"] :\\ BVT 1) (["x", "y"] :\\ BVT 1)
(["x", "y"] :\\ BVT 0), (["x", "y"] :\\ BVT 0),
testEq "λ x ⇒ [a] = λ x ⇒ [a] (Y vs N)" $ testEq "λ x. [a] = λ x. [a] (Y vs N)" $
equalT empty (Arr Zero (FT "B") (FT "A")) equalT empty (Arr Zero (FT "B") (FT "A"))
(Lam $ SY ["x"] $ FT "a") (Lam $ SY ["x"] $ FT "a")
(Lam $ SN $ FT "a"), (Lam $ SN $ FT "a"),
testEq "λ x ⇒ [f [x]] = [f] (η)" $ testEq "λ x. [f [x]] = [f] (η)" $
equalT empty (Arr One (FT "A") (FT "A")) equalT empty (Arr One (FT "A") (FT "A"))
(["x"] :\\ E (F "f" :@ BVT 0)) (["x"] :\\ E (F "f" :@ BVT 0))
(FT "f") (FT "f")
@ -169,7 +169,7 @@ tests = "equality & subtyping" :- [
refl a x = (DLam $ S ["_"] $ N x) :# (Eq0 a x x) refl a x = (DLam $ S ["_"] $ N x) :# (Eq0 a x x)
in in
[ [
note #""refl [A] x" is an abbreviation for "(δ i ⇒ x) ∷ (x ≡ x : A)""#, note #""refl [A] x" is an abbreviation for "(δ i. x) ∷ (x ≡ x : A)""#,
note "binds before ∥ are globals, after it are BVs", note "binds before ∥ are globals, after it are BVs",
testEq "refl [A] a = refl [A] a" $ testEq "refl [A] a = refl [A] a" $
equalE empty (refl (FT "A") (FT "a")) (refl (FT "A") (FT "a")), equalE empty (refl (FT "A") (FT "a")) (refl (FT "A") (FT "a")),
@ -250,7 +250,7 @@ tests = "equality & subtyping" :- [
"term d-closure" :- [ "term d-closure" :- [
testEq "★₀‹𝟎› = ★₀ : ★₁" $ testEq "★₀‹𝟎› = ★₀ : ★₁" $
equalTD 1 empty (TYPE 1) (DCloT (TYPE 0) (K Zero ::: id)) (TYPE 0), equalTD 1 empty (TYPE 1) (DCloT (TYPE 0) (K Zero ::: id)) (TYPE 0),
testEq "(δ i ⇒ a)‹𝟎› = (δ i ⇒ a) : (a ≡ a : A)" $ testEq "(δ i. a)‹𝟎› = (δ i. a) : (a ≡ a : A)" $
equalTD 1 empty equalTD 1 empty
(Eq0 (FT "A") (FT "a") (FT "a")) (Eq0 (FT "A") (FT "a") (FT "a"))
(DCloT (["i"] :\\% FT "a") (K Zero ::: id)) (DCloT (["i"] :\\% FT "a") (K Zero ::: id))
@ -315,24 +315,24 @@ tests = "equality & subtyping" :- [
equalE empty (F "f" :@ FT "a") (F "f" :@ FT "a"), equalE empty (F "f" :@ FT "a") (F "f" :@ FT "a"),
testEq "f [a] <: f [a]" $ testEq "f [a] <: f [a]" $
subE empty (F "f" :@ FT "a") (F "f" :@ FT "a"), subE empty (F "f" :@ FT "a") (F "f" :@ FT "a"),
testEq "(λ x ⇒ [x] ∷ A ⊸ A) a = ([a ∷ A] ∷ A) (β)" $ testEq "(λ x. [x] ∷ A ⊸ A) a = ([a ∷ A] ∷ A) (β)" $
equalE empty equalE empty
(((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a") (((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
(E (FT "a" :# FT "A") :# FT "A"), (E (FT "a" :# FT "A") :# FT "A"),
testEq "(λ x ⇒ [x] ∷ A ⊸ A) a = a (βυ)" $ testEq "(λ x. [x] ∷ A ⊸ A) a = a (βυ)" $
equalE empty equalE empty
(((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a") (((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
(F "a"), (F "a"),
testEq "(λ g ⇒ [g [a]] ∷ ⋯)) [f] = (λ y ⇒ [f [y]] ∷ ⋯) [a] (β↘↙)" $ testEq "(λ g. [g [a]] ∷ ⋯)) [f] = (λ y. [f [y]] ∷ ⋯) [a] (β↘↙)" $
let a = FT "A"; a2a = (Arr One a a) in let a = FT "A"; a2a = (Arr One a a) in
equalE empty equalE empty
(((["g"] :\\ E (BV 0 :@ FT "a")) :# Arr One a2a a) :@ FT "f") (((["g"] :\\ E (BV 0 :@ FT "a")) :# Arr One a2a a) :@ FT "f")
(((["y"] :\\ E (F "f" :@ BVT 0)) :# a2a) :@ FT "a"), (((["y"] :\\ E (F "f" :@ BVT 0)) :# a2a) :@ FT "a"),
testEq "(λ x ⇒ [x] ∷ A ⊸ A) a <: a" $ testEq "(λ x. [x] ∷ A ⊸ A) a <: a" $
subE empty subE empty
(((["x"] :\\ BVT 0) :# (Arr One (FT "A") (FT "A"))) :@ FT "a") (((["x"] :\\ BVT 0) :# (Arr One (FT "A") (FT "A"))) :@ FT "a")
(F "a"), (F "a"),
note "id : A ⊸ A ≔ λ x ⇒ [x]", note "id : A ⊸ A ≔ λ x. [x]",
testEq "id [a] = a" $ equalE empty (F "id" :@ FT "a") (F "a"), testEq "id [a] = a" $ equalE empty (F "id" :@ FT "a") (F "a"),
testEq "id [a] <: a" $ subE empty (F "id" :@ FT "a") (F "a") testEq "id [a] <: a" $ subE empty (F "id" :@ FT "a") (F "a")
], ],
@ -340,13 +340,13 @@ tests = "equality & subtyping" :- [
todo "dim application", todo "dim application",
"annotation" :- [ "annotation" :- [
testEq "(λ x ⇒ f [x]) ∷ A ⊸ A = [f] ∷ A ⊸ A" $ testEq "(λ x. f [x]) ∷ A ⊸ A = [f] ∷ A ⊸ A" $
equalE empty equalE empty
((["x"] :\\ E (F "f" :@ BVT 0)) :# Arr One (FT "A") (FT "A")) ((["x"] :\\ E (F "f" :@ BVT 0)) :# Arr One (FT "A") (FT "A"))
(FT "f" :# Arr One (FT "A") (FT "A")), (FT "f" :# Arr One (FT "A") (FT "A")),
testEq "[f] ∷ A ⊸ A = f" $ testEq "[f] ∷ A ⊸ A = f" $
equalE empty (FT "f" :# Arr One (FT "A") (FT "A")) (F "f"), equalE empty (FT "f" :# Arr One (FT "A") (FT "A")) (F "f"),
testEq "(λ x ⇒ f [x]) ∷ A ⊸ A = f" $ testEq "(λ x. f [x]) ∷ A ⊸ A = f" $
equalE empty equalE empty
((["x"] :\\ E (F "f" :@ BVT 0)) :# Arr One (FT "A") (FT "A")) ((["x"] :\\ E (F "f" :@ BVT 0)) :# Arr One (FT "A") (FT "A"))
(F "f") (F "f")

85
tests/Tests/Typechecker.idr
View file

@ -207,31 +207,14 @@ tests = "typechecker" :- [
], ],
"enum types" :- [ "enum types" :- [
testTC "0 · {} ⇐ ★₀" $ check_ (ctx [<]) szero (enum []) (TYPE 0), testTC "0 · `{} ⇐ ★₀" $ check_ (ctx [<]) szero (enum []) (TYPE 0),
testTC "0 · {} ⇐ ★₃" $ check_ (ctx [<]) szero (enum []) (TYPE 3), testTC "0 · `{} ⇐ ★₃" $ check_ (ctx [<]) szero (enum []) (TYPE 3),
testTC "0 · {a,b,c} ⇐ ★₀" $ testTC "0 · `{a,b,c} ⇐ ★₀" $
check_ (ctx [<]) szero (enum ["a", "b", "c"]) (TYPE 0), check_ (ctx [<]) szero (enum ["a", "b", "c"]) (TYPE 0),
testTC "0 · {a,b,c} ⇐ ★₃" $ testTC "0 · `{a,b,c} ⇐ ★₃" $
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), check_ (ctx [<]) szero (enum ["a", "b", "c"]) (TYPE 3),
testTCFail "1 · {} ⇍ ★₀" $ check_ (ctx [<]) sone (enum []) (TYPE 0), testTCFail "1 · `{} ⇍ ★₀" $ check_ (ctx [<]) sone (enum []) (TYPE 0),
testTC "0=1 ⊢ 1 · {} ⇐ ★₀" $ check_ (ctx01 [<]) sone (enum []) (TYPE 0) testTC "0=1 ⊢ 1 · `{} ⇐ ★₀" $ check_ (ctx01 [<]) sone (enum []) (TYPE 0)
], ],
"free vars" :- [ "free vars" :- [
@ -246,7 +229,7 @@ tests = "typechecker" :- [
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
], ],
@ -265,21 +248,21 @@ tests = "typechecker" :- [
"lambda" :- [ "lambda" :- [
note "linear & unrestricted identity", note "linear & unrestricted identity",
testTC "1 · (λ x ⇒ x) ⇐ A ⊸ A" $ testTC "1 · (λ x. x) ⇐ A ⊸ A" $
check_ (ctx [<]) sone (["x"] :\\ BVT 0) (Arr One (FT "A") (FT "A")), check_ (ctx [<]) sone (["x"] :\\ BVT 0) (Arr One (FT "A") (FT "A")),
testTC "1 · (λ x ⇒ x) ⇐ A → A" $ testTC "1 · (λ x. x) ⇐ A → A" $
check_ (ctx [<]) sone (["x"] :\\ BVT 0) (Arr Any (FT "A") (FT "A")), check_ (ctx [<]) sone (["x"] :\\ BVT 0) (Arr Any (FT "A") (FT "A")),
note "(fail) zero binding used relevantly", note "(fail) zero binding used relevantly",
testTCFail "1 · (λ x ⇒ x) ⇍ A ⇾ A" $ testTCFail "1 · (λ x. x) ⇍ A ⇾ A" $
check_ (ctx [<]) sone (["x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")), check_ (ctx [<]) sone (["x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")),
note "(but ok in overall erased context)", note "(but ok in overall erased context)",
testTC "0 · (λ x ⇒ x) ⇐ A ⇾ A" $ testTC "0 · (λ x. x) ⇐ A ⇾ A" $
check_ (ctx [<]) szero (["x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")), check_ (ctx [<]) szero (["x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")),
testTC "1 · (λ A x ⇒ refl A x) ⇐ ⋯ # (type of refl)" $ testTC "1 · (λ A x. refl A x) ⇐ ⋯ # (type of refl)" $
check_ (ctx [<]) sone check_ (ctx [<]) sone
(["A", "x"] :\\ E (F "refl" :@@ [BVT 1, BVT 0])) (["A", "x"] :\\ E (F "refl" :@@ [BVT 1, BVT 0]))
reflTy, reflTy,
testTC "1 · (λ A x ⇒ δ i ⇒ x) ⇐ ⋯ # (def. and type of refl)" $ testTC "1 · (λ A x. δ i. x) ⇐ ⋯ # (def. and type of refl)" $
check_ (ctx [<]) sone reflDef reflTy check_ (ctx [<]) sone reflDef reflTy
], ],
@ -289,59 +272,59 @@ tests = "typechecker" :- [
testTC "x : A ⊢ 1 · (x, x) ⇐ A × A ⊳ ω·x" $ testTC "x : A ⊢ 1 · (x, x) ⇐ A × A ⊳ ω·x" $
checkQ (ctx [< FT "A"]) sone checkQ (ctx [< FT "A"]) sone
(Pair (BVT 0) (BVT 0)) (FT "A" `And` FT "A") [< Any], (Pair (BVT 0) (BVT 0)) (FT "A" `And` FT "A") [< Any],
testTC "1 · (a, δ i ⇒ a) ⇐ (x : A) × (x ≡ a)" $ testTC "1 · (a, δ i. a) ⇐ (x : A) × (x ≡ a)" $
check_ (ctx [<]) sone check_ (ctx [<]) sone
(Pair (FT "a") (["i"] :\\% FT "a")) (Pair (FT "a") (["i"] :\\% FT "a"))
(Sig_ "x" (FT "A") $ Eq0 (FT "A") (BVT 0) (FT "a")) (Sig_ "x" (FT "A") $ Eq0 (FT "A") (BVT 0) (FT "a"))
], ],
"unpairing" :- [ "unpairing" :- [
testTC "x : A × A ⊢ 1 · (case1 x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 1·x" $ 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 inferAsQ (ctx [< FT "A" `And` FT "A"]) sone
(CasePair One (BV 0) (SN $ FT "B") (CasePair One (BV 0) (SN $ FT "B")
(SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])) (SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0]))
(FT "B") [< One], (FT "B") [< One],
testTC "x : A × A ⊢ 1 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ ω·x" $ 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 inferAsQ (ctx [< FT "A" `And` FT "A"]) sone
(CasePair Any (BV 0) (SN $ FT "B") (CasePair Any (BV 0) (SN $ FT "B")
(SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])) (SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0]))
(FT "B") [< Any], (FT "B") [< Any],
testTC "x : A × A ⊢ 0 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 0·x" $ 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 inferAsQ (ctx [< FT "A" `And` FT "A"]) szero
(CasePair Any (BV 0) (SN $ FT "B") (CasePair Any (BV 0) (SN $ FT "B")
(SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])) (SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0]))
(FT "B") [< Zero], (FT "B") [< Zero],
testTCFail "x : A × A ⊢ 1 · (case0 x return B of (l,r) ⇒ f2 l r) ⇏" $ testTCFail "x : A × A ⊢ 1 · (case0 x return B of (l,r). f2 l r) ⇏" $
infer_ (ctx [< FT "A" `And` FT "A"]) sone infer_ (ctx [< FT "A" `And` FT "A"]) sone
(CasePair Zero (BV 0) (SN $ FT "B") (CasePair Zero (BV 0) (SN $ FT "B")
(SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])), (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" $ testTC "x : A × B ⊢ 1 · (caseω x return A of (l,r). l) ⇒ A ⊳ ω·x" $
inferAsQ (ctx [< FT "A" `And` FT "B"]) sone inferAsQ (ctx [< FT "A" `And` FT "B"]) sone
(CasePair Any (BV 0) (SN $ FT "A") (CasePair Any (BV 0) (SN $ FT "A")
(SY ["l", "r"] $ BVT 1)) (SY ["l", "r"] $ BVT 1))
(FT "A") [< Any], (FT "A") [< Any],
testTC "x : A × B ⊢ 0 · (case1 x return A of (l,r) ⇒ l) ⇒ A ⊳ 0·x" $ testTC "x : A × B ⊢ 0 · (case1 x return A of (l,r). l) ⇒ A ⊳ 0·x" $
inferAsQ (ctx [< FT "A" `And` FT "B"]) szero inferAsQ (ctx [< FT "A" `And` FT "B"]) szero
(CasePair One (BV 0) (SN $ FT "A") (CasePair One (BV 0) (SN $ FT "A")
(SY ["l", "r"] $ BVT 1)) (SY ["l", "r"] $ BVT 1))
(FT "A") [< Zero], (FT "A") [< Zero],
testTCFail "x : A × B ⊢ 1 · (case1 x return A of (l,r) ⇒ l) ⇏" $ testTCFail "x : A × B ⊢ 1 · (case1 x return A of (l,r). l) ⇏" $
infer_ (ctx [< FT "A" `And` FT "B"]) sone infer_ (ctx [< FT "A" `And` FT "B"]) sone
(CasePair One (BV 0) (SN $ FT "A") (CasePair One (BV 0) (SN $ FT "A")
(SY ["l", "r"] $ BVT 1)), (SY ["l", "r"] $ BVT 1)),
note "fst : (0·A : ★₁) → (0·B : A ↠ ★₁) → ((x : A) × B x) ↠ A", note "fst : (0·A : ★₁) → (0·B : A ↠ ★₁) → ((x : A) × B x) ↠ A",
note " ≔ (λ A B p ⇒ caseω p return A of (x, y) ⇒ x)", note " ≔ (λ A B p. caseω p return A of (x, y). x)",
testTC "0 · ‹type of fst› ⇐ ★₂" $ testTC "0 · ‹type of fst› ⇐ ★₂" $
check_ (ctx [<]) szero fstTy (TYPE 2), check_ (ctx [<]) szero fstTy (TYPE 2),
testTC "1 · ‹def of fst› ⇐ ‹type of fst›" $ testTC "1 · ‹def of fst› ⇐ ‹type of fst›" $
check_ (ctx [<]) sone fstDef fstTy, check_ (ctx [<]) sone fstDef fstTy,
note "snd : (0·A : ★₁) → (0·B : A ↠ ★₁) → (ω·p : (x : A) × B x) → B (fst A B p)", 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)", note " ≔ (λ A B p. caseω p return p. B (fst A B p) of (x, y). y)",
testTC "0 · ‹type of snd› ⇐ ★₂" $ testTC "0 · ‹type of snd› ⇐ ★₂" $
check_ (ctx [<]) szero sndTy (TYPE 2), check_ (ctx [<]) szero sndTy (TYPE 2),
testTC "1 · ‹def of snd› ⇐ ‹type of snd›" $ testTC "1 · ‹def of snd› ⇐ ‹type of snd›" $
check_ (ctx [<]) sone sndDef sndTy, check_ (ctx [<]) sone sndDef sndTy,
testTC "0 · snd ★₀ (λ x ⇒ x) ⇒ (ω·p : (A : ★₀) × A) → fst ★₀ (λ x ⇒ x) p" $ testTC "0 · snd ★₀ (λ x. x) ⇒ (ω·p : (A : ★₀) × A) → fst ★₀ (λ x. x) p" $
inferAs (ctx [<]) szero inferAs (ctx [<]) szero
(F "snd" :@@ [TYPE 0, ["x"] :\\ BVT 0]) (F "snd" :@@ [TYPE 0, ["x"] :\\ BVT 0])
(Pi_ Any "A" (Sig_ "A" (TYPE 0) $ BVT 0) $ (Pi_ Any "A" (Sig_ "A" (TYPE 0) $ BVT 0) $
@ -349,27 +332,27 @@ tests = "typechecker" :- [
], ],
"enums" :- [ "enums" :- [
testTC "1 · `a ⇐ {a}" $ testTC "1 · `a ⇐ `{a}" $
check_ (ctx [<]) sone (Tag "a") (enum ["a"]), check_ (ctx [<]) sone (Tag "a") (enum ["a"]),
testTC "1 · `a ⇐ {a, b, c}" $ testTC "1 · `a ⇐ `{a, b, c}" $
check_ (ctx [<]) sone (Tag "a") (enum ["a", "b", "c"]), check_ (ctx [<]) sone (Tag "a") (enum ["a", "b", "c"]),
testTCFail "1 · `a ⇍ {b, c}" $ testTCFail "1 · `a ⇍ `{b, c}" $
check_ (ctx [<]) sone (Tag "a") (enum ["b", "c"]), check_ (ctx [<]) sone (Tag "a") (enum ["b", "c"]),
testTC "0=1 ⊢ 1 · `a ⇐ {b, c}" $ testTC "0=1 ⊢ 1 · `a ⇐ `{b, c}" $
check_ (ctx01 [<]) sone (Tag "a") (enum ["b", "c"]) check_ (ctx01 [<]) sone (Tag "a") (enum ["b", "c"])
], ],
"equalities" :- [ "equalities" :- [
testTC "1 · (δ i ⇒ a) ⇐ a ≡ a" $ testTC "1 · (δ i. a) ⇐ a ≡ a" $
check_ (ctx [<]) sone (DLam $ SN $ FT "a") check_ (ctx [<]) sone (DLam $ SN $ FT "a")
(Eq0 (FT "A") (FT "a") (FT "a")), (Eq0 (FT "A") (FT "a") (FT "a")),
testTC "0 · (λ p q ⇒ δ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q" $ testTC "0 · (λ p q. δ i. p) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
check_ (ctx [<]) szero check_ (ctx [<]) szero
(["p","q"] :\\ ["i"] :\\% BVT 1) (["p","q"] :\\ ["i"] :\\% BVT 1)
(Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $ (Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $
Pi_ Any "q" (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)), Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0)),
testTC "0 · (λ p q ⇒ δ i ⇒ q) ⇐ (ω·p q : a ≡ a') → p ≡ q" $ testTC "0 · (λ p q. δ i. q) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
check_ (ctx [<]) szero check_ (ctx [<]) szero
(["p","q"] :\\ ["i"] :\\% BVT 0) (["p","q"] :\\ ["i"] :\\% BVT 0)
(Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $ (Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $
@ -380,8 +363,8 @@ tests = "typechecker" :- [
"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)))
@ -393,7 +376,7 @@ tests = "typechecker" :- [
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