lib/cstack: various improvements

- renaming reflecting the semantic of functions
- ability to edit the stack at the top of a _focused_zone_

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

2 files changed, 102 insertions, 27 deletions

diff --git a/lib/cStack.ml b/lib/cStack.ml
index 4fab9c1733..41ea5bf034 100644
--- a/lib/cStack.ml
+++ b/lib/cStack.ml
@@ -6,30 +6,85 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open CSig
-
 exception Empty = Stack.Empty
 
-type 'a t = 'a list ref
+type 'a t = {
+  mutable stack : 'a list;
+  mutable context : ('a list * 'a list) option
+}
+
+let create () = { stack = []; context = None }
+
+let push x s = s.stack <- x :: s.stack
+
+let pop = function
+  | { stack = [] } -> raise Stack.Empty
+  | { stack = x::xs } as s -> s.stack <- xs; x
+
+let top = function
+  | { stack = [] } -> raise Stack.Empty
+  | { stack = x::_ } -> x
 
-let create () = ref []
-let push x l = l := x :: !l
-let pop l = match !l with [] -> raise Stack.Empty | x::xs -> l := xs; x
-let top l = match !l with [] -> raise Stack.Empty | x::_ -> x
-let find f l = List.find f !l
-let find_map f l =
+let to_list = function
+  | { context = None; stack = s } -> s
+  | { context = Some (a,b); stack = s } -> a @ s @ b
+
+let to_lists = function
+  | { context = None; stack = s } -> [],s,[]
+  | { context = Some (a,b); stack = s } -> a,s,b
+
+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 !l
-let seek f accu l =
+  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 !l
-let is_empty l = match !l with [] -> true | _ -> false
-let iter f l = List.iter f !l
-let clear l = l := []
-let length l = List.length !l
-let to_list l = !l
+  aux accu s.stack
+
+let is_empty = function
+  | { stack = []; context = None } -> true
+  | _ -> false
+
+let iter f = function
+  | { stack = s; context = None } -> List.iter f s
+  | { stack = s; context = Some(a,b) } ->
+        List.iter f a; List.iter f s; List.iter f b
+
+let clear s = s.stack <- []; s.context <- None
+
+let length = function
+  | { stack = s; context = None } -> List.length s
+  | { stack = s; context = Some(a,b) } ->
+        List.length a + List.length s + List.length b
+
+let focus s ~cond_top:c_start ~cond_bot:c_stop =
+  if s.context <> None then raise (Invalid_argument "CStack.focus");
+  let rec aux (a,s,b) grab = function
+    | [] -> raise (Invalid_argument "CStack.focus")
+    | x::xs when not grab ->
+        if c_start x then aux (a,s,b) true (x::xs)
+        else aux (x::a,s,b) grab xs
+    | x::xs ->
+        if c_stop x then a, x::s, xs
+        else aux (a,x::s,b) grab xs in
+  let a, stack, b = aux ([],[],[]) false s.stack in
+  s.stack <- List.rev stack;
+  s.context <- Some (List.rev a, b)
+
+let unfocus = function
+  | { context = None } -> raise (Invalid_argument "CStack.unfocus")
+  | { context = Some (a,b); stack } as s ->
+       s.context <- None;
+       s.stack <- a @ stack @ b
+
+let focused { context } = context <> None
+
diff --git a/lib/cStack.mli b/lib/cStack.mli
index edca854488..78d2563a17 100644
--- a/lib/cStack.mli
+++ b/lib/cStack.mli
@@ -8,8 +8,6 @@
 
 (** Extended interface for OCaml stacks. *)
 
-open CSig
-
 type 'a t
 
 exception Empty
@@ -25,14 +23,6 @@ val find : ('a -> bool) -> 'a t -> 'a
 (** Find the first element satisfying the predicate.
     @raise Not_found it there is none. *)
 
-val find_map : ('a -> 'b option) -> 'a t -> 'b
-(** Find the first element that returns [Some _].
-    @raise Not_found it there is none. *)
-
-val seek : ('c -> 'a -> ('b, 'c) seek) -> 'c -> 'a t -> 'b
-(** Find the first element that returns [Some _].
-    @raise Not_found it there is none. *)
-
 val is_empty : 'a t -> bool
 (** Whether a stack is empty. *)
 
@@ -56,3 +46,33 @@ val top  : 'a t -> 'a
 val to_list : 'a t -> 'a list
 (** Convert to a list. *)
 
+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
+
+(** After [focus s c1 c2] the top of [s] is the topmost element [x] such that
+    [c1 x] is [true] and the bottom is the first element [y] following [x]
+    such that [c2 y] is [true].  After a focus push/pop/top/fold_until
+    only use the focused part.
+    @raise Invalid_argument "CStack.focus" if there is no such [x] and [y] *)
+val focus : 'a t -> cond_top:('a -> bool) -> cond_bot:('a -> bool) -> unit
+
+(** Undoes a [focus].
+    @raise Invalid_argument "CStack.unfocus" if the stack is not focused *)
+val unfocus : 'a t -> unit
+
+(** Is the stack focused *)
+val focused : 'a t -> bool
+
+(** Returns [top, s, bot] where [top @ s @ bot] is the full stack, and [s]
+    the focused part *)
+val to_lists : 'a t -> 'a list * 'a list * 'a list
+