An interactive Elab shell

This mirrors the interactive prover, but it uses Elab tactics instead of
the old built-in tactic language.

docs/reference/elaborator-reflection.rst

@@ -70,6 +70,14 @@ We can generate identity functions at any concrete type using the same script:
     idString : String -> String
     idString = %runElab mkId
 
+Interactively Building Elab Scripts
+===================================
+
+To build an ``Elab`` script interactively, use the ``:elab`` command at the REPL.
+It takes the name of a metavariable as an argument.
+The interface is largely the same as in Idris's interactive prover, except all meta-commands start with colon.
+For example, use ``:qed`` instead of ``qed``, ``:abandon`` instead of ``abandon``, and ``:undo`` instead of ``undo``.
+
 
 Failure
 =======

src/Idris/AbsSyntaxTree.hs

@@ -209,7 +209,7 @@ data IState = IState {
     idris_cgflags :: [(Codegen, String)],
     idris_hdrs :: [(Codegen, String)],
     idris_imported :: [(FilePath, Bool)], -- ^ Imported ibc file names, whether public
-    proof_list :: [(Name, [String])],
+    proof_list :: [(Name, (Bool, [String]))],
     errSpan :: Maybe FC,
     parserWarnings :: [(FC, Err)],
     lastParse :: Maybe Name,
@@ -377,7 +377,7 @@ data Command = Quit
              | Execute PTerm
              | ExecVal PTerm
              | Metavars
-             | Prove Name
+             | Prove Bool Name -- ^ If false, use prover, if true, use elab shell
              | AddProof (Maybe Name)
              | RmProof Name
              | ShowProof Name
@@ -486,6 +486,11 @@ data Opt = Filename String
          | UseConsoleWidth ConsoleWidth
     deriving (Show, Eq)
 
+data ElabShellCmd = EQED | EAbandon | EUndo | EProofState | EProofTerm
+                  | EEval PTerm | ECheck PTerm | ESearch PTerm
+                  | EDocStr (Either Name Const)
+  deriving (Show, Eq)
+
 -- Parsed declarations
 
 data Fixity = Infixl { prec :: Int }

src/Idris/Elab/Term.hs

@@ -1697,10 +1697,10 @@ case_ ind autoSolve ist fn tm = do
   when autoSolve solveAll
 
 
-runTactical :: IState -> FC -> Env -> Term -> [String] -> ElabD ()
+runTactical :: IState -> FC -> Env -> Term -> [String] -> ElabD Term
 runTactical ist fc env tm ns = do tm' <- eval tm
                                   runTacTm tm'
-                                  return ()
+
   where
     eval tm = do ctxt <- get_context
                  return $ normaliseAll ctxt env (finalise tm)

src/Idris/Elab/Value.hs

@@ -50,7 +50,7 @@ import Data.List.Split (splitOn)
 
 import Util.Pretty(pretty, text)
 
--- Elaborate a value, returning any new bindings created (this will only
+-- | Elaborate a value, returning any new bindings created (this will only
 -- happen if elaborating as a pattern clause)
 elabValBind :: ElabInfo -> ElabMode -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])
 elabValBind info aspat norm tm_in
@@ -116,7 +116,7 @@ elabDocTerms info str = do typechecked <- Traversable.mapM decorate str
                                             else Checked tm
           | otherwise                   = Unchecked
 
