src/Idris/Output.hs · Idris-dev

git.iko.soy/Idris-dev

on da672ec help sign in

Idris-dev/src/Idris/Output.hs

370 lines 15 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.Colours (hStartColourise, hEndColourise)

10import Idris.Delaborate

11import Idris.Docstrings

12import Idris.IdeMode

14import Util.Pretty

15import Util.ScreenSize (getScreenWidth)

17import Control.Monad.Trans.Except (ExceptT (ExceptT), runExceptT)

19import System.Console.Haskeline.MonadException

20 (MonadException (controlIO), RunIO (RunIO))

21import System.IO (stdout, Handle, hPutStrLn, hPutStr)

22import System.FilePath (replaceExtension)

24import Prelude hiding ((<$>))

26import Data.Char (isAlpha)

27import Data.List (nub, intersperse)

28import Data.Maybe (fromMaybe)

30instance MonadException m => MonadException (ExceptT Err m) where

31 controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let

32 run' = RunIO (fmap ExceptT . run . runExceptT)

33 in fmap runExceptT $ f run'

35pshow :: IState -> Err -> String

36pshow ist err = displayDecorated (consoleDecorate ist) .

37 renderPretty 1.0 80 .

38 fmap (fancifyAnnots ist True) $ pprintErr ist err

40iWarn :: FC -> Doc OutputAnnotation -> Idris ()

41iWarn fc err =

42 do i <- getIState

43 case idris_outputmode i of

44 RawOutput h ->

45 do err' <- iRender . fmap (fancifyAnnots i True) $

46 case fc of

47 FC fn _ _ | fn /= "" -> text (show fc) <> colon <//> err

48 _ -> err

49 hWriteDoc h i err'

50 IdeMode n h ->

51 do err' <- iRender . fmap (fancifyAnnots i True) $ err

52 let (str, spans) = displaySpans err'

53 runIO . hPutStrLn h $

54 convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n

56iRender :: Doc a -> Idris (SimpleDoc a)

57iRender d = do w <- getWidth

58 ist <- getIState

59 let ideMode = case idris_outputmode ist of

60 IdeMode _ _ -> True

61 _ -> False

62 case w of

63 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d

64 ColsWide n -> return $

65 if n < 1

66 then renderPretty 1.0 1000000000 d

67 else renderPretty 0.8 n d

68 AutomaticWidth | ideMode -> return $ renderPretty 1.0 80 d

69 | otherwise -> do width <- runIO getScreenWidth

70 return $ renderPretty 0.8 width d

72hWriteDoc :: Handle -> IState -> SimpleDoc OutputAnnotation -> Idris ()

73hWriteDoc h ist rendered =

74 do runIO $ displayDecoratedA

75 (hPutStr h)

76 (maybe (return ()) (hStartColourise h))

77 (maybe (return ()) (hEndColourise h))

78 (fmap (annotationColour ist) rendered)

79 runIO $ hPutStr h "\n" -- newline translation on the output

80 -- stream should take care of this for

81 -- Windows

83-- | Write a pretty-printed term to the console with semantic coloring

84consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()

85consoleDisplayAnnotated h output =

86 do ist <- getIState

87 rendered <- iRender output

88 hWriteDoc h ist rendered

90iPrintTermWithType :: Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

91iPrintTermWithType tm ty = iRenderResult (tm <+> colon <+> align ty)

93-- | Pretty-print a collection of overloadings to REPL or IDEMode - corresponds to :t name

94iPrintFunTypes :: [(Name, Bool)] -> Name -> [(Name, Doc OutputAnnotation)] -> Idris ()

95iPrintFunTypes bnd n [] = iPrintError $ "No such variable " ++ show n

96iPrintFunTypes bnd n overloads = do ist <- getIState

97 let ppo = ppOptionIst ist

98 let infixes = idris_infixes ist

99 let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)

100 iRenderResult output

101 where fullName ppo n | length overloads > 1 = prettyName True True bnd n

102 | otherwise = prettyName True (ppopt_impl ppo) bnd n

103 ppOverload ppo infixes n tm =

104 fullName ppo n <+> colon <+> align tm

105

106iRenderOutput :: Doc OutputAnnotation -> Idris ()

107iRenderOutput doc =

108 do i <- getIState

