git.iko.soy/Idris-dev
on ff01a4c help sign in
Idris-dev/src/Idris/Output.hs
377 lines 16 kB history raw
1{-|
2Module : Idris.Output
3Description : Utilities to display Idris' internals and other informtation to the user.
4Copyright :
5License : BSD3
6Maintainer : The Idris Community.
7-}
9{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
11module Idris.Output where
13import Idris.AbsSyntax
14import Idris.Colours (hEndColourise, hStartColourise)
15import Idris.Core.Evaluate (isDConName, isFnName, isTConName, normaliseAll)
16import Idris.Core.TT
17import Idris.Delaborate
18import Idris.Docstrings
19import Idris.IdeMode
21import Util.Pretty
22import Util.ScreenSize (getScreenWidth)
23import Util.System (isATTY)
25import Prelude hiding ((<$>))
27import Control.Monad.Trans.Except (ExceptT(ExceptT), runExceptT)
28import Data.Char (isAlpha)
29import Data.List (intersperse, nub)
30import Data.Maybe (fromMaybe)
31import System.Console.Haskeline.MonadException (MonadException(controlIO),
32 RunIO(RunIO))
33import System.FilePath (replaceExtension)
34import System.IO (Handle, hPutStr, hPutStrLn, stdout)
36instance MonadException m => MonadException (ExceptT Err m) where
37 controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let
38 run' = RunIO (fmap ExceptT . run . runExceptT)
39 in fmap runExceptT $ f run'
41pshow :: IState -> Err -> String
42pshow ist err = displayDecorated (consoleDecorate ist) .
43 renderPretty 1.0 80 .
44 fmap (fancifyAnnots ist True) $ pprintErr ist err
46iWarn :: FC -> Doc OutputAnnotation -> Idris ()
47iWarn fc err =
48 do i <- getIState
49 case idris_outputmode i of
50 RawOutput h ->
51 do err' <- iRender . fmap (fancifyAnnots i True) $
52 case fc of
53 FC fn _ _ | fn /= "" -> text (show fc) <> colon <//> err
54 _ -> err
55 hWriteDoc h i err'
56 IdeMode n h ->
57 do err' <- iRender . fmap (fancifyAnnots i True) $ err
58 let (str, spans) = displaySpans err'
59 runIO . hPutStrLn h $
60 convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n
62iRender :: Doc a -> Idris (SimpleDoc a)
63iRender d = do w <- getWidth
64 ist <- getIState
65 let ideMode = case idris_outputmode ist of
66 IdeMode _ _ -> True
67 _ -> False
68 tty <- runIO isATTY
69 case w of
70 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d
71 ColsWide n -> return $
72 if n < 1
73 then renderPretty 1.0 1000000000 d
74 else renderPretty 0.8 n d
75 AutomaticWidth | ideMode || not tty -> return $ renderPretty 1.0 80 d
76 | otherwise -> do width <- runIO getScreenWidth
77 return $ renderPretty 0.8 width d
79hWriteDoc :: Handle -> IState -> SimpleDoc OutputAnnotation -> Idris ()
80hWriteDoc h ist rendered =
81 do runIO $ displayDecoratedA
82 (hPutStr h)
83 (maybe (return ()) (hStartColourise h))
84 (maybe (return ()) (hEndColourise h))
85 (fmap (annotationColour ist) rendered)
86 runIO $ hPutStr h "\n" -- newline translation on the output
87 -- stream should take care of this for
88 -- Windows
90-- | Write a pretty-printed term to the console with semantic coloring
91consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()
92consoleDisplayAnnotated h output =
93 do ist <- getIState
94 rendered <- iRender output
95 hWriteDoc h ist rendered
97iPrintTermWithType :: Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
98iPrintTermWithType tm ty = iRenderResult (tm <+> colon <+> align ty)
100-- | Pretty-print a collection of overloadings to REPL or IDEMode - corresponds to :t name
101iPrintFunTypes :: [(Name, Bool)] -> Name -> [(Name, Doc OutputAnnotation)] -> Idris ()
102iPrintFunTypes bnd n [] = iPrintError $ "No such variable " ++ show n
103iPrintFunTypes bnd n overloads = do ist <- getIState
104 let ppo = ppOptionIst ist
105 let infixes = idris_infixes ist
106 let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)
107 iRenderResult output
108 where fullName ppo n | length overloads > 1 = prettyName True True bnd n
109 | otherwise = prettyName True (ppopt_impl ppo) bnd n
110 ppOverload ppo infixes n tm =
111 fullName ppo n <+> colon <+> align tm
113iRenderOutput :: Doc OutputAnnotation -> Idris ()
114iRenderOutput doc =
115 do i <- getIState
116 case idris_outputmode i of
117 RawOutput h -> do out <- iRender doc
118 hWriteDoc h i out
120 IdeMode n h ->
121 do (str, spans) <- fmap displaySpans . iRender . fmap (fancifyAnnots i True) $ doc
122 let out = [toSExp str, toSExp spans]
123 runIO . hPutStrLn h $ convSExp "write-decorated" out n
125iRenderResult :: Doc OutputAnnotation -> Idris ()
126iRenderResult d = do ist <- getIState
127 case idris_outputmode ist of
128 RawOutput h -> consoleDisplayAnnotated h d
129 IdeMode n h -> ideModeReturnAnnotated n h d
131ideModeReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()
132ideModeReturnWithStatus status n h out = do
133 ist <- getIState
134 (str, spans) <- fmap displaySpans .
135 iRender .
136 fmap (fancifyAnnots ist True) $
137 out
138 let good = [SymbolAtom status, toSExp str, toSExp spans]
139 runIO . hPutStrLn h $ convSExp "return" good n
142-- | Write pretty-printed output to IDEMode with semantic annotations
143ideModeReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
144ideModeReturnAnnotated = ideModeReturnWithStatus "ok"
146-- | Show an error with semantic highlighting
147iRenderError :: Doc OutputAnnotation -> Idris ()
148iRenderError e = do ist <- getIState
149 case idris_outputmode ist of
150 RawOutput h -> consoleDisplayAnnotated h e
151 IdeMode n h -> ideModeReturnWithStatus "error" n h e
153iPrintWithStatus :: String -> String -> Idris ()
154iPrintWithStatus status s = do
155 i <- getIState
156 case idris_outputmode i of
157 RawOutput h -> case s of
158 "" -> return ()
159 s -> runIO $ hPutStrLn h s
160 IdeMode n h ->
161 let good = SexpList [SymbolAtom status, toSExp s] in
162 runIO $ hPutStrLn h $ convSExp "return" good n
165iPrintResult :: String -> Idris ()
166iPrintResult = iPrintWithStatus "ok"
168iPrintError :: String -> Idris ()
169iPrintError = iPrintWithStatus "error"
171iputStrLn :: String -> Idris ()
172iputStrLn s = do i <- getIState
173 case idris_outputmode i of
174 RawOutput h -> runIO $ hPutStrLn h s
175 IdeMode n h -> runIO . hPutStrLn h $ convSExp "write-string" s n
178idemodePutSExp :: SExpable a => String -> a -> Idris ()
179idemodePutSExp cmd info = do i <- getIState
180 case idris_outputmode i of
181 IdeMode n h ->
182 runIO . hPutStrLn h $
183 convSExp cmd info n
184 _ -> return ()
186-- TODO: send structured output similar to the metavariable list
187iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
188iputGoal g = do i <- getIState
189 case idris_outputmode i of
190 RawOutput h -> hWriteDoc h i g
191 IdeMode n h ->
192 let (str, spans) = displaySpans . fmap (fancifyAnnots i True) $ g
193 goal = [toSExp str, toSExp spans]
194 in runIO . hPutStrLn h $ convSExp "write-goal" goal n
196-- | Warn about totality problems without failing to compile
197warnTotality :: Idris ()
198warnTotality = do ist <- getIState
199 mapM_ (warn ist) (nub (idris_totcheckfail ist))
200 where warn ist (fc, e) = iWarn fc (pprintErr ist (Msg e))
203printUndefinedNames :: [Name] -> Doc OutputAnnotation
204printUndefinedNames ns = text "Undefined " <> names <> text "."
205 where names = encloseSep empty empty (char ',') $ map ppName ns
206 ppName = prettyName True True []
209prettyDocumentedIst :: IState
210 -> (Name, PTerm, Maybe (Docstring DocTerm))
211 -> Doc OutputAnnotation
212prettyDocumentedIst ist (name, ty, docs) =
213 prettyName True True [] name <+> colon <+> align (prettyIst ist ty) <$>
214 fromMaybe empty (fmap (\d -> renderDocstring (renderDocTerm ppTm norm) d <> line) docs)
215 where ppTm = pprintDelab ist
216 norm = normaliseAll (tt_ctxt ist) []
218sendParserHighlighting :: Idris ()
219sendParserHighlighting =
220 do ist <- getIState
221 let hs = map unwrap . nub . map wrap $ idris_parserHighlights ist
222 sendHighlighting hs
223 ist <- getIState
224 putIState ist {idris_parserHighlights = []}
225 where wrap (fc, a) = (FC' fc, a)
226 unwrap (fc', a) = (unwrapFC fc', a)
228sendHighlighting :: [(FC, OutputAnnotation)] -> Idris ()
229sendHighlighting highlights =
230 do ist <- getIState
231 case idris_outputmode ist of
232 RawOutput _ -> updateIState $
233 \ist -> ist { idris_highlightedRegions =
234 highlights ++ idris_highlightedRegions ist }
235 IdeMode n h ->
236 let fancier = [ toSExp (fc, fancifyAnnots ist False annot)
237 | (fc, annot) <- highlights, fullFC fc
238 ]
239 in case fancier of
240 [] -> return ()
241 _ -> runIO . hPutStrLn h $
242 convSExp "output"
243 (SymbolAtom "ok",
244 (SymbolAtom "highlight-source", fancier)) n
246 where fullFC (FC _ _ _) = True
247 fullFC _ = False
249-- | Write the highlighting information to a file, for use in external tools
250-- or in editors that don't support the IDE protocol
251writeHighlights :: FilePath -> Idris ()
252writeHighlights f =
253 do ist <- getIState
254 let hs = reverse $ idris_highlightedRegions ist
255 let hfile = replaceExtension f "idh"
256 let annots = toSExp [ (fc, fancifyAnnots ist False annot)
257 | (fc@(FC _ _ _), annot) <- hs
258 ]
259 runIO $ writeFile hfile $ sExpToString annots
261clearHighlights :: Idris ()
262clearHighlights = updateIState $ \ist -> ist { idris_highlightedRegions = [] }
264renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String
265renderExternal fmt width doc
266 | width < 1 = throwError . Msg $ "There must be at least one column for the pretty-printer."
267 | otherwise =
268 do ist <- getIState
269 return . wrap fmt .
270 displayDecorated (decorate fmt) .
271 renderPretty 1.0 width .
272 fmap (fancifyAnnots ist True) $
273 doc
274 where
275 decorate _ (AnnFC _) = id
277 decorate HTMLOutput (AnnName _ (Just TypeOutput) d _) =
278 tag "idris-type" d
279 decorate HTMLOutput (AnnName _ (Just FunOutput) d _) =
280 tag "idris-function" d
281 decorate HTMLOutput (AnnName _ (Just DataOutput) d _) =
282 tag "idris-data" d
283 decorate HTMLOutput (AnnName _ (Just MetavarOutput) d _) =
284 tag "idris-metavar" d
285 decorate HTMLOutput (AnnName _ (Just PostulateOutput) d _) =
286 tag "idris-postulate" d
287 decorate HTMLOutput (AnnName _ _ _ _) = id
288 decorate HTMLOutput (AnnBoundName _ True) = tag "idris-bound idris-implicit" Nothing
289 decorate HTMLOutput (AnnBoundName _ False) = tag "idris-bound" Nothing
290 decorate HTMLOutput (AnnConst c) =
291 tag (if constIsType c then "idris-type" else "idris-data")
292 (Just $ constDocs c)
293 decorate HTMLOutput (AnnData _ _) = tag "idris-data" Nothing
294 decorate HTMLOutput (AnnType _ _) = tag "idris-type" Nothing
295 decorate HTMLOutput AnnKeyword = tag "idris-keyword" Nothing
296 decorate HTMLOutput (AnnTextFmt fmt) =
297 case fmt of
298 BoldText -> mkTag "strong"
299 ItalicText -> mkTag "em"
300 UnderlineText -> tag "idris-underlined" Nothing
301 where mkTag t x = "<"++t++">"++x++"</"++t++">"
302 decorate HTMLOutput (AnnTerm _ _) = id
303 decorate HTMLOutput (AnnSearchResult _) = id
304 decorate HTMLOutput (AnnErr _) = id
305 decorate HTMLOutput (AnnNamespace _ _) = id
306 decorate HTMLOutput (AnnLink url) =
307 \txt -> "<a href=\"" ++ url ++ "\">" ++ txt ++ "</a>"
308 decorate HTMLOutput AnnQuasiquote = id
309 decorate HTMLOutput AnnAntiquote = id
311 decorate LaTeXOutput (AnnName _ (Just TypeOutput) _ _) =
312 latex "IdrisType"
313 decorate LaTeXOutput (AnnName _ (Just FunOutput) _ _) =
314 latex "IdrisFunction"
315 decorate LaTeXOutput (AnnName _ (Just DataOutput) _ _) =
316 latex "IdrisData"
317 decorate LaTeXOutput (AnnName _ (Just MetavarOutput) _ _) =
318 latex "IdrisMetavar"
319 decorate LaTeXOutput (AnnName _ (Just PostulateOutput) _ _) =
320 latex "IdrisPostulate"
321 decorate LaTeXOutput (AnnName _ _ _ _) = id
322 decorate LaTeXOutput (AnnBoundName _ True) = latex "IdrisImplicit"
323 decorate LaTeXOutput (AnnBoundName _ False) = latex "IdrisBound"
324 decorate LaTeXOutput (AnnConst c) =
325 latex $ if constIsType c then "IdrisType" else "IdrisData"
326 decorate LaTeXOutput (AnnData _ _) = latex "IdrisData"
327 decorate LaTeXOutput (AnnType _ _) = latex "IdrisType"
328 decorate LaTeXOutput AnnKeyword = latex "IdrisKeyword"
329 decorate LaTeXOutput (AnnTextFmt fmt) =
330 case fmt of
331 BoldText -> latex "textbf"
332 ItalicText -> latex "emph"
333 UnderlineText -> latex "underline"
334 decorate LaTeXOutput (AnnTerm _ _) = id
335 decorate LaTeXOutput (AnnSearchResult _) = id
336 decorate LaTeXOutput (AnnErr _) = id
337 decorate LaTeXOutput (AnnNamespace _ _) = id
338 decorate LaTeXOutput (AnnLink url) = (++ "(\\url{" ++ url ++ "})")
339 decorate LaTeXOutput AnnQuasiquote = id
340 decorate LaTeXOutput AnnAntiquote = id
342 tag cls docs str = "<span class=\""++cls++"\""++title++">" ++ str ++ "</span>"
343 where title = maybe "" (\d->" title=\"" ++ d ++ "\"") docs
345 latex cmd str = "\\"++cmd++"{"++str++"}"
347 wrap HTMLOutput str =
348 "<!doctype html><html><head><style>" ++ css ++ "</style></head>" ++
349 "<body><!-- START CODE --><pre>" ++ str ++ "</pre><!-- END CODE --></body></html>"
350 where css = concat . intersperse "\n" $
351 [".idris-data { color: red; } ",
352 ".idris-type { color: blue; }",
353 ".idris-function {color: green; }",
354 ".idris-keyword { font-weight: bold; }",
355 ".idris-bound { color: purple; }",
356 ".idris-implicit { font-style: italic; }",
357 ".idris-underlined { text-decoration: underline; }"]
358 wrap LaTeXOutput str =
359 concat . intersperse "\n" $
360 ["\\documentclass{article}",
361 "\\usepackage{fancyvrb}",
362 "\\usepackage[usenames]{xcolor}"] ++
363 map (\(cmd, color) ->
364 "\\newcommand{\\"++ cmd ++
365 "}[1]{\\textcolor{"++ color ++"}{#1}}")
366 [("IdrisData", "red"), ("IdrisType", "blue"),
367 ("IdrisBound", "magenta"), ("IdrisFunction", "green")] ++
368 ["\\newcommand{\\IdrisKeyword}[1]{{\\underline{#1}}}",
369 "\\newcommand{\\IdrisImplicit}[1]{{\\itshape \\IdrisBound{#1}}}",
370 "\n",
371 "\\begin{document}",
372 "% START CODE",
373 "\\begin{Verbatim}[commandchars=\\\\\\{\\}]",
374 str,
375 "\\end{Verbatim}",
376 "% END CODE",
377 "\\end{document}"]