20b02c5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1547 from david-christiansen/pprint-command

New command :pprint for outputting paper/slide bits

commit20b02c59964ae242c9b9e49ccbe5252647cd166e authorDavid Christiansen <david@davidchristiansen.dk> dateWed 24 Sep 2014, 23:32 (12 years ago) parent38fd2b0 b7010b2

5 files changed+156−24

compare with master

unifiedsplit

CHANGELOG+2 src/Idris/AbsSyntaxTree.hs+3 src/Idris/Output.hs+96−1 src/Idris/REPL.hs+43−23 src/Idris/REPLParser.hs+12

CHANGELOG+2

@@ -18,6 +18,8 @@ New in 0.9.15:

1818 to DSL authors.

1919* The Java and LLVM backends have been factored out for separate maintenance. Now, the

2020 compiler distribution only ships with the C and JavaScript backends.

21+* New REPL command :printdef displays the internal definition of a name

22+* New REPL command :pprint pretty-prints a definition or term with LaTeX or HTML highlighting

2123

2224New in 0.9.14:

2325--------------

src/Idris/AbsSyntaxTree.hs+3

@@ -364,6 +364,9 @@ data Command = Quit

364364 | MakeDoc String -- IdrisDoc

365365 | Warranty

366366 | PrintDef Name

367+ | PPrint OutputFmt Int PTerm

368+

369+data OutputFmt = HTMLOutput | LaTeXOutput

367370

368371data Opt = Filename String

369372 | Quiet

src/Idris/Output.hs+96−1

@@ -1,3 +1,5 @@

1+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

13module Idris.Output where

35import Idris.Core.TT

@@ -13,10 +15,12 @@ import Util.ScreenSize (getScreenWidth)

1315

1416import Debug.Trace

1517

18+import Control.Monad.Error (throwError)

19+

1620import System.IO (stdout, Handle, hPutStrLn)

1721

1822import Data.Char (isAlpha)

19−import Data.List (nub)

23+import Data.List (nub, intersperse)

2024import Data.Maybe (fromMaybe)

2125

2226pshow :: IState -> Err -> String

@@ -170,3 +174,94 @@ printUndefinedNames :: [Name] -> Doc OutputAnnotation

170174printUndefinedNames ns = text "Undefined " <> names <> text "."

171175 where names = encloseSep empty empty (char ',') $ map ppName ns

172176 ppName = prettyName True True []

177+

178+renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String

179+renderExternal fmt width doc

180+ | width < 1 = throwError . Msg $ "There must be at least one column for the pretty-printer."

181+ | otherwise =

182+ do ist <- getIState

183+ return . wrap fmt .

184+ displayDecorated (decorate fmt) .

185+ renderPretty 1.0 width .

186+ fmap (fancifyAnnots ist) $

187+ doc

188+ where

189+ decorate _ (AnnFC _) = id

190+

191+ decorate HTMLOutput (AnnName _ (Just TypeOutput) d _) =

192+ tag "idris-type" d

193+ decorate HTMLOutput (AnnName _ (Just FunOutput) d _) =

194+ tag "idris-function" d

195+ decorate HTMLOutput (AnnName _ (Just DataOutput) d _) =

196+ tag "idris-data" d

197+ decorate HTMLOutput (AnnName _ (Just MetavarOutput) d _) =

198+ tag "idris-metavar" d

199+ decorate HTMLOutput (AnnName _ (Just PostulateOutput) d _) =

200+ tag "idris-postulate" d

201+ decorate HTMLOutput (AnnName _ _ _ _) = id

202+ decorate HTMLOutput (AnnBoundName _ True) = tag "idris-bound idris-implicit" Nothing

203+ decorate HTMLOutput (AnnBoundName _ False) = tag "idris-bound" Nothing

204+ decorate HTMLOutput (AnnConst _) = id -- TODO

205+ decorate HTMLOutput (AnnData _ _) = tag "idris-data" Nothing

206+ decorate HTMLOutput (AnnType _ _) = tag "idris-type" Nothing

207+ decorate HTMLOutput AnnKeyword = tag "idris-keyword" Nothing

208+ decorate HTMLOutput (AnnTextFmt _) = id -- TODO

209+ decorate HTMLOutput (AnnTerm _ _) = id

210+ decorate HTMLOutput (AnnSearchResult _) = id

211+

212+ decorate LaTeXOutput (AnnName _ (Just TypeOutput) _ _) =

213+ latex "IdrisType"

214+ decorate LaTeXOutput (AnnName _ (Just FunOutput) _ _) =

215+ latex "IdrisFunction"

216+ decorate LaTeXOutput (AnnName _ (Just DataOutput) _ _) =

