git.iko.soy/Idris-dev
on 2b0224a help sign in
Idris-dev/src/Idris/Output.hs
323 lines 14 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)
22import Prelude hiding ((<$>))
24import Data.Char (isAlpha)
25import Data.List (nub, intersperse)
26import Data.Maybe (fromMaybe)
28instance MonadException m => MonadException (ExceptT Err m) where
29 controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let
30 run' = RunIO (fmap ExceptT . run . runExceptT)
31 in fmap runExceptT $ f run'
33pshow :: IState -> Err -> String
34pshow ist err = displayDecorated (consoleDecorate ist) .
35 renderPretty 1.0 80 .
36 fmap (fancifyAnnots ist True) $ pprintErr ist err
38iWarn :: FC -> Doc OutputAnnotation -> Idris ()
39iWarn fc err =
40 do i <- getIState
41 case idris_outputmode i of
42 RawOutput h ->
43 do err' <- iRender . fmap (fancifyAnnots i True) $
44 case fc of
45 FC fn _ _ | fn /= "" -> text (show fc) <> colon <//> err
46 _ -> err
47 runIO . hPutStrLn h $ displayDecorated (consoleDecorate i) err'
48 IdeMode n h ->
49 do err' <- iRender . fmap (fancifyAnnots i True) $ err
50 let (str, spans) = displaySpans err'
51 runIO . hPutStrLn h $
52 convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n
54iRender :: Doc a -> Idris (SimpleDoc a)
55iRender d = do w <- getWidth
56 ist <- getIState
57 let ideMode = case idris_outputmode ist of
58 IdeMode _ _ -> True
59 _ -> False
60 case w of
61 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d
62 ColsWide n -> return $
63 if n < 1
64 then renderPretty 1.0 1000000000 d
65 else renderPretty 0.8 n d
66 AutomaticWidth | ideMode -> return $ renderPretty 1.0 80 d
67 | otherwise -> do width <- runIO getScreenWidth
68 return $ renderPretty 0.8 width d
70-- | Write a pretty-printed term to the console with semantic coloring
71consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()
72consoleDisplayAnnotated h output = do ist <- getIState
73 rendered <- iRender $ output
74 runIO . hPutStrLn h .
75 displayDecorated (consoleDecorate ist) $
76 rendered
78iPrintTermWithType :: Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
79iPrintTermWithType tm ty = iRenderResult (tm <+> colon <+> align ty)
81-- | Pretty-print a collection of overloadings to REPL or IDEMode - corresponds to :t name
82iPrintFunTypes :: [(Name, Bool)] -> Name -> [(Name, Doc OutputAnnotation)] -> Idris ()
83iPrintFunTypes bnd n [] = iPrintError $ "No such variable " ++ show n
84iPrintFunTypes bnd n overloads = do ist <- getIState
85 let ppo = ppOptionIst ist
86 let infixes = idris_infixes ist
87 let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)
88 iRenderResult output
89 where fullName n = prettyName True True bnd n
90 ppOverload ppo infixes n tm =
91 fullName n <+> colon <+> align tm
93iRenderOutput :: Doc OutputAnnotation -> Idris ()
94iRenderOutput doc =
95 do i <- getIState
96 case idris_outputmode i of
97 RawOutput h -> do out <- iRender doc
98 runIO $ putStrLn (displayDecorated (consoleDecorate i) out)
99 IdeMode n h ->
100 do (str, spans) <- fmap displaySpans . iRender . fmap (fancifyAnnots i True) $ doc
101 let out = [toSExp str, toSExp spans]
102 runIO . hPutStrLn h $ convSExp "write-decorated" out n
104iRenderResult :: Doc OutputAnnotation -> Idris ()
105iRenderResult d = do ist <- getIState
106 case idris_outputmode ist of
107 RawOutput h -> consoleDisplayAnnotated h d
108 IdeMode n h -> ideModeReturnAnnotated n h d
110ideModeReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()
111ideModeReturnWithStatus status n h out = do
112 ist <- getIState
113 (str, spans) <- fmap displaySpans .
114 iRender .
115 fmap (fancifyAnnots ist True) $
116 out
117 let good = [SymbolAtom status, toSExp str, toSExp spans]
118 runIO . hPutStrLn h $ convSExp "return" good n
121-- | Write pretty-printed output to IDEMode with semantic annotations
122ideModeReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
123ideModeReturnAnnotated = ideModeReturnWithStatus "ok"
125-- | Show an error with semantic highlighting
126iRenderError :: Doc OutputAnnotation -> Idris ()
127iRenderError e = do ist <- getIState
128 case idris_outputmode ist of
129 RawOutput h -> consoleDisplayAnnotated h e
130 IdeMode n h -> ideModeReturnWithStatus "error" n h e
132iPrintWithStatus :: String -> String -> Idris ()
133iPrintWithStatus status s = do
134 i <- getIState
135 case idris_outputmode i of
136 RawOutput h -> case s of
137 "" -> return ()
138 s -> runIO $ hPutStrLn h s
139 IdeMode n h ->
140 let good = SexpList [SymbolAtom status, toSExp s] in
141 runIO $ hPutStrLn h $ convSExp "return" good n
144iPrintResult :: String -> Idris ()
145iPrintResult = iPrintWithStatus "ok"
147iPrintError :: String -> Idris ()
148iPrintError = iPrintWithStatus "error"
150iputStrLn :: String -> Idris ()
151iputStrLn s = do i <- getIState
152 case idris_outputmode i of
153 RawOutput h -> runIO $ hPutStrLn h s
154 IdeMode n h -> runIO . hPutStrLn h $ convSExp "write-string" s n
157idemodePutSExp :: SExpable a => String -> a -> Idris ()
158idemodePutSExp cmd info = do i <- getIState
159 case idris_outputmode i of
160 IdeMode n h ->
161 runIO . hPutStrLn h $
162 convSExp cmd info n
163 _ -> return ()
165-- TODO: send structured output similar to the metavariable list
166iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
167iputGoal g = do i <- getIState
168 case idris_outputmode i of
169 RawOutput h -> runIO $ hPutStrLn h (displayDecorated (consoleDecorate i) g)
170 IdeMode n h ->
171 let (str, spans) = displaySpans . fmap (fancifyAnnots i True) $ g
172 goal = [toSExp str, toSExp spans]
173 in runIO . hPutStrLn h $ convSExp "write-goal" goal n
175-- | Warn about totality problems without failing to compile
176warnTotality :: Idris ()
177warnTotality = do ist <- getIState
178 mapM_ (warn ist) (nub (idris_totcheckfail ist))
179 where warn ist (fc, e) = iWarn fc (pprintErr ist (Msg e))
182printUndefinedNames :: [Name] -> Doc OutputAnnotation
183printUndefinedNames ns = text "Undefined " <> names <> text "."
184 where names = encloseSep empty empty (char ',') $ map ppName ns
185 ppName = prettyName True True []
188prettyDocumentedIst :: IState
189 -> (Name, PTerm, Maybe (Docstring DocTerm))
190 -> Doc OutputAnnotation
191prettyDocumentedIst ist (name, ty, docs) =
192 prettyName True True [] name <+> colon <+> align (prettyIst ist ty) <$>
193 fromMaybe empty (fmap (\d -> renderDocstring (renderDocTerm ppTm norm) d <> line) docs)
194 where ppTm = pprintDelab ist
195 norm = normaliseAll (tt_ctxt ist) []
197sendHighlighting :: [(FC, OutputAnnotation)] -> Idris ()
198sendHighlighting highlights =
199 do ist <- getIState
200 case idris_outputmode ist of
201 RawOutput _ -> return ()
202 IdeMode n h ->
203 let fancier = [ toSExp (fc, fancifyAnnots ist False annot)
204 | (fc, annot) <- highlights, fullFC fc
205 ]
206 in case fancier of
207 [] -> return ()
208 _ -> runIO . hPutStrLn h $
209 convSExp "output"
210 (SymbolAtom "ok",
211 (SymbolAtom "highlight-source", fancier)) n
213 where fullFC (FC _ _ _) = True
214 fullFC _ = False
217renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String
218renderExternal fmt width doc
219 | width < 1 = throwError . Msg $ "There must be at least one column for the pretty-printer."
220 | otherwise =
221 do ist <- getIState
222 return . wrap fmt .
223 displayDecorated (decorate fmt) .
224 renderPretty 1.0 width .
225 fmap (fancifyAnnots ist True) $
226 doc
227 where
228 decorate _ (AnnFC _) = id
230 decorate HTMLOutput (AnnName _ (Just TypeOutput) d _) =
231 tag "idris-type" d
232 decorate HTMLOutput (AnnName _ (Just FunOutput) d _) =
233 tag "idris-function" d
234 decorate HTMLOutput (AnnName _ (Just DataOutput) d _) =
235 tag "idris-data" d
236 decorate HTMLOutput (AnnName _ (Just MetavarOutput) d _) =
237 tag "idris-metavar" d
238 decorate HTMLOutput (AnnName _ (Just PostulateOutput) d _) =
239 tag "idris-postulate" d
240 decorate HTMLOutput (AnnName _ _ _ _) = id
241 decorate HTMLOutput (AnnBoundName _ True) = tag "idris-bound idris-implicit" Nothing
242 decorate HTMLOutput (AnnBoundName _ False) = tag "idris-bound" Nothing
243 decorate HTMLOutput (AnnConst c) =
244 tag (if constIsType c then "idris-type" else "idris-data")
245 (Just $ constDocs c)
246 decorate HTMLOutput (AnnData _ _) = tag "idris-data" Nothing
247 decorate HTMLOutput (AnnType _ _) = tag "idris-type" Nothing
248 decorate HTMLOutput AnnKeyword = tag "idris-keyword" Nothing
249 decorate HTMLOutput (AnnTextFmt fmt) =
250 case fmt of
251 BoldText -> mkTag "strong"
252 ItalicText -> mkTag "em"
253 UnderlineText -> tag "idris-underlined" Nothing
254 where mkTag t x = "<"++t++">"++x++"</"++t++">"
255 decorate HTMLOutput (AnnTerm _ _) = id
256 decorate HTMLOutput (AnnSearchResult _) = id
257 decorate HTMLOutput (AnnErr _) = id
258 decorate HTMLOutput (AnnNamespace _ _) = id
260 decorate LaTeXOutput (AnnName _ (Just TypeOutput) _ _) =
261 latex "IdrisType"
262 decorate LaTeXOutput (AnnName _ (Just FunOutput) _ _) =
263 latex "IdrisFunction"
264 decorate LaTeXOutput (AnnName _ (Just DataOutput) _ _) =
265 latex "IdrisData"
266 decorate LaTeXOutput (AnnName _ (Just MetavarOutput) _ _) =
267 latex "IdrisMetavar"
268 decorate LaTeXOutput (AnnName _ (Just PostulateOutput) _ _) =
269 latex "IdrisPostulate"
270 decorate LaTeXOutput (AnnName _ _ _ _) = id
271 decorate LaTeXOutput (AnnBoundName _ True) = latex "IdrisImplicit"
272 decorate LaTeXOutput (AnnBoundName _ False) = latex "IdrisBound"
273 decorate LaTeXOutput (AnnConst c) =
274 latex $ if constIsType c then "IdrisType" else "IdrisData"
275 decorate LaTeXOutput (AnnData _ _) = latex "IdrisData"
276 decorate LaTeXOutput (AnnType _ _) = latex "IdrisType"
277 decorate LaTeXOutput AnnKeyword = latex "IdrisKeyword"
278 decorate LaTeXOutput (AnnTextFmt fmt) =
279 case fmt of
280 BoldText -> latex "textbf"
281 ItalicText -> latex "emph"
282 UnderlineText -> latex "underline"
283 decorate LaTeXOutput (AnnTerm _ _) = id
284 decorate LaTeXOutput (AnnSearchResult _) = id
285 decorate LaTeXOutput (AnnErr _) = id
286 decorate LaTeXOutput (AnnNamespace _ _) = id
288 tag cls docs str = "<span class=\""++cls++"\""++title++">" ++ str ++ "</span>"
289 where title = maybe "" (\d->" title=\"" ++ d ++ "\"") docs
291 latex cmd str = "\\"++cmd++"{"++str++"}"
293 wrap HTMLOutput str =
294 "<!doctype html><html><head><style>" ++ css ++ "</style></head>" ++
295 "<body><!-- START CODE --><pre>" ++ str ++ "</pre><!-- END CODE --></body></html>"
296 where css = concat . intersperse "\n" $
297 [".idris-data { color: red; } ",
298 ".idris-type { color: blue; }",
299 ".idris-function {color: green; }",
300 ".idris-keyword { font-weight: bold; }",
301 ".idris-bound { color: purple; }",
302 ".idris-implicit { font-style: italic; }",
303 ".idris-underlined { text-decoration: underline; }"]
304 wrap LaTeXOutput str =
305 concat . intersperse "\n" $
306 ["\\documentclass{article}",
307 "\\usepackage{fancyvrb}",
308 "\\usepackage[usenames]{xcolor}"] ++
309 map (\(cmd, color) ->
310 "\\newcommand{\\"++ cmd ++
311 "}[1]{\\textcolor{"++ color ++"}{#1}}")
312 [("IdrisData", "red"), ("IdrisType", "blue"),
313 ("IdrisBound", "magenta"), ("IdrisFunction", "green")] ++
314 ["\\newcommand{\\IdrisKeyword}[1]{{\\underline{#1}}}",
315 "\\newcommand{\\IdrisImplicit}[1]{{\\itshape \\IdrisBound{#1}}}",
316 "\n",
317 "\\begin{document}",
318 "% START CODE",
319 "\\begin{Verbatim}[commandchars=\\\\\\{\\}]",
320 str,
321 "\\end{Verbatim}",
322 "% END CODE",
323 "\\end{document}"]