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