--- Try running the term directly (as IO ()), then printing it as an Integer
+-- | Try running the term directly (as IO ()), then printing it as an Integer
 -- (as a default numeric tye), then printing it as any Showable thing
 elabExec :: FC -> PTerm -> PTerm
 elabExec fc tm = runtm (PAlternative FirstSuccess

src/Idris/ParseExpr.hs

@@ -1375,10 +1375,10 @@ tactics =
   , noArgs ["instance"] TCInstance
   , noArgs ["solve"] Solve
   , noArgs ["attack"] Attack
-  , noArgs ["state"] ProofState
-  , noArgs ["term"] ProofTerm
-  , noArgs ["undo"] Undo
-  , noArgs ["qed"] Qed
+  , noArgs ["state", ":state"] ProofState
+  , noArgs ["term", ":term"] ProofTerm
+  , noArgs ["undo", ":undo"] Undo
+  , noArgs ["qed", ":qed"] Qed
   , noArgs ["abandon", ":q"] Abandon
   , noArgs ["skip"] Skip
   , noArgs ["sourceLocation"] SourceFC

src/Idris/Parser.hs

@@ -62,6 +62,7 @@ import Data.List
 import Data.Monoid
 import Data.Char
 import Data.Ord
+import Data.Foldable (asum)
 import Data.Generics.Uniplate.Data (descendM)
 import qualified Data.Map as M
 import qualified Data.HashSet as HS
@@ -1238,6 +1239,30 @@ parseConst st = runparser (fmap fst constant) st "(input)"
 parseTactic :: IState -> String -> Result PTactic
 parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
 
+{- | Parses a do-step from input (used in the elab shell) -}
+parseElabShellStep :: IState -> String -> Result (Either ElabShellCmd PDo)
+parseElabShellStep ist = runparser (fmap Right (do_ defaultSyntax) <|> fmap Left elabShellCmd) ist "(input)"
+  where elabShellCmd = char ':' >>
+                       (reserved "qed"     >> pure EQED       ) <|>
+                       (reserved "abandon" >> pure EAbandon   ) <|>
+                       (reserved "undo"    >> pure EUndo      ) <|>
+                       (reserved "state"   >> pure EProofState) <|>
+                       (reserved "term"    >> pure EProofTerm ) <|>
+                       (expressionTactic ["e", "eval"] EEval ) <|>
+                       (expressionTactic ["t", "type"] ECheck) <|>
+                       (expressionTactic ["search"] ESearch   ) <|>
+                       (do reserved "doc"
+                           doc <- (Right . fst <$> constant) <|> (Left . fst <$> fnName)
+                           eof
+                           return (EDocStr doc))
+                       <?> "elab command"
+        expressionTactic cmds tactic =
+           do asum (map reserved cmds)
+              t <- spaced (expr defaultSyntax)
+              i <- get
+              return $ tactic (desugar defaultSyntax i t)
+        spaced parser = indentPropHolds gtProp *> parser
+
 -- | Parse module header and imports
 parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Delta)
 parseImports fname input

src/Idris/Prover.hs

@@ -1,5 +1,5 @@
 {-# LANGUAGE PatternGuards #-}
-module Idris.Prover where
+module Idris.Prover (prover, showProof, showRunElab) where
 
 import Idris.Core.Elaborate hiding (Tactic(..))
 import Idris.Core.TT
@@ -35,13 +35,14 @@ import Control.DeepSeq
 import Util.Pretty
 import Debug.Trace
 
-prover :: Bool -> Name -> Idris ()
-prover lit x =
+-- | Launch the proof shell
+prover :: Bool -> Bool -> Name -> Idris ()
+prover mode lit x =
            do ctxt <- getContext
               i <- getIState
               case lookupTy x ctxt of
                   [t] -> if elem x (map fst (idris_metavars i))
-                               then prove (idris_optimisation i) ctxt lit x t
+                               then prove mode (idris_optimisation i) ctxt lit x t
                                else ifail $ show x ++ " is not a metavariable"
                   _ -> fail "No such metavariable"
 
@@ -53,6 +54,15 @@ showProof lit n ps
   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
 
@@ -64,18 +74,24 @@ assumptionNames e
         names ((MN _ _, _) : bs) = names bs
         names ((n, _) : bs) = show n : names bs
 
-prove :: Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()
-prove opt ctxt lit n ty
+prove :: Bool -> Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()
+prove mode opt ctxt lit n ty
     = do ps <- fmap (\ist -> initElaborator n ctxt (idris_datatypes ist) ty) getIState
          idemodePutSExp "start-proof-mode" n
-         (tm, prf) <- ploop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) Nothing
+         (tm, prf) <-
+            if mode
+              then elabloop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) [] Nothing []
+              else ploop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) Nothing
          iLOG $ "Adding " ++ show tm
          i <- getIState
+         let shower = if mode
+                         then showRunElab
+                         else showProof
          case idris_outputmode i of
-           IdeMode _ _ -> idemodePutSExp "end-proof-mode" (n, showProof lit n prf)
-           _            -> iputStrLn $ showProof lit n prf
+           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, prf) : proofs })
+         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 (fileFC "proof") id [] tm
@@ -117,16 +133,17 @@ elabStep st e = case runStateT eCheck st of
                                   return res
                          ((_,_,_,_,e,_,_):_) -> lift $ Error e
 
-dumpState :: IState -> ProofState -> Idris ()
-dumpState ist ps | [] <- holes ps =
+dumpState :: IState -> [(Name, Type, Term)] -> ProofState -> Idris ()
+dumpState ist menv ps | [] <- holes ps =
   do let nm = thname ps
      rendered <- iRender $ prettyName True False [] nm <> colon <+> text "No more goals."
      iputGoal rendered
