quox/tests/Tests/Equal.idr

module Tests.Equal

import Quox.Equal as Lib
import Quox.Pretty
import Quox.Syntax.Qty.Three
import TAP

export
ToInfo (Error Three) where
  toInfo (NotInScope x) =
    [("type", "NotInScope"),
     ("name", show x)]
  toInfo (ExpectedTYPE t) =
    [("type", "ExpectedTYPE"),
     ("got", prettyStr True t)]
  toInfo (ExpectedPi t) =
    [("type", "ExpectedPi"),
     ("got", prettyStr True t)]
  toInfo (BadUniverse k l) =
    [("type", "BadUniverse"),
     ("low",  show k),
     ("high", show l)]
  toInfo (ClashT mode s t) =
    [("type", "ClashT"),
     ("mode",  show mode),
     ("left",  prettyStr True s),
     ("right", prettyStr True t)]
  toInfo (ClashU mode k l) =
    [("type", "ClashU"),
     ("mode",  show mode),
     ("left",  prettyStr True k),
     ("right", prettyStr True l)]
  toInfo (ClashQ pi rh) =
    [("type", "ClashQ"),
     ("left",  prettyStr True pi),
     ("right", prettyStr True rh)]


0 M : Type -> Type
M = ReaderT (Definitions Three) (Either (Error Three))

parameters (label : String) (act : Lazy (M ()))
           {default empty globals : Definitions Three}
  testEq : Test
  testEq = test label $ runReaderT globals act

  testNeq : Test
  testNeq = testThrows label (const True) $ runReaderT globals act


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

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

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

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


