From 7d3ab7e00453e259939535618e4e10c624a37ec9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 15 Feb 2015 19:03:18 +0100 Subject: Undo: back to 8.4 semantics (Close #3514) Only tactics are taken into account. --- CHANGES | 3 --- stm/stm.ml | 58 +++++++++++++++++++++++------------------------ test-suite/output/simpl.v | 6 ++--- 3 files changed, 32 insertions(+), 35 deletions(-) diff --git a/CHANGES b/CHANGES index 8b4a4fc93..19da2a4c8 100644 --- a/CHANGES +++ b/CHANGES @@ -62,9 +62,6 @@ Vernacular commands Coq: terms, modules, tactics, etc. The old behavior of the command can be retrieved using the "Locate Term" command. - New "Derive" command to help writing program by derivation. -- "Undo" undoes any command, not just tactics. -- "Undo. Undo." does not work in CoqIDE or Proof General, it works only - in coqtop. "Undo 2" should be used intead. - New "Refine Instance Mode" option that allows to deactivate the generation of obligations in incomplete typeclass instances, raising an error instead. - "Collection" command to name sets of section hypotheses. Named collections diff --git a/stm/stm.ml b/stm/stm.ml index 207afd8ae..4ff163e08 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -132,6 +132,7 @@ type branch_type = | `Proof of proof_mode * depth | `Edit of proof_mode * Stateid.t * Stateid.t ] type cmd_t = { + ctac : bool; (* is a tactic, needed by the 8.4 semantics of Undo *) cast : ast; cids : Id.t list; cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch ] } @@ -144,7 +145,7 @@ type qed_t = { brinfo : branch_type Vcs_.branch_info } type seff_t = ast option -type alias_t = Stateid.t +type alias_t = Stateid.t * ast type transaction = | Cmd of cmd_t | Fork of fork_t @@ -315,7 +316,7 @@ end = struct (* {{{ *) (try string_of_ppcmds (pr_ast t) with _ -> "ERR") | Sideff None -> "EnvChange" | Noop -> " " - | Alias id -> sprintf "Alias(%s)" (Stateid.to_string id) + | Alias (id,_) -> sprintf "Alias(%s)" (Stateid.to_string id) | Qed { qast } -> string_of_ppcmds (pr_ast qast) in let is_green id = match get_info vcs id with @@ -769,19 +770,20 @@ end = struct (* {{{ *) match info.vcs_backup with | None, _ -> next acc | Some vcs, _ -> - let ids = - if id = Stateid.initial || id = Stateid.dummy then [] else + let ids, tactic, undo = + if id = Stateid.initial || id = Stateid.dummy then [],false,0 else match VCS.visit id with - | { step = `Fork ((_,_,_,l),_) } -> l - | { step = `Cmd { cids = l } } -> l - | _ -> [] in - match f acc (id, vcs, ids) with + | { step = `Fork ((_,_,_,l),_) } -> l, false,0 + | { step = `Cmd { cids = l; ctac } } -> l, ctac,0 + | { step = `Alias (_,{ expr = VernacUndo n}) } -> [], false, n + | _ -> [],false,0 in + match f acc (id, vcs, ids, tactic, undo) with | `Stop x -> x | `Cont acc -> next acc let back_safe () = let id = - fold_until (fun n (id,_,_) -> + fold_until (fun n (id,_,_,_,_) -> if n >= 0 && State.is_cached id then `Stop id else `Cont (succ n)) 0 (VCS.get_branch_pos (VCS.current_branch ())) in backto id @@ -797,7 +799,7 @@ end = struct (* {{{ *) let id = VCS.get_branch_pos (VCS.current_branch ()) in (try let oid = - fold_until (fun b (id,_,label) -> + fold_until (fun b (id,_,label,_,_) -> if b then `Stop id else `Cont (List.mem name label)) false id in VtStm (VtBack oid, true), VtNow @@ -805,17 +807,15 @@ end = struct (* {{{ *) VtStm (VtBack id, true), VtNow) | VernacBack n -> let id = VCS.get_branch_pos (VCS.current_branch ()) in - let oid = fold_until (fun n (id,_,_) -> + let oid = fold_until (fun n (id,_,_,_,_) -> if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in VtStm (VtBack oid, true), VtNow | VernacUndo n -> let id = VCS.get_branch_pos (VCS.current_branch ()) in - let oid = fold_until (fun n (id,_,_) -> - if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in - if n = 1 && !Flags.coqtop_ui && not !Flags.batch_mode && - not !Flags.print_emacs then - VtStm (VtBack oid, false), VtNow - else VtStm (VtBack oid, true), VtLater + let oid = fold_until (fun n (id,_,_,tactic,undo) -> + let value = (if tactic then 1 else 0) - undo in + if Int.equal n 0 then `Stop id else `Cont (n-value)) n id in + VtStm (VtBack oid, true), VtLater | VernacUndoTo _ | VernacRestart as e -> let m = match e with VernacUndoTo m -> m | _ -> 0 in @@ -826,15 +826,15 @@ end = struct (* {{{ *) | Some vcs, _ -> vcs in let cb, _ = Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs) in - let n = fold_until (fun n (_,vcs,_) -> + let n = fold_until (fun n (_,vcs,_,_,_) -> if List.mem cb (Vcs_.branches vcs) then `Cont (n+1) else `Stop n) 0 id in - let oid = fold_until (fun n (id,_,_) -> + let oid = fold_until (fun n (id,_,_,_,_) -> if Int.equal n 0 then `Stop id else `Cont (n-1)) (n-m-1) id in VtStm (VtBack oid, true), VtLater | VernacAbortAll -> let id = VCS.get_branch_pos (VCS.current_branch ()) in - let oid = fold_until (fun () (id,vcs,_) -> + let oid = fold_until (fun () (id,vcs,_,_,_) -> match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ()) () id in VtStm (VtBack oid, true), VtLater @@ -1667,7 +1667,7 @@ let known_state ?(redefine_qed=false) ~cache id = let step, cache_step, feedback_processed = let view = VCS.visit id in match view.step with - | `Alias id -> (fun () -> + | `Alias (id,_) -> (fun () -> reach view.next; reach id ), cache, true | `Cmd { cast = x; cqueue = `TacQueue cancel } -> (fun () -> @@ -1968,11 +1968,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = List.iter (fun b -> if not(VCS.Branch.equal b head) then begin VCS.checkout b; - VCS.commit (VCS.new_node ()) (Alias oid); + VCS.commit (VCS.new_node ()) (Alias (oid,x)); end) (VCS.branches ()); VCS.checkout_shallowest_proof_branch (); - VCS.commit id (Alias oid); + VCS.commit id (Alias (oid,x)); Backtrack.record (); if w == VtNow then finish (); `Ok | VtStm (VtBack id, false), VtNow -> prerr_endline ("undo to state " ^ Stateid.to_string id); @@ -2001,7 +2001,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = let queue = if !Flags.async_proofs_full then `QueryQueue (ref false) else `MainQueue in - VCS.commit id (Cmd { cast = x; cids = []; cqueue = queue }); + VCS.commit id (Cmd {ctac=false;cast = x; cids = []; cqueue = queue }); Backtrack.record (); if w == VtNow then finish (); `Ok | VtQuery (false,_), VtLater -> anomaly(str"classifier: VtQuery + VtLater must imply part_of_script") @@ -2025,7 +2025,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = | VtProofMode mode, VtNow -> let id = VCS.new_node ~id:newtip () in VCS.checkout VCS.Branch.master; - VCS.commit id (Cmd {cast = x; cids=[]; cqueue = `MainQueue}); + VCS.commit id (Cmd {ctac=false;cast = x;cids=[];cqueue = `MainQueue}); VCS.propagate_sideff (Some x); List.iter (fun bn -> match VCS.get_branch bn with @@ -2044,7 +2044,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = | VtProofStep paral, w -> let id = VCS.new_node ~id:newtip () in let queue = if paral then `TacQueue (ref false) else `MainQueue in - VCS.commit id (Cmd {cast = x; cids = []; cqueue = queue }); + VCS.commit id (Cmd {ctac = true;cast = x;cids = [];cqueue = queue }); Backtrack.record (); if w == VtNow then finish (); `Ok | VtQed keep, w -> let valid = if tty then Some(VCS.get_branch_pos head) else None in @@ -2060,7 +2060,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = | VtSideff l, w -> let id = VCS.new_node ~id:newtip () in VCS.checkout VCS.Branch.master; - VCS.commit id (Cmd { cast = x; cids = l; cqueue = `MainQueue}); + VCS.commit id (Cmd {ctac=false;cast=x;cids=l;cqueue=`MainQueue}); VCS.propagate_sideff (Some x); VCS.checkout_shallowest_proof_branch (); Backtrack.record (); if w == VtNow then finish (); `Ok @@ -2084,7 +2084,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1)); Proof_global.activate_proof_mode "Classic"; end else begin - VCS.commit id (Cmd { cast = x; cids = []; cqueue = `MainQueue}); + VCS.commit id (Cmd {ctac=false; cast = x; cids = []; cqueue = `MainQueue}); VCS.propagate_sideff (Some x); VCS.checkout_shallowest_proof_branch (); end in @@ -2332,7 +2332,7 @@ let get_script prf = find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next | `Sideff (`Id id) -> find acc id | `Cmd {cast = x} -> find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next - | `Alias id -> find acc id + | `Alias (id,_) -> find acc id | `Fork _ -> find acc view.next in find [] (VCS.get_branch_pos branch) diff --git a/test-suite/output/simpl.v b/test-suite/output/simpl.v index 89638eedd..5f1926f14 100644 --- a/test-suite/output/simpl.v +++ b/test-suite/output/simpl.v @@ -4,10 +4,10 @@ Goal forall x, 0+x = 1+x. intro x. simpl (_ + x). Show. -Undo 2. +Undo. simpl (_ + x) at 2. Show. -Undo 2. +Undo. simpl (0 + _). Show. -Undo 2. +Undo. -- cgit v1.2.3