109 case idris_outputmode i of

110 RawOutput h -> do out <- iRender doc

111 hWriteDoc h i out

112

113 IdeMode n h ->

114 do (str, spans) <- fmap displaySpans . iRender . fmap (fancifyAnnots i True) $ doc

115 let out = [toSExp str, toSExp spans]

116 runIO . hPutStrLn h $ convSExp "write-decorated" out n

117

118iRenderResult :: Doc OutputAnnotation -> Idris ()

119iRenderResult d = do ist <- getIState

120 case idris_outputmode ist of

121 RawOutput h -> consoleDisplayAnnotated h d

122 IdeMode n h -> ideModeReturnAnnotated n h d

123

124ideModeReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()

125ideModeReturnWithStatus status n h out = do

126 ist <- getIState

127 (str, spans) <- fmap displaySpans .

128 iRender .

129 fmap (fancifyAnnots ist True) $

130 out

131 let good = [SymbolAtom status, toSExp str, toSExp spans]

132 runIO . hPutStrLn h $ convSExp "return" good n

133

134

135-- | Write pretty-printed output to IDEMode with semantic annotations

136ideModeReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()

137ideModeReturnAnnotated = ideModeReturnWithStatus "ok"

138

139-- | Show an error with semantic highlighting

140iRenderError :: Doc OutputAnnotation -> Idris ()

141iRenderError e = do ist <- getIState

142 case idris_outputmode ist of

143 RawOutput h -> consoleDisplayAnnotated h e

144 IdeMode n h -> ideModeReturnWithStatus "error" n h e

145

146iPrintWithStatus :: String -> String -> Idris ()

147iPrintWithStatus status s = do

148 i <- getIState

149 case idris_outputmode i of

150 RawOutput h -> case s of

151 "" -> return ()

152 s -> runIO $ hPutStrLn h s

153 IdeMode n h ->

154 let good = SexpList [SymbolAtom status, toSExp s] in

155 runIO $ hPutStrLn h $ convSExp "return" good n

156

157

158iPrintResult :: String -> Idris ()

159iPrintResult = iPrintWithStatus "ok"

160

161iPrintError :: String -> Idris ()

162iPrintError = iPrintWithStatus "error"

163

164iputStrLn :: String -> Idris ()

165iputStrLn s = do i <- getIState

166 case idris_outputmode i of

167 RawOutput h -> runIO $ hPutStrLn h s

168 IdeMode n h -> runIO . hPutStrLn h $ convSExp "write-string" s n

169

170

171idemodePutSExp :: SExpable a => String -> a -> Idris ()

172idemodePutSExp cmd info = do i <- getIState

173 case idris_outputmode i of

174 IdeMode n h ->

175 runIO . hPutStrLn h $

176 convSExp cmd info n

177 _ -> return ()

178

179-- TODO: send structured output similar to the metavariable list

180iputGoal :: SimpleDoc OutputAnnotation -> Idris ()

181iputGoal g = do i <- getIState

182 case idris_outputmode i of

183 RawOutput h -> hWriteDoc h i g

184 IdeMode n h ->

185 let (str, spans) = displaySpans . fmap (fancifyAnnots i True) $ g

186 goal = [toSExp str, toSExp spans]

187 in runIO . hPutStrLn h $ convSExp "write-goal" goal n

188

189-- | Warn about totality problems without failing to compile

190warnTotality :: Idris ()

191warnTotality = do ist <- getIState

192 mapM_ (warn ist) (nub (idris_totcheckfail ist))

193 where warn ist (fc, e) = iWarn fc (pprintErr ist (Msg e))

194

195

196printUndefinedNames :: [Name] -> Doc OutputAnnotation

197printUndefinedNames ns = text "Undefined " <> names <> text "."

198 where names = encloseSep empty empty (char ',') $ map ppName ns

199 ppName = prettyName True True []

200

201

202prettyDocumentedIst :: IState

203 -> (Name, PTerm, Maybe (Docstring DocTerm))

204 -> Doc OutputAnnotation

205prettyDocumentedIst ist (name, ty, docs) =

206 prettyName True True [] name <+> colon <+> align (prettyIst ist ty) <$>

207 fromMaybe empty (fmap (\d -> renderDocstring (renderDocTerm ppTm norm) d <> line) docs)

