Implementation of a new backtracking system, that allow to go back

anywhere in a script (provided no suspend/resume is used):

* the command "Backtrack n m p" (vernac_bactrack) performs the
  following operation:

** do abort p times,
** do undo on the current proof (after the aborts) in order to reach a
   stack depth of m (see vernac_undo_todepth)
** resets the global state to state labelled with n.

* The coq prompt in emacs mode has more informations, it contains:

** the usual coq prompt plus:
** the state number (global state label)
** the depth of the current proof stack
** the names of all pending proofs, in *unspecified* order, separated by '|'

 Example:

     state                        proof stack
      num                           depth
       __                              _
 aux < 12 |aux|SmallStepAntiReflexive| 4 < ù
 ^^^^^^   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^     ^
 usual           pending proofs           usual
                                          special char


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6947 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 103 insertions, 3 deletions

diff --git a/lib/edit.ml b/lib/edit.ml
index 096fa5dc13..06a55d171d 100644
--- a/lib/edit.ml
+++ b/lib/edit.ml
@@ -84,6 +84,28 @@ let undo e n =
 	  errorlabstrm "Edit.undo" (str"Undo stack exhausted");
         repeat n Bstack.pop bs
 
+(* Return the depth of the focused proof of [e] stack, this is used to
+   put informations in coq prompt (in emacs mode). *)
+let depth e =
+  match e.focus with
+    | None -> invalid_arg "Edit.depth"
+    | Some d ->
+	let (bs,_) = Hashtbl.find e.buf d in
+	Bstack.depth bs
+
+(* Undo focused proof of [e] to reach depth [n] *)
+let undo_todepth e n =
+  match e.focus with
+    | None -> 
+	if n <> 0 
+	then errorlabstrm "Edit.undo_todepth" (str"No proof in progress")
+	else () (* if there is no proof in progress, then n must be zero *)
+    | Some d ->
+	let (bs,_) = Hashtbl.find e.buf d in
+	if Bstack.depth bs < n then
+	  errorlabstrm "Edit.undo_todepth" (str"Undo stack would be exhausted");
+        repeat (Bstack.depth bs - n) Bstack.pop bs
+
 let create e (d,b,c,udepth) =
   if Hashtbl.mem e.buf d then
     errorlabstrm "Edit.create" 
