git.iko.soy/Idris-dev
on f3ecd90 help sign in
Idris-dev/src/Idris/Output.hs
270 lines 11 kB history raw
1{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3module Idris.Output where
5import Idris.Core.TT
6import Idris.Core.Evaluate (isDConName, isTConName, isFnName)
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 []
178renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String
179renderExternal fmt width doc
180 | width < 1 = throwError . Msg $ "There must be at least one column for the pretty-printer."
181 | otherwise =
182 do ist <- getIState
183 return . wrap fmt .
184 displayDecorated (decorate fmt) .
185 renderPretty 1.0 width .
186 fmap (fancifyAnnots ist) $
187 doc
188 where
189 decorate _ (AnnFC _) = id
191 decorate HTMLOutput (AnnName _ (Just TypeOutput) d _) =
192 tag "idris-type" d
193 decorate HTMLOutput (AnnName _ (Just FunOutput) d _) =
194 tag "idris-function" d
195 decorate HTMLOutput (AnnName _ (Just DataOutput) d _) =
196 tag "idris-data" d
197 decorate HTMLOutput (AnnName _ (Just MetavarOutput) d _) =
198 tag "idris-metavar" d
199 decorate HTMLOutput (AnnName _ (Just PostulateOutput) d _) =
200 tag "idris-postulate" d
201 decorate HTMLOutput (AnnName _ _ _ _) = id
202 decorate HTMLOutput (AnnBoundName _ True) = tag "idris-bound idris-implicit" Nothing
203 decorate HTMLOutput (AnnBoundName _ False) = tag "idris-bound" Nothing
204 decorate HTMLOutput (AnnConst c) =
205 tag (if constIsType c then "idris-type" else "idris-data")
206 (Just $ constDocs c)
207 decorate HTMLOutput (AnnData _ _) = tag "idris-data" Nothing
208 decorate HTMLOutput (AnnType _ _) = tag "idris-type" Nothing
209 decorate HTMLOutput AnnKeyword = tag "idris-keyword" Nothing
210 decorate HTMLOutput (AnnTextFmt _) = id -- TODO
211 decorate HTMLOutput (AnnTerm _ _) = id
212 decorate HTMLOutput (AnnSearchResult _) = id
214 decorate LaTeXOutput (AnnName _ (Just TypeOutput) _ _) =
215 latex "IdrisType"
216 decorate LaTeXOutput (AnnName _ (Just FunOutput) _ _) =
217 latex "IdrisFunction"
218 decorate LaTeXOutput (AnnName _ (Just DataOutput) _ _) =
219 latex "IdrisData"
220 decorate LaTeXOutput (AnnName _ (Just MetavarOutput) _ _) =
221 latex "IdrisMetavar"
222 decorate LaTeXOutput (AnnName _ (Just PostulateOutput) _ _) =
223 latex "IdrisPostulate"
224 decorate LaTeXOutput (AnnName _ _ _ _) = id
225 decorate LaTeXOutput (AnnBoundName _ True) = latex "IdrisImplicit"
226 decorate LaTeXOutput (AnnBoundName _ False) = latex "IdrisBound"
227 decorate LaTeXOutput (AnnConst c) =
228 latex $ if constIsType c then "IdrisType" else "IdrisData"
229 decorate LaTeXOutput (AnnData _ _) = latex "IdrisData"
230 decorate LaTeXOutput (AnnType _ _) = latex "IdrisType"
231 decorate LaTeXOutput AnnKeyword = latex "IdrisKeyword"
232 decorate LaTeXOutput (AnnTextFmt _) = id -- TODO
233 decorate LaTeXOutput (AnnTerm _ _) = id
234 decorate LaTeXOutput (AnnSearchResult _) = id
236 tag cls docs str = "<span class=\""++cls++"\""++title++">" ++ str ++ "</span>"
237 where title = maybe "" (\d->" title=\"" ++ d ++ "\"") docs
239 latex cmd str = "\\"++cmd++"{"++str++"}"
241 wrap HTMLOutput str =
242 "<!doctype html><html><head><style>" ++ css ++ "</style></head>" ++
243 "<body><!-- START CODE --><pre>" ++ str ++ "</pre><!-- END CODE --></body></html>"
244 where css = concat . intersperse "\n" $
245 [".idris-data { color: red; } ",
246 ".idris-type { color: blue; }",
247 ".idris-function {color: green; }",
248 ".idris-keyword { font-weight: bold; }",
249 ".idris-bound { color: purple; }",
250 ".idris-implicit { font-style: italic; }"]
251 wrap LaTeXOutput str =
252 concat . intersperse "\n" $
253 ["\\documentclass{article}",
254 "\\usepackage{fancyvrb}",
255 "\\usepackage[usenames]{xcolor}"] ++
256 map (\(cmd, color) ->
257 "\\newcommand{\\"++ cmd ++
258 "}[1]{\\textcolor{"++ color ++"}{#1}}")
259 [("IdrisData", "red"), ("IdrisType", "blue"),
260 ("IdrisBound", "magenta"), ("IdrisFunction", "green")] ++
261 ["\\newcommand{\\IdrisKeyword}[1]{{\\underline{#1}}}",
262 "\\newcommand{\\IdrisImplicit}[1]{{\\itshape \\IdrisBound{#1}}}",
263 "\n",
264 "\\begin{document}",
265 "% START CODE",
266 "\\begin{Verbatim}[commandchars=\\\\\\{\\}]",
267 str,
268 "\\end{Verbatim}",
269 "% END CODE",
270 "\\end{document}"]