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