git.iko.soy/Idris-dev
on 449089d help sign in
Idris-dev/src/Idris/Prover.hs
550 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) (idris_name 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 emptyFC 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 OK env = envAtFocus ps
160 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 null env then empty
219 else
220 text "---------- Assumptions: ----------" <>
221 nest nestingSize (prettyPs inElab g [] $ reverse env)
223 prettyOtherGoals hs =
224 if null hs then empty
225 else
226 text "---------- Other goals: ----------" <$$>
227 nest nestingSize (align . cat . punctuate (text ",") . map (`bindingOf` False) $ hs)
229 freeEnvNames :: Env -> [Name]
230 freeEnvNames = concatMap (\(n, b) -> freeNames (Bind n b Erased))
232lifte :: ElabState EState -> ElabD a -> Idris a
233lifte st e = do (v, _) <- elabStep st e
234 return v
236receiveInput :: Handle -> ElabState EState -> Idris (Maybe String)
237receiveInput h e =
238 do i <- getIState
239 let inh = if h == stdout then stdin else h
240 len' <- runIO $ IdeMode.getLen inh
241 len <- case len' of
242 Left err -> ierror err
243 Right n -> return n
244 l <- runIO $ IdeMode.getNChar inh len ""
245 (sexp, id) <- case IdeMode.parseMessage l of
246 Left err -> ierror err
247 Right (sexp, id) -> return (sexp, id)
248 putIState $ i { idris_outputmode = IdeMode id h }
249 case IdeMode.sexpToCommand sexp of
250 Just (IdeMode.REPLCompletions prefix) ->
251 do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")
252 let good = IdeMode.SexpList [IdeMode.SymbolAtom "ok", IdeMode.toSExp (map replacement compls, reverse unused)]
253 idemodePutSExp "return" good
254 receiveInput h e
255 Just (IdeMode.Interpret cmd) -> return (Just cmd)
256 Just (IdeMode.TypeOf str) -> return (Just (":t " ++ str))
257 Just (IdeMode.DocsFor str _) -> return (Just (":doc " ++ str))
258 _ -> return Nothing
260data ElabShellHistory = ElabStep | LetStep | BothStep
262undoStep :: [String] -> [(Name, Type, Term)] -> ElabState EState -> ElabShellHistory -> Idris ([String], [(Name, Type, Term)], ElabState EState)
263undoStep prf env st ElabStep = do (_, st') <- elabStep st loadState
264 return (init prf, env, st')
265undoStep prf env st LetStep = return (init prf, tail env, st)
266undoStep prf env st BothStep = do (_, st') <- elabStep st loadState
267 return (init prf, tail env, st')
269undoElab :: [String] -> [(Name, Type, Term)] -> ElabState EState -> [ElabShellHistory] -> Idris ([String], [(Name, Type, Term)], ElabState EState, [ElabShellHistory])
270undoElab prf env st [] = ifail "Nothing to undo"
271undoElab prf env st (h:hs) = do (prf', env', st') <- undoStep prf env st h
272 return (prf', env', st', hs)
274runWithInterrupt
275 :: ElabState EState
276 -> Idris a -- ^ run with SIGINT handler
277 -> Idris b -- ^ run if mTry finished
278 -> Idris b -- ^ run if mTry was interrupted
279 -> Idris b
280runWithInterrupt elabState mTry mSuccess mFailure = do
281 ist <- getIState
282 case idris_outputmode ist of
283 RawOutput _ -> do
284 success <- runInputT (proverSettings elabState) $
285 handleInterrupt (return False) $
286 withInterrupt (lift mTry >> return True)
287 if success then mSuccess else mFailure
288 IdeMode _ _ -> mTry >> mSuccess
290elabloop :: Name -> Bool -> String -> [String] -> ElabState EState -> [ElabShellHistory] -> Maybe History -> [(Name, Type, Term)] -> Idris (Term, [String])
291elabloop fn d prompt prf e prev h env
292 = do ist <- getIState
293 when d $ dumpState ist True env (proof e)
294 (x, h') <-
295 case idris_outputmode ist of
296 RawOutput _ ->
297 runInputT (proverSettings e) $
298 do case h of
299 Just history -> putHistory history
300 Nothing -> return ()
301 l <- handleInterrupt (return $ Just "") $ withInterrupt $ getInputLine (prompt ++ "> ")
302 h' <- getHistory
303 return (l, Just h')
304 IdeMode _ handle ->
305 do isetPrompt prompt
306 i <- receiveInput handle e
307 return (i, h)
308 (cmd, step) <- case x of
309 Nothing -> do iPrintError "" ; ifail "Abandoned"
310 Just input -> return (parseElabShellStep ist input, input)
312 -- if we're abandoning, it has to be outside the scope of the catch
313 case cmd of
314 Success (Left EAbandon) -> do iPrintError ""; ifail "Abandoned"
315 _ -> return ()
317 (d, prev', st, done, prf', env', res) <-
318 idrisCatch
319 (case cmd of
320 Failure err ->
321 return (False, prev, e, False, prf, env, Left . Msg . show . fixColour (idris_colourRepl ist) $ err)
322 Success (Left cmd') ->
323 case cmd' of
324 EQED -> do hs <- lifte e get_holes
325 unless (null hs) $ ifail "Incomplete proof"
326 iputStrLn "Proof completed!"
327 return (False, prev, e, True, prf, env, Right $ iPrintResult "")
328 EUndo -> do (prf', env', st', prev') <- undoElab prf env e prev
329 return (True, prev', st', False, prf', env', Right $ iPrintResult "")
330 EAbandon ->
331 error "the impossible happened - should have been matched on outer scope"
332 EProofState -> return (True, prev, e, False, prf, env, Right $ iPrintResult "")
333 EProofTerm ->
334 do tm <- lifte e get_term
335 return (False, prev, e, False, prf, env, Right $ iRenderResult (text "TT:" <+> pprintTT [] tm))
336 EEval tm -> do (d', st', done, prf', go) <- evalTerm e prf tm
337 return (d', prev, st', done, prf', env, go)
338 ECheck (PRef _ _ n) ->
339 do (d', st', done, prf', go) <- checkNameType e prf n
340 return (d', prev, st', done, prf', env, go)
341 ECheck tm -> do (d', st', done, prf', go) <- checkType e prf tm
342 return (d', prev, st', done, prf', env, go)
343 ESearch ty -> do (d', st', done, prf', go) <- search e prf ty
344 return (d', prev, st', done, prf', env, go)
345 EDocStr d -> do (d', st', done, prf', go) <- docStr e prf d
346 return (d', prev, st', done, prf', env, go)
347 Success (Right cmd') ->
348 case cmd' of
349 DoLetP {} -> ifail "Pattern-matching let not supported here"
350 DoBindP {} -> ifail "Pattern-matching <- not supported here"
351 DoLet fc i ifc Placeholder expr ->
352 do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)
353 ctxt <- getContext
354 let tm' = normaliseAll ctxt [] tm
355 ty' = normaliseAll ctxt [] ty
356 return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult ""))
357 DoLet fc i ifc ty expr ->
358 do (tm, ty) <- elabVal recinfo ERHS
359 (PApp NoFC (PRef NoFC [] (sUN "the"))
360 [ pexp (inLets ist env ty)
361 , pexp (inLets ist env expr)
362 ])
363 ctxt <- getContext
364 let tm' = normaliseAll ctxt [] tm
365 ty' = normaliseAll ctxt [] ty
366 return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult ""))
367 DoBind fc i ifc expr ->
368 do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)
369 (_, e') <- elabStep e saveState -- enable :undo
370 (res, e'') <- elabStep e' $
371 runElabAction ist NoFC [] tm ["Shell"]
372 ctxt <- getContext
373 (v, vty) <- tclift $ check ctxt [] (forget res)
374 let v' = normaliseAll ctxt [] v
375 vty' = normaliseAll ctxt [] vty
376 return (True, BothStep:prev, e'', False, prf ++ [step], (i, vty', v') : env, Right (iPrintResult ""))
377 DoExp fc expr ->
378 do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)
379 -- TODO: call elaborator with Elab () as goal here
380 (_, e') <- elabStep e saveState -- enable :undo
381 (_, e'') <- elabStep e' $
382 runElabAction ist NoFC [] tm ["Shell"]
383 return (True, ElabStep:prev, e'', False, prf ++ [step], env, Right (iPrintResult "")))
384 (\err -> return (False, prev, e, False, prf, env, Left err))
385 idemodePutSExp "write-proof-state" (prf', length prf')
386 case res of
387 Left err -> do ist <- getIState
388 iRenderError $ pprintErr ist err
389 elabloop fn d prompt prf' st prev' h' env'
390 Right ok ->
391 if done then do (tm, _) <- elabStep st get_term
392 return (tm, prf')
393 else runWithInterrupt e ok
394 (elabloop fn d prompt prf' st prev' h' env')
395 (elabloop fn d prompt prf e prev h' env)
397 where
398 -- A bit of a hack: wrap the value up in a let binding, which will
399 -- normalise away. It would be better to figure out how to call
400 -- the elaborator with a custom environment here to avoid the
401 -- delab step.
402 inLets :: IState -> [(Name, Type, Term)] -> PTerm -> PTerm
403 inLets ist lets tm = foldr (\(n, ty, v) b -> PLet NoFC n NoFC (delab ist ty) (delab ist v) b) tm (reverse lets)
407ploop :: Name -> Bool -> String -> [String] -> ElabState EState -> Maybe History -> Idris (Term, [String])
408ploop fn d prompt prf e h
409 = do i <- getIState
410 let autoSolve = opt_autoSolve (idris_options i)
411 when d $ dumpState i False [] (proof e)
412 (x, h') <-
413 case idris_outputmode i of
414 RawOutput _ ->
415 runInputT (proverSettings e) $
416 -- Manually track the history so that we can use the proof state
417 do case h of
418 Just history -> putHistory history
419 Nothing -> return ()
420 l <- handleInterrupt (return $ Just "") $ withInterrupt $ getInputLine (prompt ++ "> ")
421 h' <- getHistory
422 return (l, Just h')
423 IdeMode _ handle ->
424 do isetPrompt prompt
425 i <- receiveInput handle e
426 return (i, h)
427 (cmd, step) <- case x of
428 Nothing -> do iPrintError ""; ifail "Abandoned"
429 Just input -> return (parseTactic i input, input)
430 case cmd of
431 Success Abandon -> do iPrintError ""; ifail "Abandoned"
432 _ -> return ()
433 (d, st, done, prf', res) <- idrisCatch
434 (case cmd of
435 Failure err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)
436 Success Undo -> do (_, st) <- elabStep e loadState
437 return (True, st, False, init prf, Right $ iPrintResult "")
438 Success ProofState -> return (True, e, False, prf, Right $ iPrintResult "")
439 Success ProofTerm -> do tm <- lifte e get_term
440 iputStrLn $ "TT: " ++ show tm ++ "\n"
441 return (False, e, False, prf, Right $ iPrintResult "")
442 Success Qed -> do hs <- lifte e get_holes
443 unless (null hs) $ ifail "Incomplete proof"
444 iputStrLn "Proof completed!"
445 return (False, e, True, prf, Right $ iPrintResult "")
446 Success (TCheck (PRef _ _ n)) -> checkNameType e prf n
447 Success (TCheck t) -> checkType e prf t
448 Success (TEval t) -> evalTerm e prf t
449 Success (TDocStr x) -> docStr e prf x
450 Success (TSearch t) -> search e prf t
451 Success tac ->
452 do (_, e) <- elabStep e saveState
453 (_, st) <- elabStep e (runTac autoSolve i (Just proverFC) fn tac)
454 return (True, st, False, prf ++ [step], Right $ iPrintResult ""))
455 (\err -> return (False, e, False, prf, Left err))
456 idemodePutSExp "write-proof-state" (prf', length prf')
457 case res of
458 Left err -> do ist <- getIState
459 iRenderError $ pprintErr ist err
460 ploop fn d prompt prf' st h'
461 Right ok ->
462 if done then do (tm, _) <- elabStep st get_term
463 return (tm, prf')
464 else runWithInterrupt e ok
465 (ploop fn d prompt prf' st h')
466 (ploop fn d prompt prf e h')
469envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env
471checkNameType :: ElabState EState -> [String] -> Name -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
472checkNameType e prf n = do
473 ctxt <- getContext
474 ist <- getIState
475 imp <- impShow
476 idrisCatch (do
477 let OK env = envAtFocus (proof e)
478 ctxt' = envCtxt env ctxt
479 bnd = map (\x -> (fst x, False)) env
480 ist' = ist { tt_ctxt = ctxt' }
481 putIState ist'
482 -- Unlike the REPL, metavars have no special treatment, to
483 -- make it easier to see how to prove with them.
484 let action = case lookupNames n ctxt' of
485 [] -> iPrintError $ "No such variable " ++ show n
486 ts -> iPrintFunTypes bnd n (map (\n -> (n, pprintDelabTy ist' n)) ts)
487 putIState ist
488 return (False, e, False, prf, Right action))
489 (\err -> do putIState ist ; ierror err)
491checkType :: ElabState EState -> [String] -> PTerm -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
492checkType e prf t = do
493 ist <- getIState
494 ctxt <- getContext
495 idrisCatch (do
496 let OK env = envAtFocus (proof e)
497 ctxt' = envCtxt env ctxt
498 putIState ist { tt_ctxt = ctxt' }
499 (tm, ty) <- elabVal recinfo ERHS t
500 let ppo = ppOptionIst ist
501 ty' = normaliseC ctxt [] ty
502 infixes = idris_infixes ist
503 action = case tm of
504 TType _ ->
505 iPrintTermWithType (prettyImp ppo (PType emptyFC)) type1Doc
506 _ -> let bnd = map (\x -> (fst x, False)) env in
507 iPrintTermWithType (pprintPTerm ppo bnd [] infixes (delab ist tm))
508 (pprintPTerm ppo bnd [] infixes (delab ist ty))
509 putIState ist
510 return (False, e, False, prf, Right action))
511 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)
513proverFC = FC "(prover shell)" (0, 0) (0, 0)
515evalTerm :: ElabState EState -> [String] -> PTerm -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
516evalTerm e prf t = withErrorReflection $
517 do ctxt <- getContext
518 ist <- getIState
519 idrisCatch (do
520 let OK env = envAtFocus (proof e)
521 ctxt' = envCtxt env ctxt
522 ist' = ist { tt_ctxt = ctxt' }
523 bnd = map (\x -> (fst x, False)) env
524 putIState ist'
525 (tm, ty) <- elabVal recinfo ERHS t
526 let tm' = force (normaliseAll ctxt' env tm)
527 ty' = force (normaliseAll ctxt' env ty)
528 ppo = ppOption (idris_options ist')
529 infixes = idris_infixes ist
530 tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')
531 tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')
532 action = iPrintTermWithType tmDoc tyDoc
533 putIState ist
534 return (False, e, False, prf, Right action))
535 (\err -> do putIState ist ; ierror err)
537docStr :: ElabState EState -> [String] -> Either Name Const -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
538docStr e prf (Left n) = do ist <- getIState
539 idrisCatch (case lookupCtxtName n (idris_docstrings ist) of
540 [] -> return (False, e, False, prf,
541 Left . Msg $ "No documentation for " ++ show n)
542 ns -> do toShow <- mapM (showDoc ist) ns
543 return (False, e, False, prf,
544 Right $ iRenderResult (vsep toShow)))
545 (\err -> do putIState ist ; ierror err)
546 where showDoc ist (n, d) = do doc <- getDocs n FullDocs
547 return $ pprintDocs ist doc
548docStr e prf (Right c) = do ist <- getIState
549 return (False, e, False, prf, Right . iRenderResult $ pprintConstDocs ist c (constDocs c))
550search e prf t = return (False, e, False, prf, Right $ searchByType [] t)