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

git.iko.soy/Idris-dev

on master help sign in

Undo tactic

89ffe9bEdwin Brady15 years ago

src/Elaborate.hs+4

compare with master

unifiedsplit

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

134qed :: Elab ()

135qed = processTactic' QED

136

137+undo :: Elab ()

138+undo = processTactic' Undo

139+

140+

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

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

138prepare_apply fn imps =

142prepare_apply fn imps =

139 do ty <- get_type fn

143 do ty <- get_type fn

src/ProofShell.hs+5−4

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

11import Control.Monad.State

12import System.Console.Readline

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

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

15− prf :: Maybe ProofState,

15+ prf :: Maybe ProofState,

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

16− exitNow :: Bool

17+ exitNow :: Bool

17 }

18 }

19−initState c = State c Nothing False

20+initState c = State c Nothing [] False

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

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

22processCommand (Theorem n ty) state

23processCommand (Theorem n ty) state

src/ProofState.hs+10−4

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

22 nextname :: Int, -- name supply

23 pterm :: Term, -- current proof term

24 ptype :: Type, -- original goal

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

25 context :: Context,

26 context :: Context,

26 done :: Bool

27 done :: Bool

27 }

28 }

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

45 | Focus Name

46 | Focus Name

46 | MoveLast Name

47 | MoveLast Name

47 | ProofState

48 | ProofState

49+ | Undo

48 | QED

50 | QED

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

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

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

58-- Some utilites on proof and tactic states

60-- Some utilites on proof and tactic states

60instance Show ProofState where

62instance Show ProofState where

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

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

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

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

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

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

64 wkenv = premises g in

66 wkenv = premises g in

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

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

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

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

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

102newProof n ctxt ty = let h = holeName 0

104newProof n ctxt ty = let h = holeName 0

103 ty' = vToP ty in

105 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

105

107

106type TState = (Int, [TacticAction])

108type TState = (Int, [TacticAction])

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

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

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

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

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

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

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

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

260processTactic 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, "")

259processTactic t ps

264processTactic t ps

260 = case holes ps of

265 = case holes ps of

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

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

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

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

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

264 return (ps' { nextname = n',

269 return (ps' { nextname = n',

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

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

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

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

272+ previous = Just ps },

267 logs actions)

273 logs actions)

268 where logs [] = ""

274 where logs [] = ""

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

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

src/ShellParser.hs+1

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

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

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

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

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

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

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

69pArgType :: Parser Bool

70pArgType :: Parser Bool