a few tests

tests/Tests/Equal.idr

@@ -0,0 +1,101 @@
+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 = Error [Equal.Error]
+
+testEq : String -> Lazy (M ()) -> Test
+testEq = test
+
+testNeq : String -> Lazy (M ()) -> Test
+testNeq = testThrows
+
+
+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"
+  ]