git.iko.soy/Idris-dev
on d3badf2 help sign in
Idris-dev/src/Idris/Output.hs
528 lines 22 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 CPP, FlexibleInstances #-}
10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
12module Idris.Output (clearHighlights, emitWarning, formatMessage, idemodePutSExp,
13 iPrintError, iPrintFunTypes, iPrintResult, iPrintTermWithType,
14 iputGoal, iputStr, iputStrLn, iRender, iRenderError,
15 iRenderOutput, iRenderResult, iWarn, prettyDocumentedIst,
16 printUndefinedNames, pshow, renderExternal, sendHighlighting,
17 sendParserHighlighting, warnTotality, writeHighlights,
18 OutputDoc(..), Message(..)) where
20import Idris.AbsSyntax
21import Idris.Colours (hEndColourise, hStartColourise)
22import Idris.Core.Evaluate (normaliseAll)
23import Idris.Core.TT
24import Idris.Delaborate
25import Idris.Docstrings
26import Idris.IdeMode
27import Idris.Options
29import Util.Pretty
30import Util.ScreenSize (getScreenWidth)
31import Util.System (isATTY)
33#if (MIN_VERSION_base(4,11,0))
34import Prelude hiding ((<$>), (<>))
35#else
36import Prelude hiding ((<$>))
37#endif
39import Control.Arrow (first)
40import Control.Monad.Trans.Except (ExceptT(ExceptT), runExceptT)
41import Data.List (intersperse, nub)
42import Data.Maybe (fromJust, fromMaybe, isJust, listToMaybe)
43import System.Console.Haskeline.MonadException (MonadException(controlIO),
44 RunIO(RunIO))
45import System.FilePath (replaceExtension)
46import System.IO (Handle, hPutStr, hPutStrLn)
47import System.IO.Error (tryIOError)
49instance MonadException m => MonadException (ExceptT Err m) where
50 controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let
51 run' = RunIO (fmap ExceptT . run . runExceptT)
52 in fmap runExceptT $ f run'
54pshow :: IState -> Err -> String
55pshow ist err = displayDecorated (consoleDecorate ist) .
56 renderPretty 1.0 80 .
57 fmap (fancifyAnnots ist True) $ pprintErr ist err
59type OutputDoc = Doc OutputAnnotation
61class Message a where
62 messageExtent :: a -> FC
63 messageText :: a -> OutputDoc
64 messageSource :: a -> Maybe String
66data Ann = AText String | ATagged OutputAnnotation Ann | ASplit Ann Ann
68data SimpleWarning = SimpleWarning FC OutputDoc
69instance Message SimpleWarning where
70 messageExtent (SimpleWarning extent _) = extent
71 messageText (SimpleWarning _ msg) = msg
72 messageSource _ = Nothing
74formatMessage :: Message w => w -> Idris OutputDoc
75formatMessage w = do
76 i <- getIState
77 maybeSource <- case messageSource w of
78 Just src -> pure (Just src)
79 Nothing -> readSource fc
80 let maybeFormattedSource = maybeSource >>= layoutSource fc (idris_highlightedRegions i)
81 return $ layoutMessage (layoutFC fc) maybeFormattedSource (messageText w)
82 where
83 fc :: FC
84 fc = messageExtent w
86 layoutFC :: FC -> OutputDoc
87 layoutFC fc@(FC fn _ _) | fn /= "" = text (show $ fc) <> colon
88 layoutFC _ = empty
90 readSource :: FC -> Idris (Maybe String)
91 readSource (FC fn _ _) = do
92 result <- runIO $ tryIOError (readFile fn)
93 case result of
94 Left _ -> pure Nothing
95 Right v -> pure (Just v)
96 readSource _ = pure Nothing
98 layoutSource :: FC -> [(FC, OutputAnnotation)] -> String -> Maybe OutputDoc
99 layoutSource (FC fn (si, sj) (ei, ej)) highlights src =
100 if haveSource
101 then Just source
102 else Nothing
103 where
104 sourceLine :: Maybe String
105 sourceLine = listToMaybe . drop (si - 1) . (++ ["<end of file>"]) . lines $ src
107 haveSource :: Bool
108 haveSource = isJust sourceLine
110 line1 :: OutputDoc
111 line1 = text $ replicate (length (show si)) ' ' ++ " |"
113 lineFC :: FC
114 lineFC = FC fn (si, 1) (si, length (fromJust sourceLine))
116 intersects :: FC -> FC -> Bool
117 intersects (FC fn1 s1 e1) (FC fn2 s2 e2)
118 | fn1 /= fn2 = False
119 | e1 < s2 = False
120 | e2 < s1 = False
121 | otherwise = True
122 intersects _ _ = False
124 intersection :: FC -> FC -> FC
125 intersection fc1@(FC fn1 s1 e1) fc2@(FC _ s2 e2)
126 | intersects fc1 fc2 = FC fn1 (max s1 s2) (min e1 e2)
127 | otherwise = NoFC
128 intersection _ _ = NoFC
130 width :: Ann -> Int
131 width (AText s) = length s
132 width (ATagged _ n) = width n
133 width (ASplit l r) = width l + width r
135 sourceDoc :: Ann -> OutputDoc
136 sourceDoc (AText s) = text s
137 sourceDoc (ATagged a n) = annotate a (sourceDoc n)
138 sourceDoc (ASplit l r) = sourceDoc l <> sourceDoc r
140 insertAnnotation :: ((Int, Int), OutputAnnotation) -> Ann -> Ann
141 insertAnnotation ((sj, ej), oa) (ATagged tag n) = ATagged tag (insertAnnotation ((sj, ej), oa) n)
142 insertAnnotation ((sj, ej), oa) (ASplit l r)
143 | w <- width l = ASplit (insertAnnotation ((sj, ej), oa) l) (insertAnnotation ((sj - w, ej - w), oa) r)
144 insertAnnotation ((sj, ej), oa) a@(AText t)
145 | sj <= 1, ej >= width a = ATagged oa a
146 | sj > 1, sj <= width a = ASplit (AText $ take (sj - 1) t) (insertAnnotation ((1, ej - sj + 1), oa) (AText $ drop (sj - 1) t))
147 | sj == 1, ej >= 1, ej < width a = ASplit (insertAnnotation ((1, ej), oa) (AText $ take ej t)) (AText $ drop ej t)
148 | otherwise = a
150 highlightedSource :: OutputDoc
151 highlightedSource = sourceDoc .
152 foldr insertAnnotation (AText $ fromJust sourceLine) .
153 map (\(FC _ (_, sj) (_, ej), ann) -> ((sj, ej), ann)) .
154 map (first (intersection lineFC)) .
155 filter (intersects lineFC . fst) $
156 highlights
158 line2 :: OutputDoc
159 line2 = text (show si ++ " | ") <> highlightedSource
161 indicator :: OutputDoc
162 indicator = text (replicate (end - sj + 1) ch) <> ellipsis
163 where
164 (end, ch, ellipsis) = case (si == ei, sj == ej) of
165 (True , True ) -> (ej, '^', empty)
166 (True , False) -> (ej, '~', empty)
167 (False, _ ) -> (length (fromJust sourceLine), '~', text " ...")
169 line3 :: OutputDoc
170 line3 = line1 <> text (replicate sj ' ') <> indicator
172 source :: OutputDoc
173 source = line1 <$$> line2 <$$> line3
174 layoutSource _ _ _ = Nothing
176 layoutMessage :: OutputDoc -> Maybe OutputDoc -> OutputDoc -> OutputDoc
177 layoutMessage loc (Just src) err = loc <$$> src <$$> err <$$> empty
178 layoutMessage loc Nothing err = loc </> err
180iWarn :: FC -> OutputDoc -> Idris ()
181iWarn fc err = emitWarning $ SimpleWarning fc err
183emitWarning :: Message w => w -> Idris ()
184emitWarning w =
185 do i <- getIState
186 case idris_outputmode i of
187 RawOutput h ->
188 do formattedErr <- formatMessage w
189 err' <- iRender . fmap (fancifyAnnots i True) $ formattedErr
190 hWriteDoc h i err'
191 IdeMode n h ->
192 do err' <- iRender . fmap (fancifyAnnots i True) $ messageText w
193 let fc = messageExtent w
194 let (str, spans) = displaySpans err'
195 runIO . hPutStrLn h $
196 convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n
198iRender :: Doc a -> Idris (SimpleDoc a)
199iRender d = do w <- getWidth
200 ist <- getIState
201 let ideMode = case idris_outputmode ist of
202 IdeMode _ _ -> True
203 _ -> False
204 tty <- runIO isATTY
205 case w of
206 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d
207 ColsWide n -> return $
208 if n < 1
209 then renderPretty 1.0 1000000000 d
210 else renderPretty 0.8 n d
211 AutomaticWidth | ideMode || not tty -> return $ renderPretty 1.0 80 d
212 | otherwise -> do width <- runIO getScreenWidth
213 return $ renderPretty 0.8 width d
215hWriteDoc :: Handle -> IState -> SimpleDoc OutputAnnotation -> Idris ()
216hWriteDoc h ist rendered =
217 do runIO $ displayDecoratedA
218 (hPutStr h)
219 (maybe (return ()) (hStartColourise h))
220 (maybe (return ()) (hEndColourise h))
221 (fmap (annotationColour ist) rendered)
222 runIO $ hPutStr h "\n" -- newline translation on the output
223 -- stream should take care of this for
224 -- Windows
226-- | Write a pretty-printed term to the console with semantic coloring
227consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()
228consoleDisplayAnnotated h output =
229 do ist <- getIState
230 rendered <- iRender output
231 hWriteDoc h ist rendered
233iPrintTermWithType :: Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
234iPrintTermWithType tm ty = iRenderResult (tm <+> colon <+> align ty)
236-- | Pretty-print a collection of overloadings to REPL or IDEMode - corresponds to :t name
237iPrintFunTypes :: [(Name, Bool)] -> Name -> [(Name, Doc OutputAnnotation)] -> Idris ()
238iPrintFunTypes bnd n [] = iPrintError $ "No such variable " ++ show n
239iPrintFunTypes bnd n overloads = do ist <- getIState
240 let ppo = ppOptionIst ist
241 let infixes = idris_infixes ist
242 let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)
243 iRenderResult output
244 where fullName ppo n | length overloads > 1 = prettyName True True bnd n
245 | otherwise = prettyName True (ppopt_impl ppo) bnd n
246 ppOverload ppo infixes n tm =
247 fullName ppo n <+> colon <+> align tm
249iRenderOutput :: Doc OutputAnnotation -> Idris ()
250iRenderOutput doc =
251 do i <- getIState
252 case idris_outputmode i of
253 RawOutput h -> do out <- iRender doc
254 hWriteDoc h i out
256 IdeMode n h ->
257 do (str, spans) <- fmap displaySpans . iRender . fmap (fancifyAnnots i True) $ doc
258 let out = [toSExp str, toSExp spans]
259 runIO . hPutStrLn h $ convSExp "write-decorated" out n
261iRenderResult :: Doc OutputAnnotation -> Idris ()
262iRenderResult d = do ist <- getIState
263 case idris_outputmode ist of
264 RawOutput h -> consoleDisplayAnnotated h d
265 IdeMode n h -> ideModeReturnAnnotated n h d
267ideModeReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()
268ideModeReturnWithStatus status n h out = do
269 ist <- getIState
270 (str, spans) <- fmap displaySpans .
271 iRender .
272 fmap (fancifyAnnots ist True) $
273 out
274 let good = [SymbolAtom status, toSExp str, toSExp spans]
275 runIO . hPutStrLn h $ convSExp "return" good n
278-- | Write pretty-printed output to IDEMode with semantic annotations
279ideModeReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
280ideModeReturnAnnotated = ideModeReturnWithStatus "ok"
282-- | Show an error with semantic highlighting
283iRenderError :: Doc OutputAnnotation -> Idris ()
284iRenderError e = do ist <- getIState
285 case idris_outputmode ist of
286 RawOutput h -> consoleDisplayAnnotated h e
287 IdeMode n h -> ideModeReturnWithStatus "error" n h e
289iPrintWithStatus :: String -> String -> Idris ()
290iPrintWithStatus status s = do
291 i <- getIState
292 case idris_outputmode i of
293 RawOutput h -> case s of
294 "" -> return ()
295 s -> runIO $ hPutStrLn h s
296 IdeMode n h ->
297 let good = SexpList [SymbolAtom status, toSExp s] in
298 runIO $ hPutStrLn h $ convSExp "return" good n
301iPrintResult :: String -> Idris ()
302iPrintResult = iPrintWithStatus "ok"
304iPrintError :: String -> Idris ()
305iPrintError = iPrintWithStatus "error"
307iputStrLn :: String -> Idris ()
308iputStrLn s = do i <- getIState
309 case idris_outputmode i of
310 RawOutput h -> runIO $ hPutStrLn h s
311 IdeMode n h -> runIO . hPutStrLn h $ convSExp "write-string" s n
313iputStr :: String -> Idris ()
314iputStr s = do i <- getIState
315 case idris_outputmode i of
316 RawOutput h -> runIO $ hPutStr h s
317 IdeMode n h -> runIO . hPutStr h $ convSExp "write-string" s n
319idemodePutSExp :: SExpable a => String -> a -> Idris ()
320idemodePutSExp cmd info = do i <- getIState
321 case idris_outputmode i of
322 IdeMode n h ->
323 runIO . hPutStrLn h $
324 convSExp cmd info n
325 _ -> return ()
327-- TODO: send structured output similar to the metavariable list
328iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
329iputGoal g = do i <- getIState
330 case idris_outputmode i of
331 RawOutput h -> hWriteDoc h i g
332 IdeMode n h ->
333 let (str, spans) = displaySpans . fmap (fancifyAnnots i True) $ g
334 goal = [toSExp str, toSExp spans]
335 in runIO . hPutStrLn h $ convSExp "write-goal" goal n
337-- | Warn about totality problems without failing to compile
338warnTotality :: Idris ()
339warnTotality = do ist <- getIState
340 mapM_ (warn ist) (nub (idris_totcheckfail ist))
341 where warn ist (fc, e) = iWarn fc (pprintErr ist (Msg e))
344printUndefinedNames :: [Name] -> Doc OutputAnnotation
345printUndefinedNames ns = text "Undefined " <> names <> text "."
346 where names = encloseSep empty empty (char ',') $ map ppName ns
347 ppName = prettyName True True []
350prettyDocumentedIst :: IState
351 -> (Name, PTerm, Maybe (Docstring DocTerm))
352 -> Doc OutputAnnotation
353prettyDocumentedIst ist (name, ty, docs) =
354 prettyName True True [] name <+> colon <+> align (prettyIst ist ty) <$>
355 fromMaybe empty (fmap (\d -> renderDocstring (renderDocTerm ppTm norm) d <> line) docs)
356 where ppTm = pprintDelab ist
357 norm = normaliseAll (tt_ctxt ist) []
359sendParserHighlighting :: Idris ()
360sendParserHighlighting =
361 do ist <- getIState
362 let hs = map unwrap . nub . map wrap $ idris_parserHighlights ist
363 sendHighlighting hs
364 ist <- getIState
365 putIState ist {idris_parserHighlights = []}
366 where wrap (fc, a) = (FC' fc, a)
367 unwrap (fc', a) = (unwrapFC fc', a)
369sendHighlighting :: [(FC, OutputAnnotation)] -> Idris ()
370sendHighlighting highlights =
371 do ist <- getIState
372 case idris_outputmode ist of
373 RawOutput _ -> updateIState $
374 \ist -> ist { idris_highlightedRegions =
375 highlights ++ idris_highlightedRegions ist }
376 IdeMode n h ->
377 let fancier = [ toSExp (fc, fancifyAnnots ist False annot)
378 | (fc, annot) <- highlights, fullFC fc
379 ]
380 in case fancier of
381 [] -> return ()
382 _ -> runIO . hPutStrLn h $
383 convSExp "output"
384 (SymbolAtom "ok",
385 (SymbolAtom "highlight-source", fancier)) n
387 where fullFC (FC _ _ _) = True
388 fullFC _ = False
390-- | Write the highlighting information to a file, for use in external tools
391-- or in editors that don't support the IDE protocol
392writeHighlights :: FilePath -> Idris ()
393writeHighlights f =
394 do ist <- getIState
395 let hs = reverse $ idris_highlightedRegions ist
396 let hfile = replaceExtension f "idh"
397 let annots = toSExp [ (fc, fancifyAnnots ist False annot)
398 | (fc@(FC _ _ _), annot) <- hs
399 ]
400 runIO $ writeFile hfile $ sExpToString annots
402clearHighlights :: Idris ()
403clearHighlights = updateIState $ \ist -> ist { idris_highlightedRegions = [] }
405renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String
406renderExternal fmt width doc
407 | width < 1 = throwError . Msg $ "There must be at least one column for the pretty-printer."
408 | otherwise =
409 do ist <- getIState
410 return . wrap fmt .
411 displayDecorated (decorate fmt) .
412 renderPretty 1.0 width .
413 fmap (fancifyAnnots ist True) $
414 doc
415 where
416 decorate _ (AnnFC _) = id
418 decorate HTMLOutput (AnnName _ (Just TypeOutput) d _) =
419 tag "idris-type" d
420 decorate HTMLOutput (AnnName _ (Just FunOutput) d _) =
421 tag "idris-function" d
422 decorate HTMLOutput (AnnName _ (Just DataOutput) d _) =
423 tag "idris-data" d
424 decorate HTMLOutput (AnnName _ (Just MetavarOutput) d _) =
425 tag "idris-metavar" d
426 decorate HTMLOutput (AnnName _ (Just PostulateOutput) d _) =
427 tag "idris-postulate" d
428 decorate HTMLOutput (AnnName _ _ _ _) = id
429 decorate HTMLOutput (AnnBoundName _ True) = tag "idris-bound idris-implicit" Nothing
430 decorate HTMLOutput (AnnBoundName _ False) = tag "idris-bound" Nothing
431 decorate HTMLOutput (AnnConst c) =
432 tag (if constIsType c then "idris-type" else "idris-data")
433 (Just $ constDocs c)
434 decorate HTMLOutput (AnnData _ _) = tag "idris-data" Nothing
435 decorate HTMLOutput (AnnType _ _) = tag "idris-type" Nothing
436 decorate HTMLOutput AnnKeyword = tag "idris-keyword" Nothing
437 decorate HTMLOutput (AnnTextFmt fmt) =
438 case fmt of
439 BoldText -> mkTag "strong"
440 ItalicText -> mkTag "em"
441 UnderlineText -> tag "idris-underlined" Nothing
442 where mkTag t x = "<"++t++">"++x++"</"++t++">"
443 decorate HTMLOutput (AnnTerm _ _) = id
444 decorate HTMLOutput (AnnSearchResult _) = id
445 decorate HTMLOutput (AnnErr _) = id
446 decorate HTMLOutput (AnnNamespace _ _) = id
447 decorate HTMLOutput (AnnLink url) =
448 \txt -> "<a href=\"" ++ url ++ "\">" ++ txt ++ "</a>"
449 decorate HTMLOutput AnnQuasiquote = id
450 decorate HTMLOutput AnnAntiquote = id
451 decorate HTMLOutput (AnnSyntax c) = \txt -> c
453 decorate LaTeXOutput (AnnName _ (Just TypeOutput) _ _) =
454 latex "IdrisType"
455 decorate LaTeXOutput (AnnName _ (Just FunOutput) _ _) =
456 latex "IdrisFunction"
457 decorate LaTeXOutput (AnnName _ (Just DataOutput) _ _) =
458 latex "IdrisData"
459 decorate LaTeXOutput (AnnName _ (Just MetavarOutput) _ _) =
460 latex "IdrisMetavar"
461 decorate LaTeXOutput (AnnName _ (Just PostulateOutput) _ _) =
462 latex "IdrisPostulate"
463 decorate LaTeXOutput (AnnName _ _ _ _) = id
464 decorate LaTeXOutput (AnnBoundName _ True) = latex "IdrisImplicit"
465 decorate LaTeXOutput (AnnBoundName _ False) = latex "IdrisBound"
466 decorate LaTeXOutput (AnnConst c) =
467 latex $ if constIsType c then "IdrisType" else "IdrisData"
468 decorate LaTeXOutput (AnnData _ _) = latex "IdrisData"
469 decorate LaTeXOutput (AnnType _ _) = latex "IdrisType"
470 decorate LaTeXOutput AnnKeyword = latex "IdrisKeyword"
471 decorate LaTeXOutput (AnnTextFmt fmt) =
472 case fmt of
473 BoldText -> latex "textbf"
474 ItalicText -> latex "emph"
475 UnderlineText -> latex "underline"
476 decorate LaTeXOutput (AnnTerm _ _) = id
477 decorate LaTeXOutput (AnnSearchResult _) = id
478 decorate LaTeXOutput (AnnErr _) = id
479 decorate LaTeXOutput (AnnNamespace _ _) = id
480 decorate LaTeXOutput (AnnLink url) = (++ "(\\url{" ++ url ++ "})")
481 decorate LaTeXOutput AnnQuasiquote = id
482 decorate LaTeXOutput AnnAntiquote = id
483 decorate LaTeXOutput (AnnSyntax c) = \txt ->
484 case c of
485 "\\" -> "\\textbackslash"
486 "{" -> "\\{"
487 "}" -> "\\}"
488 "%" -> "\\%"
489 _ -> c
491 tag cls docs str = "<span class=\""++cls++"\""++title++">" ++ str ++ "</span>"
492 where title = maybe "" (\d->" title=\"" ++ d ++ "\"") docs
494 latex cmd str = "\\"++cmd++"{"++str++"}"
496 wrap HTMLOutput str =
497 "<!doctype html><html><head><style>" ++ css ++ "</style></head>" ++
498 "<body><!-- START CODE --><pre>" ++ str ++ "</pre><!-- END CODE --></body></html>"
499 where css = concat . intersperse "\n" $
500 [".idris-data { color: red; } ",
501 ".idris-type { color: blue; }",
502 ".idris-function {color: green; }",
503 ".idris-metavar {color: turquoise; }",
504 ".idris-keyword { font-weight: bold; }",
505 ".idris-bound { color: purple; }",
506 ".idris-implicit { font-style: italic; }",
507 ".idris-underlined { text-decoration: underline; }"]
508 wrap LaTeXOutput str =
509 concat . intersperse "\n" $
510 ["\\documentclass{article}",
511 "\\usepackage{fancyvrb}",
512 "\\usepackage[usenames]{xcolor}"] ++
513 map (\(cmd, color) ->
514 "\\newcommand{\\"++ cmd ++
515 "}[1]{\\textcolor{"++ color ++"}{#1}}")
516 [("IdrisData", "red"), ("IdrisType", "blue"),
517 ("IdrisBound", "magenta"), ("IdrisFunction", "green"),
518 ("IdrisMetavar", "cyan")] ++
519 ["\\newcommand{\\IdrisKeyword}[1]{{\\underline{#1}}}",
520 "\\newcommand{\\IdrisImplicit}[1]{{\\itshape \\IdrisBound{#1}}}",
521 "\n",
522 "\\begin{document}",
523 "% START CODE",
524 "\\begin{Verbatim}[commandchars=\\\\\\{\\}]",
525 str,
526 "\\end{Verbatim}",
527 "% END CODE",
528 "\\end{document}"]