Improve pretty printer.

2 files changed, 153 insertions, 94 deletions

diff --git a/src/Inky/Term/Pretty.idr b/src/Inky/Term/Pretty.idr
index a9055d4..91a42b8 100644
--- a/src/Inky/Term/Pretty.idr
+++ b/src/Inky/Term/Pretty.idr
@@ -1,32 +1,54 @@
 module Inky.Term.Pretty
 
 import Data.Singleton
+import Data.String
 
 import Inky.Decidable.Maybe
 import Inky.Term
 import Inky.Type.Pretty
 import Text.PrettyPrint.Prettyprinter
 
-appPrec, prjPrec, unrollPrec, annotPrec,
-  letPrec, absPrec, injPrec, tupPrec, casePrec, rollPrec, foldPrec : Prec
-appPrec = App
-prjPrec = User 9
-unrollPrec = PrefixMinus
-annotPrec = Equal
-letPrec = Open
-absPrec = Open
-injPrec = App
-tupPrec = Open
-casePrec = Open
-rollPrec = PrefixMinus
-foldPrec = Open
+public export
+data TermPrec = Atom | Prefix | Suffix | App | Annot | Open
+
+%name TermPrec d
+
+Eq TermPrec where
+  Atom == Atom = True
+  Prefix == Prefix = True
+  Suffix == Suffix = True
+  App == App = True
+  Annot == Annot = True
+  Open == Open = True
+  _ == _ = False
+
+Ord TermPrec where
+  compare Atom Atom = EQ
+  compare Atom d2 = LT
+  compare Prefix Atom = GT
+  compare Prefix Prefix = EQ
+  compare Prefix d2 = LT
+  compare Suffix Atom = GT
+  compare Suffix Prefix = GT
+  compare Suffix Suffix = EQ
+  compare Suffix d2 = LT
+  compare App App = EQ
+  compare App Annot = LT
+  compare App Open = LT
+  compare App d2 = GT
+  compare Annot Annot = EQ
+  compare Annot Open = LT
+  compare Annot d2 = GT
+  compare Open Open = EQ
+  compare Open d2 = GT
 
 export
-prettyTerm : {tyCtx, tmCtx : SnocList String} -> Term tyCtx tmCtx -> Prec -> Doc ann
-prettyAllTerm : {tyCtx, tmCtx : SnocList String} -> List (Term tyCtx tmCtx) -> Prec -> List (Doc ann)
-prettyTermCtx : {tyCtx, tmCtx : SnocList String} -> Context (Term tyCtx tmCtx) -> Prec -> SnocList (Doc ann)
+prettyTerm : {tyCtx, tmCtx : SnocList String} -> Term tyCtx tmCtx -> TermPrec -> Doc ann
+prettyAllTerm : {tyCtx, tmCtx : SnocList String} -> List (Term tyCtx tmCtx) -> TermPrec -> List (Doc ann)
+prettyTermCtx : {tyCtx, tmCtx : SnocList String} -> Context (Term tyCtx tmCtx) -> TermPrec -> SnocList (Doc ann)
 prettyCases : {tyCtx, tmCtx : SnocList String} -> Context (x ** Term tyCtx (tmCtx :< x)) -> SnocList (Doc ann)
-lessPrettyTerm : {tyCtx, tmCtx : SnocList String} -> Term tyCtx tmCtx -> Prec -> Doc ann
+prettyLet : Doc ann -> Doc ann -> Doc ann
+lessPrettyTerm : {tyCtx, tmCtx : SnocList String} -> Term tyCtx tmCtx -> TermPrec -> Doc ann
 
 prettyTerm t d =
   case isLit t <|> isCheckLit t of
@@ -43,88 +65,106 @@ prettyTermCtx [<] d = [<]
 prettyTermCtx (ts :< (l :- t)) d = prettyTermCtx ts d :< (pretty l <+> ":" <++> prettyTerm t d)
 
 prettyCases [<] = [<]
+prettyCases (ts :< (l :- (x ** Abs (bound ** t)))) =
+  prettyCases ts :<
+  (group $ align $
+    pretty l <++> pretty x <++> "=>" <++>
+      "\\" <+> concatWith (surround $ "," <++> neutral) (map pretty bound) <++> "=>" <+> line <+>
+    prettyTerm t Open)
 prettyCases (ts :< (l :- (x ** t))) =