208 where ppTm = pprintDelab ist

209 norm = normaliseAll (tt_ctxt ist) []

210

211sendParserHighlighting :: Idris ()

212sendParserHighlighting =

213 do ist <- getIState

214 let hs = map unwrap . nub . map wrap $ idris_parserHighlights ist

215 sendHighlighting hs

216 ist <- getIState

217 putIState ist {idris_parserHighlights = []}

218 where wrap (fc, a) = (FC' fc, a)

219 unwrap (fc', a) = (unwrapFC fc', a)

220

221sendHighlighting :: [(FC, OutputAnnotation)] -> Idris ()

222sendHighlighting highlights =

223 do ist <- getIState

224 case idris_outputmode ist of

225 RawOutput _ -> updateIState $

226 \ist -> ist { idris_highlightedRegions =

227 highlights ++ idris_highlightedRegions ist }

228 IdeMode n h ->

229 let fancier = [ toSExp (fc, fancifyAnnots ist False annot)

230 | (fc, annot) <- highlights, fullFC fc

231 ]

232 in case fancier of

233 [] -> return ()

234 _ -> runIO . hPutStrLn h $

235 convSExp "output"

236 (SymbolAtom "ok",

237 (SymbolAtom "highlight-source", fancier)) n

238

239 where fullFC (FC _ _ _) = True

240 fullFC _ = False

241

242-- | Write the highlighting information to a file, for use in external tools

243-- or in editors that don't support the IDE protocol

244writeHighlights :: FilePath -> Idris ()

245writeHighlights f =

246 do ist <- getIState

247 let hs = reverse $ idris_highlightedRegions ist

248 let hfile = replaceExtension f "idh"

249 let annots = toSExp [ (fc, fancifyAnnots ist False annot)

250 | (fc@(FC _ _ _), annot) <- hs

251 ]

252 runIO $ writeFile hfile $ sExpToString annots

253

254clearHighlights :: Idris ()

255clearHighlights = updateIState $ \ist -> ist { idris_highlightedRegions = [] }

256

257renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String

258renderExternal fmt width doc

259 | width < 1 = throwError . Msg $ "There must be at least one column for the pretty-printer."

260 | otherwise =

261 do ist <- getIState

262 return . wrap fmt .

263 displayDecorated (decorate fmt) .

264 renderPretty 1.0 width .

265 fmap (fancifyAnnots ist True) $

266 doc

267 where

268 decorate _ (AnnFC _) = id

269

270 decorate HTMLOutput (AnnName _ (Just TypeOutput) d _) =

271 tag "idris-type" d

272 decorate HTMLOutput (AnnName _ (Just FunOutput) d _) =

273 tag "idris-function" d

274 decorate HTMLOutput (AnnName _ (Just DataOutput) d _) =

275 tag "idris-data" d

276 decorate HTMLOutput (AnnName _ (Just MetavarOutput) d _) =

277 tag "idris-metavar" d

278 decorate HTMLOutput (AnnName _ (Just PostulateOutput) d _) =

279 tag "idris-postulate" d

280 decorate HTMLOutput (AnnName _ _ _ _) = id

281 decorate HTMLOutput (AnnBoundName _ True) = tag "idris-bound idris-implicit" Nothing

282 decorate HTMLOutput (AnnBoundName _ False) = tag "idris-bound" Nothing

283 decorate HTMLOutput (AnnConst c) =

284 tag (if constIsType c then "idris-type" else "idris-data")

285 (Just $ constDocs c)

286 decorate HTMLOutput (AnnData _ _) = tag "idris-data" Nothing

287 decorate HTMLOutput (AnnType _ _) = tag "idris-type" Nothing

288 decorate HTMLOutput AnnKeyword = tag "idris-keyword" Nothing

289 decorate HTMLOutput (AnnTextFmt fmt) =

290 case fmt of

291 BoldText -> mkTag "strong"

292 ItalicText -> mkTag "em"

293 UnderlineText -> tag "idris-underlined" Nothing

294 where mkTag t x = "<"++t++">"++x++"</"++t++">"

295 decorate HTMLOutput (AnnTerm _ _) = id

296 decorate HTMLOutput (AnnSearchResult _) = id

297 decorate HTMLOutput (AnnErr _) = id

298 decorate HTMLOutput (AnnNamespace _ _) = id

299 decorate HTMLOutput (AnnLink url) =

300 \txt -> "<a href=\"" ++ url ++ "\">" ++ txt ++ "</a>"

301 decorate HTMLOutput AnnQuasiquote = id

302 decorate HTMLOutput AnnAntiquote = id

303

304 decorate LaTeXOutput (AnnName _ (Just TypeOutput) _ _) =

305 latex "IdrisType"

306 decorate LaTeXOutput (AnnName _ (Just FunOutput) _ _) =

307 latex "IdrisFunction"

308 decorate LaTeXOutput (AnnName _ (Just DataOutput) _ _) =

309 latex "IdrisData"

310 decorate LaTeXOutput (AnnName _ (Just MetavarOutput) _ _) =

311 latex "IdrisMetavar"

312 decorate LaTeXOutput (AnnName _ (Just PostulateOutput) _ _) =

313 latex "IdrisPostulate"

314 decorate LaTeXOutput (AnnName _ _ _ _) = id

315 decorate LaTeXOutput (AnnBoundName _ True) = latex "IdrisImplicit"

316 decorate LaTeXOutput (AnnBoundName _ False) = latex "IdrisBound"

317 decorate LaTeXOutput (AnnConst c) =

318 latex $ if constIsType c then "IdrisType" else "IdrisData"

319 decorate LaTeXOutput (AnnData _ _) = latex "IdrisData"

320 decorate LaTeXOutput (AnnType _ _) = latex "IdrisType"

321 decorate LaTeXOutput AnnKeyword = latex "IdrisKeyword"

322 decorate LaTeXOutput (AnnTextFmt fmt) =

323 case fmt of

324 BoldText -> latex "textbf"

325 ItalicText -> latex "emph"

326 UnderlineText -> latex "underline"

327 decorate LaTeXOutput (AnnTerm _ _) = id

328 decorate LaTeXOutput (AnnSearchResult _) = id

329 decorate LaTeXOutput (AnnErr _) = id

330 decorate LaTeXOutput (AnnNamespace _ _) = id

331 decorate LaTeXOutput (AnnLink url) = (++ "(\\url{" ++ url ++ "})")

332 decorate LaTeXOutput AnnQuasiquote = id

333 decorate LaTeXOutput AnnAntiquote = id

334

335 tag cls docs str = "<span class=\""++cls++"\""++title++">" ++ str ++ "</span>"

336 where title = maybe "" (\d->" title=\"" ++ d ++ "\"") docs

337

338 latex cmd str = "\\"++cmd++"{"++str++"}"

339

340 wrap HTMLOutput str =

341 "<!doctype html><html><head><style>" ++ css ++ "</style></head>" ++

342 "<body><pre>" ++ str ++ "</pre></body></html>"

343 where css = concat . intersperse "\n" $

344 [".idris-data { color: red; } ",

345 ".idris-type { color: blue; }",

346 ".idris-function {color: green; }",

347 ".idris-keyword { font-weight: bold; }",

348 ".idris-bound { color: purple; }",

349 ".idris-implicit { font-style: italic; }",

350 ".idris-underlined { text-decoration: underline; }"]

351 wrap LaTeXOutput str =

352 concat . intersperse "\n" $

353 ["\\documentclass{article}",

354 "\\usepackage{fancyvrb}",

355 "\\usepackage[usenames]{xcolor}"] ++

356 map (\(cmd, color) ->

357 "\\newcommand{\\"++ cmd ++

358 "}[1]{\\textcolor{"++ color ++"}{#1}}")

359 [("IdrisData", "red"), ("IdrisType", "blue"),

360 ("IdrisBound", "magenta"), ("IdrisFunction", "green")] ++

361 ["\\newcommand{\\IdrisKeyword}[1]{{\\underline{#1}}}",

362 "\\newcommand{\\IdrisImplicit}[1]{{\\itshape \\IdrisBound{#1}}}",

363 "\n",

364 "\\begin{document}",

365 "% START CODE",

366 "\\begin{Verbatim}[commandchars=\\\\\\{\\}]",

367 str,

368 "\\end{Verbatim}",

369 "% END CODE",

370 "\\end{document}"]