Cleaning backtracking code, optimized "Backtrack n x y" when n is

current state.

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

2 files changed, 38 insertions, 21 deletions

diff --git a/library/lib.ml b/library/lib.ml
index 49e685f63..ac710c357 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -150,19 +150,21 @@ let find_split_p p =
   in
   find !lib_stk
 
-let split_lib sp = 
+let split_lib_gen test = 
   let rec collect after equal = function
-    | ((sp',_) as hd)::before ->
-      	if sp = sp' then collect after (hd::equal) before else after,equal,hd::before
+    | hd::before ->
+      	if test hd then collect after (hd::equal) before else after,equal,hd::before
     | [] -> after,equal,[]
   in
   let rec findeq after = function
-    | ((sp',_) as hd)::before ->
-      	if sp = sp' then collect after [hd] before else findeq (hd::after) before
+    | hd :: before ->
+      	if test hd then collect after [hd] before else findeq (hd::after) before
     | [] -> error "no such entry"
   in 
   findeq [] !lib_stk
 
+let split_lib sp = split_lib_gen (fun x -> (fst x) = sp)
+
 (* Adding operations. *)
 
 let add_entry sp node =
@@ -491,6 +493,10 @@ let close_section id =
 (*****************)
 (* Backtracking. *)
 
+let (inLabel,outLabel) =
+  declare_object {(default_object "DOT") with
+				classify_function = (fun _ -> Dispose)}
+
 let recache_decl = function
   | (sp, Leaf o) -> cache_object (sp,o)
   | (_,OpenedSection _) -> add_section ()
@@ -501,8 +507,8 @@ let recache_context ctx =
 
 let is_frozen_state = function (_,FrozenState _) -> true | _ -> false
 
-let reset_to sp =
-  let (_,_,before) = split_lib sp in
+let reset_to_gen test =
+  let (_,_,before) = split_lib_gen test in
   lib_stk := before;
   recalc_path_prefix ();
   let spf = match find_entry_p is_frozen_state with
@@ -510,7 +516,10 @@ let reset_to sp =
     | _ -> assert false
   in
   let (after,_,_) = split_lib spf in
-  recache_context after
+  let res = recache_context after in
+  res
+
+let reset_to sp = reset_to_gen (fun x -> (fst x) = sp)
 
 let reset_name (loc,id) =
   let (sp,_) = 
@@ -549,10 +558,6 @@ let reset_mod (loc,id) =
   recache_context after
 
 
-let (inLabel,outLabel) =
-  declare_object {(default_object "DOT") with
-				classify_function = (fun _ -> Dispose)}
-
 let mark_end_of_command, current_command_label, set_command_label =
   let n = ref 0 in
   (fun () ->
@@ -562,17 +567,23 @@ let mark_end_of_command, current_command_label, set_command_label =
   (fun () -> !n),
   (fun x -> n:=x)
 
-let rec reset_label_stk n stk =
-  match stk with
-      (sp,Leaf o)::tail when object_tag o = "DOT" && n = outLabel o -> sp
-    | _::tail -> reset_label_stk n tail
-    | [] -> error "Unknown state number"
+let is_label_n n x =
+  match x with
+    | (sp,Leaf o) when object_tag o = "DOT" && n = outLabel o -> true
+    | _ -> false
 
+(* Reset the label registered by [mark_end_of_command()] with number n. *)
 let reset_label n = 
-  let res = reset_label_stk n !lib_stk in
-  set_command_label (n-1); (* forget state numbers after n only if reset succeeded *)
-  reset_to res
-
+  let current = current_command_label() in
+  if n < current then
+    let res = reset_to_gen (is_label_n n) in
+    set_command_label (n-1); (* forget state numbers after n only if reset succeeded *)
+    res
+  else (* optimisation to avoid recaching when not necessary (why is it so long??) *)
+    match !lib_stk with
+      | [] -> ()
+      | x :: ls -> (lib_stk := ls;set_command_label (n-1))
+    
 let rec back_stk n stk =
   match stk with
       (sp,Leaf o)::tail when object_tag o = "DOT" ->
diff --git a/library/lib.mli b/library/lib.mli
index 52e6b7bd7..5639ffed7 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -65,8 +65,14 @@ val add_anonymous_leaf : obj -> unit
 val add_leaves : identifier -> obj list -> object_name
 
 val add_frozen_state : unit -> unit
+
+(* Adds a "dummy" entry in lib_stk with a unique new label number. *)
 val mark_end_of_command : unit -> unit
+(* Returns the current label number *)
 val current_command_label : unit -> int
+(* [reset_label n ] resets [lib_stk] to the label n registered by
+   [mark_end_of_command()]. That is it forgets the label and anything
+   registered after it. *)
 val reset_label : int -> unit
 
 (*s The function [contents_after] returns the current library segment,