From 51468f54fcbf79c7bd9db36c457199b2f476cc09 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sat, 18 Mar 2023 02:47:15 +0100
Subject: [PATCH] misc parse/print tests

---
 tests/Tests/Parser.idr     | 17 +++++++++++++++-
 tests/Tests/PrettyTerm.idr | 40 ++++++++++++++++++++++++++++++++++++--
 2 files changed, 54 insertions(+), 3 deletions(-)

diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr
index b7f8e1a..fe9d8f0 100644
--- a/tests/Tests/Parser.idr
+++ b/tests/Tests/Parser.idr
@@ -283,6 +283,21 @@ tests = "parser" :- [
       [PD $ PDef $ MkPDef Zero "A" (Just $ TYPE 0) (Enum []),
        PD $ PDef $ MkPDef Zero "B" (Just $ TYPE 1) (V "A")],
     parsesAs input "" [] {label = "[empty input]"},
-    parsesAs input ";;;;;;;;;;;;;;;;;;;;;;;;;;" []
+    parsesAs input ";;;;;;;;;;;;;;;;;;;;;;;;;;" [],
+    parsesAs input "namespace a {}" [PD $ PNs $ MkPNamespace [< "a"] []],
+    parsesAs input "namespace a.b.c {}"
+      [PD $ PNs $ MkPNamespace [< "a", "b", "c"] []],
+    parsesAs input "namespace a {namespace b {}}"
+      [PD $ PNs $ MkPNamespace [< "a"] [PNs $ MkPNamespace [< "b"] []]],
+    parsesAs input "namespace a {def x = 't ∷ {t}}"
+      [PD $ PNs $ MkPNamespace [< "a"]
+        [PDef $ MkPDef Any "x" Nothing (Tag "t" :# Enum ["t"])]],
+    parsesAs input "namespace a {def x = 't ∷ {t}} def y = a.x"
+      [PD $ PNs $ MkPNamespace [< "a"]
+        [PDef $ MkPDef Any "x" Nothing (Tag "t" :# Enum ["t"])],
+       PD $ PDef $ MkPDef Any "y" Nothing (V $ MakePName [< "a"] "x")],
+    parsesAs input #" load "a.quox"; def b = a.b "#
+      [PLoad "a.quox",
+       PD $ PDef $ MkPDef Any "b" Nothing (V $ MakePName [< "a"] "b")]
   ]
 ]
diff --git a/tests/Tests/PrettyTerm.idr b/tests/Tests/PrettyTerm.idr
index 4ffd35e..3839de7 100644
--- a/tests/Tests/PrettyTerm.idr
+++ b/tests/Tests/PrettyTerm.idr
@@ -150,6 +150,42 @@ tests = "pretty printing terms" :- [
   ],
 
   todo "equality types",
-  todo "case",
-  todo "annotations"
+
+  "case" :- [
+    note "todo: print using case1 and caseω???",
+    testPrettyE [<] [<]
+      (CasePair One (F "a") (SN $ TYPE 1) (SN $ TYPE 0))
+      "case 1.a return _ ⇒ ★₁ of { (_, _) ⇒ ★₀ }"
+      "case 1.a return _ => Type1 of { (_, _) => Type0 }",
+    testPrettyT [<] [<]
+      ([< "u"] :\\
+        E (CaseEnum One (F "u")
+            (SY [< "x"] $ Eq0 (enum ["tt"]) (BVT 0) (Tag "tt"))
+            (fromList [("tt", [< Unused] :\\% Tag "tt")])))
+      "λ u ⇒ case 1.u return x ⇒ x ≡ 'tt : {tt} of { 'tt ⇒ δ _ ⇒ 'tt }"
+      """
+        fun u =>
+        case 1.u return x => x == 'tt : {tt} of { 'tt => dfun _ => 'tt }
+      """
+  ],
+
+  "annotations" :- [
+    testPrettyE [<] [<] (FT "a" :# FT "A") "a ∷ A" "a :: A",
+    testPrettyE [<] [<]
+      (FT "a" :# E (FT "A" :# FT "𝐀"))
+      "a ∷ A ∷ 𝐀"
+      "a :: A :: 𝐀",
+    testPrettyE [<] [<]
+      (E (FT "α" :# FT "a") :# FT "A")
+      "(α ∷ a) ∷ A"
+      "(α :: a) :: A",
+    testPrettyE [<] [<]
+      (([< "x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A"))
+      "(λ x ⇒ x) ∷ (1._ : A) → A"
+      "(fun x => x) :: (1._ : A) -> A",
+    testPrettyE [<] [<]
+      (Arr One (FT "A") (FT "A") :# TYPE 7)
+      "((1._ : A) → A) ∷ ★₇"
+      "((1._ : A) -> A) :: Type7"
+  ]
 ]