quox/tests/Tests/Equal.idr
rhiannon morris 0514fff481 represent ℕ constants directly
instead of as huge `succ (succ (succ ⋯))` terms
2023-11-03 18:05:54 +01:00

630 lines
24 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 Control.Monad.ST
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 : Eff 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 : {default SOne sg : SQty} ->
Term d n -> Term d n -> Term d n -> Eff TC ()
subT ty s t {sg} = lift $ Term.sub noLoc ctx sg ty s t
equalT ty s t {sg} = lift $ Term.equal noLoc ctx sg ty s t
equalTy : Term d n -> Term d n -> Eff TC ()
equalTy s t = lift $ Term.equalType noLoc ctx s t
subE, equalE : {default SOne sg : SQty} ->
Elim d n -> Elim d n -> Eff TC ()
subE e f {sg} = lift $ Elim.sub noLoc ctx sg e f
equalE e f {sg} = lift $ Elim.equal noLoc ctx sg 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"#,
note "binds before ∥ are globals, after it are BVs",
"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 #"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 (^Nat 4) (^NAT))
(SN $ ^NAT)
(^Zero)
(SY [< "n", ^BN Unused] $ ^BVT 1))
(^Nat 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",
"box types" :- [
testEq "[1.A] = [1.A] : ★" $
equalT empty
(^TYPE 0)
(^BOX One (^FT "A" 0))
(^BOX One (^FT "A" 0)),
testNeq "[1.A] ≠ [ω.A] : ★" $
equalT empty
(^TYPE 0)
(^BOX One (^FT "A" 0))
(^BOX Any (^FT "A" 0)),
testNeq "[1.A] ≠ [1.B] : ★" $
equalT empty
(^TYPE 0)
(^BOX One (^FT "A" 0))
(^BOX One (^FT "B" 0)),
testNeq "[1.A] ≠ A : ★" $
equalT empty
(^TYPE 0)
(^BOX One (^FT "A" 0))
(^FT "A" 0),
testEq "0=1 ⊢ [1.A] = [1.B] : ★" $
equalT empty01
(^TYPE 0)
(^BOX One (^FT "A" 0))
(^BOX One (^FT "B" 0))
],
"boxes" :- [
testEq "[a] = [a] : [ω.A]" $
equalT empty
(^BOX Any (^FT "A" 0))
(^Box (^FT "a" 0))
(^Box (^FT "a" 0)),
testNeq "[a] ≠ [a'] : [ω.A]" $
equalT empty
(^BOX Any (^FT "A" 0))
(^Box (^FT "a" 0))
(^Box (^FT "a'" 0)),
testEq "ω.x : [ω.A] ⊢ x = [case1 b return A of {[y] ⇒ y}] : [ω.A]" $
equalT (ctx [< ("x", ^BOX Any (^FT "A" 0))])
(^BOX Any (^FT "A" 0))
(^BVT 0)
(^Box (E $ ^CaseBox One (^BV 0) (SN $ ^FT "A" 0) (SY [< "y"] (^BVT 0))))
],
"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"
]
]