8ed6000 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #2358 from david-christiansen/wip/tactical

8ed6000David Christiansen11 years ago

CHANGELOG+2

compare with master

unifiedsplit

@@ -12,6 +12,8 @@ New in 0.9.19:

12* Compiler output shows applications of >>= in do-notation

13* fromInteger i where i is an integer constant is now shown just as i in

14 compiler output

15+* An interactive shell, similar to the prover, for running reflected elaborator

16+ actions. Access it with :elab from the REPL.

16New in 0.9.18:

18New in 0.9.18:

17--------------

19--------------

docs/reference/elaborator-reflection.rst+8

@@ -70,6 +70,14 @@ We can generate identity functions at any concrete type using the same script:

70 idString : String -> String

71 idString = %runElab mkId

73+Interactively Building Elab Scripts

74+===================================

75+

76+To build an ``Elab`` script interactively, use the ``:elab`` command at the REPL.

77+It takes the name of a metavariable as an argument.

78+The interface is largely the same as in Idris's interactive prover, except all meta-commands start with colon.

79+For example, use ``:qed`` instead of ``qed``, ``:abandon`` instead of ``abandon``, and ``:undo`` instead of ``undo``.

80+

74Failure

82Failure

75=======

83=======

libs/prelude/Language/Reflection/Elab.idr+9

@@ -88,6 +88,7 @@ data Elab : Type -> Type where

88 prim__Check : Raw -> Elab (TT, TT)

90 prim__SourceLocation : Elab SourceLocation

91+ prim__Namespace : Elab (List String)

92 prim__Forget : TT -> Elab Raw

93 prim__Forget : TT -> Elab Raw

@@ -280,6 +281,14 @@ namespace Tactics

280 fill (quote loc)

281 fill (quote loc)

281 solve

282 solve

282

283

284+ ||| Get the current namespace at the point of tactic execution. This

285+ ||| allows scripts to define top-level names conveniently.

286+ |||

287+ ||| The namespace is represented as a reverse-order list of strings,

288+ ||| just as in the representation of names.

289+ currentNamespace : Elab (List String)

290+ currentNamespace = prim__Namespace

291+

283 ||| Attempt to rewrite the goal using an equality.

292 ||| Attempt to rewrite the goal using an equality.

284 |||

293 |||

285 ||| The tactic searches the goal for applicable subterms, and

294 ||| The tactic searches the goal for applicable subterms, and

src/Idris/AbsSyntax.hs+5−5

@@ -1040,7 +1040,7 @@ expandParams dec ps ns infs tm = en tm

1040 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)

1041 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)

1042 en (PIfThenElse fc c t f) = PIfThenElse fc (en c) (en t) (en f)

1043− en (PRunElab fc tm) = PRunElab fc (en tm)

1043+ en (PRunElab fc tm ns) = PRunElab fc (en tm) ns

1044 en t = t

1045

1046 nselem x [] = False

@@ -1506,7 +1506,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1506 imps top env (PHidden tm) = imps False env tm

1507 imps top env (PUnifyLog tm) = imps False env tm

1508 imps top env (PNoImplicits tm) = imps False env tm

1509− imps top env (PRunElab fc tm) = imps False env tm

1509+ imps top env (PRunElab fc tm ns) = imps False env tm

1510 imps top env _ = return ()

1511

1512 pibind using [] sc = sc

@@ -1631,7 +1631,7 @@ addImpl' inpat env infns imp_meths ist ptm

1631 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)

1632 (fmap (ai True env ds) g)

1633 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)

1634− ai qq env ds (PRunElab fc tm) = PRunElab fc (ai False env ds tm)

1634+ ai qq env ds (PRunElab fc tm ns) = PRunElab fc (ai False env ds tm) ns

1635 ai qq env ds tm = tm

1636

1637 handleErr (Left err) = PElabError err

@@ -2060,7 +2060,7 @@ substMatchShadow n shs tm t = sm shs t where

2060 sm xs (PHidden x) = PHidden (sm xs x)

2061 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)

2062 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)

2063− sm xs (PRunElab fc script) = PRunElab fc (sm xs script)

2063+ sm xs (PRunElab fc script ns) = PRunElab fc (sm xs script) ns

2064 sm xs x = x

2065

2066 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))

@@ -2189,5 +2189,5 @@ mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where

2189 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)

2190 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)

2191 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)

2192− mkUniq (PRunElab fc ts) = liftM (PRunElab fc ) (mkUniq ts)

2192+ mkUniq (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq ts)

2193 mkUniq t = return t

src/Idris/AbsSyntaxTree.hs+9−4

@@ -209,7 +209,7 @@ data IState = IState {

209 idris_cgflags :: [(Codegen, String)],

210 idris_hdrs :: [(Codegen, String)],

211 idris_imported :: [(FilePath, Bool)], -- ^ Imported ibc file names, whether public

212− proof_list :: [(Name, [String])],

212+ proof_list :: [(Name, (Bool, [String]))],

213 errSpan :: Maybe FC,

214 parserWarnings :: [(FC, Err)],

215 lastParse :: Maybe Name,

@@ -377,7 +377,7 @@ data Command = Quit

377 | Execute PTerm

378 | ExecVal PTerm

379 | Metavars

380− | Prove Name

380+ | Prove Bool Name -- ^ If false, use prover, if true, use elab shell

381 | AddProof (Maybe Name)

382 | RmProof Name

383 | ShowProof Name

@@ -486,6 +486,11 @@ data Opt = Filename String

486 | UseConsoleWidth ConsoleWidth

487 deriving (Show, Eq)

488

489+data ElabShellCmd = EQED | EAbandon | EUndo | EProofState | EProofTerm

490+ | EEval PTerm | ECheck PTerm | ESearch PTerm

491+ | EDocStr (Either Name Const)

492+ deriving (Show, Eq)

493+

489-- Parsed declarations

494-- Parsed declarations

490

495

491data Fixity = Infixl { prec :: Int }

496data Fixity = Infixl { prec :: Int }

@@ -864,7 +869,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

864 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])

869 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])

865 | PUnquote PTerm -- ^ ~Term

870 | PUnquote PTerm -- ^ ~Term

866 | PQuoteName Name -- ^ `{n}

871 | PQuoteName Name -- ^ `{n}

