quox/tests/Tests/Equal.idr

585 lines
22 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.Equal
import Quox.Equal
import Quox.Typechecker
import public TypingImpls
import TAP
import Quox.EffExtra
import AstExtra
defGlobals : Definitions
defGlobals = fromList
[("A", ^mkPostulate gzero (^TYPE 0)),
("B", ^mkPostulate gzero (^TYPE 0)),
("a", ^mkPostulate gany (^FT "A" 0)),
("a'", ^mkPostulate gany (^FT "A" 0)),
("b", ^mkPostulate gany (^FT "B" 0)),
("f", ^mkPostulate gany (^Arr One (^FT "A" 0) (^FT "A" 0))),
("id", ^mkDef gany (^Arr One (^FT "A" 0) (^FT "A" 0)) (^LamY "x" (^BVT 0))),
("eq-AB", ^mkPostulate gzero (^Eq0 (^TYPE 0) (^FT "A" 0) (^FT "B" 0))),
("two", ^mkDef gany (^Nat) (^Succ (^Succ (^Zero))))]
parameters (label : String) (act : Equal ())
{default defGlobals globals : Definitions}
testEq : Test
testEq = test label $ runEqual globals act
testNeq : Test
testNeq = testThrows label (const True) $ runTC globals act $> "()"
parameters (ctx : TyContext d n)
subT, equalT : Term d n -> Term d n -> Term d n -> TC ()
subT ty s t = lift $ Term.sub noLoc ctx ty s t
equalT ty s t = lift $ Term.equal noLoc ctx ty s t
equalTy : Term d n -> Term d n -> TC ()
equalTy s t = lift $ Term.equalType noLoc ctx s t
subE, equalE : Elim d n -> Elim d n -> TC ()
subE e f = lift $ Elim.sub noLoc ctx e f
equalE e f = lift $ Elim.equal noLoc ctx e f
export
tests : Test
tests = "equality & subtyping" :- [
note #""s{t,…}" for term substs; "sp,…›" for dim substs"#,
note #""0=1 ⊢ 𝒥" means that 𝒥 holds in an inconsistent dim context"#,
"universes" :- [
testEq "★₀ = ★₀" $
equalT empty (^TYPE 1) (^TYPE 0) (^TYPE 0),
testNeq "★₀ ≠ ★₁" $
equalT empty (^TYPE 2) (^TYPE 0) (^TYPE 1),
testNeq "★₁ ≠ ★₀" $
equalT empty (^TYPE 2) (^TYPE 1) (^TYPE 0),
testEq "★₀ <: ★₀" $
subT empty (^TYPE 1) (^TYPE 0) (^TYPE 0),
testEq "★₀ <: ★₁" $
subT empty (^TYPE 2) (^TYPE 0) (^TYPE 1),
testNeq "★₁ ≮: ★₀" $
subT empty (^TYPE 2) (^TYPE 1) (^TYPE 0)
],
"function types" :- [
note "cumulativity",
testEq "0.★₀ → ★₀ = 0.★₀ → ★₀" $
let tm = ^Arr Zero (^TYPE 0) (^TYPE 0) in
equalT empty (^TYPE 1) tm tm,
testEq "0.★₀ → ★₀ <: 0.★₀ → ★₀" $
let tm = ^Arr Zero (^TYPE 0) (^TYPE 0) in
subT empty (^TYPE 1) tm tm,
testNeq "0.★₁ → ★₀ ≠ 0.★₀ → ★₀" $
let tm1 = ^Arr Zero (^TYPE 1) (^TYPE 0)
tm2 = ^Arr Zero (^TYPE 0) (^TYPE 0) in
equalT empty (^TYPE 2) tm1 tm2,
testEq "1.★₁ → ★₀ <: 1.★₀ → ★₀" $
let tm1 = ^Arr One (^TYPE 1) (^TYPE 0)
tm2 = ^Arr One (^TYPE 0) (^TYPE 0) in
subT empty (^TYPE 2) tm1 tm2,
testEq "1.★₀ → ★₀ <: 1.★₀ → ★₁" $
let tm1 = ^Arr One (^TYPE 0) (^TYPE 0)
tm2 = ^Arr One (^TYPE 0) (^TYPE 1) in
subT empty (^TYPE 2) tm1 tm2,
testEq "1.★₀ → ★₀ <: 1.★₀ → ★₁" $
let tm1 = ^Arr One (^TYPE 0) (^TYPE 0)
tm2 = ^Arr One (^TYPE 0) (^TYPE 1) in
subT empty (^TYPE 2) tm1 tm2,
testEq "1.A → B = 1.A → B" $
let tm = ^Arr One (^FT "A" 0) (^FT "B" 0) in
equalT empty (^TYPE 0) tm tm,
testEq "1.A → B <: 1.A → B" $
let tm = ^Arr One (^FT "A" 0) (^FT "B" 0) in
subT empty (^TYPE 0) tm tm,
note "incompatible quantities",
testNeq "1.★₀ → ★₀ ≠ 0.★₀ → ★₁" $
let tm1 = ^Arr Zero (^TYPE 0) (^TYPE 0)
tm2 = ^Arr Zero (^TYPE 0) (^TYPE 1) in
equalT empty (^TYPE 2) tm1 tm2,
testNeq "0.A → B ≠ 1.A → B" $
let tm1 = ^Arr Zero (^FT "A" 0) (^FT "B" 0)
tm2 = ^Arr One (^FT "A" 0) (^FT "B" 0) in
equalT empty (^TYPE 0) tm1 tm2,
testNeq "0.A → B ≮: 1.A → B" $
let tm1 = ^Arr Zero (^FT "A" 0) (^FT "B" 0)
tm2 = ^Arr One (^FT "A" 0) (^FT "B" 0) in
subT empty (^TYPE 0) tm1 tm2,
testEq "0=1 ⊢ 0.A → B = 1.A → B" $
let tm1 = ^Arr Zero (^FT "A" 0) (^FT "B" 0)
tm2 = ^Arr One (^FT "A" 0) (^FT "B" 0) in
equalT empty01 (^TYPE 0) tm1 tm2,
todo "dependent function types"
],
"lambda" :- [
testEq "λ x ⇒ x = λ x ⇒ x" $
equalT empty (^Arr One (^FT "A" 0) (^FT "A" 0))
(^LamY "x" (^BVT 0))
(^LamY "x" (^BVT 0)),
testEq "λ x ⇒ x <: λ x ⇒ x" $
subT empty (^Arr One (^FT "A" 0) (^FT "A" 0))
(^LamY "x" (^BVT 0))
(^LamY "x" (^BVT 0)),
testEq "λ x ⇒ x = λ y ⇒ y" $
equalT empty (^Arr One (^FT "A" 0) (^FT "A" 0))
(^LamY "x" (^BVT 0))
(^LamY "y" (^BVT 0)),
testEq "λ x ⇒ x <: λ y ⇒ y" $
subT empty (^Arr One (^FT "A" 0) (^FT "A" 0))
(^LamY "x" (^BVT 0))
(^LamY "y" (^BVT 0)),
testNeq "λ x y ⇒ x ≠ λ x y ⇒ y" $
equalT empty
(^Arr One (^FT "A" 0) (^Arr One (^FT "A" 0) (^FT "A" 0)))
(^LamY "x" (^LamY "y" (^BVT 1)))
(^LamY "x" (^LamY "y" (^BVT 0))),
testEq "λ x ⇒ a = λ x ⇒ a (Y vs N)" $
equalT empty
(^Arr Zero (^FT "B" 0) (^FT "A" 0))
(^LamY "x" (^FT "a" 0))
(^LamN (^FT "a" 0)),
testEq "λ x ⇒ f x = f (η)" $
equalT empty
(^Arr One (^FT "A" 0) (^FT "A" 0))
(^LamY "x" (E $ ^App (^F "f" 0) (^BVT 0)))
(^FT "f" 0)
],
"eq type" :- [
testEq "(★₀ ≡ ★₀ : ★₁) = (★₀ ≡ ★₀ : ★₁)" $
let tm = ^Eq0 (^TYPE 1) (^TYPE 0) (^TYPE 0) in
equalT empty (^TYPE 2) tm tm,
testEq "A ≔ ★₁ ⊢ (★₀ ≡ ★₀ : ★₁) = (★₀ ≡ ★₀ : A)"
{globals = fromList [("A", ^mkDef gzero (^TYPE 2) (^TYPE 1))]} $
equalT empty (^TYPE 2)
(^Eq0 (^TYPE 1) (^TYPE 0) (^TYPE 0))
(^Eq0 (^FT "A" 0) (^TYPE 0) (^TYPE 0)),
todo "dependent equality types"
],
"equalities and uip" :-
let refl : Term d n -> Term d n -> Elim d n
refl a x = ^Ann (^DLam (SN x)) (^Eq0 a x x)
in
[
note "binds before ∥ are globals, after it are BVs",
note #"refl A x is an abbreviation for "(δ i ⇒ x)(x ≡ x : A)""#,
testEq "refl A a = refl A a" $
equalE empty
(refl (^FT "A" 0) (^FT "a" 0))
(refl (^FT "A" 0) (^FT "a" 0)),
testEq "p : (a ≡ a' : A), q : (a ≡ a' : A) ∥ ⊢ p = q (free)"
{globals =
let def = ^mkPostulate gzero
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0))
in defGlobals `mergeLeft` fromList [("p", def), ("q", def)]} $
equalE empty (^F "p" 0) (^F "q" 0),
testEq "∥ x : (a ≡ a' : A), y : (a ≡ a' : A) ⊢ x = y (bound)" $
let ty : forall n. Term 0 n :=
^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0) in
equalE (extendTyN [< (Any, "x", ty), (Any, "y", ty)] empty)
(^BV 0) (^BV 1),
testEq "∥ x : (a ≡ a' : A) ∷ Type 0, y : [ditto] ⊢ x = y" $
let ty : forall n. Term 0 n :=
E $ ^Ann (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0)) (^TYPE 0) in
equalE (extendTyN [< (Any, "x", ty), (Any, "y", ty)] empty)
(^BV 0) (^BV 1),
testEq "E ≔ a ≡ a' : A, EE ≔ E ∥ x : EE, y : EE ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList
[("E", ^mkDef gzero (^TYPE 0)
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0))),
("EE", ^mkDef gzero (^TYPE 0) (^FT "E" 0))]} $
equalE
(extendTyN [< (Any, "x", ^FT "EE" 0), (Any, "y", ^FT "EE" 0)] empty)
(^BV 0) (^BV 1),
testEq "E ≔ a ≡ a' : A, EE ≔ E ∥ x : EE, y : E ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList
[("E", ^mkDef gzero (^TYPE 0)
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0))),
("EE", ^mkDef gzero (^TYPE 0) (^FT "E" 0))]} $
equalE
(extendTyN [< (Any, "x", ^FT "EE" 0), (Any, "y", ^FT "E" 0)] empty)
(^BV 0) (^BV 1),
testEq "E ≔ a ≡ a' : A ∥ x : E, y : E ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList
[("E", ^mkDef gzero (^TYPE 0)
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0)))]} $
equalE (extendTyN [< (Any, "x", ^FT "E" 0), (Any, "y", ^FT "E" 0)] empty)
(^BV 0) (^BV 1),
testEq "E ≔ a ≡ a' : A ∥ x : (E×E), y : (E×E) ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList
[("E", ^mkDef gzero (^TYPE 0)
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0)))]} $
let ty : forall n. Term 0 n := ^Sig (^FT "E" 0) (SN $ ^FT "E" 0) in
equalE (extendTyN [< (Any, "x", ty), (Any, "y", ty)] empty)
(^BV 0) (^BV 1),
testEq "E ≔ a ≡ a' : A, W ≔ E × E ∥ x : W, y : E×E ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList
[("E", ^mkDef gzero (^TYPE 0)
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0))),
("W", ^mkDef gzero (^TYPE 0) (^And (^FT "E" 0) (^FT "E" 0)))]} $
equalE
(extendTyN [< (Any, "x", ^FT "W" 0),
(Any, "y", ^And (^FT "E" 0) (^FT "E" 0))] empty)
(^BV 0) (^BV 1)
],
"term closure" :- [
note "bold numbers for de bruijn indices",
testEq "𝟎{} = 𝟎 : A" $
equalT (extendTy Any "x" (^FT "A" 0) empty)
(^FT "A" 0)
(CloT (Sub (^BVT 0) id))
(^BVT 0),
testEq "𝟎{a} = a : A" $
equalT empty (^FT "A" 0)
(CloT (Sub (^BVT 0) (^F "a" 0 ::: id)))
(^FT "a" 0),
testEq "𝟎{a,b} = a : A" $
equalT empty (^FT "A" 0)
(CloT (Sub (^BVT 0) (^F "a" 0 ::: ^F "b" 0 ::: id)))
(^FT "a" 0),
testEq "𝟏{a,b} = b : A" $
equalT empty (^FT "A" 0)
(CloT (Sub (^BVT 1) (^F "a" 0 ::: ^F "b" 0 ::: id)))
(^FT "b" 0),
testEq "(λy ⇒ 𝟏){a} = λy ⇒ a : 0.B → A (N)" $
equalT empty (^Arr Zero (^FT "B" 0) (^FT "A" 0))
(CloT (Sub (^LamN (^BVT 0)) (^F "a" 0 ::: id)))
(^LamN (^FT "a" 0)),
testEq "(λy ⇒ 𝟏){a} = λy ⇒ a : 0.B → A (Y)" $
equalT empty (^Arr Zero (^FT "B" 0) (^FT "A" 0))
(CloT (Sub (^LamY "y" (^BVT 1)) (^F "a" 0 ::: id)))
(^LamY "y" (^FT "a" 0))
],
"term d-closure" :- [
testEq "★₀0 = ★₀ : ★₁" $
equalT (extendDim "𝑗" empty)
(^TYPE 1) (DCloT (Sub (^TYPE 0) (^K Zero ::: id))) (^TYPE 0),
testEq "(δ i ⇒ a)0 = (δ i ⇒ a) : (a ≡ a : A)" $
equalT (extendDim "𝑗" empty)
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0))
(DCloT (Sub (^DLamN (^FT "a" 0)) (^K Zero ::: id)))
(^DLamN (^FT "a" 0)),
note "it is hard to think of well-typed terms with big dctxs"
],
"free var" :-
let au_bu = fromList
[("A", ^mkDef gany (^TYPE 1) (^TYPE 0)),
("B", ^mkDef gany (^TYPE 1) (^TYPE 0))]
au_ba = fromList
[("A", ^mkDef gany (^TYPE 1) (^TYPE 0)),
("B", ^mkDef gany (^TYPE 1) (^FT "A" 0))]
in [
testEq "A = A" $
equalE empty (^F "A" 0) (^F "A" 0),
testNeq "A ≠ B" $
equalE empty (^F "A" 0) (^F "B" 0),
testEq "0=1 ⊢ A = B" $
equalE empty01 (^F "A" 0) (^F "B" 0),
testEq "A : ★₁ ≔ ★₀ ⊢ A = (★₀ ∷ ★₁)" {globals = au_bu} $
equalE empty (^F "A" 0) (^Ann (^TYPE 0) (^TYPE 1)),
testEq "A : ★₁ ≔ ★₀ ⊢ A = ★₀" {globals = au_bu} $
equalT empty (^TYPE 1) (^FT "A" 0) (^TYPE 0),
testEq "A ≔ ★₀, B ≔ ★₀ ⊢ A = B" {globals = au_bu} $
equalE empty (^F "A" 0) (^F "B" 0),
testEq "A ≔ ★₀, B ≔ A ⊢ A = B" {globals = au_ba} $
equalE empty (^F "A" 0) (^F "B" 0),
testEq "A <: A" $
subE empty (^F "A" 0) (^F "A" 0),
testNeq "A ≮: B" $
subE empty (^F "A" 0) (^F "B" 0),
testEq "A : ★₃ ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: B"
{globals = fromList [("A", ^mkDef gany (^TYPE 3) (^TYPE 0)),
("B", ^mkDef gany (^TYPE 3) (^TYPE 2))]} $
subE empty (^F "A" 0) (^F "B" 0),
note "(A and B in different universes)",
testEq "A : ★₁ ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: B"
{globals = fromList [("A", ^mkDef gany (^TYPE 1) (^TYPE 0)),
("B", ^mkDef gany (^TYPE 3) (^TYPE 2))]} $
subE empty (^F "A" 0) (^F "B" 0),
testEq "0=1 ⊢ A <: B" $
subE empty01 (^F "A" 0) (^F "B" 0)
],
"bound var" :- [
note "bold numbers for de bruijn indices",
testEq "𝟎 = 𝟎" $
equalE (extendTy Any "A" (^TYPE 0) empty) (^BV 0) (^BV 0),
testEq "𝟎 <: 𝟎" $
subE (extendTy Any "A" (^TYPE 0) empty) (^BV 0) (^BV 0),
testNeq "𝟎𝟏" $
equalE (extendTyN [< (Any, "A", ^TYPE 0), (Any, "B", ^TYPE 0)] empty)
(^BV 0) (^BV 1),
testNeq "𝟎 ≮: 𝟏" $
subE (extendTyN [< (Any, "A", ^TYPE 0), (Any, "B", ^TYPE 0)] empty)
(^BV 0) (^BV 1),
testEq "0=1 ⊢ 𝟎 = 𝟏" $
equalE (extendTyN [< (Any, "A", ^TYPE 0), (Any, "B", ^TYPE 0)] empty01)
(^BV 0) (^BV 1)
],
"application" :- [
testEq "f a = f a" $
equalE empty (^App (^F "f" 0) (^FT "a" 0)) (^App (^F "f" 0) (^FT "a" 0)),
testEq "f a <: f a" $
subE empty (^App (^F "f" 0) (^FT "a" 0)) (^App (^F "f" 0) (^FT "a" 0)),
testEq "(λ x ⇒ x ∷ 1.A → A) a = ((a ∷ A) ∷ A) (β)" $
equalE empty
(^App (^Ann (^LamY "x" (^BVT 0)) (^Arr One (^FT "A" 0) (^FT "A" 0)))
(^FT "a" 0))
(^Ann (E $ ^Ann (^FT "a" 0) (^FT "A" 0)) (^FT "A" 0)),
testEq "(λ x ⇒ x ∷ A ⊸ A) a = a (βυ)" $
equalE empty
(^App (^Ann (^LamY "x" (^BVT 0)) (^Arr One (^FT "A" 0) (^FT "A" 0)))
(^FT "a" 0))
(^F "a" 0),
testEq "((λ g ⇒ g a) ∷ 1.(1.A → A) → A) f = ((λ y ⇒ f y) ∷ 1.A → A) a # β↘↙" $
let a = ^FT "A" 0; a2a = ^Arr One a a; aa2a = ^Arr One a2a a in
equalE empty
(^App (^Ann (^LamY "g" (E $ ^App (^BV 0) (^FT "a" 0))) aa2a)
(^FT "f" 0))
(^App (^Ann (^LamY "y" (E $ ^App (^F "f" 0) (^BVT 0))) a2a)
(^FT "a" 0)),
testEq "((λ x ⇒ x) ∷ 1.A → A) a <: a" $
subE empty
(^App (^Ann (^LamY "x" (^BVT 0)) (^Arr One (^FT "A" 0) (^FT "A" 0)))
(^FT "a" 0))
(^F "a" 0),
note "id : A ⊸ A ≔ λ x ⇒ x",
testEq "id a = a" $ equalE empty (^App (^F "id" 0) (^FT "a" 0)) (^F "a" 0),
testEq "id a <: a" $ subE empty (^App (^F "id" 0) (^FT "a" 0)) (^F "a" 0)
],
"dim application" :- [
testEq "eq-AB @0 = eq-AB @0" $
equalE empty
(^DApp (^F "eq-AB" 0) (^K Zero))
(^DApp (^F "eq-AB" 0) (^K Zero)),
testNeq "eq-AB @0 ≠ eq-AB @1" $
equalE empty
(^DApp (^F "eq-AB" 0) (^K Zero))
(^DApp (^F "eq-AB" 0) (^K One)),
testEq "𝑖 | ⊢ eq-AB @𝑖 = eq-AB @𝑖" $
equalE
(extendDim "𝑖" empty)
(^DApp (^F "eq-AB" 0) (^BV 0))
(^DApp (^F "eq-AB" 0) (^BV 0)),
testNeq "𝑖 | ⊢ eq-AB @𝑖 ≠ eq-AB @0" $
equalE (extendDim "𝑖" empty)
(^DApp (^F "eq-AB" 0) (^BV 0))
(^DApp (^F "eq-AB" 0) (^K Zero)),
testEq "𝑖, 𝑖=0 | ⊢ eq-AB @𝑖 = eq-AB @0" $
equalE (eqDim (^BV 0) (^K Zero) $ extendDim "𝑖" empty)
(^DApp (^F "eq-AB" 0) (^BV 0))
(^DApp (^F "eq-AB" 0) (^K Zero)),
testNeq "𝑖, 𝑖=1 | ⊢ eq-AB @𝑖 ≠ eq-AB @0" $
equalE (eqDim (^BV 0) (^K One) $ extendDim "𝑖" empty)
(^DApp (^F "eq-AB" 0) (^BV 0))
(^DApp (^F "eq-AB" 0) (^K Zero)),
testNeq "𝑖, 𝑗 | ⊢ eq-AB @𝑖 ≠ eq-AB @𝑗" $
equalE (extendDim "𝑗" $ extendDim "𝑖" empty)
(^DApp (^F "eq-AB" 0) (^BV 1))
(^DApp (^F "eq-AB" 0) (^BV 0)),
testEq "𝑖, 𝑗, 𝑖=𝑗 | ⊢ eq-AB @𝑖 = eq-AB @𝑗" $
equalE (eqDim (^BV 0) (^BV 1) $ extendDim "𝑗" $ extendDim "𝑖" empty)
(^DApp (^F "eq-AB" 0) (^BV 1))
(^DApp (^F "eq-AB" 0) (^BV 0)),
testEq "𝑖, 𝑗, 𝑖=0, 𝑗=0 | ⊢ eq-AB @𝑖 = eq-AB @𝑗" $
equalE
(eqDim (^BV 0) (^K Zero) $ eqDim (^BV 1) (^K Zero) $
extendDim "𝑗" $ extendDim "𝑖" empty)
(^DApp (^F "eq-AB" 0) (^BV 1))
(^DApp (^F "eq-AB" 0) (^BV 0)),
testEq "0=1 | ⊢ eq-AB @𝑖 = eq-AB @𝑗" $
equalE (extendDim "𝑗" $ extendDim "𝑖" empty01)
(^DApp (^F "eq-AB" 0) (^BV 1))
(^DApp (^F "eq-AB" 0) (^BV 0)),
testEq "eq-AB @0 = A" $
equalE empty (^DApp (^F "eq-AB" 0) (^K Zero)) (^F "A" 0),
testEq "eq-AB @1 = B" $
equalE empty (^DApp (^F "eq-AB" 0) (^K One)) (^F "B" 0),
testEq "((δ i ⇒ a) ∷ a ≡ a : A) @0 = a" $
equalE empty
(^DApp (^Ann (^DLamN (^FT "a" 0))
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0)))
(^K Zero))
(^F "a" 0),
testEq "((δ i ⇒ a) ∷ a ≡ a : A) @0 = ((δ i ⇒ a) ∷ a ≡ a : A) @1" $
equalE empty
(^DApp (^Ann (^DLamN (^FT "a" 0))
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0)))
(^K Zero))
(^DApp (^Ann (^DLamN (^FT "a" 0))
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0)))
(^K One))
],
"annotation" :- [
testEq "(λ x ⇒ f x) ∷ 1.A → A = f ∷ 1.A → A" $
equalE empty
(^Ann (^LamY "x" (E $ ^App (^F "f" 0) (^BVT 0)))
(^Arr One (^FT "A" 0) (^FT "A" 0)))
(^Ann (^FT "f" 0) (^Arr One (^FT "A" 0) (^FT "A" 0))),
testEq "f ∷ 1.A → A = f" $
equalE empty
(^Ann (^FT "f" 0) (^Arr One (^FT "A" 0) (^FT "A" 0)))
(^F "f" 0),
testEq "(λ x ⇒ f x) ∷ 1.A → A = f" $
equalE empty
(^Ann (^LamY "x" (E $ ^App (^F "f" 0) (^BVT 0)))
(^Arr One (^FT "A" 0) (^FT "A" 0)))
(^F "f" 0)
],
"natural type" :- [
testEq " = " $ equalTy empty (^Nat) (^Nat),
testEq " = : ★₀" $ equalT empty (^TYPE 0) (^Nat) (^Nat),
testEq " = : ★₆₉" $ equalT empty (^TYPE 69) (^Nat) (^Nat),
testNeq " ≠ {}" $ equalTy empty (^Nat) (^enum []),
testEq "0=1 ⊢ = {}" $ equalTy empty01 (^Nat) (^enum [])
],
"natural numbers" :- [
testEq "0 = 0" $ equalT empty (^Nat) (^Zero) (^Zero),
testEq "succ two = succ two" $
equalT empty (^Nat) (^Succ (^FT "two" 0)) (^Succ (^FT "two" 0)),
testNeq "succ two ≠ two" $
equalT empty (^Nat) (^Succ (^FT "two" 0)) (^FT "two" 0),
testNeq "0 ≠ 1" $
equalT empty (^Nat) (^Zero) (^Succ (^Zero)),
testEq "0=1 ⊢ 0 = 1" $
equalT empty01 (^Nat) (^Zero) (^Succ (^Zero))
],
"natural elim" :- [
testEq "caseω 0 return {a,b} of {zero ⇒ 'a; succ _ ⇒ 'b} = 'a" $
equalT empty
(^enum ["a", "b"])
(E $ ^CaseNat Any Zero (^Ann (^Zero) (^Nat))
(SN $ ^enum ["a", "b"])
(^Tag "a")
(SN $ ^Tag "b"))
(^Tag "a"),
testEq "caseω 1 return {a,b} of {zero ⇒ 'a; succ _ ⇒ 'b} = 'b" $
equalT empty
(^enum ["a", "b"])
(E $ ^CaseNat Any Zero (^Ann (^Succ (^Zero)) (^Nat))
(SN $ ^enum ["a", "b"])
(^Tag "a")
(SN $ ^Tag "b"))
(^Tag "b"),
testEq "caseω 4 return of {0 ⇒ 0; succ n ⇒ n} = 3" $
equalT empty
(^Nat)
(E $ ^CaseNat Any Zero (^Ann (^makeNat 4) (^Nat))
(SN $ ^Nat)
(^Zero)
(SY [< "n", ^BN Unused] $ ^BVT 1))
(^makeNat 3)
],
todo "pair types",
"pairs" :- [
testEq "('a, 'b) = ('a, 'b) : {a} × {b}" $
equalT empty
(^And (^enum ["a"]) (^enum ["b"]))
(^Pair (^Tag "a") (^Tag "b"))
(^Pair (^Tag "a") (^Tag "b")),
testNeq "('a, 'b) ≠ ('b, 'a) : {a,b} × {a,b}" $
equalT empty
(^And (^enum ["a", "b"]) (^enum ["a", "b"]))
(^Pair (^Tag "a") (^Tag "b"))
(^Pair (^Tag "b") (^Tag "a")),
testEq "0=1 ⊢ ('a, 'b) = ('b, 'a) : {a,b} × {a,b}" $
equalT empty01
(^And (^enum ["a", "b"]) (^enum ["a", "b"]))
(^Pair (^Tag "a") (^Tag "b"))
(^Pair (^Tag "b") (^Tag "a")),
testEq "0=1 ⊢ ('a, 'b) = ('b, 'a) : " $
equalT empty01
(^Nat)
(^Pair (^Tag "a") (^Tag "b"))
(^Pair (^Tag "b") (^Tag "a"))
],
todo "pair elim",
todo "enum types",
todo "enum",
todo "enum elim",
todo "box types",
todo "boxes",
todo "box elim",
"elim closure" :- [
note "bold numbers for de bruijn indices",
testEq "𝟎{a} = a" $
equalE empty (CloE (Sub (^BV 0) (^F "a" 0 ::: id))) (^F "a" 0),
testEq "𝟏{a} = 𝟎" $
equalE (extendTy Any "x" (^FT "A" 0) empty)
(CloE (Sub (^BV 1) (^F "a" 0 ::: id))) (^BV 0)
],
"elim d-closure" :- [
note "bold numbers for de bruijn indices",
note "0·eq-AB : (A ≡ B : ★₀)",
testEq "(eq-AB @𝟎)0 = eq-AB @0" $
equalE empty
(DCloE (Sub (^DApp (^F "eq-AB" 0) (^BV 0)) (^K Zero ::: id)))
(^DApp (^F "eq-AB" 0) (^K Zero)),
testEq "(eq-AB @𝟎)0 = A" $
equalE empty
(DCloE (Sub (^DApp (^F "eq-AB" 0) (^BV 0)) (^K Zero ::: id)))
(^F "A" 0),
testEq "(eq-AB @𝟎)1 = B" $
equalE empty
(DCloE (Sub (^DApp (^F "eq-AB" 0) (^BV 0)) (^K One ::: id)))
(^F "B" 0),
testNeq "(eq-AB @𝟎)1 ≠ A" $
equalE empty
(DCloE (Sub (^DApp (^F "eq-AB" 0) (^BV 0)) (^K One ::: id)))
(^F "A" 0),
testEq "(eq-AB @𝟎)𝟎,0 = (eq-AB 𝟎)" $
equalE (extendDim "𝑖" empty)
(DCloE (Sub (^DApp (^F "eq-AB" 0) (^BV 0)) (^BV 0 ::: ^K Zero ::: id)))
(^DApp (^F "eq-AB" 0) (^BV 0)),
testNeq "(eq-AB 𝟎)0 ≠ (eq-AB 0)" $
equalE (extendDim "𝑖" empty)
(DCloE (Sub (^DApp (^F "eq-AB" 0) (^BV 0)) (^BV 0 ::: ^K Zero ::: id)))
(^DApp (^F "eq-AB" 0) (^K Zero)),
testEq "𝟎0 = 𝟎 # term and dim vars distinct" $
equalE
(extendTy Any "x" (^FT "A" 0) empty)
(DCloE (Sub (^BV 0) (^K Zero ::: id))) (^BV 0),
testEq "a0 = a" $
equalE empty
(DCloE (Sub (^F "a" 0) (^K Zero ::: id))) (^F "a" 0),
testEq "(f a)0 = f0 a0" $
let th = ^K Zero ::: id in
equalE empty
(DCloE (Sub (^App (^F "f" 0) (^FT "a" 0)) th))
(^App (DCloE (Sub (^F "f" 0) th)) (DCloT (Sub (^FT "a" 0) th)))
],
"clashes" :- [
testNeq "★₀ ≠ 0.★₀ → ★₀" $
equalT empty (^TYPE 1) (^TYPE 0) (^Arr Zero (^TYPE 0) (^TYPE 0)),
testEq "0=1 ⊢ ★₀ = 0.★₀ → ★₀" $
equalT empty01 (^TYPE 1) (^TYPE 0) (^Arr Zero (^TYPE 0) (^TYPE 0)),
todo "others"
]
]