217+ latex "IdrisData"

218+ decorate LaTeXOutput (AnnName _ (Just MetavarOutput) _ _) =

219+ latex "IdrisMetavar"

220+ decorate LaTeXOutput (AnnName _ (Just PostulateOutput) _ _) =

221+ latex "IdrisPostulate"

222+ decorate LaTeXOutput (AnnName _ _ _ _) = id

223+ decorate LaTeXOutput (AnnBoundName _ True) = latex "IdrisImplicit"

224+ decorate LaTeXOutput (AnnBoundName _ False) = latex "IdrisBound"

225+ decorate LaTeXOutput (AnnConst _) = id -- TODO

226+ decorate LaTeXOutput (AnnData _ _) = latex "IdrisData"

227+ decorate LaTeXOutput (AnnType _ _) = latex "IdrisType"

228+ decorate LaTeXOutput AnnKeyword = latex "IdrisKeyword"

229+ decorate LaTeXOutput (AnnTextFmt _) = id -- TODO

230+ decorate LaTeXOutput (AnnTerm _ _) = id

231+ decorate LaTeXOutput (AnnSearchResult _) = id

232+

233+ tag cls docs str = "<span class=\""++cls++"\""++title++">" ++ str ++ "</span>"

234+ where title = maybe "" (\d->" title=\"" ++ d ++ "\"") docs

235+

236+ latex cmd str = "\\"++cmd++"{"++str++"}"

237+

238+ wrap HTMLOutput str =

239+ "<!doctype html><html><head><style>" ++ css ++ "</style></head>" ++

240+ "<body><pre>" ++ str ++ "</pre></body></html>"

241+ where css = concat . intersperse "\n" $

242+ [".idris-data { color: red; } ",

243+ ".idris-type { color: blue; }",

244+ ".idris-function {color: green; }",

245+ ".idris-keyword { font-weight: bold; }",

246+ ".idris-bound { color: purple; }",

247+ ".idris-implicit { font-style: italic; }"]

248+ wrap LaTeXOutput str =

249+ concat . intersperse "\n" $

250+ ["\\documentclass{article}",

251+ "\\usepackage{fancyvrb}",

252+ "\\usepackage[usenames]{xcolor}"] ++

253+ map (\(cmd, color) ->

254+ "\\newcommand{\\"++ cmd ++

255+ "}[1]{\\textcolor{"++ color ++"}{#1}}")

256+ [("IdrisData", "red"), ("IdrisType", "blue"),

257+ ("IdrisBound", "magenta"), ("IdrisFunction", "green")] ++

258+ ["\\newcommand{\\IdrisKeyword}[1]{{\\underline{#1}}}",

259+ "\\newcommand{\\IdrisImplicit}[1]{{\\itshape \\IdrisBound{#1}}}",

260+ "\n",

261+ "\\begin{document}",

262+ "% START CODE",

263+ "\\begin{Verbatim}[commandchars=\\\\\\{\\}]",

264+ str,

265+ "\\end{Verbatim}",

266+ "% END CODE",

267+ "\\end{document}"]

src/Idris/REPL.hs+43−23

@@ -1181,17 +1181,54 @@ process fn (MakeDoc s) =

11811181 case result of Right _ -> iputStrLn "IdrisDoc generated"

11821182 Left err -> iPrintError err

11831183process fn (PrintDef n) =

1184+ do result <- pprintDef n

1185+ case result of

1186+ [] -> iPrintError "Not found"

1187+ outs -> iRenderResult . vsep $ outs

1188+

1189+

1190+process fn (PPrint fmt width (PRef _ n))

1191+ = do outs <- pprintDef n

1192+ iputStrLn =<< renderExternal fmt width (vsep outs)

1193+

1194+

1195+process fn (PPrint fmt width t)

1196+ = do (tm, ty) <- elabVal recinfo ERHS t

1197+ ctxt <- getContext

1198+ ist <- getIState

1199+ let ppo = ppOptionIst ist

1200+ ty' = normaliseC ctxt [] ty

1201+ iputStrLn =<< renderExternal fmt width (pprintDelab ist tm)

1202+

1203+

1204+showTotal :: Totality -> IState -> String

1205+showTotal t@(Partial (Other ns)) i

1206+ = show t ++ "\n\t" ++ showSep "\n\t" (map (showTotalN i) ns)

1207+showTotal t i = show t

1208+showTotalN i n = case lookupTotal n (tt_ctxt i) of

1209+ [t] -> showTotal t i

1210+ _ -> ""

1211+

1212+displayHelp = let vstr = showVersion version in