867− | PRunElab FC PTerm -- ^ %runElab tm - New-style proof script

872+ | PRunElab FC PTerm [String] -- ^ %runElab tm - New-style proof script. Args are location, script, enclosing namespace.

868 deriving (Eq, Data, Typeable)

873 deriving (Eq, Data, Typeable)

869

874

870data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed

875data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed

@@ -1234,7 +1239,7 @@ initDSL = DSL (PRef f (sUN ">>="))

1234

1239

1235data Using = UImplicit Name PTerm

1240data Using = UImplicit Name PTerm

1236 | UConstraint Name [Name]

1241 | UConstraint Name [Name]

1237− deriving (Show, Eq)

1242+ deriving (Show, Eq, Data, Typeable)

1238{-!

1243{-!

1239deriving instance Binary Using

1244deriving instance Binary Using

1240deriving instance NFData Using

1245deriving instance NFData Using

src/Idris/DSL.hs+2−2

@@ -112,7 +112,7 @@ expandSugar dsl (PDoBlock ds)

112 block b _ = PElabError (Msg "Invalid statement in do block")

113

114expandSugar dsl (PIdiom fc e) = expandSugar dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e

115−expandSugar dsl (PRunElab fc tm) = PRunElab fc $ expandSugar dsl tm

115+expandSugar dsl (PRunElab fc tm ns) = PRunElab fc (expandSugar dsl tm) ns

116expandSugar dsl t = t

117

118-- | Replace DSL-bound variable in a term

@@ -198,7 +198,7 @@ debind b tm = let (tm', (bs, _)) = runState (db' tm) ([], 0) in

198 db' (PDPair fc p l t r) = do l' <- db' l

199 r' <- db' r

200 return (PDPair fc p l' t r')

201− db' (PRunElab fc t) = fmap (PRunElab fc) (db' t)

201+ db' (PRunElab fc t ns) = fmap (\tm -> PRunElab fc tm ns) (db' t)

202 db' t = return t

203

204 dbArg a = do t' <- db' (getTm a)

src/Idris/DeepSeq.hs+1−1

@@ -262,7 +262,7 @@ instance NFData PTerm where

262 rnf (PQuasiquote x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

263 rnf (PUnquote x1) = rnf x1 `seq` ()

264 rnf (PQuoteName x1) = rnf x1 `seq` ()

265− rnf (PRunElab x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

265+ rnf (PRunElab x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

266

267instance NFData PAltType where

268 rnf (ExactlyOne x1) = rnf x1 `seq` ()

src/Idris/Elab/Term.hs+14−10

@@ -16,7 +16,7 @@ import Idris.Core.TT

16import Idris.Core.Evaluate

17import Idris.Core.Unify

18import Idris.Core.ProofTerm (getProofTerm)

19−import Idris.Core.Typecheck (check, recheck, isType)

19+import Idris.Core.Typecheck (check, recheck, converts, isType)

20import Idris.Coverage (buildSCG, checkDeclTotality, genClauses, recoverableCoverage, validCoverageCase)

21import Idris.ErrReverse (errReverse)

22import Idris.ElabQuasiquote (extractUnquotes)

@@ -1136,7 +1136,7 @@ elab ist info emode opts fn tm

1136 delayElab 10 $ do focus h

1137 dotterm

1138 elab' ina fc t

1139− elab' ina fc (PRunElab fc' tm) =

1139+ elab' ina fc (PRunElab fc' tm ns) =

1140 do attack

1141 n <- getNameFrom (sMN 0 "tacticScript")

1142 n' <- getNameFrom (sMN 0 "tacticExpr")

@@ -1149,7 +1149,7 @@ elab ist info emode opts fn tm

1149 focus n

1150 elab' ina (Just fc') tm

1151 env <- get_env

1152− runTactical ist (maybe fc' id fc) env (P Bound n' Erased)

1152+ runTactical ist (maybe fc' id fc) env (P Bound n' Erased) ns

1153 solve

1154 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

1155

@@ -1697,10 +1697,10 @@ case_ ind autoSolve ist fn tm = do

1697 when autoSolve solveAll

1698

1699

1700−runTactical :: IState -> FC -> Env -> Term -> ElabD ()

1700+runTactical :: IState -> FC -> Env -> Term -> [String] -> ElabD Term

1701−runTactical ist fc env tm = do tm' <- eval tm

1701+runTactical ist fc env tm ns = do tm' <- eval tm

1702− runTacTm tm'

1702+ runTacTm tm'

1703− return ()

1703+

1704 where

1705 eval tm = do ctxt <- get_context

1706 return $ normaliseAll ctxt env (finalise tm)

@@ -1721,8 +1721,9 @@ runTactical ist fc env tm = do tm' <- eval tm

1721 let info = CaseInfo True True False -- TODO document and figure out

1722 clauses' <- forM clauses (\case

1723 RMkFunClause lhs rhs ->

1724− do lhs' <- fmap fst . lift $ check ctxt [] lhs

