summaryrefslogtreecommitdiff
path: root/toplevel/backtrack.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/backtrack.ml')
-rw-r--r--toplevel/backtrack.ml243
1 files changed, 243 insertions, 0 deletions
diff --git a/toplevel/backtrack.ml b/toplevel/backtrack.ml
new file mode 100644
index 00000000..f444fc2d
--- /dev/null
+++ b/toplevel/backtrack.ml
@@ -0,0 +1,243 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Names
+open Vernacexpr
+
+(** Command history stack
+
+ We maintain a stack of the past states of the system. Each
+ successfully interpreted command adds an [info] element
+ to this stack, storing what were the (label / current proof / ...)
+ just _after_ the interpretation of this command.
+
+ - A label is just an integer, starting from Lib.first_command_label
+ initially, and incremented at each new successful command.
+ - If some proofs are opened, we have their number in [nproofs],
+ the name of the current proof in [prfname], the current depth in
+ [prfdepth].
+ - Otherwise, [nproofs = 0], [prfname = None], [prfdepth = 0]
+ - The text of the command is stored (for Show Script currently).
+ - A command can be tagged later as non-"reachable" when the current proof
+ at the time of this command has been ended by Qed/Abort/Restart,
+ meaning we can't backtrack there.
+*)
+
+type info = {
+ label : int;
+ nproofs : int;
+ prfname : identifier option;
+ prfdepth : int;
+ ngoals : int;
+ cmd : vernac_expr;
+ mutable reachable : bool;
+}
+
+let history : info Stack.t = Stack.create ()
+
+(** Is this stack active (i.e. nonempty) ?
+ The stack is currently inactive when compiling files (coqc). *)
+
+let is_active () = not (Stack.is_empty history)
+
+(** For debug purpose, a dump of the history *)
+
+let dump_history () =
+ let l = ref [] in
+ Stack.iter (fun i -> l:=i::!l) history;
+ !l
+
+(** Basic manipulation of the command history stack *)
+
+exception Invalid
+
+let pop () = ignore (Stack.pop history)
+
+let npop n =
+ (* Since our history stack always contains an initial entry,
+ it's invalid to try to completely empty it *)
+ if n < 0 || n >= Stack.length history then raise Invalid
+ else for i = 1 to n do pop () done
+
+let top () =
+ try Stack.top history with Stack.Empty -> raise Invalid
+
+(** Search the history stack for a suitable location. We perform first
+ a non-destructive search: in case of search failure, the stack is
+ unchanged. *)
+
+exception Found of info
+
+let search test =
+ try
+ Stack.iter (fun i -> if test i then raise (Found i)) history;
+ raise Invalid
+ with Found i ->
+ while i != Stack.top history do pop () done
+
+(** An auxiliary function to retrieve the number of remaining subgoals *)
+
+let get_ngoals () =
+ try
+ let prf = Proof_global.give_me_the_proof () in
+ List.length (Evd.sig_it (Proof.V82.background_subgoals prf))
+ with Proof_global.NoCurrentProof -> 0
+
+(** Register the end of a command and store the current state *)
+
+let mark_command ast =
+ Lib.add_frozen_state();
+ Lib.mark_end_of_command();
+ Stack.push
+ { label = Lib.current_command_label ();
+ nproofs = List.length (Pfedit.get_all_proof_names ());
+ prfname =
+ (try Some (Pfedit.get_current_proof_name ())
+ with Proof_global.NoCurrentProof -> None);
+ prfdepth = max 0 (Pfedit.current_proof_depth ());
+ reachable = true;
+ ngoals = get_ngoals ();
+ cmd = ast }
+ history
+
+(** Backtrack by aborting [naborts] proofs, then setting proof-depth back to
+ [pnum] and finally going to state number [snum]. *)
+
+let raw_backtrack snum pnum naborts =
+ for i = 1 to naborts do Pfedit.delete_current_proof () done;
+ Pfedit.undo_todepth pnum;
+ Lib.reset_label snum
+
+(** Re-sync the state of the system (label, proofs) with the top
+ of the history stack. We may end on some earlier state to avoid
+ re-opening proofs. This function will return the final label
+ and the number of extra backtracking steps performed. *)
+
+let sync nb_opened_proofs =
+ (* Backtrack by enough additional steps to avoid re-opening proofs.
+ Typically, when a Qed has been crossed, we backtrack to the proof start.
+ NB: We cannot reach the empty stack, since the first entry in the
+ stack has no opened proofs and is tagged as reachable.
+ *)
+ let extra = ref 0 in
+ while not (top()).reachable do incr extra; pop () done;
+ let target = top ()
+ in
+ (* Now the opened proofs at target is a subset of the opened proofs before
+ the backtrack, we simply abort the extra proofs (if any).
+ NB: It is critical here that proofs are nested in a regular way
+ (i.e. no more Resume or Suspend commands as earlier). This way, we can
+ simply count the extra proofs to abort instead of taking care of their
+ names.
+ *)
+ let naborts = nb_opened_proofs - target.nproofs in
+ (* We are now ready to do a low-level backtrack *)
+ raw_backtrack target.label target.prfdepth naborts;
+ (target.label, !extra)
+
+(** Backtracking by a certain number of (non-state-preserving) commands.
+ This is used by Coqide.
+ It may actually undo more commands than asked : for instance instead
+ of jumping back in the middle of a finished proof, we jump back before
+ this proof. The number of extra backtracked command is returned at
+ the end. *)
+
+let back count =
+ if count = 0 then 0
+ else
+ let nb_opened_proofs = List.length (Pfedit.get_all_proof_names ()) in
+ npop count;
+ snd (sync nb_opened_proofs)
+
+(** Backtracking to a certain state number, and reset proofs accordingly.
+ We may end on some earlier state if needed to avoid re-opening proofs.
+ Return the final state number. *)
+
+let backto snum =
+ if snum = Lib.current_command_label () then snum
+ else
+ let nb_opened_proofs = List.length (Pfedit.get_all_proof_names ()) in
+ search (fun i -> i.label = snum);
+ fst (sync nb_opened_proofs)
+
+(** Old [Backtrack] code with corresponding update of the history stack.
+ [Backtrack] is now deprecated (in favor of [BackTo]) but is kept for
+ compatibility with ProofGeneral. It's completely up to ProofGeneral
+ to decide where to go and how to adapt proofs. Note that the choices
+ of ProofGeneral are currently not always perfect (for instance when
+ backtracking an Undo). *)
+
+let backtrack snum pnum naborts =
+ raw_backtrack snum pnum naborts;
+ search (fun i -> i.label = snum)
+
+(** [reset_initial] resets the system and clears the command history
+ stack, only pushing back the initial entry. It should be equivalent
+ to [backto Lib.first_command_label], but sligthly more efficient. *)
+
+let reset_initial () =
+ let init_label = Lib.first_command_label in
+ if Lib.current_command_label () = init_label then ()
+ else begin
+ Pfedit.delete_all_proofs ();
+ Lib.reset_label init_label;
+ Stack.clear history;
+ Stack.push
+ { label = init_label;
+ nproofs = 0;
+ prfname = None;
+ prfdepth = 0;
+ ngoals = 0;
+ reachable = true;
+ cmd = VernacNop }
+ history
+ end
+
+(** Reset to the last known state just before defining [id] *)
+
+let reset_name id =
+ let lbl =
+ try Lib.label_before_name id with Not_found -> raise Invalid
+ in
+ ignore (backto lbl)
+
+(** When a proof is ended (via either Qed/Admitted/Restart/Abort),
+ old proof steps should be marked differently to avoid jumping back
+ to them:
+ - either this proof isn't there anymore in the proof engine
+ - either it's there but it's a more recent attempt after a Restart,
+ so we shouldn't mix the two.
+ We also mark as unreachable the proof steps cancelled via a Undo. *)
+
+let mark_unreachable ?(after=0) prf_lst =
+ let fix i = match i.prfname with
+ | None -> raise Not_found (* stop hacking the history outside of proofs *)
+ | Some p ->
+ if List.mem p prf_lst && i.prfdepth > after
+ then i.reachable <- false
+ in
+ try Stack.iter fix history with Not_found -> ()
+
+(** Parse the history stack for printing the script of a proof *)
+
+let get_script prf =
+ let script = ref [] in
+ let select i = match i.prfname with
+ | None -> raise Not_found
+ | Some p when p=prf && i.reachable -> script := i :: !script
+ | _ -> ()
+ in
+ (try Stack.iter select history with Not_found -> ());
+ (* Get rid of intermediate commands which don't grow the proof depth *)
+ let rec filter n = function
+ | [] -> []
+ | {prfdepth=d; cmd=c; ngoals=ng}::l when n < d -> (c,ng) :: filter d l
+ | {prfdepth=d}::l -> filter d l
+ in
+ (* initial proof depth (after entering the lemma statement) is 1 *)
+ filter 1 !script