From 443da20c4b90772c29a49fda6ab18fd5a18cdce9 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sat, 18 Mar 2023 23:32:53 +0100
Subject: [PATCH] =?UTF-8?q?print=20non-dependent=20function=20types=20as?=
 =?UTF-8?q?=20"=CF=80.A=20=E2=86=92=20B"?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 lib/Quox/Syntax/Term/Pretty.idr |  8 ++++++--
 tests/Tests/PrettyTerm.idr      | 20 ++++++++++----------
 2 files changed, 16 insertions(+), 12 deletions(-)

diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index 6a62ed6..e44dfcc 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -165,8 +165,12 @@ parameters (showSubsts : Bool)
   where
     prettyM (TYPE l) =
       parensIfM App $ !typeD <+> hl Syntax !(prettyUnivSuffix l)
-    prettyM (Pi qty s (S [< x] t)) =
-      prettyBindType (Just qty) x s !arrowD t.term
+    prettyM (Pi qty s (S _ (N t))) = do
+      dom <- pretty0M $ MkWithQty qty s
+      cod <- withPrec AnnR $ prettyM t
+      parensIfM AnnR $ asep [dom <++> !arrowD, cod]
+    prettyM (Pi qty s (S [< x] (Y t))) =
+      prettyBindType (Just qty) x s !arrowD t
     prettyM (Lam (S x t)) =
       let GotLams {names, body, _} = getLams' x t.term Refl in
       prettyLams (Just !lamD) T (toSnocList' names) body
diff --git a/tests/Tests/PrettyTerm.idr b/tests/Tests/PrettyTerm.idr
index 0e142b9..76f79e6 100644
--- a/tests/Tests/PrettyTerm.idr
+++ b/tests/Tests/PrettyTerm.idr
@@ -97,13 +97,13 @@ tests = "pretty printing terms" :- [
       "1.(x : A) -> B x",
     testPrettyT [<] [<]
       (Pi_ Zero "A" (TYPE 0) $ Arr Any (BVT 0) (BVT 0))
-      "0.(A : ★₀) → ω.(_ : A) → A"
-      "0.(A : Type0) -> #.(_ : A) -> A",
+      "0.(A : ★₀) → ω.A → A"
+      "0.(A : Type0) -> #.A -> A",
     todo #"print (and parse) the below as "(A ↠ A) ↠ A""#,
     testPrettyT [<] [<]
       (Arr Any (Arr Any (FT "A") (FT "A")) (FT "A"))
-      "ω.(_ : ω.(_ : A) → A) → A"
-      "#.(_ : #.(_ : A) -> A) -> A",
+      "ω.(ω.A → A) → A"
+      "#.(#.A -> A) -> A",
     todo "non-dependent, left and right nested"
   ],
 
@@ -128,8 +128,8 @@ tests = "pretty printing terms" :- [
     testPrettyT1 [<] [<] (Pair (Pair (FT "A") (FT "B")) (FT "C")) "((A, B), C)",
     testPrettyT [<] [<]
       (Pair ([< "x"] :\\ BVT 0) (Arr One (FT "B₁") (FT "B₂")))
-      "(λ x ⇒ x, 1.(_ : B₁) → B₂)"
-      "(fun x => x, 1.(_ : B₁) -> B₂)"
+      "(λ x ⇒ x, 1.B₁ → B₂)"
+      "(fun x => x, 1.B₁ -> B₂)"
   ],
 
   "enum types" :- [
@@ -180,11 +180,11 @@ tests = "pretty printing terms" :- [
       "(α :: a) :: A",
     testPrettyE [<] [<]
       (([< "x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A"))
-      "(λ x ⇒ x) ∷ 1.(_ : A) → A"
-      "(fun x => x) :: 1.(_ : A) -> 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"
+      "(1.A → A) ∷ ★₇"
+      "(1.A -> A) :: Type7"
   ]
 ]