git.iko.soy/Idris-dev
on 40481dc help sign in
Idris-dev/src/Idris/Output.hs
358 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 ist <- getIState
205 putIState ist {idris_parserHighlights = []}
206 where wrap (fc, a) = (FC' fc, a)
207 unwrap (fc', a) = (unwrapFC fc', a)
209sendHighlighting :: [(FC, OutputAnnotation)] -> Idris ()
210sendHighlighting highlights =
211 do ist <- getIState
212 case idris_outputmode ist of
213 RawOutput _ -> updateIState $
214 \ist -> ist { idris_highlightedRegions =
215 highlights ++ idris_highlightedRegions ist }
216 IdeMode n h ->
217 let fancier = [ toSExp (fc, fancifyAnnots ist False annot)
218 | (fc, annot) <- highlights, fullFC fc
219 ]
220 in case fancier of
221 [] -> return ()
222 _ -> runIO . hPutStrLn h $
223 convSExp "output"
224 (SymbolAtom "ok",
225 (SymbolAtom "highlight-source", fancier)) n
227 where fullFC (FC _ _ _) = True
228 fullFC _ = False
230-- | Write the highlighting information to a file, for use in external tools
231-- or in editors that don't support the IDE protocol
232writeHighlights :: FilePath -> Idris ()
233writeHighlights f =
234 do ist <- getIState
235 let hs = reverse $ idris_highlightedRegions ist
236 let hfile = replaceExtension f "idh"
237 let annots = toSExp [ (fc, fancifyAnnots ist False annot)
238 | (fc@(FC _ _ _), annot) <- hs
239 ]
240 runIO $ writeFile hfile $ sExpToString annots
242clearHighlights :: Idris ()
243clearHighlights = updateIState $ \ist -> ist { idris_highlightedRegions = [] }
245renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String
246renderExternal fmt width doc
247 | width < 1 = throwError . Msg $ "There must be at least one column for the pretty-printer."
248 | otherwise =
249 do ist <- getIState
250 return . wrap fmt .
251 displayDecorated (decorate fmt) .
252 renderPretty 1.0 width .
253 fmap (fancifyAnnots ist True) $
254 doc
255 where
256 decorate _ (AnnFC _) = id
258 decorate HTMLOutput (AnnName _ (Just TypeOutput) d _) =
259 tag "idris-type" d
260 decorate HTMLOutput (AnnName _ (Just FunOutput) d _) =
261 tag "idris-function" d
262 decorate HTMLOutput (AnnName _ (Just DataOutput) d _) =
263 tag "idris-data" d
264 decorate HTMLOutput (AnnName _ (Just MetavarOutput) d _) =
265 tag "idris-metavar" d
266 decorate HTMLOutput (AnnName _ (Just PostulateOutput) d _) =
267 tag "idris-postulate" d
268 decorate HTMLOutput (AnnName _ _ _ _) = id
269 decorate HTMLOutput (AnnBoundName _ True) = tag "idris-bound idris-implicit" Nothing
270 decorate HTMLOutput (AnnBoundName _ False) = tag "idris-bound" Nothing
271 decorate HTMLOutput (AnnConst c) =
272 tag (if constIsType c then "idris-type" else "idris-data")
273 (Just $ constDocs c)
274 decorate HTMLOutput (AnnData _ _) = tag "idris-data" Nothing
275 decorate HTMLOutput (AnnType _ _) = tag "idris-type" Nothing
276 decorate HTMLOutput AnnKeyword = tag "idris-keyword" Nothing
277 decorate HTMLOutput (AnnTextFmt fmt) =
278 case fmt of
279 BoldText -> mkTag "strong"
280 ItalicText -> mkTag "em"
281 UnderlineText -> tag "idris-underlined" Nothing
282 where mkTag t x = "<"++t++">"++x++"</"++t++">"
283 decorate HTMLOutput (AnnTerm _ _) = id
284 decorate HTMLOutput (AnnSearchResult _) = id
285 decorate HTMLOutput (AnnErr _) = id
286 decorate HTMLOutput (AnnNamespace _ _) = id
287 decorate HTMLOutput (AnnLink url) =
288 \txt -> "<a href=\"" ++ url ++ "\">" ++ txt ++ "</a>"
289 decorate HTMLOutput AnnQuasiquote = id
290 decorate HTMLOutput AnnAntiquote = id
292 decorate LaTeXOutput (AnnName _ (Just TypeOutput) _ _) =
293 latex "IdrisType"
294 decorate LaTeXOutput (AnnName _ (Just FunOutput) _ _) =
295 latex "IdrisFunction"
296 decorate LaTeXOutput (AnnName _ (Just DataOutput) _ _) =
297 latex "IdrisData"
298 decorate LaTeXOutput (AnnName _ (Just MetavarOutput) _ _) =
299 latex "IdrisMetavar"
300 decorate LaTeXOutput (AnnName _ (Just PostulateOutput) _ _) =
301 latex "IdrisPostulate"
302 decorate LaTeXOutput (AnnName _ _ _ _) = id
303 decorate LaTeXOutput (AnnBoundName _ True) = latex "IdrisImplicit"
304 decorate LaTeXOutput (AnnBoundName _ False) = latex "IdrisBound"
305 decorate LaTeXOutput (AnnConst c) =
306 latex $ if constIsType c then "IdrisType" else "IdrisData"
307 decorate LaTeXOutput (AnnData _ _) = latex "IdrisData"
308 decorate LaTeXOutput (AnnType _ _) = latex "IdrisType"
309 decorate LaTeXOutput AnnKeyword = latex "IdrisKeyword"
310 decorate LaTeXOutput (AnnTextFmt fmt) =
311 case fmt of
312 BoldText -> latex "textbf"
313 ItalicText -> latex "emph"
314 UnderlineText -> latex "underline"
315 decorate LaTeXOutput (AnnTerm _ _) = id
316 decorate LaTeXOutput (AnnSearchResult _) = id
317 decorate LaTeXOutput (AnnErr _) = id
318 decorate LaTeXOutput (AnnNamespace _ _) = id
319 decorate LaTeXOutput (AnnLink url) = (++ "(\\url{" ++ url ++ "})")
320 decorate LaTeXOutput AnnQuasiquote = id
321 decorate LaTeXOutput AnnAntiquote = id
323 tag cls docs str = "<span class=\""++cls++"\""++title++">" ++ str ++ "</span>"
324 where title = maybe "" (\d->" title=\"" ++ d ++ "\"") docs
326 latex cmd str = "\\"++cmd++"{"++str++"}"
328 wrap HTMLOutput str =
329 "<!doctype html><html><head><style>" ++ css ++ "</style></head>" ++
330 "<body><!-- START CODE --><pre>" ++ str ++ "</pre><!-- END CODE --></body></html>"
331 where css = concat . intersperse "\n" $
332 [".idris-data { color: red; } ",
333 ".idris-type { color: blue; }",
334 ".idris-function {color: green; }",
335 ".idris-keyword { font-weight: bold; }",
336 ".idris-bound { color: purple; }",
337 ".idris-implicit { font-style: italic; }",
338 ".idris-underlined { text-decoration: underline; }"]
339 wrap LaTeXOutput str =
340 concat . intersperse "\n" $
341 ["\\documentclass{article}",
342 "\\usepackage{fancyvrb}",
343 "\\usepackage[usenames]{xcolor}"] ++
344 map (\(cmd, color) ->
345 "\\newcommand{\\"++ cmd ++
346 "}[1]{\\textcolor{"++ color ++"}{#1}}")
347 [("IdrisData", "red"), ("IdrisType", "blue"),
348 ("IdrisBound", "magenta"), ("IdrisFunction", "green")] ++
349 ["\\newcommand{\\IdrisKeyword}[1]{{\\underline{#1}}}",
350 "\\newcommand{\\IdrisImplicit}[1]{{\\itshape \\IdrisBound{#1}}}",
351 "\n",
352 "\\begin{document}",
353 "% START CODE",
354 "\\begin{Verbatim}[commandchars=\\\\\\{\\}]",
355 str,
356 "\\end{Verbatim}",
357 "% END CODE",
358 "\\end{document}"]