git.iko.soy/Idris-dev
on master help sign in
Idris-dev/src/Idris/Prover.hs
553 lines 27 kB history raw
1{-|
2Module : Idris.Prover
3Description : Idris' theorem prover.
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 -> do
321 msg <- fmap (Left . Msg . show) (formatMessage err)
322 return (False, prev, e, False, prf, env, msg)
323 Right (Left cmd') ->
324 case cmd' of
325 EQED -> do hs <- lifte e get_holes
326 unless (null hs) $ ifail "Incomplete proof"
327 iputStrLn "Proof completed!"
328 return (False, prev, e, True, prf, env, Right $ iPrintResult "")
329 EUndo -> do (prf', env', st', prev') <- undoElab prf env e prev
330 return (True, prev', st', False, prf', env', Right $ iPrintResult "")
331 EAbandon ->
332 error "the impossible happened - should have been matched on outer scope"
333 EProofState -> return (True, prev, e, False, prf, env, Right $ iPrintResult "")
334 EProofTerm ->
335 do tm <- lifte e get_term
336 return (False, prev, e, False, prf, env, Right $ iRenderResult (text "TT:" <+> pprintTT [] tm))
337 EEval tm -> do (d', st', done, prf', go) <- evalTerm e prf tm
338 return (d', prev, st', done, prf', env, go)
339 ECheck (PRef _ _ n) ->
340 do (d', st', done, prf', go) <- checkNameType e prf n
341 return (d', prev, st', done, prf', env, go)
342 ECheck tm -> do (d', st', done, prf', go) <- checkType e prf tm
343 return (d', prev, st', done, prf', env, go)
344 ESearch ty -> do (d', st', done, prf', go) <- search e prf ty
345 return (d', prev, st', done, prf', env, go)
346 EDocStr d -> do (d', st', done, prf', go) <- docStr e prf d
347 return (d', prev, st', done, prf', env, go)
348 Right (Right cmd') ->
349 case cmd' of
350 DoLetP {} -> ifail "Pattern-matching let not supported here"
351 DoRewrite {} -> ifail "Pattern-matching do-rewrite not supported here"
352 DoBindP {} -> ifail "Pattern-matching <- not supported here"
353 DoLet fc rig i ifc Placeholder expr ->
354 do (tm, ty) <- elabVal (recinfo proverfc) ERHS (inLets ist env expr)
355 ctxt <- getContext
356 let tm' = normaliseAll ctxt [] tm
357 ty' = normaliseAll ctxt [] ty
358 return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult ""))
359 DoLet fc rig i ifc ty expr ->
360 do (tm, ty) <- elabVal (recinfo proverfc) ERHS
361 (PApp NoFC (PRef NoFC [] (sUN "the"))
362 [ pexp (inLets ist env ty)
363 , pexp (inLets ist env expr)
364 ])
365 ctxt <- getContext
366 let tm' = normaliseAll ctxt [] tm
367 ty' = normaliseAll ctxt [] ty
368 return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult ""))
369 DoBind fc i ifc expr ->
370 do (tm, ty) <- elabVal (recinfo proverfc) ERHS (inLets ist env expr)
371 (_, e') <- elabStep e saveState -- enable :undo
372 (res, e'') <- elabStep e' $
373 runElabAction info ist NoFC [] tm ["Shell"]
374 ctxt <- getContext
375 (v, vty) <- tclift $ check ctxt [] (forget res)
376 let v' = normaliseAll ctxt [] v
377 vty' = normaliseAll ctxt [] vty
378 return (True, BothStep:prev, e'', False, prf ++ [step], (i, vty', v') : env, Right (iPrintResult ""))
379 DoExp fc expr ->
380 do (tm, ty) <- elabVal (recinfo proverfc) ERHS (inLets ist env expr)
381 -- TODO: call elaborator with Elab () as goal here
382 (_, e') <- elabStep e saveState -- enable :undo
383 (_, e'') <- elabStep e' $
384 runElabAction info ist NoFC [] tm ["Shell"]
385 return (True, ElabStep:prev, e'', False, prf ++ [step], env, Right (iPrintResult "")))
386 (\err -> return (False, prev, e, False, prf, env, Left err))
387 idemodePutSExp "write-proof-state" (prf', length prf')
388 case res of
389 Left err -> do ist <- getIState
390 iRenderError $ pprintErr ist err
391 elabloop info fn d prompt prf' st prev' h' env'
392 Right ok ->
393 if done then do (tm, _) <- elabStep st get_term
394 return (tm, prf')
395 else runWithInterrupt e ok
396 (elabloop info fn d prompt prf' st prev' h' env')
397 (elabloop info fn d prompt prf e prev h' env)
399 where
400 -- A bit of a hack: wrap the value up in a let binding, which will
401 -- normalise away. It would be better to figure out how to call
402 -- the elaborator with a custom environment here to avoid the
403 -- delab step.
404 inLets :: IState -> [(Name, Type, Term)] -> PTerm -> PTerm
405 inLets ist lets tm = foldr (\(n, ty, v) b -> PLet NoFC RigW n NoFC (delab ist ty) (delab ist v) b) tm (reverse lets)
409ploop :: Name -> Bool -> String -> [String] -> ElabState EState -> Maybe History -> Idris (Term, [String])
410ploop fn d prompt prf e h
411 = do i <- getIState
412 let autoSolve = opt_autoSolve (idris_options i)
413 when d $ dumpState i False [] (proof e)
414 (x, h') <-
415 case idris_outputmode i of
416 RawOutput _ ->
417 runInputT (proverSettings e) $
418 -- Manually track the history so that we can use the proof state
419 do case h of
420 Just history -> putHistory history
421 Nothing -> return ()
422 l <- handleInterrupt (return $ Just "") $ withInterrupt $ getInputLine (prompt ++ "> ")
423 h' <- getHistory
424 return (l, Just h')
425 IdeMode _ handle ->
426 do isetPrompt prompt
427 i <- receiveInput handle e
428 return (i, h)
429 (cmd, step) <- case x of
430 Nothing -> do iPrintError ""; ifail "Abandoned"
431 Just input -> return (parseTactic i input, input)
432 case cmd of
433 Right Abandon -> do iPrintError ""; ifail "Abandoned"
434 _ -> return ()
435 (d, st, done, prf', res) <- idrisCatch
436 (case cmd of
437 Left err -> do
438 msg <- fmap (Left . Msg . show) (formatMessage err)
439 return (False, e, False, prf, msg)
440 Right Undo -> do (_, st) <- elabStep e loadState
441 return (True, st, False, init prf, Right $ iPrintResult "")
442 Right ProofState -> return (True, e, False, prf, Right $ iPrintResult "")
443 Right ProofTerm -> do tm <- lifte e get_term
444 iputStrLn $ "TT: " ++ show tm ++ "\n"
445 return (False, e, False, prf, Right $ iPrintResult "")
446 Right 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 Right (TCheck (PRef _ _ n)) -> checkNameType e prf n
451 Right (TCheck t) -> checkType e prf t
452 Right (TEval t) -> evalTerm e prf t
453 Right (TDocStr x) -> docStr e prf x
454 Right (TSearch t) -> search e prf t
455 Right 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 infixes = idris_infixes ist
506 action = case tm of
507 TType _ ->
508 iPrintTermWithType (prettyImp ppo (PType emptyFC)) type1Doc
509 _ -> let bnd = map (\x -> (fstEnv x, False)) env in
510 iPrintTermWithType (pprintPTerm ppo bnd [] infixes (delab ist tm))
511 (pprintPTerm ppo bnd [] infixes (delab ist ty))
512 putIState ist
513 return (False, e, False, prf, Right action))
514 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)
516proverFC = FC "(prover shell)" (0, 0) (0, 0)
518evalTerm :: ElabState EState -> [String] -> PTerm -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
519evalTerm e prf t = withErrorReflection $
520 do ctxt <- getContext
521 ist <- getIState
522 idrisCatch (do
523 let OK env = envAtFocus (proof e)
524 ctxt' = envCtxt env ctxt
525 ist' = ist { tt_ctxt = ctxt' }
526 bnd = map (\x -> (fstEnv x, False)) env
527 putIState ist'
528 (tm, ty) <- elabVal (recinfo proverfc) ERHS t
529 let tm' = force (normaliseAll ctxt' env tm)
530 ty' = force (normaliseAll ctxt' env ty)
531 ppo = ppOption (idris_options ist')
532 infixes = idris_infixes ist
533 tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')
534 tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')
535 action = iPrintTermWithType tmDoc tyDoc
536 putIState ist
537 return (False, e, False, prf, Right action))
538 (\err -> do putIState ist ; ierror err)
540docStr :: ElabState EState -> [String] -> Either Name Const -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
541docStr e prf (Left n) = do ist <- getIState
542 idrisCatch (case lookupCtxtName n (idris_docstrings ist) of
543 [] -> return (False, e, False, prf,
544 Left . Msg $ "No documentation for " ++ show n)
545 ns -> do toShow <- mapM (showDoc ist) ns
546 return (False, e, False, prf,
547 Right $ iRenderResult (vsep toShow)))
548 (\err -> do putIState ist ; ierror err)
549 where showDoc ist (n, d) = do doc <- getDocs n FullDocs
550 return $ pprintDocs ist doc
551docStr e prf (Right c) = do ist <- getIState
552 return (False, e, False, prf, Right . iRenderResult $ pprintConstDocs ist c (constDocs c))
553search e prf t = return (False, e, False, prf, Right $ searchByType [] t)