export
tests : Test
tests = "equality & subtyping" :- [
    "universes" :- [
      testEq "★₀ ≡ ★₀" $
        equalT (TYPE 0) (TYPE 0),
      testNeq "★₀ ≢ ★₁" $
        equalT (TYPE 0) (TYPE 1),
      testNeq "★₁ ≢ ★₀" $
        equalT (TYPE 1) (TYPE 0),
      testEq "★₀ <: ★₀" $
        subT (TYPE 0) (TYPE 0),
      testEq "★₀ <: ★₁" $
        subT (TYPE 0) (TYPE 1),
      testNeq "★₁ ≮: ★₀" $
        subT (TYPE 1) (TYPE 0)
    ],

    "pi" :- [
      -- ⊸ for →₁, ⇾ for →₀
      testEq "A ⊸ B ≡ A ⊸ B" $
        let tm = Arr One (FT "A") (FT "B") in
        equalT tm tm,
      testNeq "A ⇾ B ≢ A ⇾ B" $
        let tm1 = Arr Zero (FT "A") (FT "B")
            tm2 = Arr One  (FT "A") (FT "B") in
        equalT tm1 tm2,
      testEq "A ⊸ B <: A ⊸ B" $
        let tm = Arr One (FT "A") (FT "B") in
        subT tm tm,
      testNeq "A ⇾ B ≮: A ⊸ B" $
        let tm1 = Arr Zero (FT "A") (FT "B")
            tm2 = Arr One  (FT "A") (FT "B") in
        subT tm1 tm2,
      testEq "★₀ ⇾ ★₀ ≡ ★₀ ⇾ ★₀" $
        let tm = Arr Zero (TYPE 0) (TYPE 0) in
        equalT tm tm,
      testEq "★₀ ⇾ ★₀ <: ★₀ ⇾ ★₀" $
        let tm = Arr Zero (TYPE 0) (TYPE 0) in
        subT tm tm,
      testNeq "★₁ ⊸ ★₀ ≢ ★₀ ⇾ ★₀" $
        let tm1 = Arr Zero (TYPE 1) (TYPE 0)
            tm2 = Arr Zero (TYPE 0) (TYPE 0) in
        equalT tm1 tm2,
      testEq "★₁ ⊸ ★₀ <: ★₀ ⊸ ★₀" $
        let tm1 = Arr One (TYPE 1) (TYPE 0)
            tm2 = Arr One (TYPE 0) (TYPE 0) in
        subT tm1 tm2,
      testNeq "★₀ ⊸ ★₀ ≢ ★₀ ⇾ ★₁" $
        let tm1 = Arr Zero (TYPE 0) (TYPE 0)
            tm2 = Arr Zero (TYPE 0) (TYPE 1) in
        equalT tm1 tm2,
      testEq "★₀ ⊸ ★₀ <: ★₀ ⊸ ★₁" $
        let tm1 = Arr One (TYPE 0) (TYPE 0)
            tm2 = Arr One (TYPE 0) (TYPE 1) in
        subT tm1 tm2,
      testEq "★₀ ⊸ ★₀ <: ★₀ ⊸ ★₁" $
        let tm1 = Arr One (TYPE 0) (TYPE 0)
            tm2 = Arr One (TYPE 0) (TYPE 1) in
        subT tm1 tm2
    ],

    "lambda" :- [
      testEq "λ x ⇒ [x] ≡ λ x ⇒ [x]" $
        equalT (Lam "x" $ TUsed $ BVT 0) (Lam "x" $ TUsed $ BVT 0),
      testEq "λ x ⇒ [x] <: λ x ⇒ [x]" $
        equalT (Lam "x" $ TUsed $ BVT 0) (Lam "x" $ TUsed $ BVT 0),
      testEq "λ x ⇒ [x] ≡ λ y ⇒ [y]" $
        equalT (Lam "x" $ TUsed $ BVT 0) (Lam "y" $ TUsed $ BVT 0),
      testEq "λ x ⇒ [x] <: λ y ⇒ [y]" $
        equalT (Lam "x" $ TUsed $ BVT 0) (Lam "y" $ TUsed $ BVT 0),
      testNeq "λ x y ⇒ [x] ≢ λ x y ⇒ [y]" $
        equalT (Lam "x" $ TUsed $ Lam "y" $ TUsed $ BVT 1)
               (Lam "x" $ TUsed $ Lam "y" $ TUsed $ BVT 0),
      testEq "λ x ⇒ [a] ≡ λ x ⇒ [a]  (TUsed vs TUnused)" $
        equalT (Lam "x" $ TUsed   $ FT "a")
               (Lam "x" $ TUnused $ FT "a"),
      skipWith "(no η yet)" $
      testEq "λ x ⇒ [f [x]] ≡ [f]  (η)" $
        equalT (Lam "x" $ TUsed $ E $ F "f" :@ BVT 0)
               (FT "f")
    ],

    "term closure" :- [
      testEq "[x]{} ≡ [x]" $
        equalT (CloT (BVT 0) id) (BVT 0) {n = 1},
      testEq "[x]{a/x} ≡ [a]" $
        equalT (CloT (BVT 0) (F "a" ::: id)) (FT "a"),
      testEq "[x]{a/x,b/y} ≡ [a]" $
        equalT (CloT (BVT 0) (F "a" ::: F "b" ::: id)) (FT "a"),
      testEq "(λy. [x]){y/y, a/x} ≡ λy. [a]  (TUnused)" $
        equalT (CloT (Lam "y" $ TUnused $ BVT 0) (F "a" ::: id))
               (Lam "y" $ TUnused $ FT "a"),
      testEq "(λy. [x]){y/y, a/x} ≡ λy. [a]  (TUsed)" $
        equalT (CloT (Lam "y" $ TUsed $ BVT 1) (F "a" ::: id))
               (Lam "y" $ TUsed $ FT "a")
    ],

    todo "term d-closure",

    "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 (F "A") (F "A"),
      testNeq "A ≢ B" $
        equalE (F "A") (F "B"),
      testEq "A ≔ ★₀, B ≔ ★₀ ⊢ A ≡ B" {globals = au_bu} $
        equalE (F "A") (F "B"),
      testEq "A ≔ ★₀, B ≔ A ⊢ A ≡ B" {globals = au_ba} $
        equalE (F "A") (F "B"),
      testEq "A <: A" $
        subE (F "A") (F "A"),
      testNeq "A ≮: B" $
        subE (F "A") (F "B")
    ],

    "bound var" :- [
      testEq "#0 ≡ #0" $
        equalE (BV 0) (BV 0) {n = 1},
      testNeq "#0 ≢ #1" $
        equalE (BV 0) (BV 1) {n = 2}
    ],

    "application" :- [
      testEq "f [a] ≡ f [a]" $
        equalE (F "f" :@ FT "a") (F "f" :@ FT "a"),
      testEq "f [a] <: f [a]" $
        subE (F "f" :@ FT "a") (F "f" :@ FT "a"),
      testEq "(λ x ⇒ [x] ∷ A ⊸ A) a ≡ ([a ∷ A] ∷ A)  (β)" $
        equalE
          ((Lam "x" (TUsed (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
          ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A")))
            :@ FT "a")
          (F "a"),
      testEq "(λ g ⇒ [g [x]] ∷ ⋯)) [f] ≡ (λ y ⇒ [f [y]] ∷ ⋯) [x]  (β↘↙)" $
        let a = FT "A"; a2a = (Arr One a a) in
        equalE
          ((Lam "g" (TUsed (E (BV 0 :@ FT "x"))) :# Arr One a2a a) :@ FT "f")
          ((Lam "y" (TUsed (E (F "f" :@ BVT 0))) :# a2a) :@ FT "x"),
      testEq "(λ x ⇒ [x] ∷ A ⊸ A) a <: a" $
        subE
          ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A")))
            :@ FT "a")
          (F "a")
    ],

    todo "annotation",

    todo "elim closure",

    todo "elim d-closure",

    "clashes" :- [
      testNeq "★₀ ≢ ★₀ ⇾ ★₀" $
        equalT (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)),
      todo "others"
    ]
  ]