-dumpState ist ps | (h : hs) <- holes ps = do
+dumpState ist menv ps | (h : hs) <- holes ps = do
   let OK ty  = goalAtFocus ps
   let OK env = envAtFocus ps
   let state = prettyOtherGoals hs <> line <>
               prettyAssumptions env <> line <>
+              prettyMetaValues (reverse menv) <>
               prettyGoal (zip (assumptionNames env) (repeat False)) ty
   rendered <- iRender state
   iputGoal rendered
@@ -156,6 +173,21 @@ dumpState ist ps | (h : hs) <- holes ps = do
       line <> bindingOf n False <+> colon <+>
       align (tPretty bnd (binderTy b)) <> prettyPs ((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
+
     prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v
     prettyG bnd b = tPretty bnd $ binderTy b
 
@@ -208,11 +240,141 @@ receiveInput h e =
        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)
+
+elabloop :: Name -> Bool -> String -> [String] -> ElabState EState -> [ElabShellHistory] -> Maybe History -> [(Name, Type, Term)] -> Idris (Term, [String])
+elabloop fn d prompt prf e prev h env
+  = do ist <- getIState
+       when d $ dumpState ist 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 <- 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
+         Success (Left EAbandon) -> do iPrintError ""; ifail "Abandoned"
+         _ -> return ()
+
+       (d, prev', st, done, prf', env', res) <-
+         idrisCatch
+           (case cmd of
+              Failure err ->
+                return (False, prev, e, False, prf, env, Left . Msg . show . fixColour (idris_colourRepl ist) $ err)
+              Success (Left cmd') ->
+                case cmd' of
+                  EQED -> do hs <- lifte e get_holes
+                             when (not (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)
+              Success (Right cmd') ->
+                case cmd' of
+                  DoLetP _ _ _ -> ifail "Pattern-matching let not supported here"
+                  DoBindP _ _ _ _ -> ifail "Pattern-matching <- not supported here"
+                  DoLet fc i ifc Placeholder expr ->
+                    do (tm, ty) <- elabVal recinfo 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 i ifc ty expr ->
+                    do (tm, ty) <- elabVal recinfo 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 ERHS (inLets ist env expr)
+                       (_, e') <- elabStep e saveState -- enable :undo
+                       (res, e'') <- elabStep e' $
+                                       runTactical 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 ERHS (inLets ist env expr)
+                       -- TODO: call elaborator with Elab () as goal here
+                       (_, e') <- elabStep e saveState -- enable :undo
+                       (_, e'') <- elabStep e' $
+                                     runTactical 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 fn d prompt prf' st prev' h' env'
+         Right ok ->
+           if done then do (tm, _) <- elabStep st get_term
+                           return (tm, prf')
+                   else do ok
+                           elabloop fn d prompt prf' st 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 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 (proof e)
+         when d $ dumpState i [] (proof e)
          (x, h') <-
            case idris_outputmode i of
              RawOutput _ ->
@@ -247,11 +409,11 @@ ploop fn d prompt prf e h
                                 when (not (null hs)) $ ifail "Incomplete proof"
                                 iputStrLn "Proof completed!"
                                 return (False, e, True, prf, Right $ iPrintResult "")
-              Success (TCheck (PRef _ n)) -> checkNameType n
-              Success (TCheck t) -> checkType t
-              Success (TEval t)  -> evalTerm t e
-              Success (TDocStr x) -> docStr x
-              Success (TSearch t) -> search t
+              Success (TCheck (PRef _ n)) -> checkNameType e prf n
+              Success (TCheck t) -> checkType e prf t
+              Success (TEval t)  -> evalTerm e prf t
+              Success (TDocStr x) -> docStr e prf x
+              Success (TSearch t) -> search e prf t
               Success tac ->
                 do (_, e) <- elabStep e saveState
                    (_, st) <- elabStep e (runTac autoSolve i (Just proverFC) fn tac)
@@ -267,80 +429,87 @@ ploop fn d prompt prf e h
                              return (tm, prf')
                      else do ok
                              ploop fn d prompt prf' st h'
-  where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env
-        checkNameType n = do
-          ctxt <- getContext
-          ist <- getIState
-          imp <- impShow
-          idrisCatch (do
-              let OK env = envAtFocus (proof e)
-                  ctxt'  = envCtxt env ctxt
-                  bnd    = map (\x -> (fst 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 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 ERHS t
-              let ppo = ppOptionIst ist
-                  ty'     = normaliseC ctxt [] ty
-                  infixes = idris_infixes ist
-                  action = case tm of
-                    TType _ ->
-                      iPrintTermWithType (prettyImp ppo (PType emptyFC)) type1Doc
-                    _ -> let bnd = map (\x -> (fst 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)
+envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env
 
-        evalTerm t e = 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 -> (fst x, False)) env
-               putIState ist'
-               (tm, ty) <- elabVal recinfo 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 :: Either Name Const -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-        docStr (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 (Right c) = do ist <- getIState
-                              return (False, e, False, prf, Right . iRenderResult $ pprintConstDocs ist c (constDocs c))
-        search t = return (False, e, False, prf, Right $ searchByType [] t)
+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 -> (fst 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 ERHS t
+        let ppo = ppOptionIst ist
+            ty'     = normaliseC ctxt [] ty
+            infixes = idris_infixes ist
+            action = case tm of
+              TType _ ->
+                iPrintTermWithType (prettyImp ppo (PType emptyFC)) type1Doc
+              _ -> let bnd = map (\x -> (fst 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 -> (fst x, False)) env
+         putIState ist'
+         (tm, ty) <- elabVal recinfo 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)

src/Idris/REPL.hs

@@ -296,9 +296,9 @@ runIdeModeCommand h id orig fn mods (IdeMode.Interpret cmd) =
      i <- getIState
      case parseCmd i "(input)" cmd of
        Failure err -> iPrintError $ show (fixColour False err)
-       Success (Right (Prove n')) ->
+       Success (Right (Prove mode n')) ->
          idrisCatch
-           (do process fn (Prove n')
+           (do process fn (Prove mode n')
                isetPrompt (mkPrompt mods)
                case idris_outputmode i of
                  IdeMode n h -> -- signal completion of proof to ide
@@ -1094,16 +1094,20 @@ process fn' (AddProof prf)
        n' <- case prf of
                 Nothing -> case proofs of
                              [] -> ifail "No proof to add"
-                             ((x, p) : _) -> return x
+                             ((x, _) : _) -> return x
                 Just nm -> return nm
        n <- resolveProof n'
        case lookup n proofs of
             Nothing -> iputStrLn "No proof to add"
-            Just p  -> do let prog' = insertScript (showProof (lit fn) n p) ls
-                          runIO $ writeSource fn (unlines prog')
-                          removeProof n
-                          iputStrLn $ "Added proof " ++ show n
-                          where ls = (lines prog)
+            Just (mode, prf) ->
+              do let script = if mode
+                                 then showRunElab (lit fn) n prf
+                                 else showProof (lit fn) n prf
+                 let prog' = insertScript script ls
+                 runIO $ writeSource fn (unlines prog')
+                 removeProof n
+                 iputStrLn $ "Added proof " ++ show n
+             where ls = (lines prog)
 
 process fn (ShowProof n')
   = do i <- getIState
@@ -1111,9 +1115,11 @@ process fn (ShowProof n')
        let proofs = proof_list i
        case lookup n proofs of
             Nothing -> iPrintError "No proof to show"
-            Just p  -> iPrintResult $ showProof False n p
+            Just (m, p)  -> iPrintResult $ if m
+                                             then showRunElab False n p
+                                             else showProof False n p
 
-process fn (Prove n')
+process fn (Prove mode n')
      = do ctxt <- getContext
           ist <- getIState
           let ns = lookupNames n' ctxt
@@ -1123,7 +1129,7 @@ process fn (Prove n')
               [(n, (_,_,False))] -> return n
               [(_, (_,_,True))]  -> ierror (Msg $ "Declarations not solvable using prover")
               ns -> ierror (CantResolveAlts (map fst ns))
-          prover (lit fn) n
+          prover mode (lit fn) n
           -- recheck totality
           i <- getIState
           totcheck (fileFC "(input)", n)

src/Idris/REPLParser.hs

@@ -63,7 +63,9 @@ parserCommandsForHelp =
   , noArgCmd ["e", "edit"] Edit "Edit current file using $EDITOR or $VISUAL"
   , noArgCmd ["m", "metavars"] Metavars "Show remaining proof obligations (metavariables)"
   , (["p", "prove"], MetaVarArg, "Prove a metavariable"
-    , nameArg Prove)
+    , nameArg (Prove False))
+  , (["elab"], MetaVarArg, "Build a metavariable using the elaboration shell"
+    , nameArg (Prove True))
   , (["a", "addproof"], NameArg, "Add proof to source file", cmd_addproof)
   , (["rmproof"], NameArg, "Remove proof from proof stack"
     , nameArg RmProof)