diff --git a/lib/edit.mli b/lib/edit.mli
index 0bd802fcc3..d13d9c6f69 100644
--- a/lib/edit.mli
+++ b/lib/edit.mli
@@ -54,3 +54,10 @@ val delete : ('a,'b,'c) t -> 'a -> unit
 val dom : ('a,'b,'c) t -> 'a list
 
 val clear : ('a,'b,'c) t -> unit
+
+(* [depth e] Returns the depth of the focused proof stack of [e], this
+   is used to put informations in coq prompt (in emacs mode). *)
+val depth : ('a,'b,'c) t -> int
+
+(* [undo_todepth e n] Undoes focused proof of [e] to reach depth [n] *)
+val undo_todepth : ('a,'b,'c) t -> int -> unit
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index a32e32538d..f0350946f7 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -647,6 +647,8 @@ GEXTEND Gram
       | IDENT "Back" -> VernacBack 1
       | IDENT "Back"; n = natural -> VernacBack n
       | IDENT "BackTo"; n = natural -> VernacBackTo n
+      | IDENT "Backtrack"; n = natural ; m = natural ; p = natural -> 
+	  VernacBacktrack (n,m,p)
 
 (* Tactic Debugger *)
       |	IDENT "Debug"; IDENT "On" -> VernacDebug true
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index bbcda792f0..f724589f69 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -174,6 +174,21 @@ let undo n =
   with (Invalid_argument "Edit.undo") ->
     errorlabstrm "Pfedit.undo" (str"No focused proof" ++ msg_proofs true)
 
+(* Undo current focused proof to reach depth [n]. This is used in
+   [vernac_backtrack]. *)
+let undo_todepth n =
+  try 
+    Edit.undo_todepth proof_edits n
+  with (Invalid_argument "Edit.undo") ->
+    errorlabstrm "Pfedit.undo" (str"No focused proof" ++ msg_proofs true)
+
+(* Return the depth of the current focused proof stack, this is used
+   to put informations in coq prompt (in emacs mode). *)
+let current_proof_depth() = 
+  try
+    Edit.depth proof_edits
+  with (Invalid_argument "Edit.depth") -> -1
+
 (*********************************************************************)
 (*                  Proof cooking                                    *)
 (*********************************************************************)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index b0aacd86c8..eca13c56cb 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -57,6 +57,14 @@ val delete_all_proofs : unit -> unit
 
 val undo : int -> unit
 
+(* Same as undo, but undoes the current proof stack to reach depth
+   [n]. This is used in [vernac_backtrack]. *)
+val undo_todepth : int -> unit
+
+(* Returns the depth of the current focused proof stack, this is used
+   to put informations in coq prompt (in emacs mode). *)
+val current_proof_depth: unit -> int
+
 (* [set_undo (Some n)] sets the size of the ``undo'' stack; [set_undo None]
    sets the size to the default value (12) *)
 
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index bfbdb598a7..9162c9fa77 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -182,14 +182,44 @@ let make_prompt () =
   with _ -> 
     "Coq < "
 
+(*let build_pending_list l = 
+  let pl = ref ">" in
+  let l' = ref l in
+  let res = 
+    while List.length !l' > 1 do 
+      pl := !pl ^ "|" Names.string_of_id x;
+      l':=List.tl !l'
+    done in
+  let last = try List.hd !l' with _ ->   in
+  "<"^l'
+*)    
+
+(* the coq prompt added to the default one when in emacs mode
+   The prompt contains the current state label [n] (for global
+   backtracking) and the current proof state [p] (for proof
+   backtracking) plus the list of open (nested) proofs (for proof
+   aborting when backtracking). It looks like:
+   
+   "n |lem1|lem2|lem3| p < "
+*)
+let make_emacs_prompt() =
+  let statnum = string_of_int (Lib.current_command_label ()) in
+  let endchar = String.make 1 (Char.chr 249) in
+  let dpth = Pfedit.current_proof_depth() in
+  let pending = Pfedit.get_all_proof_names() in
+  let pendingprompt = 
+    List.fold_left 
+      (fun acc x -> acc ^ (if acc <> "" then "|" else "") ^ Names.string_of_id x)
+      "" pending in
+  let proof_info = if dpth >= 0 then string_of_int dpth else "0" in
+  statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < " ^ endchar
+
 (* A buffer to store the current command read on stdin. It is
  * initialized when a vernac command is immediately followed by "\n",
  * or after a Drop. *)
 let top_buffer =
   let pr() = 
-    (make_prompt())^
-    (Printer.emacs_str ("*" ^ string_of_int (Lib.current_command_label ()) ^
-                String.make 1 (Char.chr 249)))
+    make_prompt() ^ Printer.emacs_str (make_emacs_prompt())
   in
   { prompt = pr;
     str = "";
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b032395e16..7d791dd745 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -620,6 +620,7 @@ let vernac_back n = Lib.back n
 
 let vernac_backto n = Lib.reset_label n
 
+(* see also [vernac_backtrack] which combines undoing and resetting *)
 (************)
 (* Commands *)
 
@@ -983,6 +984,17 @@ let vernac_undo n =
   undo n;
   print_subgoals ()
 
+(* backtrack with [naborts] abort, then undo_todepth to [pnum], then
+   back-to state number [snum]. This allows to backtrack proofs and
+   state with one command (easier for proofgeneral). *)
+let vernac_backtrack snum pnum naborts =
+  for i = 1 to naborts do vernac_abort None done;
+  undo_todepth pnum;
+  vernac_backto snum;
+  (* there may be no proof in progress, even if no abort *)
+  (try print_subgoals () with UserError _ -> ())
+  
+
   (* Est-ce normal que "Focus" ne semble pas se comporter comme "Focus 1" ? *)
 let vernac_focus = function
   | None -> traverse_nth_goal 1; print_subgoals ()
@@ -1156,6 +1168,7 @@ let interp c = match c with
   | VernacSuspend -> vernac_suspend ()
   | VernacResume id -> vernac_resume id
   | VernacUndo n -> vernac_undo n
+  | VernacBacktrack (snum,pnum,naborts) -> vernac_backtrack snum pnum naborts
   | VernacFocus n -> vernac_focus n
   | VernacUnfocus -> vernac_unfocus ()
   | VernacGo g -> vernac_go g
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 2fab2b0da0..0d54fb66db 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -278,6 +278,7 @@ type vernac_expr =
   | VernacSuspend
   | VernacResume of lident option
   | VernacUndo of int
+  | VernacBacktrack of int*int*int
   | VernacFocus of int option
   | VernacUnfocus
   | VernacGo of goable
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 1adc2aeb18..6bea86fec4 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -475,6 +475,8 @@ let rec pr_vernac = function
   | VernacAbort id -> str"Abort" ++ pr_opt pr_lident id
   | VernacResume id -> str"Resume" ++ pr_opt pr_lident id
   | VernacUndo i -> if i=1 then str"Undo" else str"Undo" ++ pr_intarg i
+  | VernacBacktrack (i,j,k) -> 
+      str "Backtrack" ++  spc() ++ prlist_with_sep sep int [i;j;k]
   | VernacFocus i -> str"Focus" ++ pr_opt int i
   | VernacGo g -> 
       let pr_goable = function