git.iko.soy/Idris-dev
on cb005bc help sign in
Idris-dev/src/Idris/Output.hs
298 lines 13 kB history raw
1{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3module Idris.Output where
5import Idris.Core.TT
6import Idris.Core.Evaluate (isDConName, isTConName, isFnName, normaliseAll)
8import Idris.AbsSyntax
9import Idris.Delaborate
10import Idris.Docstrings
11import Idris.IdeSlave
13import Util.Pretty
14import Util.ScreenSize (getScreenWidth)
16import Control.Monad.Trans.Except (ExceptT (ExceptT), runExceptT)
18import System.Console.Haskeline.MonadException
19 (MonadException (controlIO), RunIO (RunIO))
20import System.IO (stdout, Handle, hPutStrLn)
22import Data.Char (isAlpha)
23import Data.List (nub, intersperse)
24import Data.Maybe (fromMaybe)
26instance MonadException m => MonadException (ExceptT Err m) where
27 controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let
28 run' = RunIO (fmap ExceptT . run . runExceptT)
29 in fmap runExceptT $ f run'
31pshow :: IState -> Err -> String
32pshow ist err = displayDecorated (consoleDecorate ist) .
33 renderPretty 1.0 80 .
34 fmap (fancifyAnnots ist) $ pprintErr ist err
36iWarn :: FC -> Doc OutputAnnotation -> Idris ()
37iWarn fc err =
38 do i <- getIState
39 case idris_outputmode i of
40 RawOutput h ->
41 do err' <- iRender . fmap (fancifyAnnots i) $
42 if fc_fname fc /= ""
43 then text (show fc) <> colon <//> err
44 else err
45 runIO . hPutStrLn h $ displayDecorated (consoleDecorate i) err'
46 IdeSlave n h ->
47 do err' <- iRender . fmap (fancifyAnnots i) $ err
48 let (str, spans) = displaySpans err'
49 runIO . hPutStrLn h $
50 convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n
52iRender :: Doc a -> Idris (SimpleDoc a)
53iRender d = do w <- getWidth
54 ist <- getIState
55 let ideSlave = case idris_outputmode ist of
56 IdeSlave _ _ -> True
57 _ -> False
58 case w of
59 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d
60 ColsWide n -> return $
61 if n < 1
62 then renderPretty 1.0 1000000000 d
63 else renderPretty 0.8 n d
64 AutomaticWidth | ideSlave -> return $ renderPretty 1.0 1000000000 d
65 | otherwise -> do width <- runIO getScreenWidth
66 return $ renderPretty 0.8 width d
68-- | Write a pretty-printed term to the console with semantic coloring
69consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()
70consoleDisplayAnnotated h output = do ist <- getIState
71 rendered <- iRender $ output
72 runIO . hPutStrLn h .
73 displayDecorated (consoleDecorate ist) $
74 rendered
76iPrintTermWithType :: Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
77iPrintTermWithType tm ty = iRenderResult (tm <+> colon <+> align ty)
79-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name
80iPrintFunTypes :: [(Name, Bool)] -> Name -> [(Name, Doc OutputAnnotation)] -> Idris ()
81iPrintFunTypes bnd n [] = iPrintError $ "No such variable " ++ show n
82iPrintFunTypes bnd n overloads = do ist <- getIState
83 let ppo = ppOptionIst ist
84 let infixes = idris_infixes ist
85 let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)
86 iRenderResult output
87 where fullName n = prettyName True True bnd n
88 ppOverload ppo infixes n tm =
89 fullName n <+> colon <+> align tm
91iRenderOutput :: Doc OutputAnnotation -> Idris ()
92iRenderOutput doc =
93 do i <- getIState
94 case idris_outputmode i of
95 RawOutput h -> do out <- iRender doc
96 runIO $ putStrLn (displayDecorated (consoleDecorate i) out)
97 IdeSlave n h ->
98 do (str, spans) <- fmap displaySpans . iRender . fmap (fancifyAnnots i) $ doc
99 let out = [toSExp str, toSExp spans]
100 runIO . hPutStrLn h $ convSExp "write-decorated" out n
102iRenderResult :: Doc OutputAnnotation -> Idris ()
103iRenderResult d = do ist <- getIState
104 case idris_outputmode ist of
105 RawOutput h -> consoleDisplayAnnotated h d
106 IdeSlave n h -> ideSlaveReturnAnnotated n h d
108ideSlaveReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()
109ideSlaveReturnWithStatus status n h out = do
110 ist <- getIState
111 (str, spans) <- fmap displaySpans .
112 iRender .
113 fmap (fancifyAnnots ist) $
114 out
115 let good = [SymbolAtom status, toSExp str, toSExp spans]
116 runIO . hPutStrLn h $ convSExp "return" good n
119-- | Write pretty-printed output to IDESlave with semantic annotations
120ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
121ideSlaveReturnAnnotated = ideSlaveReturnWithStatus "ok"
123-- | Show an error with semantic highlighting
124iRenderError :: Doc OutputAnnotation -> Idris ()
125iRenderError e = do ist <- getIState
126 case idris_outputmode ist of
127 RawOutput h -> consoleDisplayAnnotated h e
128 IdeSlave n h -> ideSlaveReturnWithStatus "error" n h e
130iPrintWithStatus :: String -> String -> Idris ()
131iPrintWithStatus status s = do
132 i <- getIState
133 case idris_outputmode i of
134 RawOutput h -> case s of
135 "" -> return ()
136 s -> runIO $ hPutStrLn h s
137 IdeSlave n h ->
138 let good = SexpList [SymbolAtom status, toSExp s] in
139 runIO $ hPutStrLn h $ convSExp "return" good n
142iPrintResult :: String -> Idris ()
143iPrintResult = iPrintWithStatus "ok"
145iPrintError :: String -> Idris ()
146iPrintError = iPrintWithStatus "error"
148iputStrLn :: String -> Idris ()
149iputStrLn s = do i <- getIState
150 case idris_outputmode i of
151 RawOutput h -> runIO $ hPutStrLn h s
152 IdeSlave n h -> runIO . hPutStrLn h $ convSExp "write-string" s n
155ideslavePutSExp :: SExpable a => String -> a -> Idris ()
156ideslavePutSExp cmd info = do i <- getIState
157 case idris_outputmode i of
158 IdeSlave n h -> runIO . hPutStrLn h $ convSExp cmd info n
159 _ -> return ()
161-- TODO: send structured output similar to the metavariable list
162iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
163iputGoal g = do i <- getIState
164 case idris_outputmode i of
165 RawOutput h -> runIO $ hPutStrLn h (displayDecorated (consoleDecorate i) g)
166 IdeSlave n h ->
167 let (str, spans) = displaySpans . fmap (fancifyAnnots i) $ g
168 goal = [toSExp str, toSExp spans]
169 in runIO . hPutStrLn h $ convSExp "write-goal" goal n
171-- | Warn about totality problems without failing to compile
172warnTotality :: Idris ()
173warnTotality = do ist <- getIState
174 mapM_ (warn ist) (nub (idris_totcheckfail ist))
175 where warn ist (fc, e) = iWarn fc (pprintErr ist (Msg e))
178printUndefinedNames :: [Name] -> Doc OutputAnnotation
179printUndefinedNames ns = text "Undefined " <> names <> text "."
180 where names = encloseSep empty empty (char ',') $ map ppName ns
181 ppName = prettyName True True []
184prettyDocumentedIst :: IState
185 -> (Name, PTerm, Maybe (Docstring DocTerm))
186 -> Doc OutputAnnotation
187prettyDocumentedIst ist (name, ty, docs) =
188 prettyName True True [] name <+> colon <+> align (prettyIst ist ty) <$>
189 fromMaybe empty (fmap (\d -> renderDocstring (renderDocTerm ppTm norm) d <> line) docs)
190 where ppTm = pprintDelab ist
191 norm = normaliseAll (tt_ctxt ist) []
194renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String
195renderExternal fmt width doc
196 | width < 1 = throwError . Msg $ "There must be at least one column for the pretty-printer."
197 | otherwise =
198 do ist <- getIState
199 return . wrap fmt .
200 displayDecorated (decorate fmt) .
201 renderPretty 1.0 width .
202 fmap (fancifyAnnots ist) $
203 doc
204 where
205 decorate _ (AnnFC _) = id
207 decorate HTMLOutput (AnnName _ (Just TypeOutput) d _) =
208 tag "idris-type" d
209 decorate HTMLOutput (AnnName _ (Just FunOutput) d _) =
210 tag "idris-function" d
211 decorate HTMLOutput (AnnName _ (Just DataOutput) d _) =
212 tag "idris-data" d
213 decorate HTMLOutput (AnnName _ (Just MetavarOutput) d _) =
214 tag "idris-metavar" d
215 decorate HTMLOutput (AnnName _ (Just PostulateOutput) d _) =
216 tag "idris-postulate" d
217 decorate HTMLOutput (AnnName _ _ _ _) = id
218 decorate HTMLOutput (AnnBoundName _ True) = tag "idris-bound idris-implicit" Nothing
219 decorate HTMLOutput (AnnBoundName _ False) = tag "idris-bound" Nothing
220 decorate HTMLOutput (AnnConst c) =
221 tag (if constIsType c then "idris-type" else "idris-data")
222 (Just $ constDocs c)
223 decorate HTMLOutput (AnnData _ _) = tag "idris-data" Nothing
224 decorate HTMLOutput (AnnType _ _) = tag "idris-type" Nothing
225 decorate HTMLOutput AnnKeyword = tag "idris-keyword" Nothing
226 decorate HTMLOutput (AnnTextFmt fmt) =
227 case fmt of
228 BoldText -> mkTag "strong"
229 ItalicText -> mkTag "em"
230 UnderlineText -> tag "idris-underlined" Nothing
231 where mkTag t x = "<"++t++">"++x++"</"++t++">"
232 decorate HTMLOutput (AnnTerm _ _) = id
233 decorate HTMLOutput (AnnSearchResult _) = id
234 decorate HTMLOutput (AnnErr _) = id
236 decorate LaTeXOutput (AnnName _ (Just TypeOutput) _ _) =
237 latex "IdrisType"
238 decorate LaTeXOutput (AnnName _ (Just FunOutput) _ _) =
239 latex "IdrisFunction"
240 decorate LaTeXOutput (AnnName _ (Just DataOutput) _ _) =
241 latex "IdrisData"
242 decorate LaTeXOutput (AnnName _ (Just MetavarOutput) _ _) =
243 latex "IdrisMetavar"
244 decorate LaTeXOutput (AnnName _ (Just PostulateOutput) _ _) =
245 latex "IdrisPostulate"
246 decorate LaTeXOutput (AnnName _ _ _ _) = id
247 decorate LaTeXOutput (AnnBoundName _ True) = latex "IdrisImplicit"
248 decorate LaTeXOutput (AnnBoundName _ False) = latex "IdrisBound"
249 decorate LaTeXOutput (AnnConst c) =
250 latex $ if constIsType c then "IdrisType" else "IdrisData"
251 decorate LaTeXOutput (AnnData _ _) = latex "IdrisData"
252 decorate LaTeXOutput (AnnType _ _) = latex "IdrisType"
253 decorate LaTeXOutput AnnKeyword = latex "IdrisKeyword"
254 decorate LaTeXOutput (AnnTextFmt fmt) =
255 case fmt of
256 BoldText -> latex "textbf"
257 ItalicText -> latex "emph"
258 UnderlineText -> latex "underline"
259 decorate LaTeXOutput (AnnTerm _ _) = id
260 decorate LaTeXOutput (AnnSearchResult _) = id
261 decorate LaTeXOutput (AnnErr _) = id
263 tag cls docs str = "<span class=\""++cls++"\""++title++">" ++ str ++ "</span>"
264 where title = maybe "" (\d->" title=\"" ++ d ++ "\"") docs
266 latex cmd str = "\\"++cmd++"{"++str++"}"
268 wrap HTMLOutput str =
269 "<!doctype html><html><head><style>" ++ css ++ "</style></head>" ++
270 "<body><!-- START CODE --><pre>" ++ str ++ "</pre><!-- END CODE --></body></html>"
271 where css = concat . intersperse "\n" $
272 [".idris-data { color: red; } ",
273 ".idris-type { color: blue; }",
274 ".idris-function {color: green; }",
275 ".idris-keyword { font-weight: bold; }",
276 ".idris-bound { color: purple; }",
277 ".idris-implicit { font-style: italic; }",
278 ".idris-underlined { text-decoration: underline; }"]
279 wrap LaTeXOutput str =
280 concat . intersperse "\n" $
281 ["\\documentclass{article}",
282 "\\usepackage{fancyvrb}",
283 "\\usepackage[usenames]{xcolor}"] ++
284 map (\(cmd, color) ->
285 "\\newcommand{\\"++ cmd ++
286 "}[1]{\\textcolor{"++ color ++"}{#1}}")
287 [("IdrisData", "red"), ("IdrisType", "blue"),
288 ("IdrisBound", "magenta"), ("IdrisFunction", "green")] ++
289 ["\\newcommand{\\IdrisKeyword}[1]{{\\underline{#1}}}",
290 "\\newcommand{\\IdrisImplicit}[1]{{\\itshape \\IdrisBound{#1}}}",
291 "\n",
292 "\\begin{document}",
293 "% START CODE",
294 "\\begin{Verbatim}[commandchars=\\\\\\{\\}]",
295 str,
296 "\\end{Verbatim}",
297 "% END CODE",
298 "\\end{document}"]