git.iko.soy/Idris-dev
on 8a3d348 help sign in
Idris-dev/src/Idris/Output.hs
302 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 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) $ 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) $
44 if fc_fname fc /= ""
45 then text (show fc) <> colon <//> err
46 else err
47 runIO . hPutStrLn h $ displayDecorated (consoleDecorate i) err'
48 IdeMode n h ->
49 do err' <- iRender . fmap (fancifyAnnots i) $ 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) $ 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) $
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) $ 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) []
198renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String
199renderExternal fmt width doc
200 | width < 1 = throwError . Msg $ "There must be at least one column for the pretty-printer."
201 | otherwise =
202 do ist <- getIState
203 return . wrap fmt .
204 displayDecorated (decorate fmt) .
205 renderPretty 1.0 width .
206 fmap (fancifyAnnots ist) $
207 doc
208 where
209 decorate _ (AnnFC _) = id
211 decorate HTMLOutput (AnnName _ (Just TypeOutput) d _) =
212 tag "idris-type" d
213 decorate HTMLOutput (AnnName _ (Just FunOutput) d _) =
214 tag "idris-function" d
215 decorate HTMLOutput (AnnName _ (Just DataOutput) d _) =
216 tag "idris-data" d
217 decorate HTMLOutput (AnnName _ (Just MetavarOutput) d _) =
218 tag "idris-metavar" d
219 decorate HTMLOutput (AnnName _ (Just PostulateOutput) d _) =
220 tag "idris-postulate" d
221 decorate HTMLOutput (AnnName _ _ _ _) = id
222 decorate HTMLOutput (AnnBoundName _ True) = tag "idris-bound idris-implicit" Nothing
223 decorate HTMLOutput (AnnBoundName _ False) = tag "idris-bound" Nothing
224 decorate HTMLOutput (AnnConst c) =
225 tag (if constIsType c then "idris-type" else "idris-data")
226 (Just $ constDocs c)
227 decorate HTMLOutput (AnnData _ _) = tag "idris-data" Nothing
228 decorate HTMLOutput (AnnType _ _) = tag "idris-type" Nothing
229 decorate HTMLOutput AnnKeyword = tag "idris-keyword" Nothing
230 decorate HTMLOutput (AnnTextFmt fmt) =
231 case fmt of
232 BoldText -> mkTag "strong"
233 ItalicText -> mkTag "em"
234 UnderlineText -> tag "idris-underlined" Nothing
235 where mkTag t x = "<"++t++">"++x++"</"++t++">"
236 decorate HTMLOutput (AnnTerm _ _) = id
237 decorate HTMLOutput (AnnSearchResult _) = id
238 decorate HTMLOutput (AnnErr _) = id
240 decorate LaTeXOutput (AnnName _ (Just TypeOutput) _ _) =
241 latex "IdrisType"
242 decorate LaTeXOutput (AnnName _ (Just FunOutput) _ _) =
243 latex "IdrisFunction"
244 decorate LaTeXOutput (AnnName _ (Just DataOutput) _ _) =
245 latex "IdrisData"
246 decorate LaTeXOutput (AnnName _ (Just MetavarOutput) _ _) =
247 latex "IdrisMetavar"
248 decorate LaTeXOutput (AnnName _ (Just PostulateOutput) _ _) =
249 latex "IdrisPostulate"
250 decorate LaTeXOutput (AnnName _ _ _ _) = id
251 decorate LaTeXOutput (AnnBoundName _ True) = latex "IdrisImplicit"
252 decorate LaTeXOutput (AnnBoundName _ False) = latex "IdrisBound"
253 decorate LaTeXOutput (AnnConst c) =
254 latex $ if constIsType c then "IdrisType" else "IdrisData"
255 decorate LaTeXOutput (AnnData _ _) = latex "IdrisData"
256 decorate LaTeXOutput (AnnType _ _) = latex "IdrisType"
257 decorate LaTeXOutput AnnKeyword = latex "IdrisKeyword"
258 decorate LaTeXOutput (AnnTextFmt fmt) =
259 case fmt of
260 BoldText -> latex "textbf"
261 ItalicText -> latex "emph"
262 UnderlineText -> latex "underline"
263 decorate LaTeXOutput (AnnTerm _ _) = id
264 decorate LaTeXOutput (AnnSearchResult _) = id
265 decorate LaTeXOutput (AnnErr _) = id
267 tag cls docs str = "<span class=\""++cls++"\""++title++">" ++ str ++ "</span>"
268 where title = maybe "" (\d->" title=\"" ++ d ++ "\"") docs
270 latex cmd str = "\\"++cmd++"{"++str++"}"
272 wrap HTMLOutput str =
273 "<!doctype html><html><head><style>" ++ css ++ "</style></head>" ++
274 "<body><!-- START CODE --><pre>" ++ str ++ "</pre><!-- END CODE --></body></html>"
275 where css = concat . intersperse "\n" $
276 [".idris-data { color: red; } ",
277 ".idris-type { color: blue; }",
278 ".idris-function {color: green; }",
279 ".idris-keyword { font-weight: bold; }",
280 ".idris-bound { color: purple; }",
281 ".idris-implicit { font-style: italic; }",
282 ".idris-underlined { text-decoration: underline; }"]
283 wrap LaTeXOutput str =
284 concat . intersperse "\n" $
285 ["\\documentclass{article}",
286 "\\usepackage{fancyvrb}",
287 "\\usepackage[usenames]{xcolor}"] ++
288 map (\(cmd, color) ->
289 "\\newcommand{\\"++ cmd ++
290 "}[1]{\\textcolor{"++ color ++"}{#1}}")
291 [("IdrisData", "red"), ("IdrisType", "blue"),
292 ("IdrisBound", "magenta"), ("IdrisFunction", "green")] ++
293 ["\\newcommand{\\IdrisKeyword}[1]{{\\underline{#1}}}",
294 "\\newcommand{\\IdrisImplicit}[1]{{\\itshape \\IdrisBound{#1}}}",
295 "\n",
296 "\\begin{document}",
297 "% START CODE",
298 "\\begin{Verbatim}[commandchars=\\\\\\{\\}]",
299 str,
300 "\\end{Verbatim}",
301 "% END CODE",
302 "\\end{document}"]