git.iko.soy/Idris-dev
on c79fb21 help sign in
Idris-dev/src/Idris/Output.hs
172 lines 7.2 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
27iWarn :: FC -> Doc OutputAnnotation -> Idris ()
28iWarn fc err =
29 do i <- getIState
30 case idris_outputmode i of
31 RawOutput h ->
32 do err' <- iRender . fmap (fancifyAnnots i) $
33 if fc_fname fc /= ""
34 then text (show fc) <> colon <//> err
35 else err
36 runIO . hPutStrLn h $ displayDecorated (consoleDecorate i) err'
37 IdeSlave n h ->
38 do err' <- iRender . fmap (fancifyAnnots i) $ err
39 let (str, spans) = displaySpans err'
40 runIO . hPutStrLn h $
41 convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n
43iRender :: Doc a -> Idris (SimpleDoc a)
44iRender d = do w <- getWidth
45 ist <- getIState
46 let ideSlave = case idris_outputmode ist of
47 IdeSlave _ _ -> True
48 _ -> False
49 case w of
50 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d
51 ColsWide n -> return $
52 if n < 1
53 then renderPretty 1.0 1000000000 d
54 else renderPretty 0.8 n d
55 AutomaticWidth | ideSlave -> return $ renderPretty 1.0 1000000000 d
56 | otherwise -> do width <- runIO getScreenWidth
57 return $ renderPretty 0.8 width d
59-- | Write a pretty-printed term to the console with semantic coloring
60consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()
61consoleDisplayAnnotated h output = do ist <- getIState
62 rendered <- iRender $ output
63 runIO . hPutStrLn h .
64 displayDecorated (consoleDecorate ist) $
65 rendered
67iPrintTermWithType :: Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
68iPrintTermWithType tm ty = iRenderResult (tm <+> colon <+> align ty)
70-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name
71iPrintFunTypes :: [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()
72iPrintFunTypes bnd n [] = iPrintError $ "No such variable " ++ show n
73iPrintFunTypes bnd n overloads = do ist <- getIState
74 let ppo = ppOptionIst ist
75 let infixes = idris_infixes ist
76 let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)
77 iRenderResult output
78 where fullName n = prettyName True True bnd n
79 ppOverload ppo infixes n tm =
80 fullName n <+> colon <+> align (pprintPTerm ppo bnd [] infixes tm)
82iRenderOutput :: Doc OutputAnnotation -> Idris ()
83iRenderOutput doc =
84 do i <- getIState
85 case idris_outputmode i of
86 RawOutput h -> do out <- iRender doc
87 runIO $ putStrLn (displayDecorated (consoleDecorate i) out)
88 IdeSlave n h ->
89 do (str, spans) <- fmap displaySpans . iRender . fmap (fancifyAnnots i) $ doc
90 let out = [toSExp str, toSExp spans]
91 runIO . hPutStrLn h $ convSExp "write-decorated" out n
93iRenderResult :: Doc OutputAnnotation -> Idris ()
94iRenderResult d = do ist <- getIState
95 case idris_outputmode ist of
96 RawOutput h -> consoleDisplayAnnotated h d
97 IdeSlave n h -> ideSlaveReturnAnnotated n h d
99ideSlaveReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()
100ideSlaveReturnWithStatus status n h out = do
101 ist <- getIState
102 (str, spans) <- fmap displaySpans .
103 iRender .
104 fmap (fancifyAnnots ist) $
105 out
106 let good = [SymbolAtom status, toSExp str, toSExp spans]
107 runIO . hPutStrLn h $ convSExp "return" good n
110-- | Write pretty-printed output to IDESlave with semantic annotations
111ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
112ideSlaveReturnAnnotated = ideSlaveReturnWithStatus "ok"
114-- | Show an error with semantic highlighting
115iRenderError :: Doc OutputAnnotation -> Idris ()
116iRenderError e = do ist <- getIState
117 case idris_outputmode ist of
118 RawOutput h -> consoleDisplayAnnotated h e
119 IdeSlave n h -> ideSlaveReturnWithStatus "error" n h e
121iPrintWithStatus :: String -> String -> Idris ()
122iPrintWithStatus status s = do
123 i <- getIState
124 case idris_outputmode i of
125 RawOutput h -> case s of
126 "" -> return ()
127 s -> runIO $ hPutStrLn h s
128 IdeSlave n h ->
129 let good = SexpList [SymbolAtom status, toSExp s] in
130 runIO $ hPutStrLn h $ convSExp "return" good n
133iPrintResult :: String -> Idris ()
134iPrintResult = iPrintWithStatus "ok"
136iPrintError :: String -> Idris ()
137iPrintError = iPrintWithStatus "error"
139iputStrLn :: String -> Idris ()
140iputStrLn s = do i <- getIState
141 case idris_outputmode i of
142 RawOutput h -> runIO $ hPutStrLn h s
143 IdeSlave n h -> runIO . hPutStrLn h $ convSExp "write-string" s n
146ideslavePutSExp :: SExpable a => String -> a -> Idris ()
147ideslavePutSExp cmd info = do i <- getIState
148 case idris_outputmode i of
149 IdeSlave n h -> runIO . hPutStrLn h $ convSExp cmd info n
150 _ -> return ()
152-- TODO: send structured output similar to the metavariable list
153iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
154iputGoal g = do i <- getIState
155 case idris_outputmode i of
156 RawOutput h -> runIO $ hPutStrLn h (displayDecorated (consoleDecorate i) g)
157 IdeSlave n h ->
158 let (str, spans) = displaySpans . fmap (fancifyAnnots i) $ g
159 goal = [toSExp str, toSExp spans]
160 in runIO . hPutStrLn h $ convSExp "write-goal" goal n
162-- | Warn about totality problems without failing to compile
163warnTotality :: Idris ()
164warnTotality = do ist <- getIState
165 mapM_ (warn ist) (nub (idris_totcheckfail ist))
166 where warn ist (fc, e) = iWarn fc (pprintErr ist (Msg e))
169printUndefinedNames :: [Name] -> Doc OutputAnnotation
170printUndefinedNames ns = text "Undefined " <> names <> text "."
171 where names = encloseSep empty empty (char ',') $ map ppName ns
172 ppName = prettyName True True []