quox/tests/Tests/Equal.idr
2023-03-31 19:26:24 +02:00

564 lines
21 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.Syntax.Qty.Three
import public TypingImpls
import TAP
0 M : Type -> Type
M = ReaderT (Definitions Three) (Either (Error Three))
defGlobals : Definitions Three
defGlobals = fromList
[("A", mkPostulate Zero $ TYPE 0),
("B", mkPostulate Zero $ 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")),
("id", mkDef Any (Arr One (FT "A") (FT "A")) ([< "x"] :\\ BVT 0)),
("eq-AB", mkPostulate Zero $ Eq0 (TYPE 0) (FT "A") (FT "B")),
("two", mkDef Any Nat (Succ (Succ Zero)))]
parameters (label : String) (act : Lazy (M ()))
{default defGlobals globals : Definitions Three}
testEq : Test
testEq = test label $ runReaderT globals act
testNeq : Test
testNeq = testThrows label (const True) $ runReaderT globals act $> "()"
parameters (0 d : Nat) (ctx : TyContext Three d n)
subTD, equalTD : Term Three d n -> Term Three d n -> Term Three d n -> M ()
subTD ty s t = Term.sub ctx ty s t
equalTD ty s t = Term.equal ctx ty s t
equalTyD : Term Three d n -> Term Three d n -> M ()
equalTyD s t = Term.equalType ctx s t
subED, equalED : Elim Three d n -> Elim Three d n -> M ()
subED e f = Elim.sub ctx e f
equalED e f = Elim.equal ctx e f
parameters (ctx : TyContext Three 0 n)
subT, equalT : Term Three 0 n -> Term Three 0 n -> Term Three 0 n -> M ()
subT = subTD 0 ctx
equalT = equalTD 0 ctx
equalTy : Term Three 0 n -> Term Three 0 n -> M ()
equalTy = equalTyD 0 ctx
subE, equalE : Elim Three 0 n -> Elim Three 0 n -> M ()
subE = subED 0 ctx
equalE = equalED 0 ctx
empty01 : TyContext q 0 0
empty01 = eqDim (K Zero) (K One) empty
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 #""𝐴𝐵" for (1·𝐴)𝐵"#,
note #""𝐴𝐵" for (0·𝐴)𝐵"#,
testEq "★₀ ⇾ ★₀ = ★₀ ⇾ ★₀" $
let tm = Arr Zero (TYPE 0) (TYPE 0) in
equalT empty (TYPE 1) tm tm,
testEq "★₀ ⇾ ★₀ <: ★₀ ⇾ ★₀" $
let tm = Arr Zero (TYPE 0) (TYPE 0) in
subT empty (TYPE 1) tm tm,
testNeq "★₁ ⊸ ★₀ ≠ ★₀ ⇾ ★₀" $
let tm1 = Arr Zero (TYPE 1) (TYPE 0)
tm2 = Arr Zero (TYPE 0) (TYPE 0) in
equalT empty (TYPE 2) tm1 tm2,
testEq "★₁ ⊸ ★₀ <: ★₀ ⊸ ★₀" $
let tm1 = Arr One (TYPE 1) (TYPE 0)
tm2 = Arr One (TYPE 0) (TYPE 0) in
subT empty (TYPE 2) tm1 tm2,
testEq "★₀ ⊸ ★₀ <: ★₀ ⊸ ★₁" $
let tm1 = Arr One (TYPE 0) (TYPE 0)
tm2 = Arr One (TYPE 0) (TYPE 1) in
subT empty (TYPE 2) tm1 tm2,
testEq "★₀ ⊸ ★₀ <: ★₀ ⊸ ★₁" $
let tm1 = Arr One (TYPE 0) (TYPE 0)
tm2 = Arr One (TYPE 0) (TYPE 1) in
subT empty (TYPE 2) tm1 tm2,
testEq "A ⊸ B = A ⊸ B" $
let tm = Arr One (FT "A") (FT "B") in
equalT empty (TYPE 0) tm tm,
testEq "A ⊸ B <: A ⊸ B" $
let tm = Arr One (FT "A") (FT "B") in
subT empty (TYPE 0) tm tm,
note "incompatible quantities",
testNeq "★₀ ⊸ ★₀ ≠ ★₀ ⇾ ★₁" $
let tm1 = Arr Zero (TYPE 0) (TYPE 0)
tm2 = Arr Zero (TYPE 0) (TYPE 1) in
equalT empty (TYPE 2) tm1 tm2,
testNeq "A ⇾ B ≠ A ⊸ B" $
let tm1 = Arr Zero (FT "A") (FT "B")
tm2 = Arr One (FT "A") (FT "B") in
equalT empty (TYPE 0) tm1 tm2,
testNeq "A ⇾ B ≮: A ⊸ B" $
let tm1 = Arr Zero (FT "A") (FT "B")
tm2 = Arr One (FT "A") (FT "B") in
subT empty (TYPE 0) tm1 tm2,
testEq "0=1 ⊢ A ⇾ B = A ⊸ B" $
let tm1 = Arr Zero (FT "A") (FT "B")
tm2 = Arr One (FT "A") (FT "B") in
equalT empty01 (TYPE 0) tm1 tm2,
todo "dependent function types",
note "[todo] should π ≤ ρ ⊢ (ρ·A) → B <: (π·A) → B?"
],
"lambda" :- [
testEq "λ x ⇒ [x] = λ x ⇒ [x]" $
equalT empty (Arr One (FT "A") (FT "A"))
([< "x"] :\\ BVT 0)
([< "x"] :\\ BVT 0),
testEq "λ x ⇒ [x] <: λ x ⇒ [x]" $
subT empty (Arr One (FT "A") (FT "A"))
([< "x"] :\\ BVT 0)
([< "x"] :\\ BVT 0),
testEq "λ x ⇒ [x] = λ y ⇒ [y]" $
equalT empty (Arr One (FT "A") (FT "A"))
([< "x"] :\\ BVT 0)
([< "y"] :\\ BVT 0),
testEq "λ x ⇒ [x] <: λ y ⇒ [y]" $
equalT empty (Arr One (FT "A") (FT "A"))
([< "x"] :\\ BVT 0)
([< "y"] :\\ BVT 0),
testNeq "λ x y ⇒ [x] ≠ λ x y ⇒ [y]" $
equalT empty (Arr One (FT "A") $ Arr One (FT "A") (FT "A"))
([< "x", "y"] :\\ BVT 1)
([< "x", "y"] :\\ BVT 0),
testEq "λ x ⇒ [a] = λ x ⇒ [a] (Y vs N)" $
equalT empty (Arr Zero (FT "B") (FT "A"))
(Lam $ SY [< "x"] $ FT "a")
(Lam $ SN $ FT "a"),
testEq "λ x ⇒ [f [x]] = [f] (η)" $
equalT empty (Arr One (FT "A") (FT "A"))
([< "x"] :\\ E (F "f" :@ BVT 0))
(FT "f")
],
"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 zero (TYPE 2) (TYPE 1))]} $
equalT empty (TYPE 2)
(Eq0 (TYPE 1) (TYPE 0) (TYPE 0))
(Eq0 (FT "A") (TYPE 0) (TYPE 0)),
todo "dependent equality types"
],
"equalities and uip" :-
let refl : Term q d n -> Term q d n -> Elim q d n
refl a x = (DLam $ S [< "_"] $ N x) :# (Eq0 a x x)
in
[
note #""refl [A] x" is an abbreviation for "(δ i ⇒ x)(x ≡ x : A)""#,
note "binds before ∥ are globals, after it are BVs",
testEq "refl [A] a = refl [A] a" $
equalE empty (refl (FT "A") (FT "a")) (refl (FT "A") (FT "a")),
testEq "p : (a ≡ a' : A), q : (a ≡ a' : A) ∥ ⊢ p = q (free)"
{globals =
let def = mkPostulate Zero $ Eq0 (FT "A") (FT "a") (FT "a'") in
defGlobals `mergeLeft` fromList [("p", def), ("q", def)]} $
equalE empty (F "p") (F "q"),
testEq "∥ x : (a ≡ a' : A), y : (a ≡ a' : A) ⊢ x = y (bound)" $
let ty : forall n. Term Three 0 n := Eq0 (FT "A") (FT "a") (FT "a'") 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 Three 0 n :=
E (Eq0 (FT "A") (FT "a") (FT "a'") :# 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 zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))),
("EE", mkDef zero (TYPE 0) (FT "E"))]} $
equalE (extendTyN [< (Any, "x", FT "EE"), (Any, "y", FT "EE")] empty)
(BV 0) (BV 1),
testEq "E ≔ a ≡ a' : A, EE ≔ E ∥ x : EE, y : E ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList
[("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))),
("EE", mkDef zero (TYPE 0) (FT "E"))]} $
equalE (extendTyN [< (Any, "x", FT "EE"), (Any, "y", FT "E")] empty)
(BV 0) (BV 1),
testEq "E ≔ a ≡ a' : A ∥ x : E, y : E ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList
[("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'")))]} $
equalE (extendTyN [< (Any, "x", FT "E"), (Any, "y", FT "E")] empty)
(BV 0) (BV 1),
testEq "E ≔ a ≡ a' : A ∥ x : (E×E), y : (E×E) ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList
[("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'")))]} $
let ty : forall n. Term Three 0 n :=
Sig (FT "E") $ S [< "_"] $ N $ FT "E" 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 : W ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList
[("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))),
("W", mkDef zero (TYPE 0) (FT "E" `And` FT "E"))]} $
equalE
(extendTyN [< (Any, "x", FT "W"), (Any, "y", FT "W")] empty)
(BV 0) (BV 1)
],
"term closure" :- [
testEq "[#0]{} = [#0] : A" $
equalT (extendTy Any "x" (FT "A") empty)
(FT "A")
(CloT (BVT 0) id)
(BVT 0),
testEq "[#0]{a} = [a] : A" $
equalT empty (FT "A")
(CloT (BVT 0) (F "a" ::: id))
(FT "a"),
testEq "[#0]{a,b} = [a] : A" $
equalT empty (FT "A")
(CloT (BVT 0) (F "a" ::: F "b" ::: id))
(FT "a"),
testEq "[#1]{a,b} = [b] : A" $
equalT empty (FT "A")
(CloT (BVT 1) (F "a" ::: F "b" ::: id))
(FT "b"),
testEq "(λy ⇒ [#1]){a} = λy ⇒ [a] : B ⇾ A (N)" $
equalT empty (Arr Zero (FT "B") (FT "A"))
(CloT (Lam $ S [< "y"] $ N $ BVT 0) (F "a" ::: id))
(Lam $ S [< "y"] $ N $ FT "a"),
testEq "(λy ⇒ [#1]){a} = λy ⇒ [a] : B ⇾ A (Y)" $
equalT empty (Arr Zero (FT "B") (FT "A"))
(CloT ([< "y"] :\\ BVT 1) (F "a" ::: id))
([< "y"] :\\ FT "a")
],
"term d-closure" :- [
testEq "★₀‹𝟎› = ★₀ : ★₁" $
equalTD 1
(extendDim "𝑗" empty)
(TYPE 1) (DCloT (TYPE 0) (K Zero ::: id)) (TYPE 0),
testEq "(δ i ⇒ a)𝟎 = (δ i ⇒ a) : (a ≡ a : A)" $
equalTD 1
(extendDim "𝑗" empty)
(Eq0 (FT "A") (FT "a") (FT "a"))
(DCloT ([< "i"] :\\% FT "a") (K Zero ::: id))
([< "i"] :\\% FT "a"),
note "it is hard to think of well-typed terms with big dctxs"
],
"free var" :-
let au_bu = fromList
[("A", mkDef Any (TYPE 1) (TYPE 0)),
("B", mkDef Any (TYPE 1) (TYPE 0))]
au_ba = fromList
[("A", mkDef Any (TYPE 1) (TYPE 0)),
("B", mkDef Any (TYPE 1) (FT "A"))]
in [
testEq "A = A" $
equalE empty (F "A") (F "A"),
testNeq "A ≠ B" $
equalE empty (F "A") (F "B"),
testEq "0=1 ⊢ A = B" $
equalE empty01 (F "A") (F "B"),
testEq "A : ★₁ ≔ ★₀ ⊢ A = (★₀ ∷ ★₁)" {globals = au_bu} $
equalE empty (F "A") (TYPE 0 :# TYPE 1),
testEq "A : ★₁ ≔ ★₀ ⊢ [A] = ★₀" {globals = au_bu} $
equalT empty (TYPE 1) (FT "A") (TYPE 0),
testEq "A ≔ ★₀, B ≔ ★₀ ⊢ A = B" {globals = au_bu} $
equalE empty (F "A") (F "B"),
testEq "A ≔ ★₀, B ≔ A ⊢ A = B" {globals = au_ba} $
equalE empty (F "A") (F "B"),
testEq "A <: A" $
subE empty (F "A") (F "A"),
testNeq "A ≮: B" $
subE empty (F "A") (F "B"),
testEq "A : ★₃ ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: B"
{globals = fromList [("A", mkDef Any (TYPE 3) (TYPE 0)),
("B", mkDef Any (TYPE 3) (TYPE 2))]} $
subE empty (F "A") (F "B"),
note "(A and B in different universes)",
testEq "A : ★₁ ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: B"
{globals = fromList [("A", mkDef Any (TYPE 1) (TYPE 0)),
("B", mkDef Any (TYPE 3) (TYPE 2))]} $
subE empty (F "A") (F "B"),
testEq "0=1 ⊢ A <: B" $
subE empty01 (F "A") (F "B")
],
"bound var" :- [
testEq "#0 = #0" $
equalE (extendTy Any "A" (TYPE 0) empty) (BV 0) (BV 0),
testEq "#0 <: #0" $
subE (extendTy Any "A" (TYPE 0) empty) (BV 0) (BV 0),
testNeq "#0 ≠ #1" $
equalE (extendTyN [< (Any, "A", TYPE 0), (Any, "B", TYPE 0)] empty)
(BV 0) (BV 1),
testNeq "#0 ≮: #1" $
subE (extendTyN [< (Any, "A", TYPE 0), (Any, "B", TYPE 0)] empty)
(BV 0) (BV 1),
testEq "0=1 ⊢ #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 (F "f" :@ FT "a") (F "f" :@ FT "a"),
testEq "f [a] <: f [a]" $
subE empty (F "f" :@ FT "a") (F "f" :@ FT "a"),
testEq "(λ x ⇒ [x] ∷ A ⊸ A) a = ([a ∷ A] ∷ A) (β)" $
equalE empty
((([< "x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
(E (FT "a" :# FT "A") :# FT "A"),
testEq "(λ x ⇒ [x] ∷ A ⊸ A) a = a (βυ)" $
equalE empty
((([< "x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
(F "a"),
testEq "(λ g ⇒ [g [a]] ∷ ⋯)) [f] = (λ y ⇒ [f [y]] ∷ ⋯) [a] (β↘↙)" $
let a = FT "A"; a2a = (Arr One a a) in
equalE empty
((([< "g"] :\\ E (BV 0 :@ FT "a")) :# Arr One a2a a) :@ FT "f")
((([< "y"] :\\ E (F "f" :@ BVT 0)) :# a2a) :@ FT "a"),
testEq "(λ x ⇒ [x] ∷ A ⊸ A) a <: a" $
subE empty
((([< "x"] :\\ BVT 0) :# (Arr One (FT "A") (FT "A"))) :@ FT "a")
(F "a"),
note "id : A ⊸ A ≔ λ x ⇒ [x]",
testEq "id [a] = a" $ equalE empty (F "id" :@ FT "a") (F "a"),
testEq "id [a] <: a" $ subE empty (F "id" :@ FT "a") (F "a")
],
"dim application" :- [
testEq "eq-AB @0 = eq-AB @0" $
equalE empty (F "eq-AB" :% K Zero) (F "eq-AB" :% K Zero),
testNeq "eq-AB @0 ≠ eq-AB @1" $
equalE empty (F "eq-AB" :% K Zero) (F "eq-AB" :% K One),
testEq "𝑖 | ⊢ eq-AB @𝑖 = eq-AB @𝑖" $
equalED 1
(extendDim "𝑖" empty)
(F "eq-AB" :% BV 0) (F "eq-AB" :% BV 0),
testNeq "𝑖 | ⊢ eq-AB @𝑖 ≠ eq-AB @0" $
equalED 1
(extendDim "𝑖" empty)
(F "eq-AB" :% BV 0) (F "eq-AB" :% K Zero),
testEq "𝑖, 𝑖=0 | ⊢ eq-AB @𝑖 = eq-AB @0" $
equalED 1
(eqDim (BV 0) (K Zero) $ extendDim "𝑖" empty)
(F "eq-AB" :% BV 0) (F "eq-AB" :% K Zero),
testNeq "𝑖, 𝑖=1 | ⊢ eq-AB @𝑖 ≠ eq-AB @0" $
equalED 1
(eqDim (BV 0) (K One) $ extendDim "𝑖" empty)
(F "eq-AB" :% BV 0) (F "eq-AB" :% K Zero),
testNeq "𝑖, 𝑗 | ⊢ eq-AB @𝑖 ≠ eq-AB @𝑗" $
equalED 2
(extendDim "𝑗" $ extendDim "𝑖" empty)
(F "eq-AB" :% BV 1) (F "eq-AB" :% BV 0),
testEq "𝑖, 𝑗, 𝑖=𝑗 | ⊢ eq-AB @𝑖 = eq-AB @𝑗" $
equalED 2
(eqDim (BV 0) (BV 1) $ extendDim "𝑗" $ extendDim "𝑖" empty)
(F "eq-AB" :% BV 1) (F "eq-AB" :% BV 0),
testEq "𝑖, 𝑗, 𝑖=0, 𝑗=0 | ⊢ eq-AB @𝑖 = eq-AB @𝑗" $
equalED 2
(eqDim (BV 0) (K Zero) $ eqDim (BV 1) (K Zero) $
extendDim "𝑗" $ extendDim "𝑖" empty)
(F "eq-AB" :% BV 1) (F "eq-AB" :% BV 0),
testEq "0=1 | ⊢ eq-AB @𝑖 = eq-AB @𝑗" $
equalED 2
(extendDim "𝑗" $ extendDim "𝑖" empty01)
(F "eq-AB" :% BV 1) (F "eq-AB" :% BV 0),
testEq "eq-AB @0 = A" $ equalE empty (F "eq-AB" :% K Zero) (F "A"),
testEq "eq-AB @1 = B" $ equalE empty (F "eq-AB" :% K One) (F "B"),
testEq "((δ i ⇒ a) ∷ a ≡ a) @0 = a" $
equalE empty
(((DLam $ SN $ FT "a") :# Eq0 (FT "A") (FT "a") (FT "a")) :% K Zero)
(F "a"),
testEq "((δ i ⇒ a) ∷ a ≡ a) @0 = ((δ i ⇒ a) ∷ a ≡ a) @1" $
equalE empty
(((DLam $ SN $ FT "a") :# Eq0 (FT "A") (FT "a") (FT "a")) :% K Zero)
(((DLam $ SN $ FT "a") :# Eq0 (FT "A") (FT "a") (FT "a")) :% K One)
],
"annotation" :- [
testEq "(λ x ⇒ f [x]) ∷ A ⊸ A = [f] ∷ A ⊸ A" $
equalE empty
(([< "x"] :\\ E (F "f" :@ BVT 0)) :# Arr One (FT "A") (FT "A"))
(FT "f" :# Arr One (FT "A") (FT "A")),
testEq "[f] ∷ A ⊸ A = f" $
equalE empty (FT "f" :# Arr One (FT "A") (FT "A")) (F "f"),
testEq "(λ x ⇒ f [x]) ∷ A ⊸ A = f" $
equalE empty
(([< "x"] :\\ E (F "f" :@ BVT 0)) :# Arr One (FT "A") (FT "A"))
(F "f")
],
"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 "zero = zero" $ equalT empty Nat Zero Zero,
testEq "succ two = succ two" $
equalT empty Nat (Succ (FT "two")) (Succ (FT "two")),
testNeq "succ two ≠ two" $
equalT empty Nat (Succ (FT "two")) (FT "two"),
testNeq "zero ≠ succ zero" $
equalT empty Nat Zero (Succ Zero),
testEq "0=1 ⊢ zero = succ zero" $
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 (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 (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 (makeNat 4 :# Nat)
(SN Nat)
Zero
(SY [< "n", Unused] $ BVT 1))
(makeNat 3)
],
todo "pair types",
"pairs" :- [
testEq "('a, 'b) = ('a, 'b) : {a} × {b}" $
equalT empty
(enum ["a"] `And` enum ["b"])
(Tag "a" `Pair` Tag "b")
(Tag "a" `Pair` Tag "b"),
testNeq "('a, 'b) ≠ ('b, 'a) : {a,b} × {a,b}" $
equalT empty
(enum ["a", "b"] `And` enum ["a", "b"])
(Tag "a" `Pair` Tag "b")
(Tag "b" `Pair` Tag "a"),
testEq "0=1 ⊢ ('a, 'b) = ('b, 'a) : {a,b} × {a,b}" $
equalT empty01
(enum ["a", "b"] `And` enum ["a", "b"])
(Tag "a" `Pair` Tag "b")
(Tag "b" `Pair` Tag "a"),
testEq "0=1 ⊢ ('a, 'b) = ('b, 'a) : " $
equalT empty01
Nat
(Tag "a" `Pair` Tag "b")
(Tag "b" `Pair` Tag "a")
],
todo "pair elim",
todo "enum types",
todo "enum",
todo "enum elim",
todo "box types",
todo "boxes",
todo "box elim",
"elim closure" :- [
testEq "#0{a} = a" $
equalE empty (CloE (BV 0) (F "a" ::: id)) (F "a"),
testEq "#1{a} = #0" $
equalE (extendTy Any "x" (FT "A") empty)
(CloE (BV 1) (F "a" ::: id)) (BV 0)
],
"elim d-closure" :- [
note "0·eq-AB : (A ≡ B : ★₀)",
testEq "(eq-AB #0)𝟎 = eq-AB 𝟎" $
equalED 1
(extendDim "𝑖" empty)
(DCloE (F "eq-AB" :% BV 0) (K Zero ::: id))
(F "eq-AB" :% K Zero),
testEq "(eq-AB #0)𝟎 = A" $
equalED 1
(extendDim "𝑖" empty)
(DCloE (F "eq-AB" :% BV 0) (K Zero ::: id)) (F "A"),
testEq "(eq-AB #0)𝟏 = B" $
equalED 1
(extendDim "𝑖" empty)
(DCloE (F "eq-AB" :% BV 0) (K One ::: id)) (F "B"),
testNeq "(eq-AB #0)𝟏 ≠ A" $
equalED 1
(extendDim "𝑖" empty)
(DCloE (F "eq-AB" :% BV 0) (K One ::: id)) (F "A"),
testEq "(eq-AB #0)#0,𝟎 = (eq-AB #0)" $
equalED 2
(extendDim "𝑗" $ extendDim "𝑖" empty)
(DCloE (F "eq-AB" :% BV 0) (BV 0 ::: K Zero ::: id))
(F "eq-AB" :% BV 0),
testNeq "(eq-AB #0)𝟎 ≠ (eq-AB 𝟎)" $
equalED 2
(extendDim "𝑗" $ extendDim "𝑖" empty)
(DCloE (F "eq-AB" :% BV 0) (BV 0 ::: K Zero ::: id))
(F "eq-AB" :% K Zero),
testEq "#0𝟎 = #0 # term and dim vars distinct" $
equalED 1
(extendTy Any "x" (FT "A") $ extendDim "𝑖" empty)
(DCloE (BV 0) (K Zero ::: id)) (BV 0),
testEq "a𝟎 = a" $
equalED 1 (extendDim "𝑖" empty) (DCloE (F "a") (K Zero ::: id)) (F "a"),
testEq "(f [a])𝟎 = f𝟎 [a]𝟎" $
let th = K Zero ::: id in
equalED 1 (extendDim "𝑖" empty)
(DCloE (F "f" :@ FT "a") th)
(DCloE (F "f") th :@ DCloT (FT "a") th)
],
"clashes" :- [
testNeq "★₀ ≠ ★₀ ⇾ ★₀" $
equalT empty (TYPE 1) (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)),
testEq "0=1 ⊢ ★₀ = ★₀ ⇾ ★₀" $
equalT empty01 (TYPE 1) (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)),
todo "others"
]
]