git.iko.soy/Idris-dev
on cd8a233 help sign in
Idris-dev/src/Idris/Output.hs
187 lines 9.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.List (nub)
20pshow :: IState -> Err -> String
21pshow ist err = displayDecorated (consoleDecorate ist) .
22 renderPretty 1.0 80 .
23 fmap (fancifyAnnots ist) $ pprintErr ist err
25ihWarn :: Handle -> FC -> Doc OutputAnnotation -> Idris ()
26ihWarn h fc err = do i <- getIState
27 case idris_outputmode i of
28 RawOutput ->
29 do err' <- iRender . fmap (fancifyAnnots i) $
30 if fc_fname fc /= ""
31 then text (show fc) <> colon <//> err
32 else err
33 runIO . hPutStrLn h $ displayDecorated (consoleDecorate i) err'
34 IdeSlave n ->
35 do err' <- iRender . fmap (fancifyAnnots i) $ err
36 let (str, spans) = displaySpans err'
37 runIO . hPutStrLn h $
38 convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n
40iRender :: Doc a -> Idris (SimpleDoc a)
41iRender d = do w <- getWidth
42 ist <- getIState
43 let ideSlave = case idris_outputmode ist of
44 IdeSlave _ -> True
45 _ -> False
46 case w of
47 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d
48 ColsWide n -> return $
49 if n < 1
50 then renderPretty 1.0 1000000000 d
51 else renderPretty 0.8 n d
52 AutomaticWidth | ideSlave -> return $ renderPretty 1.0 1000000000 d
53 | otherwise -> do width <- runIO getScreenWidth
54 return $ renderPretty 0.8 width d
56ihPrintResult :: Handle -> String -> Idris ()
57ihPrintResult h s = do i <- getIState
58 case idris_outputmode i of
59 RawOutput -> case s of
60 "" -> return ()
61 s -> runIO $ hPutStrLn h s
62 IdeSlave n ->
63 let good = SexpList [SymbolAtom "ok", toSExp s] in
64 runIO $ hPutStrLn h $ convSExp "return" good n
66-- | Write a pretty-printed term to the console with semantic coloring
67consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()
68consoleDisplayAnnotated h output = do ist <- getIState
69 rendered <- iRender $ output
70 runIO . hPutStrLn h .
71 displayDecorated (consoleDecorate ist) $
72 rendered
75-- | Write pretty-printed output to IDESlave with semantic annotations
76ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
77ideSlaveReturnAnnotated n h out = do ist <- getIState
78 (str, spans) <- fmap displaySpans .
79 iRender .
80 fmap (fancifyAnnots ist) $
81 out
82 let good = [SymbolAtom "ok", toSExp str, toSExp spans]
83 runIO . hPutStrLn h $ convSExp "return" good n
85ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
86ihPrintTermWithType h tm ty = do ist <- getIState
87 let output = tm <+> colon <+> align ty
88 case idris_outputmode ist of
89 RawOutput -> consoleDisplayAnnotated h output
90 IdeSlave n -> ideSlaveReturnAnnotated n h output
92-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name
93ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()
94ihPrintFunTypes h bnd n [] = ihPrintError h $ "No such variable " ++ show n
95ihPrintFunTypes h bnd n overloads = do ist <- getIState
96 let ppo = ppOptionIst ist
97 let infixes = idris_infixes ist
98 let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)
99 case idris_outputmode ist of
100 RawOutput -> consoleDisplayAnnotated h output
101 IdeSlave n -> ideSlaveReturnAnnotated n h output
102 where fullName n = prettyName True bnd n
103 ppOverload ppo infixes n tm =
104 fullName n <+> colon <+> align (pprintPTerm ppo bnd [] infixes tm)
106ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()
107ihRenderResult h d = do ist <- getIState
108 case idris_outputmode ist of
109 RawOutput -> consoleDisplayAnnotated h d
110 IdeSlave n -> ideSlaveReturnAnnotated n h d
112fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
113fancifyAnnots ist annot@(AnnName n _ _ _) =
114 do let ctxt = tt_ctxt ist
115 docs = docOverview ist n
116 ty = Just (getTy ist n)
117 case () of
118 _ | isDConName n ctxt -> AnnName n (Just DataOutput) docs ty
119 _ | isFnName n ctxt -> AnnName n (Just FunOutput) docs ty
120 _ | isTConName n ctxt -> AnnName n (Just TypeOutput) docs ty
121 _ | isMetavarName n ist -> AnnName n (Just MetavarOutput) docs ty
122 _ | otherwise -> annot
123 where docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs
124 docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)
125 let o = overview (fst docs)
126 -- TODO make width configurable
127 out = displayS . renderPretty 1.0 50 $ renderDocstring o
128 return (out "")
129 getTy :: IState -> Name -> String -- fails if name not already extant!
130 getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $
131 delabTy ist n
132 in (displayS . renderPretty 1.0 50 $ theTy) ""
133fancifyAnnots _ annot = annot
135-- | Show an error with semantic highlighting
136ihRenderError :: Handle -> Doc OutputAnnotation -> Idris ()
137ihRenderError h e = do ist <- getIState
138 case idris_outputmode ist of
139 RawOutput -> consoleDisplayAnnotated h e
140 IdeSlave n -> do
141 (str, spans) <- fmap displaySpans .
142 iRender .
143 fmap (fancifyAnnots ist) $
144 e
145 let good = [SymbolAtom "error", toSExp str, toSExp spans]
146 runIO . hPutStrLn h $ convSExp "return" good n
148ihPrintError :: Handle -> String -> Idris ()
149ihPrintError h s = do i <- getIState
150 case idris_outputmode i of
151 RawOutput -> case s of
152 "" -> return ()
153 s -> runIO $ hPutStrLn h s
154 IdeSlave n ->
155 let good = SexpList [SymbolAtom "error", toSExp s] in
156 runIO . hPutStrLn h $ convSExp "return" good n
158ihputStrLn :: Handle -> String -> Idris ()
159ihputStrLn h s = do i <- getIState
160 case idris_outputmode i of
161 RawOutput -> runIO $ hPutStrLn h s
162 IdeSlave n -> runIO . hPutStrLn h $ convSExp "write-string" s n
164iputStrLn = ihputStrLn stdout
165iPrintError = ihPrintError stdout
166iPrintResult = ihPrintResult stdout
167iWarn = ihWarn stdout
169ideslavePutSExp :: SExpable a => String -> a -> Idris ()
170ideslavePutSExp cmd info = do i <- getIState
171 case idris_outputmode i of
172 IdeSlave n -> runIO . putStrLn $ convSExp cmd info n
173 _ -> return ()
175-- this needs some typing magic and more structured output towards emacs
176iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
177iputGoal g = do i <- getIState
178 case idris_outputmode i of
179 RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)
180 IdeSlave n -> runIO . putStrLn $
181 convSExp "write-goal" (displayS (fmap (fancifyAnnots i) g) "") n
183-- | Warn about totality problems without failing to compile
184warnTotality :: Idris ()
185warnTotality = do ist <- getIState
186 mapM_ (warn ist) (nub (idris_totcheckfail ist))
187 where warn ist (fc, e) = iWarn fc (pprintErr ist (Msg e))