From 1211272420ae72d3cd2f8f4e34be6133c4928d80 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 2 Apr 2023 15:50:56 +0200
Subject: [PATCH] factor out some pretty printing stuff

---
 lib/Quox/Pretty.idr             | 31 ++++++++++++++------
 lib/Quox/Syntax/Term/Pretty.idr | 50 ++++++++++++++++++++-------------
 2 files changed, 53 insertions(+), 28 deletions(-)

diff --git a/lib/Quox/Pretty.idr b/lib/Quox/Pretty.idr
index 0b4695f..fd6c1ee 100644
--- a/lib/Quox/Pretty.idr
+++ b/lib/Quox/Pretty.idr
@@ -197,14 +197,6 @@ pretty0 : PrettyHL a => (unicode : Bool) -> a -> Doc HL
 pretty0 unicode = pretty0With unicode [<] [<]
 
 
-export
-(forall a. PrettyHL (f a)) => PrettyHL (Exists f) where
-  prettyM x = prettyM x.snd
-
-export
-PrettyHL a => PrettyHL (Subset a b) where
-  prettyM x = prettyM x.fst
-
 
 export PrettyHL BaseName where prettyM = pure . pretty . baseStr
 export PrettyHL Name     where prettyM = pure . pretty . toDots
@@ -263,3 +255,26 @@ export %inline PrettyHL TVarName where prettyM (TV x) = hlF TVar $ prettyM x
 ||| wrapper for names that pretty-prints highlighted as a `DVar`.
 public export data DVarName = DV BaseName
 export %inline PrettyHL DVarName where prettyM (DV x) = hlF DVar $ prettyM x
+
+
+export
+(forall a. PrettyHL (f a)) => PrettyHL (Exists f) where
+  prettyM x = prettyM x.snd
+
+export
+PrettyHL a => PrettyHL (Subset a b) where
+  prettyM x = prettyM x.fst
+
+public export
+WithPretty : Type -> Type
+WithPretty a = (PrettyHL a, a)
+
+export %inline PrettyHL (WithPretty a) where prettyM x = prettyM $ snd x
+
+export %inline
+epretty : PrettyHL a => a -> Exists WithPretty
+epretty @{p} x = Evidence a (p, x)
+
+
+public export data Lit = L (Doc HL)
+export PrettyHL Lit where prettyM (L doc) = pure doc
diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index c3c3a8c..0523341 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -103,18 +103,32 @@ prettyLams lam sort names body = do
   let header = sep $ maybe header (:: header) lam
   parensIfM Outer =<< prettyArm sort names header body
 
+
+public export
+data TypeLine a = MkTypeLine BaseName a
+
+export
+PrettyHL a => PrettyHL (TypeLine a) where
+  prettyM (MkTypeLine i ty) =
+    map bracks $ withPrec Outer $ prettyLams Nothing D [< i] ty
+
+
+export
+prettyApps' : PrettyHL f => PrettyHL a => Pretty.HasEnv m =>
+              f -> List (Maybe (Doc HL), a) -> m (Doc HL)
+prettyApps' fun args = do
+  fun  <- withPrec App $ prettyM fun
+  args <- traverse prettyArg args
+  parensIfM App $ hang 2 $ sep $ fun :: args
+ where
+  prettyArg : (Maybe (Doc HL), a) -> m (Doc HL)
+  prettyArg (Nothing,  arg) = withPrec Arg (prettyM arg)
+  prettyArg (Just pfx, arg) = (hl Delim pfx <+>) <$> withPrec Arg (prettyM arg)
+
 export
 prettyApps : PrettyHL f => PrettyHL a => Pretty.HasEnv m =>
              Maybe (Doc HL) -> f -> List a -> m (Doc HL)
-prettyApps pfx fun args = do
-  fun  <- withPrec App $ prettyM fun
-  args <- traverse (withPrec Arg . prettyArg) args
-  parensIfM App $ hang 2 $ sep $ fun :: args
- where
-  prettyArg : a -> m (Doc HL)
-  prettyArg = case pfx of
-    Nothing  => prettyM
-    Just pfx => \x => pure $ hl Delim pfx <+> !(prettyM x)
+prettyApps pfx f args = prettyApps' f (map (pfx,) args)
 
 export
 prettyTuple : PrettyHL a => Pretty.HasEnv m => List a -> m (Doc HL)
@@ -213,10 +227,8 @@ parameters (showSubsts : Bool)
       ty <- withPrec InEq $ prettyM ty
       parensIfM Eq $ asep [l <++> !eqndD, r <++> colonD, ty]
     prettyM (Eq (S [< i] (Y ty)) l r) = do
-      ty <- bracks <$> withPrec Outer (prettyLams Nothing D [< i] ty)
-      l  <- withPrec Arg $ prettyM l
-      r  <- withPrec Arg $ prettyM r
-      parensIfM App $ eqD <++> asep [ty, l, r]
+      prettyApps Nothing (L eqD)
+        [epretty $ MkTypeLine i ty, epretty l, epretty r]
     prettyM (DLam (S i t)) =
       let GotDLams {names, body, _} = getDLams' i t.term Refl in
       prettyLams (Just !dlamD) D (toSnocList' names) body
@@ -225,9 +237,7 @@ parameters (showSubsts : Bool)
     prettyM (Succ n) =
       case toNatLit n of
         Just n  => pure $ hl Syntax $ pretty $ S n
-        Nothing => do
-          n <- withPrec Arg $ prettyM n
-          parensIfM App $ succD <++> n
+        Nothing => prettyApps Nothing (L succD) [n]
     prettyM (BOX pi ty) = do
       pi <- pretty0M pi
       ty <- pretty0M ty
@@ -269,10 +279,10 @@ parameters (showSubsts : Bool)
          ([< s, ih], !succPat, eterm suc.term)]
       where
         succPat : m (Doc HL)
-        succPat = case ih of
-          Unused => pure $ hsep [succD, !(pretty0M s)]
-          _      => pure $ sep [hsep [succD, !(pretty0M s)] <+> comma,
-                                !(pretty0M $ MkWithQty pi' ih)]
+        succPat = case (ih, pi') of
+          (Unused, Zero) => pure $ succD <++> !(pretty0M s)
+          _ => pure $ asep [succD <++> !(pretty0M s) <+> comma,
+                            !(pretty0M $ MkWithQty pi' ih)]
     prettyM (CaseBox pi box (S [< r] ret) (S [< u] body)) =
       prettyCase pi box r ret.term
         [([< u], !(prettyBoxVal $ TV u), body.term)]