54cd5a6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

An interactive Elab shell

54cd5a6David Raymond Christiansen11 years ago

docs/reference/elaborator-reflection.rst+8

compare with master

unifiedsplit

@@ -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=======

src/Idris/AbsSyntaxTree.hs+7−2

@@ -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 }

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

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

1697 when autoSolve solveAll

1698

1699

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

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

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

1702 runTacTm tm'

1703− return ()

1703+

1704 where

1705 eval tm = do ctxt <- get_context

1706 return $ normaliseAll ctxt env (finalise tm)

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/ParseExpr.hs+4−4

@@ -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)