quox/tests/Tests/Equal.idr

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", mkAbstract Zero $ TYPE 0),
   ("B", mkAbstract Zero $ TYPE 0),
   ("a", mkAbstract Any $ FT "A"),
   ("a'", mkAbstract Any $ FT "A"),
   ("b", mkAbstract Any $ FT "B"),
   ("f", mkAbstract Any $ Arr One (FT "A") (FT "A")),
   ("id", mkDef Any (Arr One (FT "A") (FT "A")) (["x"] :\\ BVT 0)),
   ("eq-ab", mkAbstract Zero $ Eq0 (TYPE 0) (FT "A") (FT "B"))]

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

  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

  subE, equalE : Elim Three 0 n -> Elim Three 0 n -> M ()
  subE = subED 0 ctx
  equalE = equalED 0 ctx



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"#,

  "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)
  ],

  "pi" :- [
    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 (MkTyContext ZeroIsOne [<]) (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 = mkAbstract 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 (MkTyContext new [< ty, ty]) (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 (MkTyContext new [< ty, ty]) (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 (MkTyContext new [< FT "EE", FT "EE"]) (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 (MkTyContext new [< FT "EE", FT "E"]) (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 (MkTyContext new [< FT "E", FT "E"]) (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 (MkTyContext new [< ty, ty]) (BV 0) (BV 1),

    testEq "E ≔ a ≡ a' : A, F ≔ E × E ∥ x : F, y : F ⊢ 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 (MkTyContext new [< FT "W", FT "W"]) (BV 0) (BV 1)
  ],

  "term closure" :- [
    testEq "[#0]{} = [#0] : A" $
      equalT (MkTyContext new [< FT "A"]) (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 empty (TYPE 1) (DCloT (TYPE 0) (K Zero ::: id)) (TYPE 0),
    testEq "(δ i. a)‹𝟎› = (δ i. a) : (a ≡ a : A)" $
      equalTD 1 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 (U 1)) (TYPE (U 0))),
         ("B", mkDef Any (TYPE (U 1)) (TYPE (U 0)))]
      au_ba = fromList
        [("A", mkDef Any (TYPE (U 1)) (TYPE (U 0))),
         ("B", mkDef Any (TYPE (U 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 (MkTyContext ZeroIsOne [<]) (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 (MkTyContext ZeroIsOne [<]) (F "A") (F "B")
  ],

  "bound var" :- [
    testEq "#0 = #0" $
      equalE (MkTyContext new [< TYPE 0]) (BV 0) (BV 0),
    testEq "#0 <: #0" $
      subE (MkTyContext new [< TYPE 0]) (BV 0) (BV 0),
    testNeq "#0 ≠ #1" $
      equalE (MkTyContext new [< TYPE 0, TYPE 0]) (BV 0) (BV 1),
    testNeq "#0 ≮: #1" $
      subE (MkTyContext new [< TYPE 0, TYPE 0]) (BV 0) (BV 1),
    testEq "0=1 ⊢ #0 = #1" $
      equalE (MkTyContext ZeroIsOne [< TYPE 0, TYPE 0]) (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")
  ],

  todo "dim application",

  "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")
  ],

  "elim closure" :- [
    testEq "#0{a} = a" $
      equalE empty (CloE (BV 0) (F "a" ::: id)) (F "a"),
    testEq "#1{a} = #0" $
      equalE (MkTyContext new [< FT "A"])
        (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 empty
        (DCloE (F "eq-ab" :% BV 0) (K Zero ::: id))
        (F "eq-ab" :% K Zero),
    testEq "(eq-ab #0)‹𝟎› = A" $
      equalED 1 empty (DCloE (F "eq-ab" :% BV 0) (K Zero ::: id)) (F "A"),
    testEq "(eq-ab #0)‹𝟏› = B" $
      equalED 1 empty (DCloE (F "eq-ab" :% BV 0) (K One  ::: id)) (F "B"),
    testNeq "(eq-ab #0)‹𝟏› ≠ A" $
      equalED 1 empty (DCloE (F "eq-ab" :% BV 0) (K One  ::: id)) (F "A"),
    testEq "(eq-ab #0)‹#0,𝟎› = (eq-ab #0)" $
      equalED 2 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 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 (MkTyContext new [< FT "A"])
        (DCloE (BV 0) (K Zero ::: id)) (BV 0),
    testEq "a‹𝟎› = a" $
      equalED 1 empty (DCloE (F "a") (K Zero ::: id)) (F "a"),
    testEq "(f [a])‹𝟎› = f‹𝟎› [a]‹𝟎›" $
      let th = K Zero ::: id in
      equalED 1 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 (MkTyContext ZeroIsOne [<])
        (TYPE 1) (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)),
    todo "others"
  ]
]