Clib: fold_left_until added to CList

CStack just calls it to implement fold_until.
CSig.seek renamed CSig.until, since there is no seek function.

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

8 files changed, 30 insertions, 34 deletions

diff --git a/lib/cList.ml b/lib/cList.ml
index cf2a54c4b..643ef7f2b 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -91,6 +91,7 @@ sig
   val index0 : 'a -> 'a list -> int
   val index0_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int
   val iteri :  (int -> 'a -> unit) -> 'a list -> unit
+  val fold_left_until : ('c -> 'a -> 'c CSig.until) -> 'c -> 'a list -> 'c
   val fold_right_i :  (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b
   val fold_left_i :  (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
   val fold_right_and_left :
@@ -424,6 +425,12 @@ let index x =
 
 let index0 x l = index x l - 1
 
+let fold_left_until f accu s =
+  let rec aux accu = function
+    | [] -> accu
+    | x :: xs -> match f accu x with CSig.Stop x -> x | CSig.Cont i -> aux i xs in
+  aux accu s
+
 let fold_right_i f i l =
   let rec it_f i l a = match l with
     | [] -> a
diff --git a/lib/cList.mli b/lib/cList.mli
index a82759daa..d891403d8 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -143,6 +143,10 @@ sig
   val iteri :  (int -> 'a -> unit) -> 'a list -> unit
   (** As [iter] but with the index argument (starting from 0). *)
 
+  val fold_left_until : ('c -> 'a -> 'c CSig.until) -> 'c -> 'a list -> 'c
+  (** acts like [fold_left f acc s] while [f] returns
+      [Cont acc']; it stops returning [c] as soon as [f] returns [Stop c]. *)
+
   val fold_right_i :  (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b
   val fold_left_i :  (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
   val fold_right_and_left :
diff --git a/lib/cSig.mli b/lib/cSig.mli
index 4858d16c3..dbc36b14f 100644
--- a/lib/cSig.mli
+++ b/lib/cSig.mli
@@ -11,5 +11,5 @@
 type ('a, 'b) union = Inl of 'a | Inr of 'b
 (** Union type *)
 
-type ('a, 'b) seek = Stop of 'a | Next of 'b
-(** Type isomorphic to union used for browsable structures. *)
+type 'a until = Stop of 'a | Cont of 'a
+(** Used for browsable-until structures. *)
diff --git a/lib/cStack.ml b/lib/cStack.ml
index 5ec872117..4acb2930c 100644
--- a/lib/cStack.ml
+++ b/lib/cStack.ml
@@ -28,20 +28,9 @@ let to_list { stack = s } = s
 
 let find f s = List.find f (to_list s)
 
-let find_map f s =
-  let rec aux = function
-  | [] -> raise Not_found
-  | x :: xs -> match f x with None -> aux xs | Some i -> i
-  in
-  aux (to_list s)
-
-type ('b, 'c) seek = ('b, 'c) CSig.seek = Stop of 'b | Next of 'c
-
-let fold_until f accu s =
-  let rec aux accu = function
-    | [] -> raise Not_found
-    | x :: xs -> match f accu x with Stop x -> x | Next i -> aux i xs in
-  aux accu s.stack
+let find_map f s = CList.find_map f s.stack
+
+let fold_until f accu s = CList.fold_left_until f accu s.stack
 
 let is_empty { stack = s } = s = []
 
diff --git a/lib/cStack.mli b/lib/cStack.mli
index 12bec1457..8dde1d1a1 100644
--- a/lib/cStack.mli
+++ b/lib/cStack.mli
@@ -50,11 +50,7 @@ val find_map : ('a -> 'b option) -> 'a t -> 'b
 (** Find the first element that returns [Some _].
     @raise Not_found it there is none. *)
 
-type ('b, 'c) seek = ('b, 'c) CSig.seek = Stop of 'b | Next of 'c
-
-(** [seek f acc s] acts like [List.fold_left f acc s] while [f] returns
-    [Next acc']; it stops returning [b] as soon as [f] returns [Stop b].
-    The stack is traversed from the top and is not altered.
-    @raise Not_found it there is none. *)
-val fold_until : ('c -> 'a -> ('b, 'c) seek) -> 'c -> 'a t -> 'b
+val fold_until : ('c -> 'a -> 'c CSig.until) -> 'c -> 'a t -> 'c
+(** Like CList.fold_left_until.
+    The stack is traversed from the top and is not altered. *)
 
diff --git a/lib/util.ml b/lib/util.ml
index 755d4657d..bc6a1ceac 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -123,7 +123,7 @@ let delayed_force f = f ()
 (* Misc *)
 
 type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b
-type ('a, 'b) seek = ('a, 'b) CSig.seek = Stop of 'a | Next of 'b
+type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
 
 (*s interruption *)
 
diff --git a/lib/util.mli b/lib/util.mli
index 8dec93e30..62db3225e 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -97,8 +97,8 @@ val delayed_force : 'a delayed -> 'a
 type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b
 (** Union type *)
 
-type ('a, 'b) seek = ('a, 'b) CSig.seek = Stop of 'a | Next of 'b
-(** Type isomorphic to union used for browsable structures. *)
+type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
+(** Used for browsable-until structures. *)
 
 (** {6 ... } *)
 (** Coq interruption: set the following boolean reference to interrupt Coq
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 478d69965..2899098b3 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -1147,8 +1147,8 @@ end = struct (* {{{ *)
           | { step = `Cmd (_,l) } -> l
           | _ -> [] in
         match f acc (id, vcs, ids) with
-        | Stop x -> x
-        | Next acc -> next acc
+        | `Stop x -> x
+        | `Cont acc -> next acc
  
   let undo_vernac_classifier v =
     try
@@ -1162,7 +1162,7 @@ end = struct (* {{{ *)
           (try
             let oid =
               fold_until (fun b (id,_,label) ->
-                if b then Stop id else Next (List.mem name label))
+                if b then `Stop id else `Cont (List.mem name label))
               false id in
             VtStm (VtBack oid, true), VtNow
           with Not_found ->
@@ -1170,12 +1170,12 @@ end = struct (* {{{ *)
       | VernacBack 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 Next (n-1)) n id in
+            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 Next (n-1)) n id in
+            if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in
           VtStm (VtBack oid, true), VtLater
       | VernacUndoTo _
       | VernacRestart as e ->
@@ -1188,15 +1188,15 @@ end = struct (* {{{ *)
           let cb, _ =
             Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs) in
           let n = fold_until (fun n (_,vcs,_) ->
-            if List.mem cb (Vcs_.branches vcs) then Next (n+1) else Stop n)
+            if List.mem cb (Vcs_.branches vcs) then `Cont (n+1) else `Stop n)
             0 id in
           let oid = fold_until (fun n (id,_,_) ->
-            if Int.equal n 0 then Stop id else Next (n-1)) (n-m-1) id in
+            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,_) ->
-            match Vcs_.branches vcs with [_] -> Stop id | _ -> Next ())
+            match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ())
             () id in
           VtStm (VtBack oid, true), VtLater
       | VernacBacktrack (id,_,_)