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