From 7e3a8e72bd94c4b5c47cb15b3990c29b71eed944 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 26 Mar 2023 14:41:36 +0200
Subject: [PATCH] clean up printing of contexts
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- just π.x : A instead of π.(x : A)
- skip the " |" if the dctx is empty
---
 lib/Quox/Typing/Context.idr | 21 ++++++++++++++++-----
 1 file changed, 16 insertions(+), 5 deletions(-)

diff --git a/lib/Quox/Typing/Context.idr b/lib/Quox/Typing/Context.idr
index d9eef60..0db97ad 100644
--- a/lib/Quox/Typing/Context.idr
+++ b/lib/Quox/Typing/Context.idr
@@ -199,6 +199,13 @@ namespace EqContext
   injectE (MkEqContext {termLen = Val n, _}) el = el // shift0 n
 
 
+private
+data CtxBinder a = MkCtxBinder BaseName a
+
+PrettyHL a => PrettyHL (CtxBinder a) where
+  prettyM (MkCtxBinder x t) = pure $
+    sep [hsep [!(pretty0M $ TV x), colonD], !(pretty0M t)]
+
 parameters {auto _ : (Eq q, PrettyHL q, IsQty q)} (unicode : Bool)
   private
   pipeD : Doc HL
@@ -210,17 +217,21 @@ parameters {auto _ : (Eq q, PrettyHL q, IsQty q)} (unicode : Bool)
     go : QContext q m -> NContext m -> TContext q d m -> SnocList (Doc HL)
     go [<]       [<]       [<] = [<]
     go (qs :< q) (xs :< x) (ctx :< t) =
-      let bind = MkWithQty q $ MkBinder x t in
+      let bind = MkWithQty q $ MkCtxBinder x t in
       go qs xs ctx :< runPretty unicode (pretty0M bind)
 
   export covering
   prettyTyContext : TyContext q d n -> Doc HL
   prettyTyContext (MkTyContext dctx dnames tctx tnames qtys) =
-    sep [prettyDimEq dnames dctx <++> pipeD,
-         prettyTContext qtys tnames tctx]
+    case dctx of
+      C [<] => prettyTContext qtys tnames tctx
+      _     => sep [prettyDimEq dnames dctx <++> pipeD,
+                    prettyTContext qtys tnames tctx]
 
   export covering
   prettyEqContext : EqContext q n -> Doc HL
   prettyEqContext (MkEqContext dassign dnames tctx tnames qtys) =
-    sep [prettyDimEq dnames (fromGround dassign) <++> pipeD,
-         prettyTContext qtys tnames tctx]
+    case dassign of
+      [<] => prettyTContext qtys tnames tctx
+      _   => sep [prettyDimEq dnames (fromGround dassign) <++> pipeD,
+                  prettyTContext qtys tnames tctx]