module Bstack et Edit

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

6 files changed, 213 insertions, 1 deletions

diff --git a/lib/bstack.ml b/lib/bstack.ml
new file mode 100644
index 000000000..c67f51092
--- /dev/null
+++ b/lib/bstack.ml
@@ -0,0 +1,44 @@
+
+(* $Id$ *)
+
+open Util
+
+type 'a t = {mutable depth : int option;
+             mutable stack : 'a list}
+
+let create depth = {depth = depth;
+                 stack = []}
+
+let set_depth bs n = bs.depth <- n
+
+let safe_chop_list len l =
+  if List.length l <= len then (l,[]) else list_chop len l
+        
+let push bs e =
+  match bs.depth with
+    | None -> bs.stack <- e :: bs.stack
+    | Some d -> bs.stack <- fst(safe_chop_list d (e :: bs.stack))
+	  
+let pop bs =
+  match bs.stack with
+    | [] -> None
+    | h::tl -> (bs.stack <- tl; Some h)
+
+let top bs =
+  match bs.stack with
+    | [] -> None
+    | h::_ -> Some h
+	  
+let app_push bs f =
+  match bs.stack with
+    | [] -> error "Nothing on the stack"
+    | h::_ -> push bs (f h)
+
+let app_repl bs f =
+  match bs.stack with
+    | [] -> error "Nothing on the stack"
+    | h::t -> bs.stack <- (f h)::t
+
+let is_empty bs = bs.stack = []
+
+let depth bs = List.length bs.stack
diff --git a/lib/bstack.mli b/lib/bstack.mli
new file mode 100644
index 000000000..d1f9ae387
--- /dev/null
+++ b/lib/bstack.mli
@@ -0,0 +1,16 @@
+
+(* $Id$ *)
+
+(* Bounded stacks. If the depth is [None], then there is no depth limit. *)
+
+type 'a t
+
+val create : int option -> 'a t
+val set_depth : 'a t -> int option -> unit
+val push : 'a t -> 'a -> unit
+val app_push : 'a t -> ('a -> 'a) -> unit
+val app_repl : 'a t -> ('a -> 'a) -> unit
+val pop : 'a t -> 'a option
+val top : 'a t -> 'a option
+val is_empty : 'a t -> bool
+val depth : 'a t -> int
diff --git a/lib/edit.ml b/lib/edit.ml
new file mode 100644
index 000000000..7ff552ef6
--- /dev/null
+++ b/lib/edit.ml
@@ -0,0 +1,99 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+
+type ('a,'b,'c) t = {
+  mutable focus : 'a option;
+  mutable last_focused_stk : 'a list;
+  buf : ('a, 'b Bstack.t * 'c) Hashtbl.t }
+
+let empty () = { 
+  focus = None;
+  last_focused_stk = [];
+  buf = Hashtbl.create 17 }
+
+let focus e nd =
+  begin match nd with
+    | None -> ()
+    | Some f -> if not (Hashtbl.mem e.buf f) then invalid_arg "Edit.focus"
+  end;
+  begin match e.focus with
+    | None -> ()
+    | Some foc -> 
+	if e.focus <> nd then
+          e.last_focused_stk <- foc::(list_except foc e.last_focused_stk)
+  end;
+  e.focus <- nd
+    
+let last_focused e =
+  match e.last_focused_stk with
+    | [] -> None
+    | f::_ -> Some f
+
+let restore_last_focus e = focus e (last_focused e)
+			     
+let focusedp e =
+  match e.focus with
+    | None -> false
+    | _    -> true
+
+let read e =
+  match e.focus with
+    | None -> None
+    | Some d ->
+	let (bs,c) = Hashtbl.find e.buf d in
+	(match Bstack.top bs with
+           | None -> anomaly "Edit.read"
+	   | Some v -> Some(d,v,c))
+
+let mutate e f =
+  match e.focus with
+    | None -> invalid_arg "Edit.mutate"
+    | Some d ->
+	let (bs,c) = Hashtbl.find e.buf d in
+	Bstack.app_push bs (f c)
+
+let rev_mutate e f =
+  match e.focus with
+    | None -> invalid_arg "Edit.rev_mutate"
+    | Some d ->
+	let (bs,c) = Hashtbl.find e.buf d in
+	Bstack.app_repl bs (f c)
+
+let undo e n =
+  match e.focus with
+    | None -> invalid_arg "Edit.undo"
+    | Some d ->
+	let (bs,_) = Hashtbl.find e.buf d in
+	if Bstack.depth bs <= n then
+          errorlabstrm "Edit.undo" [< 'sTR"Undo stack would be exhausted" >];
+        repeat n (fun () -> let _ = Bstack.pop bs in ()) ()
+
+let create e (d,b,c,udepth) =
+  if Hashtbl.mem e.buf d then
+    errorlabstrm "Edit.create" 
+      [< 'sTR"Already editing something of that name" >];
+  let bs = Bstack.create udepth in
+  Bstack.push bs b;
+  Hashtbl.add e.buf d (bs,c)
+
+let delete e d =
+  if not(Hashtbl.mem e.buf d) then
+    errorlabstrm "Edit.delete" [< 'sTR"No such editor" >];
+  Hashtbl.remove e.buf d;
+  e.last_focused_stk <- (list_except d e.last_focused_stk);
+  match e.focus with
+    | Some d' -> if d = d' then (e.focus <- None ; (restore_last_focus e))
+    | None -> ()
+
+let dom e = 
+  let l = ref [] in
+  Hashtbl.iter (fun x _ -> l := x :: !l) e.buf;
+  !l
+	      
+let clear e =
+  e.focus <- None;
+  e.last_focused_stk <- [];
+  Hashtbl.clear e.buf
diff --git a/lib/edit.mli b/lib/edit.mli
new file mode 100644
index 000000000..6d5744259
--- /dev/null
+++ b/lib/edit.mli
@@ -0,0 +1,47 @@
+
+(* $Id$ *)
+
+(* The type of editors.
+ * An editor is a finite map, ['a -> 'b], which knows how to apply
+ * modification functions to the value in the range, and how to
+ * focus on a member of the range.
+ * It also supports the notion of a limited-depth undo, and that certain
+ * modification actions do not push onto the undo stack, since they are
+ * reversible. *)
+
+type ('a,'b,'c) t
+
+val empty : unit -> ('a,'b,'c) t
+
+(* sets the focus to the specified domain element, or if [None],
+ * unsets the focus *)
+val focus : ('a,'b,'c) t -> 'a option -> unit
+
+(* gives the last focused element or [None] if none *)
+val last_focused : ('a,'b,'c) t -> 'a option
+
+(* are we focused ? *)
+val focusedp : ('a,'b,'c) t -> bool
+
+(* If we are focused, then return the current domain,range pair. *)
+val read : ('a,'b,'c) t -> ('a * 'b * 'c) option
+
+(* mutates the currently-focused range element, pushing its
+ * old value onto the undo stack
+ *)
+val mutate : ('a,'b,'c) t -> ('c -> 'b -> 'b) -> unit
+
+(* mutates the currently-focused range element, in place. *)
+val rev_mutate : ('a,'b,'c) t -> ('c -> 'b -> 'b) -> unit
+
+(* Pops the specified number of elements off of the undo stack, *
+  reinstating the last popped element. The undo stack is independently
+  managed for each range element. *)
+val undo : ('a,'b,'c) t -> int -> unit
+
+val create : ('a,'b,'c) t -> 'a * 'b * 'c * int option -> unit
+val delete : ('a,'b,'c) t -> 'a -> unit
+
+val dom : ('a,'b,'c) t -> 'a list
+
+val clear : ('a,'b,'c) t -> unit
diff --git a/lib/util.ml b/lib/util.ml
index b010e5e0c..f7e50204c 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -123,6 +123,8 @@ let list_for_all_i p =
   in 
   for_all_p
 
+let list_except x l = List.filter (fun y -> not (x = y)) l
+
 (* Arrays *)
 
 let array_exists f v = 
@@ -240,6 +242,9 @@ let iterate f =
     if n <= 0 then x else iterate_f (pred n) (f x)
   in 
   iterate_f
+
+let repeat n f x =
+  for i = 1 to n do f x done
  
 (* Misc *)
 
@@ -251,7 +256,6 @@ let out_some = function
   | Some x -> x
   | None -> failwith "out_some"
 
-
 let option_app f = function
   | None -> None
   | Some x -> Some (f x)
diff --git a/lib/util.mli b/lib/util.mli
index b7596e439..a9d7d05b3 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -39,6 +39,7 @@ val list_map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
 val list_index : 'a -> 'a list -> int
 val list_fold_left_i :  (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
 val list_for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
+val list_except : 'a -> 'a list -> 'a list
 
 (*s Arrays. *)
 
@@ -65,6 +66,7 @@ val array_map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
 
 val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
 val iterate : ('a -> 'a) -> int -> 'a -> 'a
+val repeat : int -> ('a -> unit) -> 'a -> unit
 
 (*s Misc. *)