From f6bc8cad1f36dab995d6d7d67fc073374575d7e5 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 5 Mar 2023 12:18:15 +0100
Subject: [PATCH] add some dim app tests

---
 tests/Tests/Equal.idr | 81 +++++++++++++++++++++++++++++++------------
 1 file changed, 59 insertions(+), 22 deletions(-)

diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr
index ce289ed..31ad5c9 100644
--- a/tests/Tests/Equal.idr
+++ b/tests/Tests/Equal.idr
@@ -17,7 +17,7 @@ defGlobals = fromList
    ("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"))]
+   ("eq-AB", mkAbstract Zero $ Eq0 (TYPE 0) (FT "A") (FT "B"))]
 
 parameters (label : String) (act : Lazy (M ()))
            {default defGlobals globals : Definitions Three}
@@ -185,8 +185,8 @@ tests = "equality & subtyping" :- [
       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
+      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"
@@ -209,8 +209,8 @@ tests = "equality & subtyping" :- [
     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
+      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"
@@ -337,7 +337,44 @@ tests = "equality & subtyping" :- [
     testEq "id [a] <: a" $ subE empty (F "id" :@ FT "a") (F "a")
   ],
 
-  todo "dim application",
+  "dim application" :- [
+    testEq "eq-AB @0 = eq-AB @0" $
+      equalE empty (F "eq-AB" :% K Zero) (F "eq-AB" :% K Zero),
+    testNeq "eq-AB @0 ≠ eq-AB @1" $
+      equalE empty (F "eq-AB" :% K Zero) (F "eq-AB" :% K One),
+    testEq "𝑖 | ⊢ eq-AB @𝑖 = eq-AB @𝑖" $
+      equalED 1 empty (F "eq-AB" :% BV 0) (F "eq-AB" :% BV 0),
+    testNeq "𝑖 | ⊢ eq-AB @𝑖 ≠ eq-AB @0" $
+      equalED 1 empty (F "eq-AB" :% BV 0) (F "eq-AB" :% K Zero),
+    testEq "𝑖, 𝑖=0 | ⊢ eq-AB @𝑖 = eq-AB @0" $
+      let ctx = MkTyContext (set (BV 0) (K Zero) new) [<] in
+      equalED 1 ctx (F "eq-AB" :% BV 0) (F "eq-AB" :% K Zero),
+    testNeq "𝑖, 𝑖=1 | ⊢ eq-AB @𝑖 ≠ eq-AB @0" $
+      let ctx = MkTyContext (set (BV 0) (K One) new) [<] in
+      equalED 1 ctx (F "eq-AB" :% BV 0) (F "eq-AB" :% K Zero),
+    testNeq "𝑖, 𝑗 | ⊢ eq-AB @𝑖 ≠ eq-AB @𝑗" $
+      equalED 2 empty (F "eq-AB" :% BV 1) (F "eq-AB" :% BV 0),
+    testEq "𝑖, 𝑗, 𝑖=𝑗 | ⊢ eq-AB @𝑖 = eq-AB @𝑗" $
+      let ctx = MkTyContext (set (BV 0) (BV 1) new) [<] in
+      equalED 2 ctx (F "eq-AB" :% BV 1) (F "eq-AB" :% BV 0),
+    testNeq "𝑖, 𝑗, 𝑖=0, 𝑗=0 | ⊢ eq-AB @𝑖 ≠ eq-AB @𝑗" $
+      let ctx : TyContext Three 2 0 :=
+            MkTyContext (C [< Just $ K Zero, Just $ K Zero]) [<] in
+      equalED 2 empty (F "eq-AB" :% BV 1) (F "eq-AB" :% BV 0),
+    testEq "0=1 | ⊢ eq-AB @𝑖 = eq-AB @𝑗" $
+      equalED 2 (MkTyContext ZeroIsOne [<])
+        (F "eq-AB" :% BV 1) (F "eq-AB" :% BV 0),
+    testEq "eq-AB @0 = A" $ equalE empty (F "eq-AB" :% K Zero) (F "A"),
+    testEq "eq-AB @1 = B" $ equalE empty (F "eq-AB" :% K One)  (F "B"),
+    testEq "((δ i ⇒ a) ∷ a ≡ a) @0 = a" $
+      equalE empty
+        (((DLam $ SN $ FT "a") :# Eq0 (FT "A") (FT "a") (FT "a")) :% K Zero)
+        (F "a"),
+    testEq "((δ i ⇒ a) ∷ a ≡ a) @0 = ((δ i ⇒ a) ∷ a ≡ a) @1" $
+      equalE empty
+        (((DLam $ SN $ FT "a") :# Eq0 (FT "A") (FT "a") (FT "a")) :% K Zero)
+        (((DLam $ SN $ FT "a") :# Eq0 (FT "A") (FT "a") (FT "a")) :% K One)
+  ],
 
   "annotation" :- [
     testEq "(λ x ⇒ f [x]) ∷ A ⊸ A = [f] ∷ A ⊸ A" $
@@ -361,25 +398,25 @@ tests = "equality & subtyping" :- [
   ],
 
   "elim d-closure" :- [
-    note "0·eq-ab : (A ≡ B : ★₀)",
-    testEq "(eq-ab #0)‹𝟎› = eq-ab 𝟎" $
+    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)" $
+        (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 𝟎)" $
+        (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),
+        (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),