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