From 1f2afb279e30b6020d95c6d60971eb5103c96c55 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sat, 30 Sep 2023 06:36:19 -0700
Subject: [PATCH] Add prettyprint, merge plicity types

---
 src/Lib/Parser.idr   |   5 +-
 src/Lib/Prettier.idr | 125 +++++++++++++++++++++++++++++++++++++++++++
 src/Main.idr         |  10 ++--
 3 files changed, 133 insertions(+), 7 deletions(-)
 create mode 100644 src/Lib/Prettier.idr

diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr
index 7135a24..820f59d 100644
--- a/src/Lib/Parser.idr
+++ b/src/Lib/Parser.idr
@@ -1,4 +1,5 @@
 module Lib.Parser
+import Lib.TT
 
 -- NEXT - need to sort out parsing implicits
 --
@@ -66,7 +67,7 @@ atom = withPos ( RVar <$> ident
     <|> parens term
 
 -- Argument to a Spine
-pArg : Parser (Plicity,Raw)
+pArg : Parser (Icit,Raw)
 pArg = (Explicit,) <$> atom <|> (Implicit,) <$> braces term
 
 --
@@ -123,7 +124,7 @@ letExpr = do
       t <- term
       pure (name,t)
 
-pLetArg : Parser (Plicity, String, Maybe Raw)
+pLetArg : Parser (Icit, String, Maybe Raw)
 pLetArg = (Implicit,,) <$> braces ident <*> optional (sym ":" >> typeExpr)
        <|> (Explicit,,) <$> parens ident <*> optional (sym ":" >> typeExpr)
        <|> (Explicit,,Nothing) <$> ident
diff --git a/src/Lib/Prettier.idr b/src/Lib/Prettier.idr
new file mode 100644
index 0000000..fdc1ec6
--- /dev/null
+++ b/src/Lib/Prettier.idr
@@ -0,0 +1,125 @@
+module Lib.Prettier
+
+import Data.String
+import Data.Nat
+
+-- A prettier printer, Wadler
+
+||| `Doc` is a pretty printing document.  Constructors are private, use
+||| methods below.  `Alt` in particular has some invariants on it, see paper
+||| for details. (Something along the lines of "the first line of left is not
+||| bigger than the first line of the right".)
+export
+data Doc = Empty | Line | Text String | Nest Nat Doc | Seq Doc Doc | Alt Doc Doc
+
+data DOC = EMPTY | TEXT String DOC | LINE Nat DOC
+
+
+flatten : Doc -> Doc
+flatten Empty = Empty
+flatten (Seq x y) = Seq (flatten x) (flatten y)
+flatten (Nest i x) = flatten x
+flatten Line = Text " "
+flatten (Text str) = Text str
+flatten (Alt x y) = flatten x
+
+group : Doc -> Doc
+group x = Alt (flatten x) x
+
+layout : DOC -> String
+layout EMPTY = ""
+layout (LINE k x) = "\n" ++ replicate k ' ' ++ layout x
+layout (TEXT str x) = str ++ layout x
+
+
+
+||| Whether a documents first line fits.
+fits : Nat -> DOC -> Bool
+fits w x = if w < 0 then False else case x of
+            EMPTY => True
+            (LINE k x) => True
+            (TEXT s x) => fits (w `minus` length s) x
+
+better : Nat -> Nat -> DOC -> DOC -> DOC
+better w k x y = if fits (w `minus` k) x then x else y
+
+be : Nat -> Nat -> List (Nat, Doc) -> DOC
+be w k [] = EMPTY
+be w k ((i, Empty) :: xs) = be w k xs
+be w k ((i, Line) :: xs) = LINE i (be w i xs)
+be w k ((i, (Text s)) :: xs) = TEXT s (be w (k + length s) xs)
+be w k ((i, (Nest j x)) :: xs) = be w k ((i+j,x)::xs)
+be w k ((i, (Seq x y)) :: xs) = be w k ((i,x) :: (i,y) :: xs)
+be w k ((i, (Alt x y)) :: xs) = better w k (be w k ((i,x)::xs))
+                                           (be w k ((i,y)::xs))
+
+best : Nat -> Nat -> Doc -> DOC
+best w k x = be w k [(0,x)]
+
+-- Public interface
+
+export
+pretty : Nat -> Doc-> String
+pretty w x = layout (best w 0 x)
+
+public export
+Semigroup Doc where x <+> y = Seq x (Seq (Text " ") y)
+
+-- Match System.File so we don't get warnings
+infixl 5 </>
+
+export
+line : Doc
+line = Line
+
+export
+text : String -> Doc
+text = Text
+
+export
+nest : Nat -> Doc -> Doc
+nest = Nest
+
+export
+(++) : Doc -> Doc -> Doc
+x ++ y = Seq x y
+
+export
+(</>) : Doc -> Doc -> Doc
+x </> y = x ++ line ++ y
+
+||| fold, but doesn't emit extra nil
+export
+folddoc : (Doc -> Doc -> Doc) -> List Doc -> Doc
+folddoc f [] = Empty
+folddoc f [x] = x
+folddoc f (x :: xs) = f x (folddoc f xs)
+
+||| separate with space
+export
+spread : List Doc -> Doc
+spread = folddoc (<+>)
+
+||| separate with new lines
+export
+stack : List Doc -> Doc
+stack = folddoc (</>)
+
+||| bracket x with l and r, indenting contents on new line
+export
+bracket : String -> Doc -> String -> Doc
+bracket l x r = group (text l ++ nest 2 (line ++ x) ++ line ++ text r)
+
+infixl 5 <+/>
+
+||| Either space or newline
+export
+(<+/>) : Doc -> Doc -> Doc
+x <+/> y = x ++ (text " " `Alt` line) ++ y
+
+||| Reformat some docs to fill. Not sure if I want this precise behavior or not.
+export
+fill : List Doc -> Doc
+fill [] = Empty
+fill [x] = x
+fill (x :: y :: xs) = (flatten x <+> fill (flatten y :: xs)) `Alt` (x </> fill (y :: xs))
diff --git a/src/Main.idr b/src/Main.idr
index 9be384d..07a7784 100644
--- a/src/Main.idr
+++ b/src/Main.idr
@@ -14,11 +14,11 @@ import Control.App
 import Syntax
 import Lib.Prettier
 
--- Put stuff in attic
--- Error printing
--- Review surface syntax
--- Prettier printer
--- First pass at typecheck
+-- [ ] Put stuff in attic
+-- [ ] Error printing
+-- [ ] Review surface syntax
+-- [x] Prettier printer
+-- [ ] First pass at typecheck
 -- Just do it in zoo order