git.iko.soy/Idris-dev
on 63ff875 help sign in
Idris-dev/src/Idris/Prover.hs
535 lines 26 kB history raw
2{-# LANGUAGE PatternGuards #-}
3module Idris.Prover (prover, showProof, showRunElab) where
5-- Hack for GHC 7.10 and earlier compat without CPP or warnings
6-- This exludes (<$>) as fmap, because wl-pprint uses it for newline
7import Prelude (Eq(..), Show(..),
8 Bool(..), Either(..), Maybe(..), String,
9 (.), ($), (++), (||), (&&),
10 concatMap, id, elem, error, fst, flip, foldl, foldr, init,
11 length, lines, map, not, null, repeat, reverse, tail, zip)
13import Idris.Core.Elaborate hiding (Tactic(..))
14import Idris.Core.TT
15import Idris.Core.Evaluate
16import Idris.Core.CaseTree
17import Idris.Core.Typecheck
19import Idris.Elab.Utils
20import Idris.Elab.Value
21import Idris.Elab.Term
23import Idris.AbsSyntax
24import Idris.AbsSyntaxTree
25import Idris.Delaborate
26import Idris.Docs (getDocs, pprintDocs, pprintConstDocs)
27import Idris.ElabDecls
28import Idris.Parser hiding (params)
29import Idris.Error
30import Idris.DataOpts
31import Idris.Completion
32import qualified Idris.IdeMode as IdeMode
33import Idris.Output
34import Idris.TypeSearch (searchByType)
36import Text.Trifecta.Result(Result(..))
38import System.IO (Handle, stdin, stdout, hPutStrLn)
39import System.Console.Haskeline
40import System.Console.Haskeline.History
41import Control.Monad.State.Strict
42import Control.DeepSeq
44import Util.Pretty
45import Debug.Trace
47-- | Launch the proof shell
48prover :: Bool -> Bool -> Name -> Idris ()
49prover mode lit x =
50 do ctxt <- getContext
51 i <- getIState
52 case lookupTy x ctxt of
53 [t] -> if elem x (map fst (idris_metavars i))
54 then prove mode (idris_optimisation i) ctxt lit x t
55 else ifail $ show x ++ " is not a hole"
56 _ -> fail "No such hole"
58showProof :: Bool -> Name -> [String] -> String
59showProof lit n ps
60 = bird ++ show n ++ " = proof" ++ break ++
61 showSep break (map (\x -> " " ++ x) ps) ++
62 break ++ "\n"
63 where bird = if lit then "> " else ""
64 break = "\n" ++ bird
66showRunElab :: Bool -> Name -> [String] -> String
67showRunElab lit n ps = birdify (displayS (renderPretty 1.0 80 doc) "")
68 where doc = text (show n) <+> text "=" <+> text "%runElab" <+>
69 enclose lparen rparen
70 (text "do" <+> (align $ vsep (map text ps)))
71 birdify = if lit
72 then concatMap ("> " ++) . lines
73 else id
75proverSettings :: ElabState EState -> Settings Idris
76proverSettings e = setComplete (proverCompletion (assumptionNames e)) defaultSettings
78assumptionNames :: ElabState EState -> [String]
79assumptionNames e
80 = case envAtFocus (proof e) of
81 OK env -> names env
82 where names [] = []
83 names ((MN _ _, _) : bs) = names bs
84 names ((n, _) : bs) = show n : names bs
86prove :: Bool -> Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()
87prove mode opt ctxt lit n ty
88 = do ps <- fmap (\ist -> initElaborator n ctxt (idris_datatypes ist) ty) getIState
89 idemodePutSExp "start-proof-mode" n
90 (tm, prf) <-
91 if mode
92 then elabloop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) [] Nothing []
93 else do iputStrLn $ "Warning: this interactive prover is deprecated and will be removed " ++
94 "in a future release. Please see :elab for a similar feature that "++
95 "will replace it."
96 ploop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) Nothing
97 logLvl 1 $ "Adding " ++ show tm
98 i <- getIState
99 let shower = if mode
100 then showRunElab
101 else showProof
102 case idris_outputmode i of
103 IdeMode _ _ -> idemodePutSExp "end-proof-mode" (n, shower lit n prf)
104 _ -> iputStrLn $ shower lit n prf
105 let proofs = proof_list i
106 putIState (i { proof_list = (n, (mode, prf)) : proofs })
107 let tree = simpleCase False (STerm Erased) False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]
108 logLvl 3 (show tree)
109 (ptm, pty) <- recheckC (fileFC "proof") id [] tm
110 logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++
111 "Expected type:" ++ show ty)
112 case converts ctxt [] ty pty of
113 OK _ -> return ()
114 Error e -> ierror (CantUnify False (ty, Nothing) (pty, Nothing) e [] 0)
115 ptm' <- applyOpts ptm
116 ei <- getErasureInfo `fmap` getIState
117 ctxt' <- do ctxt <- getContext
118 tclift $ addCasedef n ei (CaseInfo True True False) False (STerm Erased) True False
119 [] [] -- argtys, inaccArgs
120 [Right (P Ref n ty, ptm)]
121 [([], P Ref n ty, ptm)]
122 [([], P Ref n ty, ptm)]
123 [([], P Ref n ty, ptm)]
124 [([], P Ref n ty, ptm')] ty
125 ctxt
126 setContext ctxt'
127 solveDeferred n
128 case idris_outputmode i of
129 IdeMode n h ->
130 runIO . hPutStrLn h $ IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", "") n
131 _ -> return ()
133elabStep :: ElabState EState -> ElabD a -> Idris (a, ElabState EState)
134elabStep st e =
135 case runStateT eCheck st of
136 OK ((a, ctxt'), ES (ps, est@EState{new_tyDecls = declTodo}) x old) ->
137 do setContext ctxt'
138 processTacticDecls toplevel declTodo
139 return (a, ES (ps, est {new_tyDecls = []}) x old)
140 Error a -> ierror a
141 where eCheck = do res <- e
142 matchProblems True
143 unifyProblems
144 probs' <- get_probs
145 case probs' of
146 [] -> do tm <- get_term
147 ctxt <- get_context
148 lift $ check ctxt [] (forget tm)
149 return (res, ctxt)
150 ((_,_,_,_,e,_,_):_) -> lift $ Error e
152dumpState :: IState -> Bool -> [(Name, Type, Term)] -> ProofState -> Idris ()
153dumpState ist inElab menv ps | [] <- holes ps =
154 do let nm = thname ps
155 rendered <- iRender $ prettyName True False [] nm <> colon <+> text "No more goals."
156 iputGoal rendered
157dumpState ist inElab menv ps | (h : hs) <- holes ps = do
158 let OK ty = goalAtFocus ps
159 let OK env = envAtFocus ps
160 let state = prettyOtherGoals hs <> line <>
161 prettyAssumptions inElab ty env <> line <>
162 prettyMetaValues (reverse menv) <>
163 prettyGoal (zip (assumptionNames env) (repeat False)) ty
164 rendered <- iRender state
165 iputGoal rendered
167 where
168 (h : hs) = holes ps -- apparently the pattern guards don't give us this
170 ppo = ppOptionIst ist
172 tPretty bnd t = annotate (AnnTerm bnd t) .
173 pprintPTerm ppo bnd [] (idris_infixes ist) $
174 delab ist t
176 assumptionNames :: Env -> [Name]
177 assumptionNames = map fst
179 prettyPs :: Bool -> Binder Type -> [(Name, Bool)] -> Env -> Doc OutputAnnotation
180 prettyPs all g bnd [] = empty
181 prettyPs all g bnd ((n@(MN _ r), _) : bs)
182 | not all && r == txt "rewrite_rule" = prettyPs all g ((n, False):bnd) bs
183 prettyPs all g bnd ((n@(MN _ _), _) : bs)
184 | not (all || n `elem` freeEnvNames bs || n `elem` goalNames g) = prettyPs all g bnd bs
185 prettyPs all g bnd ((n, Let t v) : bs) =
186 line <> bindingOf n False <+> text "=" <+> tPretty bnd v <+> colon <+>
187 align (tPretty bnd t) <> prettyPs all g ((n, False):bnd) bs
188 prettyPs all g bnd ((n, b) : bs) =
189 line <> bindingOf n False <+> colon <+>
190 align (tPretty bnd (binderTy b)) <> prettyPs all g ((n, False):bnd) bs
192 prettyMetaValues [] = empty
193 prettyMetaValues mvs =
194 text "---------- Meta-values: ----------" <$$>
195 prettyMetaValues' [] mvs <> line <> line
196 prettyMetaValues' _ [] = empty
197 prettyMetaValues' bnd [mv] = ppMv bnd mv
198 prettyMetaValues' bnd ((mv@(n, ty, tm)) : mvs) =
199 ppMv bnd mv <$>
200 prettyMetaValues' ((n, False):bnd) mvs
202 ppMv bnd (n, ty, tm) = kwd "let" <+> bindingOf n False <+> colon <+>
203 tPretty bnd ty <+> text "=" <+> tPretty bnd tm
205 kwd = annotate AnnKeyword . text
207 goalNames (Guess t v) = freeNames t ++ freeNames v
208 goalNames b = freeNames (binderTy b)
210 prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v
211 prettyG bnd b = tPretty bnd $ binderTy b
213 prettyGoal bnd ty =
214 text "---------- Goal: ----------" <$$>
215 bindingOf h False <+> colon <+> align (prettyG bnd ty)
217 prettyAssumptions inElab g env =
218 if length env == 0 then
219 empty
220 else
221 text "---------- Assumptions: ----------" <>
222 nest nestingSize (prettyPs inElab g [] $ reverse env)
224 prettyOtherGoals hs =
225 if length hs == 0 then
226 empty
227 else
228 text "---------- Other goals: ----------" <$$>
229 nest nestingSize (align . cat . punctuate (text ",") . map (flip bindingOf False) $ hs)
231 freeEnvNames :: Env -> [Name]
232 freeEnvNames = foldl (++) [] . map (\(n, b) -> freeNames (Bind n b Erased))
234lifte :: ElabState EState -> ElabD a -> Idris a
235lifte st e = do (v, _) <- elabStep st e
236 return v
238receiveInput :: Handle -> ElabState EState -> Idris (Maybe String)
239receiveInput h e =
240 do i <- getIState
241 let inh = if h == stdout then stdin else h
242 len' <- runIO $ IdeMode.getLen inh
243 len <- case len' of
244 Left err -> ierror err
245 Right n -> return n
246 l <- runIO $ IdeMode.getNChar inh len ""
247 (sexp, id) <- case IdeMode.parseMessage l of
248 Left err -> ierror err
249 Right (sexp, id) -> return (sexp, id)
250 putIState $ i { idris_outputmode = (IdeMode id h) }
251 case IdeMode.sexpToCommand sexp of
252 Just (IdeMode.REPLCompletions prefix) ->
253 do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")
254 let good = IdeMode.SexpList [IdeMode.SymbolAtom "ok", IdeMode.toSExp (map replacement compls, reverse unused)]
255 idemodePutSExp "return" good
256 receiveInput h e
257 Just (IdeMode.Interpret cmd) -> return (Just cmd)
258 Just (IdeMode.TypeOf str) -> return (Just (":t " ++ str))
259 Just (IdeMode.DocsFor str _) -> return (Just (":doc " ++ str))
260 _ -> return Nothing
262data ElabShellHistory = ElabStep | LetStep | BothStep
264undoStep :: [String] -> [(Name, Type, Term)] -> ElabState EState -> ElabShellHistory -> Idris ([String], [(Name, Type, Term)], ElabState EState)
265undoStep prf env st ElabStep = do (_, st') <- elabStep st loadState
266 return (init prf, env, st')
267undoStep prf env st LetStep = return (init prf, tail env, st)
268undoStep prf env st BothStep = do (_, st') <- elabStep st loadState
269 return (init prf, tail env, st')
271undoElab :: [String] -> [(Name, Type, Term)] -> ElabState EState -> [ElabShellHistory] -> Idris ([String], [(Name, Type, Term)], ElabState EState, [ElabShellHistory])
272undoElab prf env st [] = ifail "Nothing to undo"
273undoElab prf env st (h:hs) = do (prf', env', st') <- undoStep prf env st h
274 return (prf', env', st', hs)
277elabloop :: Name -> Bool -> String -> [String] -> ElabState EState -> [ElabShellHistory] -> Maybe History -> [(Name, Type, Term)] -> Idris (Term, [String])
278elabloop fn d prompt prf e prev h env
279 = do ist <- getIState
280 when d $ dumpState ist True env (proof e)
281 (x, h') <-
282 case idris_outputmode ist of
283 RawOutput _ ->
284 runInputT (proverSettings e) $
285 do case h of
286 Just history -> putHistory history
287 Nothing -> return ()
288 l <- getInputLine (prompt ++ "> ")
289 h' <- getHistory
290 return (l, Just h')
291 IdeMode _ handle ->
292 do isetPrompt prompt
293 i <- receiveInput handle e
294 return (i, h)
295 (cmd, step) <- case x of
296 Nothing -> do iPrintError "" ; ifail "Abandoned"
297 Just input -> return (parseElabShellStep ist input, input)
299 -- if we're abandoning, it has to be outside the scope of the catch
300 case cmd of
301 Success (Left EAbandon) -> do iPrintError ""; ifail "Abandoned"
302 _ -> return ()
304 (d, prev', st, done, prf', env', res) <-
305 idrisCatch
306 (case cmd of
307 Failure err ->
308 return (False, prev, e, False, prf, env, Left . Msg . show . fixColour (idris_colourRepl ist) $ err)
309 Success (Left cmd') ->
310 case cmd' of
311 EQED -> do hs <- lifte e get_holes
312 when (not (null hs)) $ ifail "Incomplete proof"
313 iputStrLn "Proof completed!"
314 return (False, prev, e, True, prf, env, Right $ iPrintResult "")
315 EUndo -> do (prf', env', st', prev') <- undoElab prf env e prev
316 return (True, prev', st', False, prf', env', Right $ iPrintResult "")
317 EAbandon ->
318 error "the impossible happened - should have been matched on outer scope"
319 EProofState -> return (True, prev, e, False, prf, env, Right $ iPrintResult "")
320 EProofTerm ->
321 do tm <- lifte e get_term
322 return (False, prev, e, False, prf, env, Right $ iRenderResult (text "TT:" <+> pprintTT [] tm))
323 EEval tm -> do (d', st', done, prf', go) <- evalTerm e prf tm
324 return (d', prev, st', done, prf', env, go)
325 ECheck (PRef _ _ n) ->
326 do (d', st', done, prf', go) <- checkNameType e prf n
327 return (d', prev, st', done, prf', env, go)
328 ECheck tm -> do (d', st', done, prf', go) <- checkType e prf tm
329 return (d', prev, st', done, prf', env, go)
330 ESearch ty -> do (d', st', done, prf', go) <- search e prf ty
331 return (d', prev, st', done, prf', env, go)
332 EDocStr d -> do (d', st', done, prf', go) <- docStr e prf d
333 return (d', prev, st', done, prf', env, go)
334 Success (Right cmd') ->
335 case cmd' of
336 DoLetP _ _ _ -> ifail "Pattern-matching let not supported here"
337 DoBindP _ _ _ _ -> ifail "Pattern-matching <- not supported here"
338 DoLet fc i ifc Placeholder expr ->
339 do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)
340 ctxt <- getContext
341 let tm' = normaliseAll ctxt [] tm
342 ty' = normaliseAll ctxt [] ty
343 return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult ""))
344 DoLet fc i ifc ty expr ->
345 do (tm, ty) <- elabVal recinfo ERHS
346 (PApp NoFC (PRef NoFC [] (sUN "the"))
347 [ pexp (inLets ist env ty)
348 , pexp (inLets ist env expr)
349 ])
350 ctxt <- getContext
351 let tm' = normaliseAll ctxt [] tm
352 ty' = normaliseAll ctxt [] ty
353 return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult ""))
354 DoBind fc i ifc expr ->
355 do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)
356 (_, e') <- elabStep e saveState -- enable :undo
357 (res, e'') <- elabStep e' $
358 runElabAction ist NoFC [] tm ["Shell"]
359 ctxt <- getContext
360 (v, vty) <- tclift $ check ctxt [] (forget res)
361 let v' = normaliseAll ctxt [] v
362 vty' = normaliseAll ctxt [] vty
363 return (True, BothStep:prev, e'', False, prf ++ [step], (i, vty', v') : env, Right (iPrintResult ""))
364 DoExp fc expr ->
365 do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)
366 -- TODO: call elaborator with Elab () as goal here
367 (_, e') <- elabStep e saveState -- enable :undo
368 (_, e'') <- elabStep e' $
369 runElabAction ist NoFC [] tm ["Shell"]
370 return (True, ElabStep:prev, e'', False, prf ++ [step], env, Right (iPrintResult "")))
371 (\err -> return (False, prev, e, False, prf, env, Left err))
372 idemodePutSExp "write-proof-state" (prf', length prf')
373 case res of
374 Left err -> do ist <- getIState
375 iRenderError $ pprintErr ist err
376 elabloop fn d prompt prf' st prev' h' env'
377 Right ok ->
378 if done then do (tm, _) <- elabStep st get_term
379 return (tm, prf')
380 else do ok
381 elabloop fn d prompt prf' st prev' h' env'
383 where
384 -- A bit of a hack: wrap the value up in a let binding, which will
385 -- normalise away. It would be better to figure out how to call
386 -- the elaborator with a custom environment here to avoid the
387 -- delab step.
388 inLets :: IState -> [(Name, Type, Term)] -> PTerm -> PTerm
389 inLets ist lets tm = foldr (\(n, ty, v) b -> PLet NoFC n NoFC (delab ist ty) (delab ist v) b) tm (reverse lets)
393ploop :: Name -> Bool -> String -> [String] -> ElabState EState -> Maybe History -> Idris (Term, [String])
394ploop fn d prompt prf e h
395 = do i <- getIState
396 let autoSolve = opt_autoSolve (idris_options i)
397 when d $ dumpState i False [] (proof e)
398 (x, h') <-
399 case idris_outputmode i of
400 RawOutput _ ->
401 runInputT (proverSettings e) $
402 -- Manually track the history so that we can use the proof state
403 do case h of
404 Just history -> putHistory history
405 Nothing -> return ()
406 l <- getInputLine (prompt ++ "> ")
407 h' <- getHistory
408 return (l, Just h')
409 IdeMode _ handle ->
410 do isetPrompt prompt
411 i <- receiveInput handle e
412 return (i, h)
413 (cmd, step) <- case x of
414 Nothing -> do iPrintError ""; ifail "Abandoned"
415 Just input -> do return (parseTactic i input, input)
416 case cmd of
417 Success Abandon -> do iPrintError ""; ifail "Abandoned"
418 _ -> return ()
419 (d, st, done, prf', res) <- idrisCatch
420 (case cmd of
421 Failure err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)
422 Success Undo -> do (_, st) <- elabStep e loadState
423 return (True, st, False, init prf, Right $ iPrintResult "")
424 Success ProofState -> return (True, e, False, prf, Right $ iPrintResult "")
425 Success ProofTerm -> do tm <- lifte e get_term
426 iputStrLn $ "TT: " ++ show tm ++ "\n"
427 return (False, e, False, prf, Right $ iPrintResult "")
428 Success Qed -> do hs <- lifte e get_holes
429 when (not (null hs)) $ ifail "Incomplete proof"
430 iputStrLn "Proof completed!"
431 return (False, e, True, prf, Right $ iPrintResult "")
432 Success (TCheck (PRef _ _ n)) -> checkNameType e prf n
433 Success (TCheck t) -> checkType e prf t
434 Success (TEval t) -> evalTerm e prf t
435 Success (TDocStr x) -> docStr e prf x
436 Success (TSearch t) -> search e prf t
437 Success tac ->
438 do (_, e) <- elabStep e saveState
439 (_, st) <- elabStep e (runTac autoSolve i (Just proverFC) fn tac)
440 return (True, st, False, prf ++ [step], Right $ iPrintResult ""))
441 (\err -> return (False, e, False, prf, Left err))
442 idemodePutSExp "write-proof-state" (prf', length prf')
443 case res of
444 Left err -> do ist <- getIState
445 iRenderError $ pprintErr ist err
446 ploop fn d prompt prf' st h'
447 Right ok ->
448 if done then do (tm, _) <- elabStep st get_term
449 return (tm, prf')
450 else do ok
451 ploop fn d prompt prf' st h'
454envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env
456checkNameType :: ElabState EState -> [String] -> Name -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
457checkNameType e prf n = do
458 ctxt <- getContext
459 ist <- getIState
460 imp <- impShow
461 idrisCatch (do
462 let OK env = envAtFocus (proof e)
463 ctxt' = envCtxt env ctxt
464 bnd = map (\x -> (fst x, False)) env
465 ist' = ist { tt_ctxt = ctxt' }
466 putIState ist'
467 -- Unlike the REPL, metavars have no special treatment, to
468 -- make it easier to see how to prove with them.
469 let action = case lookupNames n ctxt' of
470 [] -> iPrintError $ "No such variable " ++ show n
471 ts -> iPrintFunTypes bnd n (map (\n -> (n, pprintDelabTy ist' n)) ts)
472 putIState ist
473 return (False, e, False, prf, Right action))
474 (\err -> do putIState ist ; ierror err)
476checkType :: ElabState EState -> [String] -> PTerm -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
477checkType e prf t = do
478 ist <- getIState
479 ctxt <- getContext
480 idrisCatch (do
481 let OK env = envAtFocus (proof e)
482 ctxt' = envCtxt env ctxt
483 putIState ist { tt_ctxt = ctxt' }
484 (tm, ty) <- elabVal recinfo ERHS t
485 let ppo = ppOptionIst ist
486 ty' = normaliseC ctxt [] ty
487 infixes = idris_infixes ist
488 action = case tm of
489 TType _ ->
490 iPrintTermWithType (prettyImp ppo (PType emptyFC)) type1Doc
491 _ -> let bnd = map (\x -> (fst x, False)) env in
492 iPrintTermWithType (pprintPTerm ppo bnd [] infixes (delab ist tm))
493 (pprintPTerm ppo bnd [] infixes (delab ist ty))
494 putIState ist
495 return (False, e, False, prf, Right action))
496 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)
498proverFC = FC "(prover shell)" (0, 0) (0, 0)
500evalTerm :: ElabState EState -> [String] -> PTerm -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
501evalTerm e prf t = withErrorReflection $
502 do ctxt <- getContext
503 ist <- getIState
504 idrisCatch (do
505 let OK env = envAtFocus (proof e)
506 ctxt' = envCtxt env ctxt
507 ist' = ist { tt_ctxt = ctxt' }
508 bnd = map (\x -> (fst x, False)) env
509 putIState ist'
510 (tm, ty) <- elabVal recinfo ERHS t
511 let tm' = force (normaliseAll ctxt' env tm)
512 ty' = force (normaliseAll ctxt' env ty)
513 ppo = ppOption (idris_options ist')
514 infixes = idris_infixes ist
515 tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')
516 tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')
517 action = iPrintTermWithType tmDoc tyDoc
518 putIState ist
519 return (False, e, False, prf, Right action))
520 (\err -> do putIState ist ; ierror err)
522docStr :: ElabState EState -> [String] -> Either Name Const -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
523docStr e prf (Left n) = do ist <- getIState
524 idrisCatch (case lookupCtxtName n (idris_docstrings ist) of
525 [] -> return (False, e, False, prf,
526 Left . Msg $ "No documentation for " ++ show n)
527 ns -> do toShow <- mapM (showDoc ist) ns
528 return (False, e, False, prf,
529 Right $ iRenderResult (vsep toShow)))
530 (\err -> do putIState ist ; ierror err)
531 where showDoc ist (n, d) = do doc <- getDocs n FullDocs
532 return $ pprintDocs ist doc
533docStr e prf (Right c) = do ist <- getIState
534 return (False, e, False, prf, Right . iRenderResult $ pprintConstDocs ist c (constDocs c))
535search e prf t = return (False, e, False, prf, Right $ searchByType [] t)