git.iko.soy/Idris-dev
on master help sign in
Rename function to better reflect purpose
commitfbbe433c63066341753a4bec79cf6cd5cd78bc09 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 10 Jun 2015, 15:05 (11 years ago) parent124074a
2 files changed+8−8
compare with master
unifiedsplit
src/Idris/Elab/Term.hs+6−6 src/Idris/Prover.hs+2−2
src/Idris/Elab/Term.hs+6−6
@@ -1145,7 +1145,7 @@ elab ist info emode opts fn tm
11451145 focus n
11461146 elab' ina (Just fc') tm
11471147 env <- get_env
1148− runTactical ist (maybe fc' id fc) env (P Bound n' Erased) ns
1148+ runElabAction ist (maybe fc' id fc) env (P Bound n' Erased) ns
11491149 solve
11501150 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
11511151
@@ -1698,9 +1698,9 @@ metavarName _ n@(NS _ _) = n
16981698metavarName (Just (ns@(_:_))) n = sNS n ns
16991699metavarName _ n = n
17001700
1701−runTactical :: IState -> FC -> Env -> Term -> [String] -> ElabD Term
1702−runTactical ist fc env tm ns = do tm' <- eval tm
1703− runTacTm tm'
1701+runElabAction :: IState -> FC -> Env -> Term -> [String] -> ElabD Term
1702+runElabAction ist fc env tm ns = do tm' <- eval tm
1703+ runTacTm tm'
17041704
17051705 where
17061706 eval tm = do ctxt <- get_context
@@ -1965,8 +1965,8 @@ runTactical ist fc env tm ns = do tm' <- eval tm
19651965 datatypes <- get_datatypes
19661966 env <- get_env
19671967 (_, ES (p, aux') _ _) <-
1968− lift $ runElab aux (runTactical ist fc [] script ns)
1969− (newProof recH ctxt datatypes goalTT)
1968+ lift $ runElab aux (runElabAction ist fc [] script ns)
1969+ (newProof recH ctxt datatypes goalTT)
19701970 let tm_out = getProofTerm (pterm p)
19711971 updateAux $ const aux'
19721972 env' <- get_env
src/Idris/Prover.hs+2−2
@@ -335,7 +335,7 @@ elabloop fn d prompt prf e prev h env
335335 do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)
336336 (_, e') <- elabStep e saveState -- enable :undo
337337 (res, e'') <- elabStep e' $
338− runTactical ist NoFC [] tm ["Shell"]
338+ runElabAction ist NoFC [] tm ["Shell"]
339339 ctxt <- getContext
340340 (v, vty) <- tclift $ check ctxt [] (forget res)
341341 let v' = normaliseAll ctxt [] v
@@ -346,7 +346,7 @@ elabloop fn d prompt prf e prev h env
346346 -- TODO: call elaborator with Elab () as goal here
347347 (_, e') <- elabStep e saveState -- enable :undo
348348 (_, e'') <- elabStep e' $
349− runTactical ist NoFC [] tm ["Shell"]
349+ runElabAction ist NoFC [] tm ["Shell"]
350350 return (True, ElabStep:prev, e'', False, prf ++ [step], env, Right (iPrintResult "")))
351351 (\err -> return (False, prev, e, False, prf, env, Left err))
352352 idemodePutSExp "write-proof-state" (prf', length prf')