{-|
Module      : Idris.Prover
Description : Idris' theorem prover.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE PatternGuards #-}
module Idris.Prover (prover, showProof, showRunElab) where

-- Hack for GHC 7.10 and earlier compat without CPP or warnings
-- This exludes (<$>) as fmap, because wl-pprint uses it for newline
import Prelude (Bool(..), Either(..), Eq(..), Maybe(..), Show(..), String,
                concatMap, elem, error, foldl, foldr, fst, id, init, length,
                lines, map, not, null, repeat, reverse, tail, zip, ($), (&&),
                (++), (.), (||))

import Idris.AbsSyntax
import Idris.Completion
import Idris.Core.CaseTree
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.DataOpts
import Idris.Delaborate
import Idris.Docs (getDocs, pprintConstDocs, pprintDocs)
import Idris.Elab.Term
import Idris.Elab.Utils
import Idris.Elab.Value
import Idris.ElabDecls
import Idris.Error
import qualified Idris.IdeMode as IdeMode
import Idris.Options
import Idris.Output
import Idris.Parser hiding (params)
import Idris.TypeSearch (searchByType)

import Util.Pretty

import Control.DeepSeq
import Control.Monad.State.Strict
import System.Console.Haskeline
import System.Console.Haskeline.History
import System.IO (Handle, hPutStrLn, stdin, stdout)

-- | Launch the proof shell
prover :: ElabInfo -> Bool -> Bool -> Name -> Idris ()
prover info mode lit x =
           do ctxt <- getContext
              i <- getIState
              case lookupTy x ctxt of
                  [t] -> if elem x (map fst (idris_metavars i))
                               then prove mode info (idris_optimisation i) ctxt lit x t
                               else ifail $ show x ++ " is not a hole"
                  _ -> fail "No such hole"

showProof :: Bool -> Name -> [String] -> String
showProof lit n ps
    = bird ++ show n ++ " = proof" ++ break ++
             showSep break (map (\x -> "  " ++ x) ps) ++
                     break ++ "\n"
  where bird = if lit then "> " else ""
        break = "\n" ++ bird

showRunElab :: Bool -> Name -> [String] -> String
showRunElab lit n ps = birdify (displayS (renderPretty 1.0 80 doc) "")
  where doc = text (show n) <+> text "=" <+> text "%runElab" <+>
              enclose lparen rparen
                (text "do" <+> (align $ vsep (map text ps)))
        birdify = if lit
                     then concatMap ("> " ++) . lines
                     else id

proverSettings :: ElabState EState -> Settings Idris
proverSettings e = setComplete (proverCompletion (assumptionNames e)) defaultSettings

assumptionNames :: ElabState EState -> [String]
assumptionNames e
  = case envAtFocus (proof e) of
         OK env -> names env
  where names [] = []
        names ((MN _ _, _, _) : bs) = names bs
        names ((n, _, _) : bs) = show n : names bs

prove :: Bool -> ElabInfo -> Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()
prove mode info opt ctxt lit n ty
    = do ps <- fmap (\ist -> initElaborator n (constraintNS info) ctxt (idris_datatypes ist) (idris_name ist) ty) getIState
         idemodePutSExp "start-proof-mode" n
         (tm, prf) <-
            if mode
              then elabloop info n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) [] Nothing []
              else do iputStrLn $ "Warning: this interactive prover is deprecated and will be removed " ++
                                  "in a future release. Please see :elab for a similar feature that "++
                                  "will replace it."
                      ploop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) Nothing
         logLvl 1 $ "Adding " ++ show tm
         i <- getIState
         let shower = if mode
                         then showRunElab
                         else showProof
         case idris_outputmode i of
           IdeMode _ _ -> idemodePutSExp "end-proof-mode" (n, shower lit n prf)
           _            -> iputStrLn $ shower lit n prf
         let proofs = proof_list i
         putIState (i { proof_list = (n, (mode, prf)) : proofs })
         let tree = simpleCase False (STerm Erased) False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]
         logLvl 3 (show tree)
         (ptm, pty) <- recheckC (constraintNS info) (fileFC "proof") id [] tm
         logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++
                   "Expected type:" ++ show ty)
         case converts ctxt [] ty pty of
              OK _ -> return ()
              Error e -> ierror (CantUnify False (ty, Nothing) (pty, Nothing) e [] 0)
         ptm' <- applyOpts ptm
         ei <- getErasureInfo `fmap` getIState
         ctxt' <- do ctxt <- getContext
                     tclift $ addCasedef n ei (CaseInfo True True False) False (STerm Erased) True False
                                [] []  -- argtys, inaccArgs
                                [Right (P Ref n ty, ptm)]
                                [([], P Ref n ty, ptm)]
                                [([], P Ref n ty, ptm')] ty
                                ctxt
         setContext ctxt'
         solveDeferred emptyFC n
         case idris_outputmode i of
           IdeMode n h ->
             runIO . hPutStrLn h $ IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", "") n
           _ -> return ()

elabStep :: ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep st e =
    case runStateT eCheck st of
        OK ((a, ctxt'), ES (ps, est@EState{new_tyDecls = declTodo}) x old) ->
          do setContext ctxt'
             processTacticDecls toplevel declTodo
             return (a, ES (ps, est {new_tyDecls = []}) x old)
        Error a -> ierror a
  where eCheck = do res <- e
                    matchProblems True
                    unifyProblems
                    probs' <- get_probs
                    case probs' of
                         [] -> do tm <- get_term
                                  ctxt <- get_context
                                  lift $ check ctxt [] (forget tm)
                                  return (res, ctxt)
                         ((_,_,_,_,e,_,_):_) -> lift $ Error e

dumpState :: IState -> Bool -> [(Name, Type, Term)] -> ProofState -> Idris ()
dumpState ist inElab menv ps | [] <- holes ps =
  do let nm = thname ps
     rendered <- iRender $ prettyName True False [] nm <> colon <+> text "No more goals."
     iputGoal rendered
dumpState ist inElab menv ps | (h : hs) <- holes ps = do
  let OK ty  = goalAtFocus ps
      OK env = envAtFocus ps
      state = prettyOtherGoals hs <> line <>
              prettyAssumptions inElab ty env <> line <>
              prettyMetaValues (reverse menv) <>
              prettyGoal (zip (assumptionNames env) (repeat False)) ty
  rendered <- iRender state
  iputGoal rendered

  where
    (h : _) = holes ps -- apparently the pattern guards don't give us this

    ppo = ppOptionIst ist

    tPretty bnd t = annotate (AnnTerm bnd t) .
                    pprintPTerm ppo bnd [] (idris_infixes ist) $
                    delab ist t

    assumptionNames :: Env -> [Name]
    assumptionNames = map fstEnv

    prettyPs :: Bool -> Binder Type -> [(Name, Bool)] -> Env -> Doc OutputAnnotation
    prettyPs all g bnd [] = empty
    prettyPs all g bnd ((n@(MN _ r), _, _) : bs)
        | not all && r == txt "rewrite_rule" = prettyPs all g ((n, False):bnd) bs
    prettyPs all g bnd ((n@(MN _ _), _, _) : bs)
        | not (all || n `elem` freeEnvNames bs || n `elem` goalNames g) = prettyPs all g bnd bs
    prettyPs all g bnd ((n, _, Let rig t v) : bs) =
      line <> bindingOf n False <+> text "=" <+> tPretty bnd v <+> colon <+>
        align (tPretty bnd t) <> prettyPs all g ((n, False):bnd) bs
    prettyPs all g bnd ((n, _, b) : bs) =
      line <> bindingOf n False <+> colon <+>
      align (tPretty bnd (binderTy b)) <> prettyPs all g ((n, False):bnd) bs

    prettyMetaValues [] = empty
    prettyMetaValues mvs =
      text "----------              Meta-values:               ----------" <$$>
      prettyMetaValues' [] mvs <> line <> line
    prettyMetaValues' _   [] = empty
    prettyMetaValues' bnd [mv] = ppMv bnd mv
    prettyMetaValues' bnd ((mv@(n, ty, tm)) : mvs) =
      ppMv bnd mv <$>
      prettyMetaValues' ((n, False):bnd) mvs

    ppMv bnd (n, ty, tm) = kwd "let" <+> bindingOf n False <+> colon <+>
                           tPretty bnd ty <+> text "=" <+> tPretty bnd tm

    kwd = annotate AnnKeyword . text

    goalNames (Guess t v) = freeNames t ++ freeNames v
    goalNames b = freeNames (binderTy b)

    prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v
    prettyG bnd b = tPretty bnd $ binderTy b

    prettyGoal bnd ty =
      text "----------                 Goal:                  ----------" <$$>
      bindingOf h False <+> colon <+> align (prettyG bnd ty)

    prettyAssumptions inElab g env =
      if null env then empty
      else
        text "----------              Assumptions:              ----------" <>
        nest nestingSize (prettyPs inElab g [] $ reverse env)

    prettyOtherGoals hs =
      if null hs then empty
      else
        text "----------              Other goals:              ----------" <$$>
        nest nestingSize (align . cat . punctuate (text ",") . map (`bindingOf` False) $ hs)

    freeEnvNames :: Env -> [Name]
    freeEnvNames = concatMap (\(n, _, b) -> freeNames (Bind n b Erased))

lifte :: ElabState EState -> ElabD a -> Idris a
lifte st e = do (v, _) <- elabStep st e
                return v

receiveInput :: Handle -> ElabState EState -> Idris (Maybe String)
receiveInput h e =
  do i <- getIState
     let inh = if h == stdout then stdin else h
     len' <- runIO $ IdeMode.getLen inh
     len <- case len' of
       Left err -> ierror err
       Right n  -> return n
     l <- runIO $ IdeMode.getNChar inh len ""
     (sexp, id) <- case IdeMode.parseMessage l of
                     Left err -> ierror err
                     Right (sexp, id) -> return (sexp, id)
     putIState $ i { idris_outputmode = IdeMode id h }
     case IdeMode.sexpToCommand sexp of
       Just (IdeMode.REPLCompletions prefix) ->
         do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")
            let good = IdeMode.SexpList [IdeMode.SymbolAtom "ok", IdeMode.toSExp (map replacement compls, reverse unused)]
            idemodePutSExp "return" good
            receiveInput h e
       Just (IdeMode.Interpret cmd) -> return (Just cmd)
       Just (IdeMode.TypeOf str) -> return (Just (":t " ++ str))
       Just (IdeMode.DocsFor str _) -> return (Just (":doc " ++ str))
       _ -> return Nothing

data ElabShellHistory = ElabStep | LetStep | BothStep

undoStep :: [String] -> [(Name, Type, Term)] -> ElabState EState -> ElabShellHistory -> Idris ([String], [(Name, Type, Term)], ElabState EState)
undoStep prf env st ElabStep = do (_, st') <- elabStep st loadState
                                  return (init prf, env, st')
undoStep prf env st LetStep = return (init prf, tail env, st)
undoStep prf env st BothStep = do (_, st') <- elabStep st loadState
                                  return (init prf, tail env, st')

undoElab :: [String] -> [(Name, Type, Term)] -> ElabState EState -> [ElabShellHistory] -> Idris ([String], [(Name, Type, Term)], ElabState EState, [ElabShellHistory])
undoElab prf env st [] = ifail "Nothing to undo"
undoElab prf env st (h:hs) = do (prf', env', st') <- undoStep prf env st h
                                return (prf', env', st', hs)

proverfc = fileFC "prover"

runWithInterrupt
  :: ElabState EState
  -> Idris a -- ^ run with SIGINT handler
  -> Idris b -- ^ run if mTry finished
  -> Idris b -- ^ run if mTry was interrupted
  -> Idris b
runWithInterrupt elabState mTry mSuccess mFailure = do
  ist <- getIState
  case idris_outputmode ist of
    RawOutput _ -> do
      success <- runInputT (proverSettings elabState) $
                   handleInterrupt (return False) $
                   withInterrupt (lift mTry >> return True)
      if success then mSuccess else mFailure
    IdeMode _ _ -> mTry >> mSuccess

elabloop :: ElabInfo -> Name -> Bool -> String -> [String] -> ElabState EState -> [ElabShellHistory] -> Maybe History -> [(Name, Type, Term)] -> Idris (Term, [String])
elabloop info fn d prompt prf e prev h env
  = do ist <- getIState
       when d $ dumpState ist True env (proof e)
       (x, h') <-
         case idris_outputmode ist of
           RawOutput _ ->
             runInputT (proverSettings e) $
               do case h of
                    Just history -> putHistory history
                    Nothing -> return ()
                  l <- handleInterrupt (return $ Just "") $ withInterrupt $ getInputLine (prompt ++ "> ")
                  h' <- getHistory
                  return (l, Just h')
           IdeMode _ handle ->
             do isetPrompt prompt
                i <- receiveInput handle e
                return (i, h)
       (cmd, step) <- case x of
                        Nothing -> do iPrintError "" ; ifail "Abandoned"
                        Just input -> return (parseElabShellStep ist input, input)

       -- if we're abandoning, it has to be outside the scope of the catch
       case cmd of
         Right (Left EAbandon) -> do iPrintError ""; ifail "Abandoned"
         _ -> return ()

       (d, prev', st, done, prf', env', res) <-
         idrisCatch
           (case cmd of
              Left err -> do
                msg <- fmap (Left . Msg . show) (formatMessage err)
                return (False, prev, e, False, prf, env, msg)
              Right (Left cmd') ->
                case cmd' of
                  EQED -> do hs <- lifte e get_holes
                             unless (null hs) $ ifail "Incomplete proof"
                             iputStrLn "Proof completed!"
                             return (False, prev, e, True, prf, env, Right $ iPrintResult "")
                  EUndo -> do (prf', env', st', prev') <- undoElab prf env e prev
                              return (True, prev', st', False, prf', env', Right $ iPrintResult "")
                  EAbandon ->
                    error "the impossible happened - should have been matched on outer scope"
                  EProofState -> return (True, prev, e, False, prf, env, Right $ iPrintResult "")
                  EProofTerm ->
                    do tm <- lifte e get_term
                       return (False, prev, e, False, prf, env, Right $ iRenderResult (text "TT:" <+> pprintTT [] tm))
                  EEval tm -> do (d', st', done, prf', go) <- evalTerm e prf tm
                                 return (d', prev, st', done, prf', env, go)
                  ECheck (PRef _ _ n) ->
                    do (d', st', done, prf', go) <- checkNameType e prf n
                       return (d', prev, st', done, prf', env, go)
                  ECheck tm -> do (d', st', done, prf', go) <- checkType e prf tm
                                  return (d', prev, st', done, prf', env, go)
                  ESearch ty -> do (d', st', done, prf', go) <- search e prf ty
                                   return (d', prev, st', done, prf', env, go)
                  EDocStr d -> do (d', st', done, prf', go) <- docStr e prf d
                                  return (d', prev, st', done, prf', env, go)
              Right (Right cmd') ->
                case cmd' of
                  DoLetP  {} -> ifail "Pattern-matching let not supported here"
                  DoRewrite  {} -> ifail "Pattern-matching do-rewrite not supported here"
                  DoBindP {} -> ifail "Pattern-matching <- not supported here"
                  DoLet fc rig i ifc Placeholder expr ->
                    do (tm, ty) <- elabVal (recinfo proverfc) ERHS (inLets ist env expr)
                       ctxt <- getContext
                       let tm' = normaliseAll ctxt [] tm
                           ty' = normaliseAll ctxt [] ty
                       return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult ""))
                  DoLet fc rig i ifc ty expr ->
                    do (tm, ty) <- elabVal (recinfo proverfc) ERHS
                                     (PApp NoFC (PRef NoFC [] (sUN "the"))
                                                [ pexp (inLets ist env ty)
                                                , pexp (inLets ist env expr)
                                                ])
                       ctxt <- getContext
                       let tm' = normaliseAll ctxt [] tm
                           ty' = normaliseAll ctxt [] ty
                       return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult ""))
                  DoBind fc i ifc expr ->
                    do (tm, ty) <- elabVal (recinfo proverfc) ERHS (inLets ist env expr)
                       (_, e') <- elabStep e saveState -- enable :undo
                       (res, e'') <- elabStep e' $
                                       runElabAction info ist NoFC [] tm ["Shell"]
                       ctxt <- getContext
                       (v, vty) <- tclift $ check ctxt [] (forget res)
                       let v'   = normaliseAll ctxt [] v
                           vty' = normaliseAll ctxt [] vty
                       return (True, BothStep:prev, e'', False, prf ++ [step], (i, vty', v') : env, Right (iPrintResult ""))
                  DoExp fc expr ->
                    do (tm, ty) <- elabVal (recinfo proverfc) ERHS (inLets ist env expr)
                       -- TODO: call elaborator with Elab () as goal here
                       (_, e') <- elabStep e saveState -- enable :undo
                       (_, e'') <- elabStep e' $
                                     runElabAction info ist NoFC [] tm ["Shell"]
                       return (True, ElabStep:prev, e'', False, prf ++ [step], env, Right (iPrintResult "")))
           (\err -> return (False, prev, e, False, prf, env, Left err))
       idemodePutSExp "write-proof-state" (prf', length prf')
       case res of
         Left err -> do ist <- getIState
                        iRenderError $ pprintErr ist err
                        elabloop info fn d prompt prf' st prev' h' env'
         Right ok ->
           if done then do (tm, _) <- elabStep st get_term
                           return (tm, prf')
                   else runWithInterrupt e ok
                           (elabloop info fn d prompt prf' st prev' h' env')
                           (elabloop info fn d prompt prf e prev h' env)

  where
    -- A bit of a hack: wrap the value up in a let binding, which will
    -- normalise away. It would be better to figure out how to call
    -- the elaborator with a custom environment here to avoid the
    -- delab step.
    inLets :: IState -> [(Name, Type, Term)] -> PTerm -> PTerm
    inLets ist lets tm = foldr (\(n, ty, v) b -> PLet NoFC RigW n NoFC (delab ist ty) (delab ist v) b) tm (reverse lets)



ploop :: Name -> Bool -> String -> [String] -> ElabState EState -> Maybe History -> Idris (Term, [String])
ploop fn d prompt prf e h
    = do i <- getIState
         let autoSolve = opt_autoSolve (idris_options i)
         when d $ dumpState i False [] (proof e)
         (x, h') <-
           case idris_outputmode i of
             RawOutput _ ->
               runInputT (proverSettings e) $
                 -- Manually track the history so that we can use the proof state
                 do case h of
                      Just history -> putHistory history
                      Nothing -> return ()
                    l <- handleInterrupt (return $ Just "") $ withInterrupt $ getInputLine (prompt ++ "> ")
                    h' <- getHistory
                    return (l, Just h')
             IdeMode _ handle ->
               do isetPrompt prompt
                  i <- receiveInput handle e
                  return (i, h)
         (cmd, step) <- case x of
            Nothing -> do iPrintError ""; ifail "Abandoned"
            Just input -> return (parseTactic i input, input)
         case cmd of
            Right Abandon -> do iPrintError ""; ifail "Abandoned"
            _ -> return ()
         (d, st, done, prf', res) <- idrisCatch
           (case cmd of
              Left err -> do
                msg <- fmap (Left . Msg . show) (formatMessage err)
                return (False, e, False, prf, msg)
              Right Undo -> do (_, st) <- elabStep e loadState
                               return (True, st, False, init prf, Right $ iPrintResult "")
              Right ProofState -> return (True, e, False, prf, Right $ iPrintResult "")
              Right ProofTerm -> do tm <- lifte e get_term
                                    iputStrLn $ "TT: " ++ show tm ++ "\n"
                                    return (False, e, False, prf, Right $ iPrintResult "")
              Right Qed -> do hs <- lifte e get_holes
                              unless (null hs) $ ifail "Incomplete proof"
                              iputStrLn "Proof completed!"
                              return (False, e, True, prf, Right $ iPrintResult "")
              Right (TCheck (PRef _ _ n)) -> checkNameType e prf n
              Right (TCheck t) -> checkType e prf t
              Right (TEval t)  -> evalTerm e prf t
              Right (TDocStr x) -> docStr e prf x
              Right (TSearch t) -> search e prf t
              Right tac ->
                do (_, e) <- elabStep e saveState
                   (_, st) <- elabStep e (runTac autoSolve i (Just proverFC) fn tac)
                   return (True, st, False, prf ++ [step], Right $ iPrintResult ""))
           (\err -> return (False, e, False, prf, Left err))
         idemodePutSExp "write-proof-state" (prf', length prf')
         case res of
           Left err -> do ist <- getIState
                          iRenderError $ pprintErr ist err
                          ploop fn d prompt prf' st h'
           Right ok ->
             if done then do (tm, _) <- elabStep st get_term
                             return (tm, prf')
                     else runWithInterrupt e ok
                             (ploop fn d prompt prf' st h')
                             (ploop fn d prompt prf e h')


envCtxt env ctxt = foldl (\c (n, _, b) -> addTyDecl n Bound (binderTy b) c) ctxt env

checkNameType :: ElabState EState -> [String] -> Name -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
checkNameType e prf n = do
    ctxt <- getContext
    ist <- getIState
    imp <- impShow
    idrisCatch (do
        let OK env = envAtFocus (proof e)
            ctxt'  = envCtxt env ctxt
            bnd    = map (\x -> (fstEnv x, False)) env
            ist'   = ist { tt_ctxt = ctxt' }
        putIState ist'
        -- Unlike the REPL, metavars have no special treatment, to
        -- make it easier to see how to prove with them.
        let action = case lookupNames n ctxt' of
                       [] -> iPrintError $ "No such variable " ++ show n
                       ts -> iPrintFunTypes bnd n (map (\n -> (n, pprintDelabTy ist' n)) ts)
        putIState ist
        return (False, e, False, prf, Right action))
      (\err -> do putIState ist ; ierror err)

checkType :: ElabState EState -> [String] -> PTerm -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
checkType e prf t = do
    ist <- getIState
    ctxt <- getContext
    idrisCatch (do
        let OK env = envAtFocus (proof e)
            ctxt'  = envCtxt env ctxt
        putIState ist { tt_ctxt = ctxt' }
        (tm, ty) <- elabVal (recinfo proverfc) ERHS t
        let ppo = ppOptionIst ist
            infixes = idris_infixes ist
            action = case tm of
              TType _ ->
                iPrintTermWithType (prettyImp ppo (PType emptyFC)) type1Doc
              _ -> let bnd = map (\x -> (fstEnv x, False)) env in
                   iPrintTermWithType (pprintPTerm ppo bnd [] infixes (delab ist tm))
                                       (pprintPTerm ppo bnd [] infixes (delab ist ty))
        putIState ist
        return (False, e, False, prf, Right action))
      (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)

proverFC = FC "(prover shell)" (0, 0) (0, 0)

evalTerm :: ElabState EState -> [String] -> PTerm -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
evalTerm e prf t = withErrorReflection $
    do ctxt <- getContext
       ist <- getIState
       idrisCatch (do
         let OK env = envAtFocus (proof e)
             ctxt'  = envCtxt env ctxt
             ist'   = ist { tt_ctxt = ctxt' }
             bnd    = map (\x -> (fstEnv x, False)) env
         putIState ist'
         (tm, ty) <- elabVal (recinfo proverfc) ERHS t
         let tm'     = force (normaliseAll ctxt' env tm)
             ty'     = force (normaliseAll ctxt' env ty)
             ppo     = ppOption (idris_options ist')
             infixes = idris_infixes ist
             tmDoc   = pprintPTerm ppo bnd [] infixes (delab ist' tm')
             tyDoc   = pprintPTerm ppo bnd [] infixes (delab ist' ty')
             action  = iPrintTermWithType tmDoc tyDoc
         putIState ist
         return (False, e, False, prf, Right action))
        (\err -> do putIState ist ; ierror err)

docStr :: ElabState EState -> [String] -> Either Name Const -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
docStr e prf (Left n) = do ist <- getIState
                           idrisCatch (case lookupCtxtName n (idris_docstrings ist) of
                                         [] -> return (False, e, False, prf,
                                                       Left . Msg $ "No documentation for " ++ show n)
                                         ns -> do toShow <- mapM (showDoc ist) ns
                                                  return (False,  e, False, prf,
                                                          Right $ iRenderResult (vsep toShow)))
                                      (\err -> do putIState ist ; ierror err)
         where showDoc ist (n, d) = do doc <- getDocs n FullDocs
                                       return $ pprintDocs ist doc
docStr e prf (Right c) = do ist <- getIState
                            return (False, e, False, prf, Right . iRenderResult $ pprintConstDocs ist c (constDocs c))
search e prf t = return (False, e, False, prf, Right $ searchByType [] t)