1724+ do (lhs', lty) <- lift $ check ctxt [] lhs

1725− rhs' <- fmap fst . lift $ check ctxt [] rhs

1725+ (rhs', rty) <- lift $ check ctxt [] rhs

1726+ lift $ converts ctxt [] lty rty

1726 return $ Right (lhs', rhs')

1727 return $ Right (lhs', rhs')

1727 RMkImpossibleClause lhs ->

1728 RMkImpossibleClause lhs ->

1728 do lhs' <- fmap fst . lift $ check ctxt [] lhs

1729 do lhs' <- fmap fst . lift $ check ctxt [] lhs

@@ -1812,6 +1813,9 @@ runTactical ist fc env tm = do tm' <- eval tm

1812 | n == tacN "prim__SourceLocation", [] <- args

1813 | n == tacN "prim__SourceLocation", [] <- args

1813 = fmap fst . checkClosed $

1814 = fmap fst . checkClosed $

1814 reflectFC fc

1815 reflectFC fc

1816+ | n == tacN "prim__Namespace", [] <- args

1817+ = fmap fst . checkClosed $

1818+ rawList (RConstant StrType) (map (RConstant . Str) ns)

1815 | n == tacN "prim__Env", [] <- args

1819 | n == tacN "prim__Env", [] <- args

1816 = do env <- get_env

1820 = do env <- get_env

1817 fmap fst . checkClosed $ reflectEnv env

1821 fmap fst . checkClosed $ reflectEnv env

@@ -1960,7 +1964,7 @@ runTactical ist fc env tm = do tm' <- eval tm

1960 datatypes <- get_datatypes

1964 datatypes <- get_datatypes

1961 env <- get_env

1965 env <- get_env

1962 (_, ES (p, aux') _ _) <-

1966 (_, ES (p, aux') _ _) <-

1963− lift $ runElab aux (runTactical ist fc [] script)

1967+ lift $ runElab aux (runTactical ist fc [] script ns)

1964 (newProof recH ctxt datatypes goalTT)

1968 (newProof recH ctxt datatypes goalTT)

1965 let tm_out = getProofTerm (pterm p)

1969 let tm_out = getProofTerm (pterm p)

1966 updateAux $ const aux'

1970 updateAux $ const aux'

src/Idris/Elab/Value.hs+2−2

@@ -50,7 +50,7 @@ import Data.List.Split (splitOn)

51import Util.Pretty(pretty, text)

53−-- Elaborate a value, returning any new bindings created (this will only

53+-- | Elaborate a value, returning any new bindings created (this will only

54-- happen if elaborating as a pattern clause)

55elabValBind :: ElabInfo -> ElabMode -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])

56elabValBind info aspat norm tm_in

@@ -116,7 +116,7 @@ elabDocTerms info str = do typechecked <- Traversable.mapM decorate str

116 else Checked tm

117 | otherwise = Unchecked

118

119−-- Try running the term directly (as IO ()), then printing it as an Integer

119+-- | Try running the term directly (as IO ()), then printing it as an Integer

120-- (as a default numeric tye), then printing it as any Showable thing

121elabExec :: FC -> PTerm -> PTerm

122elabExec fc tm = runtm (PAlternative FirstSuccess

src/Idris/ElabQuasiquote.hs+2−2

@@ -166,8 +166,8 @@ extractUnquotes n (PUnquote tm)

166 return (PRef (fileFC "(unquote)") n, [(n, tm)])

167 | otherwise = fmap (\(tm', ex) -> (PUnquote tm', ex)) $

168 extractUnquotes (n-1) tm

169−extractUnquotes n (PRunElab fc tm)

169+extractUnquotes n (PRunElab fc tm ns)

170− = fmap (\(tm', ex) -> (PRunElab fc tm', ex)) $ extractUnquotes n tm

170+ = fmap (\(tm', ex) -> (PRunElab fc tm' ns, ex)) $ extractUnquotes n tm

171extractUnquotes n x = return (x, []) -- no subterms!

172

173

src/Idris/Error.hs+1−1

@@ -150,4 +150,4 @@ warnDisamb ist (PUnquote tm) = warnDisamb ist tm

150warnDisamb ist (PQuoteName _) = return ()

151warnDisamb ist (PAs _ _ tm) = warnDisamb ist tm

152warnDisamb ist (PAppImpl tm _) = warnDisamb ist tm

153−warnDisamb ist (PRunElab _ tm) = warnDisamb ist tm

153+warnDisamb ist (PRunElab _ tm _) = warnDisamb ist tm

src/Idris/IBC.hs+6−4

@@ -1625,9 +1625,10 @@ instance Binary PTerm where

1625 put x2

1626 PUniverse x1 -> do putWord8 38

1627 put x1

1628− PRunElab x1 x2 -> do putWord8 39

1628+ PRunElab x1 x2 x3 -> do putWord8 39

1629− put x1

1629+ put x1

1630− put x2

1630+ put x2

1631+ put x3

1631 PAs x1 x2 x3 -> do putWord8 40

1632 PAs x1 x2 x3 -> do putWord8 40

1632 put x1

1633 put x1

1633 put x2

1634 put x2

@@ -1763,7 +1764,8 @@ instance Binary PTerm where

1763 return (PUniverse x1)

1764 return (PUniverse x1)

1764 39 -> do x1 <- get

1765 39 -> do x1 <- get

1765 x2 <- get

1766 x2 <- get

1767+ x3 <- get

1766− return (PRunElab x1 x2)

1768+ return (PRunElab x1 x2 x3)

1767 40 -> do x1 <- get

1769 40 -> do x1 <- get

1768 x2 <- get

1770 x2 <- get

1769 x3 <- get

1771 x3 <- get

src/Idris/IdrisDoc.hs+1−1

@@ -320,7 +320,7 @@ extractPTermNames (PCoerced p) = extract p

320extractPTermNames (PDisamb _ p) = extract p

321extractPTermNames (PUnifyLog p) = extract p

322extractPTermNames (PNoImplicits p) = extract p

323−extractPTermNames (PRunElab _ p) = extract p

323+extractPTermNames (PRunElab _ p _) = extract p

324extractPTermNames _ = []

325

326-- | Shorter name for extractPTermNames

src/Idris/ParseExpr.hs+5−5

@@ -510,7 +510,7 @@ runElab syn = do try (lchar '%' *> reserved "runElab")

510 fc <- getFC

511 tm <- simpleExpr syn

512 i <- get

513− return $ PRunElab fc tm

513+ return $ PRunElab fc tm (syn_namespace syn)

514 <?> "new-style tactics expression"

515

516{- | Parses a disambiguation expression

@@ -1375,10 +1375,10 @@ tactics =

1375 , noArgs ["instance"] TCInstance

1376 , noArgs ["solve"] Solve

1377 , noArgs ["attack"] Attack

1378− , noArgs ["state"] ProofState

1378+ , noArgs ["state", ":state"] ProofState

1379− , noArgs ["term"] ProofTerm

1379+ , noArgs ["term", ":term"] ProofTerm

1380− , noArgs ["undo"] Undo

1380+ , noArgs ["undo", ":undo"] Undo

1381− , noArgs ["qed"] Qed

1381+ , noArgs ["qed", ":qed"] Qed

1382 , noArgs ["abandon", ":q"] Abandon

1383 , noArgs ["skip"] Skip

1384 , noArgs ["sourceLocation"] SourceFC

src/Idris/Parser.hs+25

@@ -62,6 +62,7 @@ import Data.List

62import Data.Monoid

63import Data.Char

64import Data.Ord

65+import Data.Foldable (asum)

65import Data.Generics.Uniplate.Data (descendM)

66import Data.Generics.Uniplate.Data (descendM)

66import qualified Data.Map as M

67import qualified Data.Map as M

67import qualified Data.HashSet as HS

68import qualified Data.HashSet as HS

@@ -1238,6 +1239,30 @@ parseConst st = runparser (fmap fst constant) st "(input)"

1238parseTactic :: IState -> String -> Result PTactic

1239parseTactic :: IState -> String -> Result PTactic

1239parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"

1240parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"

1240

1241

1242+{- | Parses a do-step from input (used in the elab shell) -}

1243+parseElabShellStep :: IState -> String -> Result (Either ElabShellCmd PDo)

1244+parseElabShellStep ist = runparser (fmap Right (do_ defaultSyntax) <|> fmap Left elabShellCmd) ist "(input)"

1245+ where elabShellCmd = char ':' >>

1246+ (reserved "qed" >> pure EQED ) <|>

1247+ (reserved "abandon" >> pure EAbandon ) <|>

1248+ (reserved "undo" >> pure EUndo ) <|>

1249+ (reserved "state" >> pure EProofState) <|>

1250+ (reserved "term" >> pure EProofTerm ) <|>

1251+ (expressionTactic ["e", "eval"] EEval ) <|>

1252+ (expressionTactic ["t", "type"] ECheck) <|>

1253+ (expressionTactic ["search"] ESearch ) <|>

1254+ (do reserved "doc"

1255+ doc <- (Right . fst <$> constant) <|> (Left . fst <$> fnName)

1256+ eof

1257+ return (EDocStr doc))

1258+ <?> "elab command"

1259+ expressionTactic cmds tactic =

1260+ do asum (map reserved cmds)

1261+ t <- spaced (expr defaultSyntax)

1262+ i <- get

1263+ return $ tactic (desugar defaultSyntax i t)

1264+ spaced parser = indentPropHolds gtProp *> parser

1265+

1241-- | Parse module header and imports

1266-- | Parse module header and imports

1242parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Delta)

1267parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Delta)

1243parseImports fname input

1268parseImports fname input

src/Idris/Prover.hs+265−96

@@ -1,5 +1,5 @@

1{-# LANGUAGE PatternGuards #-}

2−module Idris.Prover where

2+module Idris.Prover (prover, showProof, showRunElab) where

4import Idris.Core.Elaborate hiding (Tactic(..))

5import Idris.Core.TT

@@ -35,13 +35,14 @@ import Control.DeepSeq

35import Util.Pretty

36import Debug.Trace

38+-- | Launch the proof shell

38−prover :: Bool -> Name -> Idris ()

39+prover :: Bool -> Bool -> Name -> Idris ()

39−prover lit x =

40+prover mode lit x =

40 do ctxt <- getContext

41 do ctxt <- getContext

41 i <- getIState

42 i <- getIState

42 case lookupTy x ctxt of

43 case lookupTy x ctxt of

43 [t] -> if elem x (map fst (idris_metavars i))

44 [t] -> if elem x (map fst (idris_metavars i))

44− then prove (idris_optimisation i) ctxt lit x t

45+ then prove mode (idris_optimisation i) ctxt lit x t

45 else ifail $ show x ++ " is not a metavariable"

46 else ifail $ show x ++ " is not a metavariable"

46 _ -> fail "No such metavariable"

47 _ -> fail "No such metavariable"

@@ -53,6 +54,15 @@ showProof lit n ps

53 where bird = if lit then "> " else ""

54 where bird = if lit then "> " else ""

54 break = "\n" ++ bird

55 break = "\n" ++ bird

57+showRunElab :: Bool -> Name -> [String] -> String

58+showRunElab lit n ps = birdify (displayS (renderPretty 1.0 80 doc) "")

59+ where doc = text (show n) <+> text "=" <+> text "%runElab" <+>

60+ enclose lparen rparen

61+ (text "do" <+> (align $ vsep (map text ps)))

62+ birdify = if lit

63+ then concatMap ("> " ++) . lines

64+ else id

65+

56proverSettings :: ElabState EState -> Settings Idris

66proverSettings :: ElabState EState -> Settings Idris

57proverSettings e = setComplete (proverCompletion (assumptionNames e)) defaultSettings

67proverSettings e = setComplete (proverCompletion (assumptionNames e)) defaultSettings

@@ -64,18 +74,24 @@ assumptionNames e

64 names ((MN _ _, _) : bs) = names bs

74 names ((MN _ _, _) : bs) = names bs

65 names ((n, _) : bs) = show n : names bs

75 names ((n, _) : bs) = show n : names bs

67−prove :: Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()

77+prove :: Bool -> Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()

68−prove opt ctxt lit n ty

78+prove mode opt ctxt lit n ty

69 = do ps <- fmap (\ist -> initElaborator n ctxt (idris_datatypes ist) ty) getIState

79 = do ps <- fmap (\ist -> initElaborator n ctxt (idris_datatypes ist) ty) getIState

70 idemodePutSExp "start-proof-mode" n

80 idemodePutSExp "start-proof-mode" n

81+ (tm, prf) <-

82+ if mode

83+ then elabloop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) [] Nothing []

71− (tm, prf) <- ploop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) Nothing

84+ else ploop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) Nothing

72 iLOG $ "Adding " ++ show tm

85 iLOG $ "Adding " ++ show tm

73 i <- getIState

86 i <- getIState

87+ let shower = if mode

88+ then showRunElab

89+ else showProof

74 case idris_outputmode i of

90 case idris_outputmode i of

75− IdeMode _ _ -> idemodePutSExp "end-proof-mode" (n, showProof lit n prf)

91+ IdeMode _ _ -> idemodePutSExp "end-proof-mode" (n, shower lit n prf)

76− _ -> iputStrLn $ showProof lit n prf

92+ _ -> iputStrLn $ shower lit n prf

77 let proofs = proof_list i

93 let proofs = proof_list i

78− putIState (i { proof_list = (n, prf) : proofs })

94+ putIState (i { proof_list = (n, (mode, prf)) : proofs })

79 let tree = simpleCase False (STerm Erased) False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]

95 let tree = simpleCase False (STerm Erased) False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]

80 logLvl 3 (show tree)

96 logLvl 3 (show tree)

81 (ptm, pty) <- recheckC (fileFC "proof") id [] tm

97 (ptm, pty) <- recheckC (fileFC "proof") id [] tm

@@ -117,16 +133,17 @@ elabStep st e = case runStateT eCheck st of

117 return res

133 return res

118 ((_,_,_,_,e,_,_):_) -> lift $ Error e

134 ((_,_,_,_,e,_,_):_) -> lift $ Error e

119

135

120−dumpState :: IState -> ProofState -> Idris ()

136+dumpState :: IState -> [(Name, Type, Term)] -> ProofState -> Idris ()

121−dumpState ist ps | [] <- holes ps =

137+dumpState ist menv ps | [] <- holes ps =

122 do let nm = thname ps

138 do let nm = thname ps

123 rendered <- iRender $ prettyName True False [] nm <> colon <+> text "No more goals."

139 rendered <- iRender $ prettyName True False [] nm <> colon <+> text "No more goals."

124 iputGoal rendered

140 iputGoal rendered

125−dumpState ist ps | (h : hs) <- holes ps = do

141+dumpState ist menv ps | (h : hs) <- holes ps = do

126 let OK ty = goalAtFocus ps

142 let OK ty = goalAtFocus ps

127 let OK env = envAtFocus ps

143 let OK env = envAtFocus ps

128 let state = prettyOtherGoals hs <> line <>

144 let state = prettyOtherGoals hs <> line <>

129 prettyAssumptions env <> line <>

145 prettyAssumptions env <> line <>

146+ prettyMetaValues (reverse menv) <>

130 prettyGoal (zip (assumptionNames env) (repeat False)) ty

147 prettyGoal (zip (assumptionNames env) (repeat False)) ty

131 rendered <- iRender state

148 rendered <- iRender state

132 iputGoal rendered

149 iputGoal rendered

@@ -156,6 +173,21 @@ dumpState ist ps | (h : hs) <- holes ps = do

156 line <> bindingOf n False <+> colon <+>

173 line <> bindingOf n False <+> colon <+>

157 align (tPretty bnd (binderTy b)) <> prettyPs ((n, False):bnd) bs

174 align (tPretty bnd (binderTy b)) <> prettyPs ((n, False):bnd) bs

158

175

176+ prettyMetaValues [] = empty

177+ prettyMetaValues mvs =

178+ text "---------- Meta-values: ----------" <$$>

179+ prettyMetaValues' [] mvs <> line <> line

180+ prettyMetaValues' _ [] = empty

181+ prettyMetaValues' bnd [mv] = ppMv bnd mv

182+ prettyMetaValues' bnd ((mv@(n, ty, tm)) : mvs) =

183+ ppMv bnd mv <$>

184+ prettyMetaValues' ((n, False):bnd) mvs

185+

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

187+ tPretty bnd ty <+> text "=" <+> tPretty bnd tm

188+

189+ kwd = annotate AnnKeyword . text

190+

159 prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v

191 prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v

160 prettyG bnd b = tPretty bnd $ binderTy b

192 prettyG bnd b = tPretty bnd $ binderTy b

161

193

@@ -208,11 +240,141 @@ receiveInput h e =

208 Just (IdeMode.DocsFor str _) -> return (Just (":doc " ++ str))

240 Just (IdeMode.DocsFor str _) -> return (Just (":doc " ++ str))

209 _ -> return Nothing

241 _ -> return Nothing

210

242

243+data ElabShellHistory = ElabStep | LetStep | BothStep

244+

245+undoStep :: [String] -> [(Name, Type, Term)] -> ElabState EState -> ElabShellHistory -> Idris ([String], [(Name, Type, Term)], ElabState EState)

246+undoStep prf env st ElabStep = do (_, st') <- elabStep st loadState

247+ return (init prf, env, st')

248+undoStep prf env st LetStep = return (init prf, tail env, st)

249+undoStep prf env st BothStep = do (_, st') <- elabStep st loadState

250+ return (init prf, tail env, st')

251+

252+undoElab :: [String] -> [(Name, Type, Term)] -> ElabState EState -> [ElabShellHistory] -> Idris ([String], [(Name, Type, Term)], ElabState EState, [ElabShellHistory])

253+undoElab prf env st [] = ifail "Nothing to undo"

254+undoElab prf env st (h:hs) = do (prf', env', st') <- undoStep prf env st h

255+ return (prf', env', st', hs)

256+

257+elabloop :: Name -> Bool -> String -> [String] -> ElabState EState -> [ElabShellHistory] -> Maybe History -> [(Name, Type, Term)] -> Idris (Term, [String])

258+elabloop fn d prompt prf e prev h env

259+ = do ist <- getIState

260+ when d $ dumpState ist env (proof e)

261+ (x, h') <-

262+ case idris_outputmode ist of

263+ RawOutput _ ->

264+ runInputT (proverSettings e) $

265+ do case h of

266+ Just history -> putHistory history

267+ Nothing -> return ()

268+ l <- getInputLine (prompt ++ "> ")

269+ h' <- getHistory

270+ return (l, Just h')

271+ IdeMode _ handle ->

272+ do isetPrompt prompt

273+ i <- receiveInput handle e

274+ return (i, h)

275+ (cmd, step) <- case x of

276+ Nothing -> do iPrintError "" ; ifail "Abandoned"

277+ Just input -> return (parseElabShellStep ist input, input)

278+

279+ -- if we're abandoning, it has to be outside the scope of the catch

280+ case cmd of

281+ Success (Left EAbandon) -> do iPrintError ""; ifail "Abandoned"

282+ _ -> return ()

283+

284+ (d, prev', st, done, prf', env', res) <-

285+ idrisCatch

286+ (case cmd of

287+ Failure err ->

288+ return (False, prev, e, False, prf, env, Left . Msg . show . fixColour (idris_colourRepl ist) $ err)

289+ Success (Left cmd') ->

290+ case cmd' of

291+ EQED -> do hs <- lifte e get_holes

292+ when (not (null hs)) $ ifail "Incomplete proof"

293+ iputStrLn "Proof completed!"

294+ return (False, prev, e, True, prf, env, Right $ iPrintResult "")

295+ EUndo -> do (prf', env', st', prev') <- undoElab prf env e prev

296+ return (True, prev', st', False, prf', env', Right $ iPrintResult "")

297+ EAbandon ->

298+ error "the impossible happened - should have been matched on outer scope"

299+ EProofState -> return (True, prev, e, False, prf, env, Right $ iPrintResult "")

300+ EProofTerm ->

301+ do tm <- lifte e get_term

302+ return (False, prev, e, False, prf, env, Right $ iRenderResult (text "TT:" <+> pprintTT [] tm))

303+ EEval tm -> do (d', st', done, prf', go) <- evalTerm e prf tm

304+ return (d', prev, st', done, prf', env, go)

305+ ECheck (PRef _ n) ->

306+ do (d', st', done, prf', go) <- checkNameType e prf n

307+ return (d', prev, st', done, prf', env, go)

308+ ECheck tm -> do (d', st', done, prf', go) <- checkType e prf tm

309+ return (d', prev, st', done, prf', env, go)

310+ ESearch ty -> do (d', st', done, prf', go) <- search e prf ty

311+ return (d', prev, st', done, prf', env, go)

312+ EDocStr d -> do (d', st', done, prf', go) <- docStr e prf d

313+ return (d', prev, st', done, prf', env, go)

314+ Success (Right cmd') ->

315+ case cmd' of

316+ DoLetP _ _ _ -> ifail "Pattern-matching let not supported here"

317+ DoBindP _ _ _ _ -> ifail "Pattern-matching <- not supported here"

318+ DoLet fc i ifc Placeholder expr ->

319+ do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)

320+ ctxt <- getContext

321+ let tm' = normaliseAll ctxt [] tm

322+ ty' = normaliseAll ctxt [] ty

323+ return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult ""))

324+ DoLet fc i ifc ty expr ->

325+ do (tm, ty) <- elabVal recinfo ERHS

326+ (PApp NoFC (PRef NoFC (sUN "the"))

327+ [ pexp (inLets ist env ty)

328+ , pexp (inLets ist env expr)

329+ ])

330+ ctxt <- getContext

331+ let tm' = normaliseAll ctxt [] tm

332+ ty' = normaliseAll ctxt [] ty

333+ return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult ""))

334+ DoBind fc i ifc expr ->

335+ do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)

336+ (_, e') <- elabStep e saveState -- enable :undo

337+ (res, e'') <- elabStep e' $

338+ runTactical ist NoFC [] tm ["Shell"]

339+ ctxt <- getContext

340+ (v, vty) <- tclift $ check ctxt [] (forget res)

341+ let v' = normaliseAll ctxt [] v

342+ vty' = normaliseAll ctxt [] vty

343+ return (True, BothStep:prev, e'', False, prf ++ [step], (i, vty', v') : env, Right (iPrintResult ""))

344+ DoExp fc expr ->

345+ do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)

346+ -- TODO: call elaborator with Elab () as goal here

347+ (_, e') <- elabStep e saveState -- enable :undo

348+ (_, e'') <- elabStep e' $

349+ runTactical ist NoFC [] tm ["Shell"]

350+ return (True, ElabStep:prev, e'', False, prf ++ [step], env, Right (iPrintResult "")))

351+ (\err -> return (False, prev, e, False, prf, env, Left err))

352+ idemodePutSExp "write-proof-state" (prf', length prf')

353+ case res of

354+ Left err -> do ist <- getIState

355+ iRenderError $ pprintErr ist err

356+ elabloop fn d prompt prf' st prev' h' env'

357+ Right ok ->

358+ if done then do (tm, _) <- elabStep st get_term

359+ return (tm, prf')

360+ else do ok

361+ elabloop fn d prompt prf' st prev' h' env'

362+

363+ where

364+ -- A bit of a hack: wrap the value up in a let binding, which will

365+ -- normalise away. It would be better to figure out how to call

366+ -- the elaborator with a custom environment here to avoid the

367+ -- delab step.

368+ inLets :: IState -> [(Name, Type, Term)] -> PTerm -> PTerm

369+ inLets ist lets tm = foldr (\(n, ty, v) b -> PLet NoFC n NoFC (delab ist ty) (delab ist v) b) tm (reverse lets)

370+

371+

372+

211ploop :: Name -> Bool -> String -> [String] -> ElabState EState -> Maybe History -> Idris (Term, [String])

373ploop :: Name -> Bool -> String -> [String] -> ElabState EState -> Maybe History -> Idris (Term, [String])

212ploop fn d prompt prf e h

374ploop fn d prompt prf e h

213 = do i <- getIState

375 = do i <- getIState

214 let autoSolve = opt_autoSolve (idris_options i)

376 let autoSolve = opt_autoSolve (idris_options i)

215− when d $ dumpState i (proof e)

377+ when d $ dumpState i [] (proof e)

216 (x, h') <-

378 (x, h') <-

217 case idris_outputmode i of

379 case idris_outputmode i of

218 RawOutput _ ->

380 RawOutput _ ->

@@ -247,11 +409,11 @@ ploop fn d prompt prf e h

247 when (not (null hs)) $ ifail "Incomplete proof"

409 when (not (null hs)) $ ifail "Incomplete proof"

248 iputStrLn "Proof completed!"

410 iputStrLn "Proof completed!"

249 return (False, e, True, prf, Right $ iPrintResult "")

411 return (False, e, True, prf, Right $ iPrintResult "")

250− Success (TCheck (PRef _ n)) -> checkNameType n

412+ Success (TCheck (PRef _ n)) -> checkNameType e prf n

251− Success (TCheck t) -> checkType t

413+ Success (TCheck t) -> checkType e prf t

252− Success (TEval t) -> evalTerm t e

414+ Success (TEval t) -> evalTerm e prf t

253− Success (TDocStr x) -> docStr x

415+ Success (TDocStr x) -> docStr e prf x

254− Success (TSearch t) -> search t

416+ Success (TSearch t) -> search e prf t

255 Success tac ->

417 Success tac ->

256 do (_, e) <- elabStep e saveState

418 do (_, e) <- elabStep e saveState

257 (_, st) <- elabStep e (runTac autoSolve i (Just proverFC) fn tac)

419 (_, st) <- elabStep e (runTac autoSolve i (Just proverFC) fn tac)

@@ -267,80 +429,87 @@ ploop fn d prompt prf e h

267 return (tm, prf')

429 return (tm, prf')

268 else do ok

430 else do ok

269 ploop fn d prompt prf' st h'

431 ploop fn d prompt prf' st h'

432+

433+

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

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

271− checkNameType n = do

435+

436+checkNameType :: ElabState EState -> [String] -> Name -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))

437+checkNameType e prf n = do

272− ctxt <- getContext

438+ ctxt <- getContext

273− ist <- getIState

439+ ist <- getIState

274− imp <- impShow

440+ imp <- impShow

275− idrisCatch (do

441+ idrisCatch (do

276− let OK env = envAtFocus (proof e)

442+ let OK env = envAtFocus (proof e)

277− ctxt' = envCtxt env ctxt

443+ ctxt' = envCtxt env ctxt

278− bnd = map (\x -> (fst x, False)) env

444+ bnd = map (\x -> (fst x, False)) env

279− ist' = ist { tt_ctxt = ctxt' }

445+ ist' = ist { tt_ctxt = ctxt' }

280− putIState ist'

446+ putIState ist'

281− -- Unlike the REPL, metavars have no special treatment, to

447+ -- Unlike the REPL, metavars have no special treatment, to

282− -- make it easier to see how to prove with them.

448+ -- make it easier to see how to prove with them.

283− let action = case lookupNames n ctxt' of

449+ let action = case lookupNames n ctxt' of

284− [] -> iPrintError $ "No such variable " ++ show n

450+ [] -> iPrintError $ "No such variable " ++ show n

285− ts -> iPrintFunTypes bnd n (map (\n -> (n, pprintDelabTy ist' n)) ts)

451+ ts -> iPrintFunTypes bnd n (map (\n -> (n, pprintDelabTy ist' n)) ts)

286− putIState ist

452+ putIState ist

287− return (False, e, False, prf, Right action))

453+ return (False, e, False, prf, Right action))

288− (\err -> do putIState ist ; ierror err)

454+ (\err -> do putIState ist ; ierror err)

289−

455+

290− checkType t = do

456+checkType :: ElabState EState -> [String] -> PTerm -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))

457+checkType e prf t = do

291− ist <- getIState

458+ ist <- getIState

292− ctxt <- getContext

459+ ctxt <- getContext

293− idrisCatch (do

460+ idrisCatch (do

294− let OK env = envAtFocus (proof e)

461+ let OK env = envAtFocus (proof e)

295− ctxt' = envCtxt env ctxt

462+ ctxt' = envCtxt env ctxt

296− putIState ist { tt_ctxt = ctxt' }

463+ putIState ist { tt_ctxt = ctxt' }

297− (tm, ty) <- elabVal recinfo ERHS t

464+ (tm, ty) <- elabVal recinfo ERHS t

298− let ppo = ppOptionIst ist

465+ let ppo = ppOptionIst ist

299− ty' = normaliseC ctxt [] ty

466+ ty' = normaliseC ctxt [] ty

300− infixes = idris_infixes ist

467+ infixes = idris_infixes ist

301− action = case tm of

468+ action = case tm of

302− TType _ ->

469+ TType _ ->

303− iPrintTermWithType (prettyImp ppo (PType emptyFC)) type1Doc

470+ iPrintTermWithType (prettyImp ppo (PType emptyFC)) type1Doc

304− _ -> let bnd = map (\x -> (fst x, False)) env in

471+ _ -> let bnd = map (\x -> (fst x, False)) env in

305− iPrintTermWithType (pprintPTerm ppo bnd [] infixes (delab ist tm))

472+ iPrintTermWithType (pprintPTerm ppo bnd [] infixes (delab ist tm))

306− (pprintPTerm ppo bnd [] infixes (delab ist ty))

473+ (pprintPTerm ppo bnd [] infixes (delab ist ty))

307− putIState ist

474+ putIState ist

308− return (False, e, False, prf, Right action))

475+ return (False, e, False, prf, Right action))

309− (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)

476+ (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)

310−

477+

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

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

312−

479+

480+evalTerm :: ElabState EState -> [String] -> PTerm -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))

313− evalTerm t e = withErrorReflection $

481+evalTerm e prf t = withErrorReflection $

314− do ctxt <- getContext

482+ do ctxt <- getContext

315− ist <- getIState

483+ ist <- getIState

316− idrisCatch (do

484+ idrisCatch (do

317− let OK env = envAtFocus (proof e)

485+ let OK env = envAtFocus (proof e)

318− ctxt' = envCtxt env ctxt

486+ ctxt' = envCtxt env ctxt

319− ist' = ist { tt_ctxt = ctxt' }

487+ ist' = ist { tt_ctxt = ctxt' }

320− bnd = map (\x -> (fst x, False)) env

488+ bnd = map (\x -> (fst x, False)) env

321− putIState ist'

489+ putIState ist'

322− (tm, ty) <- elabVal recinfo ERHS t

490+ (tm, ty) <- elabVal recinfo ERHS t

323− let tm' = force (normaliseAll ctxt' env tm)

491+ let tm' = force (normaliseAll ctxt' env tm)

324− ty' = force (normaliseAll ctxt' env ty)

492+ ty' = force (normaliseAll ctxt' env ty)

325− ppo = ppOption (idris_options ist')

493+ ppo = ppOption (idris_options ist')

326− infixes = idris_infixes ist

494+ infixes = idris_infixes ist

327− tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')

495+ tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')

328− tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')

496+ tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')

329− action = iPrintTermWithType tmDoc tyDoc

497+ action = iPrintTermWithType tmDoc tyDoc

330− putIState ist

498+ putIState ist

331− return (False, e, False, prf, Right action))

499+ return (False, e, False, prf, Right action))

332− (\err -> do putIState ist ; ierror err)

500+ (\err -> do putIState ist ; ierror err)

501+

333− docStr :: Either Name Const -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))

502+docStr :: ElabState EState -> [String] -> Either Name Const -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))

334− docStr (Left n) = do ist <- getIState

503+docStr e prf (Left n) = do ist <- getIState

335− idrisCatch (case lookupCtxtName n (idris_docstrings ist) of

504+ idrisCatch (case lookupCtxtName n (idris_docstrings ist) of

336− [] -> return (False, e, False, prf,

505+ [] -> return (False, e, False, prf,

337− Left . Msg $ "No documentation for " ++ show n)

506+ Left . Msg $ "No documentation for " ++ show n)

338− ns -> do toShow <- mapM (showDoc ist) ns

507+ ns -> do toShow <- mapM (showDoc ist) ns

339− return (False, e, False, prf,

508+ return (False, e, False, prf,

340− Right $ iRenderResult (vsep toShow)))

509+ Right $ iRenderResult (vsep toShow)))

341− (\err -> do putIState ist ; ierror err)

510+ (\err -> do putIState ist ; ierror err)

342− where showDoc ist (n, d) = do doc <- getDocs n FullDocs

511+ where showDoc ist (n, d) = do doc <- getDocs n FullDocs

343− return $ pprintDocs ist doc

512+ return $ pprintDocs ist doc

344− docStr (Right c) = do ist <- getIState

513+docStr e prf (Right c) = do ist <- getIState

345− return (False, e, False, prf, Right . iRenderResult $ pprintConstDocs ist c (constDocs c))

514+ return (False, e, False, prf, Right . iRenderResult $ pprintConstDocs ist c (constDocs c))

346− search t = return (False, e, False, prf, Right $ searchByType [] t)

515+search e prf t = return (False, e, False, prf, Right $ searchByType [] t)

src/Idris/REPL.hs+17−11

@@ -296,9 +296,9 @@ runIdeModeCommand h id orig fn mods (IdeMode.Interpret cmd) =

296 i <- getIState

297 case parseCmd i "(input)" cmd of

298 Failure err -> iPrintError $ show (fixColour False err)

299− Success (Right (Prove n')) ->

299+ Success (Right (Prove mode n')) ->

300 idrisCatch

301− (do process fn (Prove n')

301+ (do process fn (Prove mode n')

302 isetPrompt (mkPrompt mods)

303 case idris_outputmode i of

304 IdeMode n h -> -- signal completion of proof to ide

@@ -1094,16 +1094,20 @@ process fn' (AddProof prf)

1094 n' <- case prf of

1095 Nothing -> case proofs of

1096 [] -> ifail "No proof to add"

1097− ((x, p) : _) -> return x

1097+ ((x, _) : _) -> return x

1098 Just nm -> return nm

1099 n <- resolveProof n'

1100 case lookup n proofs of

1101 Nothing -> iputStrLn "No proof to add"

1102+ Just (mode, prf) ->

1103+ do let script = if mode

1104+ then showRunElab (lit fn) n prf

1105+ else showProof (lit fn) n prf

1102− Just p -> do let prog' = insertScript (showProof (lit fn) n p) ls

1106+ let prog' = insertScript script ls

1103− runIO $ writeSource fn (unlines prog')

1107+ runIO $ writeSource fn (unlines prog')

1104− removeProof n

1108+ removeProof n

1105− iputStrLn $ "Added proof " ++ show n

1109+ iputStrLn $ "Added proof " ++ show n

1106− where ls = (lines prog)

1110+ where ls = (lines prog)

1107

1111

1108process fn (ShowProof n')

1112process fn (ShowProof n')

1109 = do i <- getIState

1113 = do i <- getIState

@@ -1111,9 +1115,11 @@ process fn (ShowProof n')

1111 let proofs = proof_list i

1115 let proofs = proof_list i

1112 case lookup n proofs of

1116 case lookup n proofs of

1113 Nothing -> iPrintError "No proof to show"

1117 Nothing -> iPrintError "No proof to show"

1114− Just p -> iPrintResult $ showProof False n p

1118+ Just (m, p) -> iPrintResult $ if m

1119+ then showRunElab False n p

1120+ else showProof False n p

1115

1121

1116−process fn (Prove n')

1122+process fn (Prove mode n')

1117 = do ctxt <- getContext

1123 = do ctxt <- getContext

1118 ist <- getIState

1124 ist <- getIState

1119 let ns = lookupNames n' ctxt

1125 let ns = lookupNames n' ctxt

@@ -1123,7 +1129,7 @@ process fn (Prove n')

1123 [(n, (_,_,False))] -> return n

1129 [(n, (_,_,False))] -> return n

1124 [(_, (_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")

1130 [(_, (_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")

1125 ns -> ierror (CantResolveAlts (map fst ns))

1131 ns -> ierror (CantResolveAlts (map fst ns))

1126− prover (lit fn) n

1132+ prover mode (lit fn) n

1127 -- recheck totality

1133 -- recheck totality

1128 i <- getIState

1134 i <- getIState

1129 totcheck (fileFC "(input)", n)

1135 totcheck (fileFC "(input)", n)

src/Idris/REPLParser.hs+3−1

@@ -63,7 +63,9 @@ parserCommandsForHelp =

63 , noArgCmd ["e", "edit"] Edit "Edit current file using $EDITOR or $VISUAL"

64 , noArgCmd ["m", "metavars"] Metavars "Show remaining proof obligations (metavariables)"

65 , (["p", "prove"], MetaVarArg, "Prove a metavariable"

66− , nameArg Prove)

66+ , nameArg (Prove False))

67+ , (["elab"], MetaVarArg, "Build a metavariable using the elaboration shell"

68+ , nameArg (Prove True))

67 , (["a", "addproof"], NameArg, "Add proof to source file", cmd_addproof)

69 , (["a", "addproof"], NameArg, "Add proof to source file", cmd_addproof)

68 , (["rmproof"], NameArg, "Remove proof from proof stack"

70 , (["rmproof"], NameArg, "Remove proof from proof stack"

69 , nameArg RmProof)

71 , nameArg RmProof)

test/meta003/BadDef.idrnew file+12

@@ -0,0 +1,12 @@

1+module BadDef

3+import Language.Reflection.Elab

5+mkN : String -> TTName

6+mkN n = NS (UN n) ["BadDef"]

8+mkBadDef1 : Elab ()

9+mkBadDef1 = do declareType $ Declare (mkN "bad1") [] `(() -> ())

10+ defineFunction $ DefineFun (mkN "bad1") [MkFunClause `(():()) `("hi")]

11+runBad1 : ()

12+runBad1 = %runElab (mkBadDef1 *> search)

test/meta003/expectednew file+6

@@ -0,0 +1,6 @@

1+BadDef.idr:12:9:

2+When checking right hand side of runBad1:

3+Type mismatch between

4+ ()

5+and

6+ String

test/meta003/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ --nocolour --check --consolewidth 70 BadDef.idr

3+rm -f *.ibc