From 9767d929529ff7752d173e732f2e0adcbaa1110b Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Fri, 15 Nov 2024 19:13:42 -0800 Subject: [PATCH] more tweaks to pretty printing. --- src/Lib/Compile.idr | 4 ---- src/Lib/CompileExp.idr | 1 + src/Lib/Elab.idr | 2 +- src/Lib/Eval.idr | 2 +- src/Lib/Prettier.idr | 10 ++++++++++ src/Lib/ProcessDecl.idr | 7 ++++--- src/Lib/Types.idr | 37 ++++++++++++++++++++++--------------- 7 files changed, 39 insertions(+), 24 deletions(-) diff --git a/src/Lib/Compile.idr b/src/Lib/Compile.idr index c1ad233..c66a41d 100644 --- a/src/Lib/Compile.idr +++ b/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 diff --git a/src/Lib/CompileExp.idr b/src/Lib/CompileExp.idr index 515d455..0e03921 100644 --- a/src/Lib/CompileExp.idr +++ b/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 diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index ec943cb..06101bb 100644 --- a/src/Lib/Elab.idr +++ b/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 diff --git a/src/Lib/Eval.idr b/src/Lib/Eval.idr index 93789f7..edc09ed 100644 --- a/src/Lib/Eval.idr +++ b/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. diff --git a/src/Lib/Prettier.idr b/src/Lib/Prettier.idr index cf99175..fefbb17 100644 --- a/src/Lib/Prettier.idr +++ b/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 diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index b7ec37f..d72ec74 100644 --- a/src/Lib/ProcessDecl.idr +++ b/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 diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index f97cd66..380eb12 100644 --- a/src/Lib/Types.idr +++ b/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 names tm = render 80 $ go 0 names tm +pprint : List String -> Tm -> Doc +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 (CaseLit lit t) = text (show lit) <+> "=>" <+/> go p names t + goAlt p names (CaseCons name args t) = text name <+> spread (map text args) <+> (nest 2 $ "=>" <+/> go p (reverse args ++ 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) = - text "({{" <+> text nm <+> ":" <+> go p names t <+> "}}" <+> "->" <+> go p (nm :: names) u <+> ")" - go p names (Pi _ nm Implicit t u) = - text "({" <+> text nm <+> ":" <+> go p names t <+> "}" <+> "->" <+> go p (nm :: names) u <+> ")" - go p names (Pi _ nm Explicit t u) = - text "((" <+> text nm <+> ":" <+> go p names t <+> ")" <+> "->" <+> go p (nm :: names) u <+> ")" + go p names (Pi _ nm Auto t u) = parens 0 p $ + text "{{" <+> text nm <+> ":" <+> go 0 names t <+> "}}" <+> "->" <+> go 0 (nm :: names) u + go p names (Pi _ nm Implicit t u) = parens 0 p $ + text "{" <+> text nm <+> ":" <+> go 0 names t <+> "}" <+> "->" <+> go 0 (nm :: names) u + go p names (Pi _ "_" Explicit t 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