From cd5d7c8207447a1a2dc78554288912d1950c9bf9 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Mon, 28 Oct 2024 17:30:38 +0000
Subject: Improve pretty printer.

---
 src/Inky/Type/Pretty.idr | 71 ++++++++++++++++++++++++++++++------------------
 1 file changed, 45 insertions(+), 26 deletions(-)

(limited to 'src/Inky/Type')

diff --git a/src/Inky/Type/Pretty.idr b/src/Inky/Type/Pretty.idr
index aaef606..ae80125 100644
--- a/src/Inky/Type/Pretty.idr
+++ b/src/Inky/Type/Pretty.idr
@@ -5,51 +5,70 @@ import Inky.Decidable
 import Inky.Type
 import Text.PrettyPrint.Prettyprinter
 
-arrowPrec, prodPrec, sumPrec, fixPrec, listPrec : Prec
-arrowPrec = Open
-prodPrec = Open
-sumPrec = Open
-fixPrec = Open
-listPrec = App
+public export
+data TyPrec = Atom | App | Open
+
+%name TyPrec d
+
+Eq TyPrec where
+  Atom == Atom = True
+  App == App = True
+  Open == Open = True
+  _ == _ = False
+
+Ord TyPrec where
+  compare Atom Atom = EQ
+  compare Atom App = LT
+  compare Atom Open = LT
+  compare App Atom = GT
+  compare App App = EQ
+  compare App Open = LT
+  compare Open Atom = GT
+  compare Open App = GT
+  compare Open Open = EQ
 
 export
-prettyType : {ctx : SnocList String} -> Ty ctx -> Prec -> Doc ann
-lessPrettyType : {ctx : SnocList String} -> Ty ctx -> Prec -> Doc ann
-lessPrettyTypeRow : {ctx : SnocList String} -> Context (Ty ctx) -> Prec -> List (Doc ann)
+prettyType : {ctx : SnocList String} -> Ty ctx -> TyPrec -> Doc ann
+lessPrettyType : {ctx : SnocList String} -> Ty ctx -> TyPrec -> Doc ann
+lessPrettyTypeCtx : {ctx : SnocList String} -> Context (Ty ctx) -> TyPrec -> SnocList (Doc ann)
 
 prettyType a d =
   if does (alpha {ctx2 = [<]} a TNat)
   then pretty "Nat"
   else case isList a of
     Just b =>
-      parenthesise (d >= listPrec) $ group $ align $ hang 2 $
+      group $ align $ hang 2 $ parenthesise (d < App) $
         pretty "List" <+> line <+>
-        prettyType (assert_smaller a b) d
+        prettyType (assert_smaller a b) Atom
     Nothing => lessPrettyType a d
 
 lessPrettyType (TVar i) d = pretty (unVal $ nameOf i)
 lessPrettyType (TArrow a b) d =
-  parenthesise (d > arrowPrec) $ group $ align $ hang 2 $
+  group $ align $ parenthesise (d < Open) $
     let parts = stripArrow b in
-    concatWith (surround $ neutral <++> "->" <+> line) (prettyType a arrowPrec :: parts)
+    concatWith (surround $ neutral <++> "->" <+> line) (prettyType a App :: parts)
   where
   stripArrow : Ty ctx -> List (Doc ann)
-  stripArrow (TArrow a b) = prettyType a arrowPrec :: stripArrow b
-  stripArrow a = [prettyType a arrowPrec]
+  stripArrow (TArrow a b) = prettyType a App :: stripArrow b
+  stripArrow a = [prettyType a App]
 lessPrettyType (TProd (MkRow as _)) d =
-  enclose "<" ">" $ group $ align $ hang 2 $
-    let parts = lessPrettyTypeRow as prodPrec in
-    concatWith (surround $ "," <+> line) parts
+  let parts = lessPrettyTypeCtx as Open <>> [] in
+  group $ align $ enclose "<" ">" $
+    flatAlt
+      (neutral <++> concatWith (surround $ line' <+> "," <++> neutral) parts <+> line)
+      (concatWith (surround $ "," <++> neutral) parts)
 lessPrettyType (TSum (MkRow as _)) d =
-  enclose "[" "]" $ group $ align $ hang 2 $
-    let parts = lessPrettyTypeRow as prodPrec in
-    concatWith (surround $ "," <+> line) parts
+  let parts = lessPrettyTypeCtx as Open <>> [] in
+  group $ align $ enclose "[" "]" $
+    flatAlt
+      (neutral <++> concatWith (surround $ line' <+> "," <++> neutral) parts <+> line)
+      (concatWith (surround $ "," <++> neutral) parts)
 lessPrettyType (TFix x a) d =
-  parens $ group $ align $ hang 2 $
+  group $ align $ hang 2 $ parens $
     "\\" <+> pretty x <++> "=>" <+> line <+>
-    prettyType a fixPrec
+    prettyType a Open
 
-lessPrettyTypeRow [<] d = []
-lessPrettyTypeRow (as :< (x :- a)) d =
+lessPrettyTypeCtx [<] d = [<]
+lessPrettyTypeCtx (as :< (x :- a)) d =
+  lessPrettyTypeCtx as d :<
   (group $ align $ hang 2 $ pretty x <+> ":" <+> line <+> prettyType a d)
-  :: lessPrettyTypeRow as d
-- 
cgit v1.2.3