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