From 82a2f92ddf0f82899781df43306d3dcffc5eb982 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 26 Feb 2023 11:20:06 +0100
Subject: [PATCH] pprint universes as a direct suffix

in subscript in unicode mode
---
 lib/Quox/Syntax/Term/Pretty.idr |  2 +-
 lib/Quox/Syntax/Universe.idr    | 11 +++++++++++
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index 93f2420..7a0089f 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -94,7 +94,7 @@ mutual
   export covering
   PrettyHL q => PrettyHL (Term q d n) where
     prettyM (TYPE l) =
-      parensIfM App $ !typeD <//> !(withPrec Arg $ prettyM l)
+      parensIfM App $ !typeD <+> hl Syntax !(prettyUnivSuffix l)
     prettyM (Pi qty s (S [x] t)) =
       prettyBindType [qty] x s !arrowD t
     prettyM (Lam (S x t)) =
diff --git a/lib/Quox/Syntax/Universe.idr b/lib/Quox/Syntax/Universe.idr
index 7a84161..ff315b8 100644
--- a/lib/Quox/Syntax/Universe.idr
+++ b/lib/Quox/Syntax/Universe.idr
@@ -22,6 +22,17 @@ PrettyHL Universe where
   prettyM UAny  = pure $ hl Delim "_"
   prettyM (U l) = pure $ hl Free $ pretty l
 
+export
+prettyUnivSuffix : Pretty.HasEnv m => Universe -> m (Doc HL)
+prettyUnivSuffix UAny  = ifUnicode "_" "₋"
+prettyUnivSuffix (U l) =
+  ifUnicode (pretty $ pack $ map sub $ unpack $ show l) (pretty l)
+ where
+  sub : Char -> Char
+  sub c = case c of
+    '0' => '₀'; '1' => '₁'; '2' => '₂'; '3' => '₃'; '4' => '₄'
+    '5' => '₅'; '6' => '₆'; '7' => '₇'; '8' => '₈'; '9' => '₉'; _ => c
+
 export %inline
 fromInteger : (x : Integer) -> (0 _ : So (x >= 0)) => Universe
 fromInteger x = U $ fromInteger x