quox/tests/Tests/Equal.idr

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 $> "ok"


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; "s‹p,…›" 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 "a‹0› = a" $
      equalE empty
        (DCloE (Sub (^F "a" 0) (^K Zero ::: id))) (^F "a" 0),
    testEq "(f a)‹0› = f‹0› a‹0›" $
      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"
  ]
]