git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/src/Idris/Output.hs
280 lines 12 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.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 (Maybe Term)))
181 -> Doc OutputAnnotation
182prettyDocumentedIst ist (name, ty, docs) =
183 prettyName True True [] name <+> colon <+> align (prettyIst ist ty) <$>
184 fromMaybe empty (fmap (\d -> renderDocstring ppTm (normaliseAll (tt_ctxt ist) []) d <> line) docs)
185 where ppTm = pprintDelab ist
188renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String
189renderExternal fmt width doc
190 | width < 1 = throwError . Msg $ "There must be at least one column for the pretty-printer."
191 | otherwise =
192 do ist <- getIState
193 return . wrap fmt .
194 displayDecorated (decorate fmt) .
195 renderPretty 1.0 width .
196 fmap (fancifyAnnots ist) $
197 doc
198 where
199 decorate _ (AnnFC _) = id
201 decorate HTMLOutput (AnnName _ (Just TypeOutput) d _) =
202 tag "idris-type" d
203 decorate HTMLOutput (AnnName _ (Just FunOutput) d _) =
204 tag "idris-function" d
205 decorate HTMLOutput (AnnName _ (Just DataOutput) d _) =
206 tag "idris-data" d
207 decorate HTMLOutput (AnnName _ (Just MetavarOutput) d _) =
208 tag "idris-metavar" d
209 decorate HTMLOutput (AnnName _ (Just PostulateOutput) d _) =
210 tag "idris-postulate" d
211 decorate HTMLOutput (AnnName _ _ _ _) = id
212 decorate HTMLOutput (AnnBoundName _ True) = tag "idris-bound idris-implicit" Nothing
213 decorate HTMLOutput (AnnBoundName _ False) = tag "idris-bound" Nothing
214 decorate HTMLOutput (AnnConst c) =
215 tag (if constIsType c then "idris-type" else "idris-data")
216 (Just $ constDocs c)
217 decorate HTMLOutput (AnnData _ _) = tag "idris-data" Nothing
218 decorate HTMLOutput (AnnType _ _) = tag "idris-type" Nothing
219 decorate HTMLOutput AnnKeyword = tag "idris-keyword" Nothing
220 decorate HTMLOutput (AnnTextFmt _) = id -- TODO
221 decorate HTMLOutput (AnnTerm _ _) = id
222 decorate HTMLOutput (AnnSearchResult _) = id
224 decorate LaTeXOutput (AnnName _ (Just TypeOutput) _ _) =
225 latex "IdrisType"
226 decorate LaTeXOutput (AnnName _ (Just FunOutput) _ _) =
227 latex "IdrisFunction"
228 decorate LaTeXOutput (AnnName _ (Just DataOutput) _ _) =
229 latex "IdrisData"
230 decorate LaTeXOutput (AnnName _ (Just MetavarOutput) _ _) =
231 latex "IdrisMetavar"
232 decorate LaTeXOutput (AnnName _ (Just PostulateOutput) _ _) =
233 latex "IdrisPostulate"
234 decorate LaTeXOutput (AnnName _ _ _ _) = id
235 decorate LaTeXOutput (AnnBoundName _ True) = latex "IdrisImplicit"
236 decorate LaTeXOutput (AnnBoundName _ False) = latex "IdrisBound"
237 decorate LaTeXOutput (AnnConst c) =
238 latex $ if constIsType c then "IdrisType" else "IdrisData"
239 decorate LaTeXOutput (AnnData _ _) = latex "IdrisData"
240 decorate LaTeXOutput (AnnType _ _) = latex "IdrisType"
241 decorate LaTeXOutput AnnKeyword = latex "IdrisKeyword"
242 decorate LaTeXOutput (AnnTextFmt _) = id -- TODO
243 decorate LaTeXOutput (AnnTerm _ _) = id
244 decorate LaTeXOutput (AnnSearchResult _) = id
246 tag cls docs str = "<span class=\""++cls++"\""++title++">" ++ str ++ "</span>"
247 where title = maybe "" (\d->" title=\"" ++ d ++ "\"") docs
249 latex cmd str = "\\"++cmd++"{"++str++"}"
251 wrap HTMLOutput str =
252 "<!doctype html><html><head><style>" ++ css ++ "</style></head>" ++
253 "<body><!-- START CODE --><pre>" ++ str ++ "</pre><!-- END CODE --></body></html>"
254 where css = concat . intersperse "\n" $
255 [".idris-data { color: red; } ",
256 ".idris-type { color: blue; }",
257 ".idris-function {color: green; }",
258 ".idris-keyword { font-weight: bold; }",
259 ".idris-bound { color: purple; }",
260 ".idris-implicit { font-style: italic; }"]
261 wrap LaTeXOutput str =
262 concat . intersperse "\n" $
263 ["\\documentclass{article}",
264 "\\usepackage{fancyvrb}",
265 "\\usepackage[usenames]{xcolor}"] ++
266 map (\(cmd, color) ->
267 "\\newcommand{\\"++ cmd ++
268 "}[1]{\\textcolor{"++ color ++"}{#1}}")
269 [("IdrisData", "red"), ("IdrisType", "blue"),
270 ("IdrisBound", "magenta"), ("IdrisFunction", "green")] ++
271 ["\\newcommand{\\IdrisKeyword}[1]{{\\underline{#1}}}",
272 "\\newcommand{\\IdrisImplicit}[1]{{\\itshape \\IdrisBound{#1}}}",
273 "\n",
274 "\\begin{document}",
275 "% START CODE",
276 "\\begin{Verbatim}[commandchars=\\\\\\{\\}]",
277 str,
278 "\\end{Verbatim}",
279 "% END CODE",
280 "\\end{document}"]