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