git.iko.soy/Idris-dev
on ccda94e help sign in
Idris-dev/src/Idris/Output.hs
169 lines 7.4 kB history raw
1module Idris.Output where
3import Idris.Core.TT
4import Idris.Core.Evaluate (isDConName, isTConName, isFnName)
6import Idris.AbsSyntax
7import Idris.Delaborate
8import Idris.Docstrings
9import Idris.IdeSlave
11import Util.Pretty
12import Util.ScreenSize (getScreenWidth)
14import Debug.Trace
16import System.IO (stdout, Handle, hPutStrLn)
18import Data.Char (isAlpha)
19import Data.List (nub)
20import Data.Maybe (fromMaybe)
22pshow :: IState -> Err -> String
23pshow ist err = displayDecorated (consoleDecorate ist) .
24 renderPretty 1.0 80 .
25 fmap (fancifyAnnots ist) $ pprintErr ist err
27ihWarn :: Handle -> FC -> Doc OutputAnnotation -> Idris ()
28ihWarn h fc err = do i <- getIState
29 case idris_outputmode i of
30 RawOutput ->
31 do err' <- iRender . fmap (fancifyAnnots i) $
32 if fc_fname fc /= ""
33 then text (show fc) <> colon <//> err
34 else err
35 runIO . hPutStrLn h $ displayDecorated (consoleDecorate i) err'
36 IdeSlave n ->
37 do err' <- iRender . fmap (fancifyAnnots i) $ err
38 let (str, spans) = displaySpans err'
39 runIO . hPutStrLn h $
40 convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n
42iRender :: Doc a -> Idris (SimpleDoc a)
43iRender d = do w <- getWidth
44 ist <- getIState
45 let ideSlave = case idris_outputmode ist of
46 IdeSlave _ -> True
47 _ -> False
48 case w of
49 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d
50 ColsWide n -> return $
51 if n < 1
52 then renderPretty 1.0 1000000000 d
53 else renderPretty 0.8 n d
54 AutomaticWidth | ideSlave -> return $ renderPretty 1.0 1000000000 d
55 | otherwise -> do width <- runIO getScreenWidth
56 return $ renderPretty 0.8 width d
58-- | Write a pretty-printed term to the console with semantic coloring
59consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()
60consoleDisplayAnnotated h output = do ist <- getIState
61 rendered <- iRender $ output
62 runIO . hPutStrLn h .
63 displayDecorated (consoleDecorate ist) $
64 rendered
66ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
67ihPrintTermWithType h tm ty = ihRenderResult h (tm <+> colon <+> align ty)
69-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name
70ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()
71ihPrintFunTypes h bnd n [] = ihPrintError h $ "No such variable " ++ show n
72ihPrintFunTypes h bnd n overloads = do ist <- getIState
73 let ppo = ppOptionIst ist
74 let infixes = idris_infixes ist
75 let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)
76 ihRenderResult h output
77 where fullName n = prettyName True True bnd n
78 ppOverload ppo infixes n tm =
79 fullName n <+> colon <+> align (pprintPTerm ppo bnd [] infixes tm)
81ihRenderOutput :: Handle -> Doc OutputAnnotation -> Idris ()
82ihRenderOutput h doc =
83 do i <- getIState
84 case idris_outputmode i of
85 RawOutput -> do out <- iRender doc
86 runIO $ putStrLn (displayDecorated (consoleDecorate i) out)
87 IdeSlave n ->
88 do (str, spans) <- fmap displaySpans . iRender . fmap (fancifyAnnots i) $ doc
89 let out = [toSExp str, toSExp spans]
90 runIO . putStrLn $ convSExp "write-decorated" out n
92ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()
93ihRenderResult h d = do ist <- getIState
94 case idris_outputmode ist of
95 RawOutput -> consoleDisplayAnnotated h d
96 IdeSlave n -> ideSlaveReturnAnnotated n h d
98ideSlaveReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()
99ideSlaveReturnWithStatus status n h out = do
100 ist <- getIState
101 (str, spans) <- fmap displaySpans .
102 iRender .
103 fmap (fancifyAnnots ist) $
104 out
105 let good = [SymbolAtom status, toSExp str, toSExp spans]
106 runIO . hPutStrLn h $ convSExp "return" good n
109-- | Write pretty-printed output to IDESlave with semantic annotations
110ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
111ideSlaveReturnAnnotated = ideSlaveReturnWithStatus "ok"
113-- | Show an error with semantic highlighting
114ihRenderError :: Handle -> Doc OutputAnnotation -> Idris ()
115ihRenderError h e = do ist <- getIState
116 case idris_outputmode ist of
117 RawOutput -> consoleDisplayAnnotated h e
118 IdeSlave n -> ideSlaveReturnWithStatus "error" n h e
120ihPrintWithStatus :: String -> Handle -> String -> Idris ()
121ihPrintWithStatus status h s = do
122 i <- getIState
123 case idris_outputmode i of
124 RawOutput -> case s of
125 "" -> return ()
126 s -> runIO $ hPutStrLn h s
127 IdeSlave n ->
128 let good = SexpList [SymbolAtom status, toSExp s] in
129 runIO $ hPutStrLn h $ convSExp "return" good n
132ihPrintResult :: Handle -> String -> Idris ()
133ihPrintResult = ihPrintWithStatus "ok"
135ihPrintError :: Handle -> String -> Idris ()
136ihPrintError = ihPrintWithStatus "error"
138ihputStrLn :: Handle -> String -> Idris ()
139ihputStrLn h s = do i <- getIState
140 case idris_outputmode i of
141 RawOutput -> runIO $ hPutStrLn h s
142 IdeSlave n -> runIO . hPutStrLn h $ convSExp "write-string" s n
144iputStrLn = ihputStrLn stdout
145iPrintError = ihPrintError stdout
146iPrintResult = ihPrintResult stdout
147iWarn = ihWarn stdout
149ideslavePutSExp :: SExpable a => String -> a -> Idris ()
150ideslavePutSExp cmd info = do i <- getIState
151 case idris_outputmode i of
152 IdeSlave n -> runIO . putStrLn $ convSExp cmd info n
153 _ -> return ()
155-- TODO: send structured output similar to the metavariable list
156iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
157iputGoal g = do i <- getIState
158 case idris_outputmode i of
159 RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)
160 IdeSlave n ->
161 let (str, spans) = displaySpans . fmap (fancifyAnnots i) $ g
162 goal = [toSExp str, toSExp spans]
163 in runIO . putStrLn $ convSExp "write-goal" goal n
165-- | Warn about totality problems without failing to compile
166warnTotality :: Idris ()
167warnTotality = do ist <- getIState
168 mapM_ (warn ist) (nub (idris_totcheckfail ist))
169 where warn ist (fc, e) = iWarn fc (pprintErr ist (Msg e))