more tweaks to pretty printing.

src/Lib/Compile.idr

@@ -188,10 +188,6 @@ jsIdent id = if elem id keywords then text ("$" ++ id) else text $ pack $ fix (u
 
 stmtToDoc : JSStmt e -> Doc
 
-||| separate with space
-export
-commaSep : List Doc -> Doc
-commaSep = folddoc (\a, b => a ++ "," <+/> b)
 
 expToDoc : JSExp -> Doc
 expToDoc (LitArray xs) = ?expToDoc_rhs_0

src/Lib/CompileExp.idr

@@ -8,6 +8,7 @@ import Data.List
 
 import Lib.Types -- Name / Tm
 import Lib.TopContext
+import Lib.Prettier
 import Lib.Eval -- lookupMeta
 import Lib.Util
 

src/Lib/Elab.idr

@@ -43,7 +43,7 @@ dumpCtx ctx = do
   pure msg
 
 
-pprint : Context -> Val -> M String
+pprint : Context -> Val -> M Doc
 pprint ctx v = pure $ pprint (names ctx) !(quote (length ctx.env) v)
 
 ||| return Bnd and type for name

src/Lib/Eval.idr

@@ -204,7 +204,7 @@ nfv env t = quote (length env) !(eval env CBV t)
 
 export
 prvalCtx : {auto ctx : Context} -> Val -> M String
-prvalCtx v = pure $ pprint (toList $ map fst ctx.types) !(quote ctx.lvl v)
+prvalCtx v = pure $ interpolate $ pprint (toList $ map fst ctx.types) !(quote ctx.lvl v)
 
 -- REVIEW - might be easier if we inserted the meta without a bunch of explicit App
 -- I believe Kovacs is doing that.

src/Lib/Prettier.idr

@@ -138,6 +138,16 @@ fill [] = Empty
 fill [x] = x
 fill (x :: y :: xs) = (flatten x <+> fill (flatten y :: xs)) `Alt` (x </> fill (y :: xs))
 
+||| separate with space
+export
+commaSep : List Doc -> Doc
+commaSep = folddoc (\a, b => a ++ text "," <+/> b)
+
 public export
 FromString Doc where
   fromString = text
+
+||| If we stick Doc into a String, try to avoid line-breaks via `flatten`
+public export
+Interpolation Doc where
+  interpolate = render 80 . flatten

src/Lib/ProcessDecl.idr

@@ -106,7 +106,7 @@ solveAutos mlen ((Unsolved fc k ctx ty AutoSolve _) :: es) = do
             [] => findMatches ctx ty top.defs
             xs => pure xs
         | res => do
-          debug "FAILED to solve \{show ty}, matches: \{show $ map (pprint [] . fst) res}"
+          debug "FAILED to solve \{show ty}, matches: \{commaSep $ map (pprint [] . fst) res}"
           solveAutos mlen es
         -- | res => error fc "FAILED to solve \{show ty}, matches: \{show $ map (pprint [] . fst) res}"
       writeIORef top.metas mc
@@ -166,7 +166,7 @@ processDecl (PMixFix{})  = pure ()
 
 processDecl (TypeSig fc names tm) = do
   putStrLn "-----"
-  putStrLn "TypeSig \{unwords names} : \{show tm}"
+
   top <- get
   mc <- readIORef top.metas
   let mstart = length mc.metas
@@ -175,6 +175,7 @@ processDecl (TypeSig fc names tm) = do
       | _ => error fc "\{show nm} is already defined"
     pure ()
   ty <- check (mkCtx top.metas fc) tm (VU fc)
+  putStrLn "TypeSig \{unwords names} : \{pprint [] ty}"
   debug "got \{pprint [] ty}"
   for_ names $ \nm => setDef nm fc ty Axiom
   -- Zoo4eg has metas in TypeSig, need to decide if I want to support leaving them unsolved here
@@ -220,7 +221,7 @@ processDecl (Def fc nm clauses) = do
   -- Day1.newt is a test case
   -- tm' <- nf [] tm
   tm' <- zonk top 0 [] tm
-  putStrLn "NF\n\{pprint[] tm'}"
+  putStrLn "NF\n\{render 80 $ pprint[] tm'}"
   debug "Add def \{nm} \{pprint [] tm'} : \{pprint [] ty}"
   updateDef nm fc ty (Fn tm')
   logMetas mstart

src/Lib/Types.idr

@@ -2,7 +2,7 @@ module Lib.Types
 
 -- For FC, Error
 import public Lib.Common
-import Lib.Prettier
+import public Lib.Prettier
 
 import public Control.Monad.Error.Either
 import public Control.Monad.Error.Interface
@@ -169,10 +169,16 @@ Eq (Tm) where
   _ == _ = False
 
 
+
+-- TODO App and Lam should have <+/> but we need to fix
+-- INFO pprint to `nest 2 ...`
+-- maybe return Doc and have an Interpolation..
+-- If we need to flatten, case is going to get in the way.
+
 ||| Pretty printer for Tm.
 export
-pprint : List String -> Tm -> String
+pprint : List String -> Tm -> Doc
-pprint names tm = render 80 $ go 0 names tm
+pprint names tm = go 0 names tm
   where
     parens : Nat -> Nat -> Doc -> Doc
     parens a b doc = if a < b
@@ -183,8 +189,9 @@ pprint names tm = render 80 $ go 0 names tm
     goAlt : Nat -> List String -> CaseAlt -> Doc
 
     goAlt p names (CaseDefault t) = "_" <+> "=>" <+> go p ("_" :: names) t
-    goAlt p names (CaseCons name args t) = text name <+> spread (map text args) <+> "=>" <+/> go p (reverse args ++ names) t
+    goAlt p names (CaseCons name args t) = text name <+> spread (map text args) <+> (nest 2 $ "=>" <+/> go p (reverse args ++ names) t)
-    goAlt p names (CaseLit lit t) = text (show lit) <+> "=>" <+/> go p names t
+    -- `;` is not in surface syntax, but sometimes we print on one line
+    goAlt p names (CaseLit lit t) = text (show lit) <+> (nest 2 $ "=>" <+/> go p names t ++ ";")
 
     go p names (Bnd _ k) = case getAt k names of
       -- Either a bug or we're printing without names
@@ -192,22 +199,22 @@ pprint names tm = render 80 $ go 0 names tm
       Just nm => text "\{nm}:\{show k}"
     go p names (Ref _ str mt) = text str
     go p names (Meta _ k) = text "?m:\{show k}"
-    go p names (Lam _ nm t) = parens 0 p $ text "\\ \{nm} =>" <+> go 0 (nm :: names) t
+    go p names (Lam _ nm t) = parens 0 p $ nest 2 $ text "\\ \{nm} =>" <+/> go 0 (nm :: names) t
     go p names (App _ t u) = parens 0 p $ go 0 names t <+> go 1 names u
     go p names (U _) = "U"
-    go p names (Pi _ nm Auto t u) =
+    go p names (Pi _ nm Auto t u) = parens 0 p $
-      text "({{" <+> text nm <+> ":" <+> go p names t <+> "}}" <+> "->" <+> go p (nm :: names) u <+> ")"
+      text "{{" <+> text nm <+> ":" <+> go 0 names t <+> "}}" <+> "->" <+> go 0 (nm :: names) u
-    go p names (Pi _ nm Implicit t u) =
+    go p names (Pi _ nm Implicit t u) = parens 0 p $
-      text "({" <+> text nm <+> ":" <+> go p names t <+> "}" <+> "->" <+> go p (nm :: names) u <+> ")"
+      text "{" <+> text nm <+> ":" <+> go 0 names t <+> "}" <+> "->" <+> go 0 (nm :: names) u
-    go p names (Pi _ nm Explicit t u) =
+    go p names (Pi _ "_" Explicit t u) =
-      text "((" <+> text nm <+> ":" <+> go p names t <+> ")" <+> "->" <+> go p (nm :: names) u <+> ")"
+      parens 0 p $ go 1 names t <+> "->" <+> go 0 ("_" :: names) u
+    go p names (Pi _ nm Explicit t u) = parens 0 p $
+      text "(" ++ text nm <+> ":" <+> go 0 names t ++ ")" <+> "->" <+> go 0 (nm :: names) u
     -- FIXME - probably way wrong on the names here.  There is implicit binding going on
     go p names (Case _ sc alts) = parens 0 p $ text "case" <+> go 0 names sc <+> text "of" ++ (nest 2 (line ++ stack (map (goAlt 0 names) alts)))
     go p names (Lit _ lit) = text (show lit)
-    go p names (Let _ nm t u) = parens 0 p $ text "let" <+> text nm <+> ":=" <+> go 0 names t </> (nest 2 $ go 0 (nm :: names) u)
+    go p names (Let _ nm t u) = parens 0 p $ text "let" <+> text nm <+> ":=" <+> go 0 names t <+> "in" </> (nest 2 $ go 0 (nm :: names) u)
 
--- public export
--- data Closure : Nat -> Type
 data Val : Type