From 40fde928236694e48e8e7a5c6251816dc30ae0b9 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Thu, 23 Dec 2021 15:50:19 +0100
Subject: [PATCH] change printing of binders

old: (1 | 1 | x : A) ->
new: (x @ 1, 1 : A) ->
---
 src/Quox/Syntax/Qty.idr  | 9 +++++++--
 src/Quox/Syntax/Term.idr | 5 +++--
 2 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/src/Quox/Syntax/Qty.idr b/src/Quox/Syntax/Qty.idr
index 3cec218..f27643f 100644
--- a/src/Quox/Syntax/Qty.idr
+++ b/src/Quox/Syntax/Qty.idr
@@ -27,11 +27,16 @@ PrettyHL Qty where
       One  => ifUnicode "𝟭" "1"
       Any  => ifUnicode "𝛚" "*"
 
+private
+commas : List (Doc HL) -> List (Doc HL)
+commas [] = []
+commas [x] = [x]
+commas (x::xs) = (x <+> hl Delim ",") :: commas xs
+
 export %inline
 prettyQtyBinds : Pretty.HasEnv m => List Qty -> m (Doc HL)
 prettyQtyBinds =
-  map (align . sep) .
-  traverse (\pi => [|pretty0M pi <++> pure (hl Delim "|")|])
+  map ((hl Delim "@" <++>) . align . sep . commas) . traverse pretty0M
 
 
 public export
diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
index b1441c5..c9461ae 100644
--- a/src/Quox/Syntax/Term.idr
+++ b/src/Quox/Syntax/Term.idr
@@ -172,8 +172,9 @@ mutual
   prettyBinder : Pretty.HasEnv m => List Qty -> Name -> Term d n -> m (Doc HL)
   prettyBinder pis x a =
     pure $ parens $ hang 2 $
-      !(prettyQtyBinds pis) <//>
-      hsep [hl TVar !(prettyM x), colonD, !(withPrec Outer $ prettyM a)]
+      hsep [hl TVar !(prettyM x),
+            sep [!(prettyQtyBinds pis),
+                 hsep [colonD, !(withPrec Outer $ prettyM a)]]]
 
 
 export FromVar (Elim d) where fromVar = B