some equality tests

tests/Tests/Equal.idr

@@ -7,17 +7,17 @@ import TAP
 export
 ToInfo Equal.Error where
   toInfo (ClashT mode s t) =
-    [("clash",  "term"),
+    [("clash", "term"),
-     ("mode",   show mode),
+     ("mode",  show mode),
      ("left",  prettyStr True s),
      ("right", prettyStr True t)]
   toInfo (ClashU mode k l) =
-    [("clash",  "universe"),
+    [("clash", "universe"),
-     ("mode",   show mode),
+     ("mode",  show mode),
      ("left",  prettyStr True k),
      ("right", prettyStr True l)]
   toInfo (ClashQ pi rh) =
-    [("clash",  "quantity"),
+    [("clash", "quantity"),
      ("left",  prettyStr True pi),
      ("right", prettyStr True rh)]
 
@@ -52,50 +52,126 @@ export
 tests : Test
 tests = "equality & subtyping" :- [
     "universes" :- [
-        testEq "Type 0 == Type 0" $
+        testEq "𝒰₀ ≡ 𝒰₀" $
-          equalT (TYPE (U 0)) (TYPE (U 0)),
+          equalT (TYPE 0) (TYPE 0),
-        testNeq "Type 0 =/= Type 1" $
+        testNeq "𝒰₀ ≢ 𝒰₁" $
-          equalT (TYPE (U 0)) (TYPE (U 1)),
+          equalT (TYPE 0) (TYPE 1),
-        testNeq "Type 1 =/= Type 0" $
+        testNeq "𝒰₁ ≢ 𝒰₀" $
-          equalT (TYPE (U 1)) (TYPE (U 0)),
+          equalT (TYPE 1) (TYPE 0),
-        testEq "Type 0 <: Type 0" $
+        testEq "𝒰₀ <: 𝒰₀" $
-          subT (TYPE (U 0)) (TYPE (U 0)),
+          subT (TYPE 0) (TYPE 0),
-        testEq "Type 0 <: Type 1" $
+        testEq "𝒰₀ <: 𝒰₁" $
-          subT (TYPE (U 0)) (TYPE (U 1)),
+          subT (TYPE 0) (TYPE 1),
-        testNeq "Type 1 </: Type 0" $
+        testNeq "𝒰₁ ≮: 𝒰₀" $
-          subT (TYPE (U 1)) (TYPE (U 0))
+          subT (TYPE 1) (TYPE 0)
       ],
-    todo "pi",
+
-    todo "lambda",
+    "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)))))
+    ],
+
     todo "term closure",
+
     todo "term d-closure",
 
     "free var" :- [
-        testEq "A == A" $
+        testEq "A ≡ A" $
           equalE (F "A") (F "A"),
-        testNeq "A =/= B" $
+        testNeq "A ≢ B" $
           equalE (F "A") (F "B"),
         testEq "A <: A" $
           subE (F "A") (F "A"),
-        testNeq "A </: B" $
+        testNeq "A ≮: B" $
           subE (F "A") (F "B")
       ],
+
     todo "bound var",
-    "application" :-
+
-      let a    = F "a"; a' = E a
+    "application" :- [
-          A    = FT "A"
+        testEq "f [a] ≡ f [a]" $
-          λxx  = Lam "x" (TUsed (BVT 0))
+          equalE (F "f" :@ FT "a") (F "f" :@ FT "a"),
-          A_A  = Arr one A A
+        testEq "f [a] <: f [a]" $
-          λxx' = λxx :# A_A
+          subE (F "f" :@ FT "a") (F "f" :@ FT "a"),
-      in [
+        testEq "(λ x ⇒ [x] ∷ A ⊸ A) a ≡ ([a ∷ A] ∷ A)  (β)" $
-        testEq "(λx. x : A -> A) a == ((a : A) : A)  (β)" $
+          equalE
-          equalE (λxx' :@ a') (E (a' :# A) :# A),
+            ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A")))
-        testEq "(λx. x : _) a == a  (βυ)" $
+              :@ FT "a")
-          equalE (λxx' :@ a') 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 "(λ 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",
 
-    todo "clashes"
+    "clashes" :- [
+      testNeq "𝒰₀ ≢ 𝒰₀ ⇾ 𝒰₀" $
+        equalT (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)),
+      todo "others"
+    ]
   ]