git.iko.soy/Idris-dev
on aeb032a help sign in
Idris-dev/src/Idris/Prover.hs
550 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, foldl, foldr, fst, id, init, length,
15 lines, map, not, null, repeat, reverse, tail, zip, ($), (&&),
16 (++), (.), (||))
18import Idris.AbsSyntax
19import Idris.Completion
20import Idris.Core.CaseTree
21import Idris.Core.Elaborate hiding (Tactic(..))
22import Idris.Core.Evaluate
23import Idris.Core.TT
24import Idris.Core.Typecheck
25import Idris.DataOpts
26import Idris.Delaborate
27import Idris.Docs (getDocs, pprintConstDocs, pprintDocs)
28import Idris.Elab.Term
29import Idris.Elab.Utils
30import Idris.Elab.Value
31import Idris.ElabDecls
32import Idris.Error
33import qualified Idris.IdeMode as IdeMode
34import Idris.Options
35import Idris.Output
36import Idris.Parser hiding (params)
37import Idris.TypeSearch (searchByType)
39import Util.Pretty
41import Control.DeepSeq
42import Control.Monad.State.Strict
43import System.Console.Haskeline
44import System.Console.Haskeline.History
45import System.IO (Handle, hPutStrLn, stdin, stdout)
47-- | Launch the proof shell
48prover :: ElabInfo -> Bool -> Bool -> Name -> Idris ()
49prover info 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 info (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 -> ElabInfo -> Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()
87prove mode info opt ctxt lit n ty
88 = do ps <- fmap (\ist -> initElaborator n (constraintNS info) ctxt (idris_datatypes ist) (idris_name ist) ty) getIState
89 idemodePutSExp "start-proof-mode" n
90 (tm, prf) <-
91 if mode
92 then elabloop info 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 (constraintNS info) (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')] ty
123 ctxt
124 setContext ctxt'
125 solveDeferred emptyFC n
126 case idris_outputmode i of
127 IdeMode n h ->
128 runIO . hPutStrLn h $ IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", "") n
129 _ -> return ()
131elabStep :: ElabState EState -> ElabD a -> Idris (a, ElabState EState)
132elabStep st e =
133 case runStateT eCheck st of
134 OK ((a, ctxt'), ES (ps, est@EState{new_tyDecls = declTodo}) x old) ->
135 do setContext ctxt'
136 processTacticDecls toplevel declTodo
137 return (a, ES (ps, est {new_tyDecls = []}) x old)
138 Error a -> ierror a
139 where eCheck = do res <- e
140 matchProblems True
141 unifyProblems
142 probs' <- get_probs
143 case probs' of
144 [] -> do tm <- get_term
145 ctxt <- get_context
146 lift $ check ctxt [] (forget tm)
147 return (res, ctxt)
148 ((_,_,_,_,e,_,_):_) -> lift $ Error e
150dumpState :: IState -> Bool -> [(Name, Type, Term)] -> ProofState -> Idris ()
151dumpState ist inElab menv ps | [] <- holes ps =
152 do let nm = thname ps
153 rendered <- iRender $ prettyName True False [] nm <> colon <+> text "No more goals."
154 iputGoal rendered
155dumpState ist inElab menv ps | (h : hs) <- holes ps = do
156 let OK ty = goalAtFocus ps
157 OK env = envAtFocus ps
158 state = prettyOtherGoals hs <> line <>
159 prettyAssumptions inElab ty env <> line <>
160 prettyMetaValues (reverse menv) <>
161 prettyGoal (zip (assumptionNames env) (repeat False)) ty
162 rendered <- iRender state
163 iputGoal rendered
165 where
166 (h : _) = holes ps -- apparently the pattern guards don't give us this
168 ppo = ppOptionIst ist
170 tPretty bnd t = annotate (AnnTerm bnd t) .
171 pprintPTerm ppo bnd [] (idris_infixes ist) $
172 delab ist t
174 assumptionNames :: Env -> [Name]
175 assumptionNames = map fstEnv
177 prettyPs :: Bool -> Binder Type -> [(Name, Bool)] -> Env -> Doc OutputAnnotation
178 prettyPs all g bnd [] = empty
179 prettyPs all g bnd ((n@(MN _ r), _, _) : bs)
180 | not all && r == txt "rewrite_rule" = prettyPs all g ((n, False):bnd) bs
181 prettyPs all g bnd ((n@(MN _ _), _, _) : bs)
182 | not (all || n `elem` freeEnvNames bs || n `elem` goalNames g) = prettyPs all g bnd bs
183 prettyPs all g bnd ((n, _, Let rig t v) : bs) =
184 line <> bindingOf n False <+> text "=" <+> tPretty bnd v <+> colon <+>
185 align (tPretty bnd t) <> prettyPs all g ((n, False):bnd) bs
186 prettyPs all g bnd ((n, _, b) : bs) =
187 line <> bindingOf n False <+> colon <+>
188 align (tPretty bnd (binderTy b)) <> prettyPs all g ((n, False):bnd) bs
190 prettyMetaValues [] = empty
191 prettyMetaValues mvs =
192 text "---------- Meta-values: ----------" <$$>
193 prettyMetaValues' [] mvs <> line <> line
194 prettyMetaValues' _ [] = empty
195 prettyMetaValues' bnd [mv] = ppMv bnd mv
196 prettyMetaValues' bnd ((mv@(n, ty, tm)) : mvs) =
197 ppMv bnd mv <$>
198 prettyMetaValues' ((n, False):bnd) mvs
200 ppMv bnd (n, ty, tm) = kwd "let" <+> bindingOf n False <+> colon <+>
201 tPretty bnd ty <+> text "=" <+> tPretty bnd tm
203 kwd = annotate AnnKeyword . text
205 goalNames (Guess t v) = freeNames t ++ freeNames v
206 goalNames b = freeNames (binderTy b)
208 prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v
209 prettyG bnd b = tPretty bnd $ binderTy b
211 prettyGoal bnd ty =
212 text "---------- Goal: ----------" <$$>
213 bindingOf h False <+> colon <+> align (prettyG bnd ty)
215 prettyAssumptions inElab g env =
216 if null env then empty
217 else
218 text "---------- Assumptions: ----------" <>
219 nest nestingSize (prettyPs inElab g [] $ reverse env)
221 prettyOtherGoals hs =
222 if null hs then empty
223 else
224 text "---------- Other goals: ----------" <$$>
225 nest nestingSize (align . cat . punctuate (text ",") . map (`bindingOf` False) $ hs)
227 freeEnvNames :: Env -> [Name]
228 freeEnvNames = concatMap (\(n, _, b) -> freeNames (Bind n b Erased))
230lifte :: ElabState EState -> ElabD a -> Idris a
231lifte st e = do (v, _) <- elabStep st e
232 return v
234receiveInput :: Handle -> ElabState EState -> Idris (Maybe String)
235receiveInput h e =
236 do i <- getIState
237 let inh = if h == stdout then stdin else h
238 len' <- runIO $ IdeMode.getLen inh
239 len <- case len' of
240 Left err -> ierror err
241 Right n -> return n
242 l <- runIO $ IdeMode.getNChar inh len ""
243 (sexp, id) <- case IdeMode.parseMessage l of
244 Left err -> ierror err
245 Right (sexp, id) -> return (sexp, id)
246 putIState $ i { idris_outputmode = IdeMode id h }
247 case IdeMode.sexpToCommand sexp of
248 Just (IdeMode.REPLCompletions prefix) ->
249 do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")
250 let good = IdeMode.SexpList [IdeMode.SymbolAtom "ok", IdeMode.toSExp (map replacement compls, reverse unused)]
251 idemodePutSExp "return" good
252 receiveInput h e
253 Just (IdeMode.Interpret cmd) -> return (Just cmd)
254 Just (IdeMode.TypeOf str) -> return (Just (":t " ++ str))
255 Just (IdeMode.DocsFor str _) -> return (Just (":doc " ++ str))
256 _ -> return Nothing
258data ElabShellHistory = ElabStep | LetStep | BothStep
260undoStep :: [String] -> [(Name, Type, Term)] -> ElabState EState -> ElabShellHistory -> Idris ([String], [(Name, Type, Term)], ElabState EState)
261undoStep prf env st ElabStep = do (_, st') <- elabStep st loadState
262 return (init prf, env, st')
263undoStep prf env st LetStep = return (init prf, tail env, st)
264undoStep prf env st BothStep = do (_, st') <- elabStep st loadState
265 return (init prf, tail env, st')
267undoElab :: [String] -> [(Name, Type, Term)] -> ElabState EState -> [ElabShellHistory] -> Idris ([String], [(Name, Type, Term)], ElabState EState, [ElabShellHistory])
268undoElab prf env st [] = ifail "Nothing to undo"
269undoElab prf env st (h:hs) = do (prf', env', st') <- undoStep prf env st h
270 return (prf', env', st', hs)
272proverfc = fileFC "prover"
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 :: ElabInfo -> Name -> Bool -> String -> [String] -> ElabState EState -> [ElabShellHistory] -> Maybe History -> [(Name, Type, Term)] -> Idris (Term, [String])
291elabloop info 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 Right (Left EAbandon) -> do iPrintError ""; ifail "Abandoned"
315 _ -> return ()
317 (d, prev', st, done, prf', env', res) <-
318 idrisCatch
319 (case cmd of
320 Left err ->
321 return (False, prev, e, False, prf, env, Left . Msg . show . fixColour (idris_colourRepl ist) . parseErrorDoc $ err)
322 Right (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 Right (Right cmd') ->
348 case cmd' of
349 DoLetP {} -> ifail "Pattern-matching let not supported here"
350 DoRewrite {} -> ifail "Pattern-matching do-rewrite not supported here"
351 DoBindP {} -> ifail "Pattern-matching <- not supported here"
352 DoLet fc rig i ifc Placeholder expr ->
353 do (tm, ty) <- elabVal (recinfo proverfc) ERHS (inLets ist env expr)
354 ctxt <- getContext
355 let tm' = normaliseAll ctxt [] tm
356 ty' = normaliseAll ctxt [] ty
357 return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult ""))
358 DoLet fc rig i ifc ty expr ->
359 do (tm, ty) <- elabVal (recinfo proverfc) ERHS
360 (PApp NoFC (PRef NoFC [] (sUN "the"))
361 [ pexp (inLets ist env ty)
362 , pexp (inLets ist env expr)
363 ])
364 ctxt <- getContext
365 let tm' = normaliseAll ctxt [] tm
366 ty' = normaliseAll ctxt [] ty
367 return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult ""))
368 DoBind fc i ifc expr ->
369 do (tm, ty) <- elabVal (recinfo proverfc) ERHS (inLets ist env expr)
370 (_, e') <- elabStep e saveState -- enable :undo
371 (res, e'') <- elabStep e' $
372 runElabAction info ist NoFC [] tm ["Shell"]
373 ctxt <- getContext
374 (v, vty) <- tclift $ check ctxt [] (forget res)
375 let v' = normaliseAll ctxt [] v
376 vty' = normaliseAll ctxt [] vty
377 return (True, BothStep:prev, e'', False, prf ++ [step], (i, vty', v') : env, Right (iPrintResult ""))
378 DoExp fc expr ->
379 do (tm, ty) <- elabVal (recinfo proverfc) ERHS (inLets ist env expr)
380 -- TODO: call elaborator with Elab () as goal here
381 (_, e') <- elabStep e saveState -- enable :undo
382 (_, e'') <- elabStep e' $
383 runElabAction info ist NoFC [] tm ["Shell"]
384 return (True, ElabStep:prev, e'', False, prf ++ [step], env, Right (iPrintResult "")))
385 (\err -> return (False, prev, e, False, prf, env, Left err))
386 idemodePutSExp "write-proof-state" (prf', length prf')
387 case res of
388 Left err -> do ist <- getIState
389 iRenderError $ pprintErr ist err
390 elabloop info fn d prompt prf' st prev' h' env'
391 Right ok ->
392 if done then do (tm, _) <- elabStep st get_term
393 return (tm, prf')
394 else runWithInterrupt e ok
395 (elabloop info fn d prompt prf' st prev' h' env')
396 (elabloop info fn d prompt prf e prev h' env)
398 where
399 -- A bit of a hack: wrap the value up in a let binding, which will
400 -- normalise away. It would be better to figure out how to call
401 -- the elaborator with a custom environment here to avoid the
402 -- delab step.
403 inLets :: IState -> [(Name, Type, Term)] -> PTerm -> PTerm
404 inLets ist lets tm = foldr (\(n, ty, v) b -> PLet NoFC RigW n NoFC (delab ist ty) (delab ist v) b) tm (reverse lets)
408ploop :: Name -> Bool -> String -> [String] -> ElabState EState -> Maybe History -> Idris (Term, [String])
409ploop fn d prompt prf e h
410 = do i <- getIState
411 let autoSolve = opt_autoSolve (idris_options i)
412 when d $ dumpState i False [] (proof e)
413 (x, h') <-
414 case idris_outputmode i of
415 RawOutput _ ->
416 runInputT (proverSettings e) $
417 -- Manually track the history so that we can use the proof state
418 do case h of
419 Just history -> putHistory history
420 Nothing -> return ()
421 l <- handleInterrupt (return $ Just "") $ withInterrupt $ getInputLine (prompt ++ "> ")
422 h' <- getHistory
423 return (l, Just h')
424 IdeMode _ handle ->
425 do isetPrompt prompt
426 i <- receiveInput handle e
427 return (i, h)
428 (cmd, step) <- case x of
429 Nothing -> do iPrintError ""; ifail "Abandoned"
430 Just input -> return (parseTactic i input, input)
431 case cmd of
432 Right Abandon -> do iPrintError ""; ifail "Abandoned"
433 _ -> return ()
434 (d, st, done, prf', res) <- idrisCatch
435 (case cmd of
436 Left err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) . parseErrorDoc $ err)
437 Right Undo -> do (_, st) <- elabStep e loadState
438 return (True, st, False, init prf, Right $ iPrintResult "")
439 Right ProofState -> return (True, e, False, prf, Right $ iPrintResult "")
440 Right ProofTerm -> do tm <- lifte e get_term
441 iputStrLn $ "TT: " ++ show tm ++ "\n"
442 return (False, e, False, prf, Right $ iPrintResult "")
443 Right Qed -> do hs <- lifte e get_holes
444 unless (null hs) $ ifail "Incomplete proof"
445 iputStrLn "Proof completed!"
446 return (False, e, True, prf, Right $ iPrintResult "")
447 Right (TCheck (PRef _ _ n)) -> checkNameType e prf n
448 Right (TCheck t) -> checkType e prf t
449 Right (TEval t) -> evalTerm e prf t
450 Right (TDocStr x) -> docStr e prf x
451 Right (TSearch t) -> search e prf t
452 Right tac ->
453 do (_, e) <- elabStep e saveState
454 (_, st) <- elabStep e (runTac autoSolve i (Just proverFC) fn tac)
455 return (True, st, False, prf ++ [step], Right $ iPrintResult ""))
456 (\err -> return (False, e, False, prf, Left err))
457 idemodePutSExp "write-proof-state" (prf', length prf')
458 case res of
459 Left err -> do ist <- getIState
460 iRenderError $ pprintErr ist err
461 ploop fn d prompt prf' st h'
462 Right ok ->
463 if done then do (tm, _) <- elabStep st get_term
464 return (tm, prf')
465 else runWithInterrupt e ok
466 (ploop fn d prompt prf' st h')
467 (ploop fn d prompt prf e h')
470envCtxt env ctxt = foldl (\c (n, _, b) -> addTyDecl n Bound (binderTy b) c) ctxt env
472checkNameType :: ElabState EState -> [String] -> Name -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
473checkNameType e prf n = do
474 ctxt <- getContext
475 ist <- getIState
476 imp <- impShow
477 idrisCatch (do
478 let OK env = envAtFocus (proof e)
479 ctxt' = envCtxt env ctxt
480 bnd = map (\x -> (fstEnv x, False)) env
481 ist' = ist { tt_ctxt = ctxt' }
482 putIState ist'
483 -- Unlike the REPL, metavars have no special treatment, to
484 -- make it easier to see how to prove with them.
485 let action = case lookupNames n ctxt' of
486 [] -> iPrintError $ "No such variable " ++ show n
487 ts -> iPrintFunTypes bnd n (map (\n -> (n, pprintDelabTy ist' n)) ts)
488 putIState ist
489 return (False, e, False, prf, Right action))
490 (\err -> do putIState ist ; ierror err)
492checkType :: ElabState EState -> [String] -> PTerm -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
493checkType e prf t = do
494 ist <- getIState
495 ctxt <- getContext
496 idrisCatch (do
497 let OK env = envAtFocus (proof e)
498 ctxt' = envCtxt env ctxt
499 putIState ist { tt_ctxt = ctxt' }
500 (tm, ty) <- elabVal (recinfo proverfc) ERHS t
501 let ppo = ppOptionIst ist
502 infixes = idris_infixes ist
503 action = case tm of
504 TType _ ->
505 iPrintTermWithType (prettyImp ppo (PType emptyFC)) type1Doc
506 _ -> let bnd = map (\x -> (fstEnv 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 -> (fstEnv x, False)) env
524 putIState ist'
525 (tm, ty) <- elabVal (recinfo proverfc) 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)