1213+ "\nIdris version " ++ vstr ++ "\n" ++

1214+ "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++

1215+ concatMap cmdInfo helphead ++

1216+ concatMap cmdInfo help

1217+ where cmdInfo (cmds, args, text) = " " ++ col 16 12 (showSep " " cmds) (show args) text

1218+ col c1 c2 l m r =

1219+ l ++ take (c1 - length l) (repeat ' ') ++

1220+ m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"

1221+

1222+pprintDef :: Name -> Idris [Doc OutputAnnotation]

1223+pprintDef n =

11841224 do ist <- getIState

11851225 ctxt <- getContext

11861226 let ambiguous = length (lookupNames n ctxt) > 1

11871227 patdefs = idris_patdefs ist

11881228 tyinfo = idris_datatypes ist

1189− result = map (ppDef ambiguous ist) (lookupCtxtName n patdefs) ++

1190− map (ppTy ambiguous ist) (lookupCtxtName n tyinfo) ++

1191− map (ppCon ambiguous ist) (filter (flip isDConName ctxt) (lookupNames n ctxt))

1192− case result of

1193− [] -> iPrintError "Not found"

1194− outs -> iRenderResult . vsep . punctuate line $ outs

1229+ return $ map (ppDef ambiguous ist) (lookupCtxtName n patdefs) ++

1230+ map (ppTy ambiguous ist) (lookupCtxtName n tyinfo) ++

1231+ map (ppCon ambiguous ist) (filter (flip isDConName ctxt) (lookupNames n ctxt))

11951232 where ppDef :: Bool -> IState -> (Name, ([([Name], Term, Term)], [PTerm])) -> Doc OutputAnnotation

11961233 ppDef amb ist (n, (clauses, missing)) =

11971234 prettyName True amb [] n <+> colon <+>

@@ -1220,23 +1257,6 @@ process fn (PrintDef n) =

12201257 kwd = annotate AnnKeyword . text

12211258 ppCon amb ist n = prettyName True amb [] n <+> colon <+> align (pprintDelabTy ist n)

12221259

1223−showTotal :: Totality -> IState -> String

1224−showTotal t@(Partial (Other ns)) i

1225− = show t ++ "\n\t" ++ showSep "\n\t" (map (showTotalN i) ns)

1226−showTotal t i = show t

1227−showTotalN i n = case lookupTotal n (tt_ctxt i) of

1228− [t] -> showTotal t i

1229− _ -> ""

1230−

1231−displayHelp = let vstr = showVersion version in

1232− "\nIdris version " ++ vstr ++ "\n" ++

1233− "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++

1234− concatMap cmdInfo helphead ++

1235− concatMap cmdInfo help

1236− where cmdInfo (cmds, args, text) = " " ++ col 16 12 (showSep " " cmds) (show args) text

1237− col c1 c2 l m r =

1238− l ++ take (c1 - length l) (repeat ' ') ++

1239− m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"

12401260

12411261helphead =

12421262 [ (["Command"], SpecialHeaderArg, "Purpose"),

src/Idris/REPLParser.hs+12

@@ -134,6 +134,14 @@ pCmd = do P.whiteSpace; do cmd ["q", "quit"]; eof; return Quit

134134 <|> do cmd ["cw", "callswho"]; P.whiteSpace; n <- P.fnName ; return (CallsWho n)

135135 <|> do cmd ["mkdoc"]; str <- many anyChar; return (MakeDoc str)

136136 <|> do cmd ["printdef"]; P.whiteSpace; n <- P.fnName; return (PrintDef n)

137+ <|> do cmd ["pp", "pprint"]

138+ P.whiteSpace

139+ fmt <- ppFormat

140+ P.whiteSpace

141+ n <- fmap fromInteger P.natural

142+ P.whiteSpace

143+ t <- P.fullExpr defaultSyntax

144+ return (PPrint fmt n t)

137145 <|> do P.whiteSpace; do eof; return NOP

138146 <|> do t <- P.fullExpr defaultSyntax; return (Eval t)

139147

@@ -157,6 +165,10 @@ pConsoleWidth = do discard (P.symbol "auto"); return AutomaticWidth

157165 <|> do discard (P.symbol "infinite"); return InfinitelyWide

158166 <|> do n <- fmap fromInteger P.natural; return (ColsWide n)

159167

168+ppFormat :: P.IdrisParser OutputFmt

169+ppFormat = (discard (P.symbol "html") >> return HTMLOutput)

170+ <|> (discard (P.symbol "latex") >> return LaTeXOutput)

171+

160172colours :: [(String, Maybe Color)]

161173colours = [ ("black", Just Black)

162174 , ("red", Just Red)