-  prettyCases ts :< (pretty l <++> pretty x <++> "=>" <++> prettyTerm t Open)
+  prettyCases ts :<
+  (group $ align $
+    pretty l <++> pretty x <++> "=>" <+> line <+>
+    prettyTerm t Open)
 
+prettyLet binding term =
+  (group $
+    pretty "let" <++>
+    (group $ hang (-2) $ binding) <+> line <+>
+    "in") <+> line <+>
+  term
 
 lessPrettyTerm (Annot t a) d =
-  parenthesise (d > annotPrec) $ group $ align $ hang 2 $
-    prettyTerm t annotPrec <++> ":" <+> line <+> prettyType a annotPrec
+  group $ align $ hang 2 $ parenthesise (d < Annot) $
+    prettyTerm t App <++> ":" <+> line <+> prettyType a Open
 lessPrettyTerm (Var i) d = pretty (unVal $ nameOf i)
 lessPrettyTerm (Let e (x ** t)) d =
-  parenthesise (d > letPrec) $ group $ align $
-    (group $ align $ hang 2 $
-      pretty x <++> "=" <+> line <+> prettyTerm e letPrec
-    ) <+> line <+>
-    "in" <+> line <+>
-    prettyTerm t letPrec
+  -- TODO: pretty print annotated abstraction
+  group $ align $ parenthesise (d < Open) $
+  prettyLet
+    (pretty x <++> "=" <+> line <+> prettyTerm e Open)
+    (prettyTerm t Open)
 lessPrettyTerm (LetTy a (x ** t)) d =
-  parenthesise (d > letPrec) $ group $ align $
-    (group $ align $ hang 2 $
-      pretty x <++> "=" <+> line <+> prettyType a letPrec
-    ) <+> line <+>
-    "in" <+> line <+>
-    prettyTerm t letPrec
+  group $ align $ parenthesise (d < Open) $
+  prettyLet
+    (pretty x <++> "=" <+> line <+> prettyType a Open)
+    (prettyTerm t Open)
 lessPrettyTerm (Abs (bound ** t)) d =
-  parenthesise (d > absPrec) $ group $ hang 2 $
+  group $ hang 2 $ parenthesise (d < Open) $
     "\\" <+> concatWith (surround $ "," <+> line) (map pretty bound) <++> "=>" <+> line <+>
-    prettyTerm t absPrec
+    prettyTerm t Open
 lessPrettyTerm (App (Map (x ** a) b c) ts) d =
-  parenthesise (d >= appPrec) $ group $ align $ hang 2 $
+  group $ align $ hang 2 $ parenthesise (d < App) $
     concatWith (surround line)
       (  pretty "map"
-      :: parens (group $ align $ hang 2 $ "\\" <+> pretty x <+> "=>" <+> line <+> prettyType a Open)
-      :: prettyType b appPrec
-      :: prettyType c appPrec
-      :: prettyAllTerm ts appPrec)
+      :: parens (group $ align $ hang 2 $ "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open)
+      :: prettyType b Atom
+      :: prettyType c Atom
+      :: prettyAllTerm ts Suffix)
 lessPrettyTerm (App (GetChildren (x ** a) b) ts) d =
-  parenthesise (d >= appPrec) $ group $ align $ hang 2 $
+  group $ align $ hang 2 $ parenthesise (d < App) $
     concatWith (surround line)
       (  pretty "getChildren"
-      :: parens (group $ align $ hang 2 $ "\\" <+> pretty x <+> "=>" <+> line <+> prettyType a Open)
-      :: prettyType b appPrec
-      :: prettyAllTerm ts appPrec)
+      :: parens (group $ align $ hang 2 $ "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open)
+      :: prettyType b Atom
+      :: prettyAllTerm ts Suffix)
 lessPrettyTerm (App f ts) d =
-  parenthesise (d >= appPrec) $ group $ align $ hang 2 $
-    concatWith (surround line) (prettyTerm f appPrec :: prettyAllTerm ts appPrec)
+  group $ align $ hang 2 $ parenthesise (d < App) $
+    concatWith (surround line) (prettyTerm f Suffix :: prettyAllTerm ts Suffix)
 lessPrettyTerm (Tup (MkRow ts _)) d =
