module Tests.Equal

import Quox.Equal
import Quox.Pretty
import TAP

export
ToInfo Equal.Error where
  toInfo (ClashT mode s t) =
    [("clash",  "term"),
     ("mode",   show mode),
     ("left",  prettyStr True s),
     ("right", prettyStr True t)]
  toInfo (ClashU mode k l) =
    [("clash",  "universe"),
     ("mode",   show mode),
     ("left",  prettyStr True k),
     ("right", prettyStr True l)]
  toInfo (ClashQ pi rh) =
    [("clash",  "quantity"),
     ("left",  prettyStr True pi),
     ("right", prettyStr True rh)]


M = Either Equal.Error

testEq : String -> Lazy (M ()) -> Test
testEq = test

testNeq : String -> Lazy (M ()) -> Test
testNeq label = testThrows label $ const True


subT : {default 0 d, n : Nat} -> Term d n -> Term d n -> M ()
subT = Quox.Equal.subT
%hide Quox.Equal.subT

equalT : {default 0 d, n : Nat} -> Term d n -> Term d n -> M ()
equalT = Quox.Equal.equalT
%hide Quox.Equal.equalT

subE : {default 0 d, n : Nat} -> Elim d n -> Elim d n -> M ()
subE = Quox.Equal.subE
%hide Quox.Equal.subE

equalE : {default 0 d, n : Nat} -> Elim d n -> Elim d n -> M ()
equalE = Quox.Equal.equalE
%hide Quox.Equal.equalE


export
tests : Test
tests = "equality & subtyping" :- [
    "universes" :- [
        testEq "Type 0 == Type 0" $
          equalT (TYPE (U 0)) (TYPE (U 0)),
        testNeq "Type 0 =/= Type 1" $
          equalT (TYPE (U 0)) (TYPE (U 1)),
        testNeq "Type 1 =/= Type 0" $
          equalT (TYPE (U 1)) (TYPE (U 0)),
        testEq "Type 0 <: Type 0" $
          subT (TYPE (U 0)) (TYPE (U 0)),
        testEq "Type 0 <: Type 1" $
          subT (TYPE (U 0)) (TYPE (U 1)),
        testNeq "Type 1 </: Type 0" $
          subT (TYPE (U 1)) (TYPE (U 0))
      ],
    todo "pi",
    todo "lambda",
    todo "term closure",
    todo "term d-closure",

    "free var" :- [
        testEq "A == A" $
          equalE (F "A") (F "A"),
        testNeq "A =/= B" $
          equalE (F "A") (F "B"),
        testEq "A <: A" $
          subE (F "A") (F "A"),
        testNeq "A </: B" $
          subE (F "A") (F "B")
      ],
    todo "bound var",
    "application" :-
      let a    = F "a"; a' = E a
          A    = FT "A"
          λxx  = Lam "x" (TUsed (BVT 0))
          A_A  = Arr one A A
          λxx' = λxx :# A_A
      in [
        testEq "(λx. x : A -> A) a == ((a : A) : A)  (β)" $
          equalE (λxx' :@ a') (E (a' :# A) :# A),
        testEq "(λx. x : _) a == a  (βυ)" $
          equalE (λxx' :@ a') a
      ],
    todo "annotation",
    todo "elim closure",
    todo "elim d-closure",

    todo "clashes"
  ]