89ffe9b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Undo tactic

commit89ffe9bead19bcda5f9991a930b6fd82a741a2bd authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 28 Sep 2011, 18:39 (15 years ago) parentffd5e72

4 files changed+20−8

compare with master

unifiedsplit

src/Elaborate.hs+4 src/ProofShell.hs+5−4 src/ProofState.hs+10−4 src/ShellParser.hs+1

src/Elaborate.hs+4

@@ -134,6 +134,10 @@ proofstate = processTactic' ProofState

134134qed :: Elab ()

135135qed = processTactic' QED

136136

137+undo :: Elab ()

138+undo = processTactic' Undo

139+

140+

137141prepare_apply :: Raw -> [Bool] -> Elab [Name]

138142prepare_apply fn imps =

139143 do ty <- get_type fn

src/ProofShell.hs+5−4

@@ -11,12 +11,13 @@ import Elaborate

1111import Control.Monad.State

1212import System.Console.Readline

1313

14−data ShellState = State { ctxt :: Context,

15− prf :: Maybe ProofState,

16− exitNow :: Bool

14+data ShellState = State { ctxt :: Context,

15+ prf :: Maybe ProofState,

16+ deferred :: [(Name, ProofState)],

17+ exitNow :: Bool

1718 }

1819

19−initState c = State c Nothing False

20+initState c = State c Nothing [] False

2021

2122processCommand :: Command -> ShellState -> (ShellState, String)

2223processCommand (Theorem n ty) state

src/ProofState.hs+10−4

@@ -22,6 +22,7 @@ data ProofState = PS { thname :: Name,

2222 nextname :: Int, -- name supply

2323 pterm :: Term, -- current proof term

2424 ptype :: Type, -- original goal

25+ previous :: Maybe ProofState, -- for undo

2526 context :: Context,

2627 done :: Bool

2728 }

@@ -45,6 +46,7 @@ data Tactic = Attack

4546 | Focus Name

4647 | MoveLast Name

4748 | ProofState

49+ | Undo

4850 | QED

4951

5052data TacticAction = AddGoal Name -- add a new goal, solve immediately

@@ -58,8 +60,8 @@ data TacticAction = AddGoal Name -- add a new goal, solve immediately

5860-- Some utilites on proof and tactic states

5961

6062instance Show ProofState where

61− show (PS nm [] _ tm _ _ _) = show nm ++ ": no more goals"

62− show (PS nm (h:hs) _ tm _ ctxt _)

63+ show (PS nm [] _ tm _ _ _ _) = show nm ++ ": no more goals"

64+ show (PS nm (h:hs) _ tm _ i_ ctxt _)

6365 = let OK g = goal (Just h) tm

6466 wkenv = premises g in

6567 showPs wkenv (reverse wkenv) ++ "\n" ++

@@ -101,7 +103,7 @@ action a = do (n, ts) <- get

101103newProof :: Name -> Context -> Type -> ProofState

102104newProof n ctxt ty = let h = holeName 0

103105 ty' = vToP ty in

104− PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty ctxt False

106+ PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty Nothing ctxt False

105107

106108type TState = (Int, [TacticAction])

107109type RunTactic = Context -> Env -> Term -> StateT TState TC Term

@@ -256,6 +258,9 @@ processTactic QED ps = case holes ps of

256258 "Proof complete: " ++ showEnv [] tm)

257259 _ -> Error "Still holes to fill."

258260processTactic ProofState ps = return (ps, showEnv [] (pterm ps))

261+processTactic Undo ps = case previous ps of

262+ Nothing -> Error "Nothing to undo."

263+ Just pold -> return (pold, "")

259264processTactic t ps

260265 = case holes ps of

261266 [] -> Error "Nothing to fill in."

@@ -263,7 +268,8 @@ processTactic t ps

263268 (ps', (n', actions)) <- runStateT (process t h ps) (n, [])

264269 return (ps' { nextname = n',

265270 pterm = updateSolved (getSolved actions) (pterm ps'),

266− holes = goals (holes ps') actions },

271+ holes = goals (holes ps') actions,

272+ previous = Just ps },

267273 logs actions)

268274 where logs [] = ""

269275 logs (Log x : xs) = x ++ "\n" ++ logs xs

src/ShellParser.hs+1

@@ -64,6 +64,7 @@ pTactic = do reserved "attack"; return attack

6464 <|> do reserved "check"; t <- pTerm; return (check_in t)

6565 <|> do reserved "focus"; n <- iName; return (focus n)

6666 <|> do reserved "state"; return proofstate

67+ <|> do reserved "undo"; return undo

6768 <|> do reserved "qed"; return qed

6869

6970pArgType :: Parser Bool