-  enclose "<" ">" $ group $ align $ hang 2 $
-    concatWith (surround $ "<" <+> line) (prettyTermCtx ts tupPrec <>> [])
+  let parts = prettyTermCtx ts Open <>> [] in
+  group $ align $ enclose "<" ">" $
+    flatAlt
+      (neutral <++> concatWith (surround $ line' <+> "," <++> neutral) parts <+> line)
+      (concatWith (surround $ "," <++> neutral) parts)
 lessPrettyTerm (Prj e l) d =
-  parenthesise (d > prjPrec) $ group $ align $ hang 2 $
-    prettyTerm e prjPrec <+> line' <+> "." <+> pretty l
+  group $ align $ hang 2 $ parenthesise (d < Suffix) $
+    prettyTerm e Suffix <+> line' <+> "." <+> pretty l
 lessPrettyTerm (Inj l t) d =
-  parenthesise (d >= injPrec) $ group $ align $ hang 2 $
-    pretty l <+> line <+> prettyTerm t absPrec
+  group $ align $ hang 2 $ parenthesise (d < App) $
+    pretty l <+> line <+> prettyTerm t Suffix
 lessPrettyTerm (Case e (MkRow ts _)) d =
-  parenthesise (d > casePrec) $ group $ align $ hang 2 $
-    "case" <++> prettyTerm e casePrec <++> "of" <+> hardline <+>
-    (braces $ group $ align $ hang 2 $
-      concatWith (surround $ ";" <+> hardline) $
-      prettyCases ts <>> [])
+  let parts = prettyCases ts <>> [] in
+  group $ align $ hang 2 $ parenthesise (d < Open) $
+    (group $ hang (-2) $ "case" <++> prettyTerm e Open <+> line <+> "of") <+> line <+>
+    (braces $
+      flatAlt
+        (neutral <++> concatWith (surround $ line' <+> ";" <++> neutral) parts <+> line)
+        (concatWith (surround $ ";" <++> neutral) parts))
 lessPrettyTerm (Roll t) d =
   pretty "~" <+>
-  (parenthesise (d > rollPrec) $ group $ align $ hang 2 $ prettyTerm t rollPrec)
+  parenthesise (d < Prefix) (group $ align $ hang 2 $ prettyTerm t Prefix)
 lessPrettyTerm (Unroll e) d =
   pretty "!" <+>
-  (parenthesise (d > unrollPrec) $ group $ align $ hang 2 $ prettyTerm e unrollPrec)
+  parenthesise (d > Prefix) (group $ align $ hang 2 $ prettyTerm e Prefix)
 lessPrettyTerm (Fold e (x ** t)) d =
-  parenthesise (d > foldPrec) $ group $ align $ hang 2 $
-    "fold" <++> prettyTerm e foldPrec <++> "by" <+> hardline <+>
-    (parens $ group $ align $ hang 2 $
+  -- TODO: foldcase
+  group $ align $ hang 2 $ parenthesise (d < Open) $
+    "fold" <++> prettyTerm e Open <++> "by" <+> hardline <+>
+    (group $ align $ hang 2 $ parens $
       "\\" <+> pretty x <++> "=>" <+> line <+> prettyTerm t Open)
 lessPrettyTerm (Map (x ** a) b c) d =
-  parenthesise (d >= appPrec) $ group $ align $ hang 2 $
+  group $ align $ hang 2 $ parenthesise (d < App) $
     concatWith (surround line)
       [ pretty "map"
-      , parens (group $ align $ hang 2 $ "\\" <+> pretty x <+> "=>" <+> line <+> prettyType a Open)
-      , prettyType b appPrec
-      , prettyType c appPrec
+      , group (align $ hang 2 $ parens $  "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open)
+      , prettyType b Atom
+      , prettyType c Atom
       ]
 lessPrettyTerm (GetChildren (x ** a) b) d =
-  parenthesise (d >= appPrec) $ group $ align $ hang 2 $
+  group $ align $ hang 2 $ parenthesise (d < App) $
     concatWith (surround line)
       [ pretty "getChildren"
-      , parens (group $ align $ hang 2 $ "\\" <+> pretty x <+> "=>" <+> line <+> prettyType a Open)
-      , prettyType b appPrec
+      , group (align $ hang 2 $ parens $  "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open)
+      , prettyType b Atom
       ]
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