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