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