git.iko.soy/Idris-dev
on f2d752a help sign in
Idris-dev/src/Idris/Output.hs
293 lines 12 kB history raw
1{-# OPTIONS_GHC -fwarn-incomplete-patterns -Werror #-}
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.IdeSlave
13import Util.Pretty
14import Util.ScreenSize (getScreenWidth)
16import Debug.Trace
18import Control.Monad.Error (throwError)
20import System.IO (stdout, Handle, hPutStrLn)
22import Data.Char (isAlpha)
23import Data.List (nub, intersperse)
24import Data.Maybe (fromMaybe)
26pshow :: IState -> Err -> String
27pshow ist err = displayDecorated (consoleDecorate ist) .
28 renderPretty 1.0 80 .
29 fmap (fancifyAnnots ist) $ pprintErr ist err
31iWarn :: FC -> Doc OutputAnnotation -> Idris ()
32iWarn fc err =
33 do i <- getIState
34 case idris_outputmode i of
35 RawOutput h ->
36 do err' <- iRender . fmap (fancifyAnnots i) $
37 if fc_fname fc /= ""
38 then text (show fc) <> colon <//> err
39 else err
40 runIO . hPutStrLn h $ displayDecorated (consoleDecorate i) err'
41 IdeSlave n h ->
42 do err' <- iRender . fmap (fancifyAnnots i) $ err
43 let (str, spans) = displaySpans err'
44 runIO . hPutStrLn h $
45 convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n
47iRender :: Doc a -> Idris (SimpleDoc a)
48iRender d = do w <- getWidth
49 ist <- getIState
50 let ideSlave = case idris_outputmode ist of
51 IdeSlave _ _ -> True
52 _ -> False
53 case w of
54 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d
55 ColsWide n -> return $
56 if n < 1
57 then renderPretty 1.0 1000000000 d
58 else renderPretty 0.8 n d
59 AutomaticWidth | ideSlave -> return $ renderPretty 1.0 1000000000 d
60 | otherwise -> do width <- runIO getScreenWidth
61 return $ renderPretty 0.8 width d
63-- | Write a pretty-printed term to the console with semantic coloring
64consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()
65consoleDisplayAnnotated h output = do ist <- getIState
66 rendered <- iRender $ output
67 runIO . hPutStrLn h .
68 displayDecorated (consoleDecorate ist) $
69 rendered
71iPrintTermWithType :: Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
72iPrintTermWithType tm ty = iRenderResult (tm <+> colon <+> align ty)
74-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name
75iPrintFunTypes :: [(Name, Bool)] -> Name -> [(Name, Doc OutputAnnotation)] -> Idris ()
76iPrintFunTypes bnd n [] = iPrintError $ "No such variable " ++ show n
77iPrintFunTypes bnd n overloads = do ist <- getIState
78 let ppo = ppOptionIst ist
79 let infixes = idris_infixes ist
80 let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)
81 iRenderResult output
82 where fullName n = prettyName True True bnd n
83 ppOverload ppo infixes n tm =
84 fullName n <+> colon <+> align tm
86iRenderOutput :: Doc OutputAnnotation -> Idris ()
87iRenderOutput doc =
88 do i <- getIState
89 case idris_outputmode i of
90 RawOutput h -> do out <- iRender doc
91 runIO $ putStrLn (displayDecorated (consoleDecorate i) out)
92 IdeSlave n h ->
93 do (str, spans) <- fmap displaySpans . iRender . fmap (fancifyAnnots i) $ doc
94 let out = [toSExp str, toSExp spans]
95 runIO . hPutStrLn h $ convSExp "write-decorated" out n
97iRenderResult :: Doc OutputAnnotation -> Idris ()
98iRenderResult d = do ist <- getIState
99 case idris_outputmode ist of
100 RawOutput h -> consoleDisplayAnnotated h d
101 IdeSlave n h -> ideSlaveReturnAnnotated n h d
103ideSlaveReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()
104ideSlaveReturnWithStatus status n h out = do
105 ist <- getIState
106 (str, spans) <- fmap displaySpans .
107 iRender .
108 fmap (fancifyAnnots ist) $
109 out
110 let good = [SymbolAtom status, toSExp str, toSExp spans]
111 runIO . hPutStrLn h $ convSExp "return" good n
114-- | Write pretty-printed output to IDESlave with semantic annotations
115ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
116ideSlaveReturnAnnotated = ideSlaveReturnWithStatus "ok"
118-- | Show an error with semantic highlighting
119iRenderError :: Doc OutputAnnotation -> Idris ()
120iRenderError e = do ist <- getIState
121 case idris_outputmode ist of
122 RawOutput h -> consoleDisplayAnnotated h e
123 IdeSlave n h -> ideSlaveReturnWithStatus "error" n h e
125iPrintWithStatus :: String -> String -> Idris ()
126iPrintWithStatus status s = do
127 i <- getIState
128 case idris_outputmode i of
129 RawOutput h -> case s of
130 "" -> return ()
131 s -> runIO $ hPutStrLn h s
132 IdeSlave n h ->
133 let good = SexpList [SymbolAtom status, toSExp s] in
134 runIO $ hPutStrLn h $ convSExp "return" good n
137iPrintResult :: String -> Idris ()
138iPrintResult = iPrintWithStatus "ok"
140iPrintError :: String -> Idris ()
141iPrintError = iPrintWithStatus "error"
143iputStrLn :: String -> Idris ()
144iputStrLn s = do i <- getIState
145 case idris_outputmode i of
146 RawOutput h -> runIO $ hPutStrLn h s
147 IdeSlave n h -> runIO . hPutStrLn h $ convSExp "write-string" s n
150ideslavePutSExp :: SExpable a => String -> a -> Idris ()
151ideslavePutSExp cmd info = do i <- getIState
152 case idris_outputmode i of
153 IdeSlave n h -> runIO . hPutStrLn h $ convSExp cmd info n
154 _ -> return ()
156-- TODO: send structured output similar to the metavariable list
157iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
158iputGoal g = do i <- getIState
159 case idris_outputmode i of
160 RawOutput h -> runIO $ hPutStrLn h (displayDecorated (consoleDecorate i) g)
161 IdeSlave n h ->
162 let (str, spans) = displaySpans . fmap (fancifyAnnots i) $ g
163 goal = [toSExp str, toSExp spans]
164 in runIO . hPutStrLn h $ convSExp "write-goal" goal n
166-- | Warn about totality problems without failing to compile
167warnTotality :: Idris ()
168warnTotality = do ist <- getIState
169 mapM_ (warn ist) (nub (idris_totcheckfail ist))
170 where warn ist (fc, e) = iWarn fc (pprintErr ist (Msg e))
173printUndefinedNames :: [Name] -> Doc OutputAnnotation
174printUndefinedNames ns = text "Undefined " <> names <> text "."
175 where names = encloseSep empty empty (char ',') $ map ppName ns
176 ppName = prettyName True True []
179prettyDocumentedIst :: IState
180 -> (Name, PTerm, Maybe (Docstring DocTerm))
181 -> Doc OutputAnnotation
182prettyDocumentedIst ist (name, ty, docs) =
183 prettyName True True [] name <+> colon <+> align (prettyIst ist ty) <$>
184 fromMaybe empty (fmap (\d -> renderDocstring (renderDocTerm ppTm norm) d <> line) docs)
185 where ppTm = pprintDelab ist
186 norm = normaliseAll (tt_ctxt ist) []
189renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String
190renderExternal fmt width doc
191 | width < 1 = throwError . Msg $ "There must be at least one column for the pretty-printer."
192 | otherwise =
193 do ist <- getIState
194 return . wrap fmt .
195 displayDecorated (decorate fmt) .
196 renderPretty 1.0 width .
197 fmap (fancifyAnnots ist) $
198 doc
199 where
200 decorate _ (AnnFC _) = id
202 decorate HTMLOutput (AnnName _ (Just TypeOutput) d _) =
203 tag "idris-type" d
204 decorate HTMLOutput (AnnName _ (Just FunOutput) d _) =
205 tag "idris-function" d
206 decorate HTMLOutput (AnnName _ (Just DataOutput) d _) =
207 tag "idris-data" d
208 decorate HTMLOutput (AnnName _ (Just MetavarOutput) d _) =
209 tag "idris-metavar" d
210 decorate HTMLOutput (AnnName _ (Just PostulateOutput) d _) =
211 tag "idris-postulate" d
212 decorate HTMLOutput (AnnName _ _ _ _) = id
213 decorate HTMLOutput (AnnBoundName _ True) = tag "idris-bound idris-implicit" Nothing
214 decorate HTMLOutput (AnnBoundName _ False) = tag "idris-bound" Nothing
215 decorate HTMLOutput (AnnConst c) =
216 tag (if constIsType c then "idris-type" else "idris-data")
217 (Just $ constDocs c)
218 decorate HTMLOutput (AnnData _ _) = tag "idris-data" Nothing
219 decorate HTMLOutput (AnnType _ _) = tag "idris-type" Nothing
220 decorate HTMLOutput AnnKeyword = tag "idris-keyword" Nothing
221 decorate HTMLOutput (AnnTextFmt fmt) =
222 case fmt of
223 BoldText -> mkTag "strong"
224 ItalicText -> mkTag "em"
225 UnderlineText -> tag "idris-underlined" Nothing
226 where mkTag t x = "<"++t++">"++x++"</"++t++">"
227 decorate HTMLOutput (AnnTerm _ _) = id
228 decorate HTMLOutput (AnnSearchResult _) = id
229 decorate HTMLOutput (AnnErr _) = id
231 decorate LaTeXOutput (AnnName _ (Just TypeOutput) _ _) =
232 latex "IdrisType"
233 decorate LaTeXOutput (AnnName _ (Just FunOutput) _ _) =
234 latex "IdrisFunction"
235 decorate LaTeXOutput (AnnName _ (Just DataOutput) _ _) =
236 latex "IdrisData"
237 decorate LaTeXOutput (AnnName _ (Just MetavarOutput) _ _) =
238 latex "IdrisMetavar"
239 decorate LaTeXOutput (AnnName _ (Just PostulateOutput) _ _) =
240 latex "IdrisPostulate"
241 decorate LaTeXOutput (AnnName _ _ _ _) = id
242 decorate LaTeXOutput (AnnBoundName _ True) = latex "IdrisImplicit"
243 decorate LaTeXOutput (AnnBoundName _ False) = latex "IdrisBound"
244 decorate LaTeXOutput (AnnConst c) =
245 latex $ if constIsType c then "IdrisType" else "IdrisData"
246 decorate LaTeXOutput (AnnData _ _) = latex "IdrisData"
247 decorate LaTeXOutput (AnnType _ _) = latex "IdrisType"
248 decorate LaTeXOutput AnnKeyword = latex "IdrisKeyword"
249 decorate LaTeXOutput (AnnTextFmt fmt) =
250 case fmt of
251 BoldText -> latex "textbf"
252 ItalicText -> latex "emph"
253 UnderlineText -> latex "underline"
254 decorate LaTeXOutput (AnnTerm _ _) = id
255 decorate LaTeXOutput (AnnSearchResult _) = id
256 decorate LaTeXOutput (AnnErr _) = id
258 tag cls docs str = "<span class=\""++cls++"\""++title++">" ++ str ++ "</span>"
259 where title = maybe "" (\d->" title=\"" ++ d ++ "\"") docs
261 latex cmd str = "\\"++cmd++"{"++str++"}"
263 wrap HTMLOutput str =
264 "<!doctype html><html><head><style>" ++ css ++ "</style></head>" ++
265 "<body><!-- START CODE --><pre>" ++ str ++ "</pre><!-- END CODE --></body></html>"
266 where css = concat . intersperse "\n" $
267 [".idris-data { color: red; } ",
268 ".idris-type { color: blue; }",
269 ".idris-function {color: green; }",
270 ".idris-keyword { font-weight: bold; }",
271 ".idris-bound { color: purple; }",
272 ".idris-implicit { font-style: italic; }",
273 ".idris-underlined { text-decoration: underline; }"]
274 wrap LaTeXOutput str =
275 concat . intersperse "\n" $
276 ["\\documentclass{article}",
277 "\\usepackage{fancyvrb}",
278 "\\usepackage[usenames]{xcolor}"] ++
279 map (\(cmd, color) ->
280 "\\newcommand{\\"++ cmd ++
281 "}[1]{\\textcolor{"++ color ++"}{#1}}")
282 [("IdrisData", "red"), ("IdrisType", "blue"),
283 ("IdrisBound", "magenta"), ("IdrisFunction", "green")] ++
284 ["\\newcommand{\\IdrisKeyword}[1]{{\\underline{#1}}}",
285 "\\newcommand{\\IdrisImplicit}[1]{{\\itshape \\IdrisBound{#1}}}",
286 "\n",
287 "\\begin{document}",
288 "% START CODE",
289 "\\begin{Verbatim}[commandchars=\\\\\\{\\}]",
290 str,
291 "\\end{Verbatim}",
292 "% END CODE",
293 "\\end{document}"]