Gestion en temps constant de la pile des Unfo

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

4 files changed, 46 insertions, 39 deletions

diff --git a/lib/bstack.ml b/lib/bstack.ml
index c52b0e713a..3754aa1620 100644
--- a/lib/bstack.ml
+++ b/lib/bstack.ml
@@ -8,44 +8,56 @@
 
 (* $Id$ *)
 
+(* Queues of a given length *)
+
 open Util
 
-type 'a t = {mutable depth : int option;
-             mutable stack : 'a list}
+type 'a t = {mutable pos : int;
+             mutable size : int;
+             stack : 'a array}
 
-let create depth = {depth = depth;
-                 stack = []}
+let create depth e =
+  {pos = 0;
+   size = 1;
+   stack = Array.create depth e}
 
+(*
 let set_depth bs n = bs.depth <- n
+*)
+
+let incr_pos bs =
+  bs.pos <- if bs.pos = Array.length bs.stack - 1 then 0 else bs.pos + 1
+
+let incr_size bs =
+  if bs.size < Array.length bs.stack then bs.size <- bs.size + 1
+
+let decr_pos bs =
+  bs.pos <- if bs.pos = 0 then Array.length bs.stack - 1 else bs.pos - 1
 
-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))
+  incr_pos bs;
+  incr_size bs;
+  bs.stack.(bs.pos) <- e
 	  
 let pop bs =
-  match bs.stack with
-    | [] -> None
-    | h::tl -> (bs.stack <- tl; Some h)
+  if bs.size > 1 then begin
+    bs.size <- bs.size - 1; 
+    let oldpos = bs.pos in
+    decr_pos bs;
+    (* Release the memory at oldpos, by coyping what is at new pos *)
+    bs.stack.(oldpos) <- bs.stack.(bs.pos)
+  end
 
 let top bs =
-  match bs.stack with
-    | [] -> None
-    | h::_ -> Some h
+  if bs.size >= 1 then bs.stack.(bs.pos)
+  else error "Nothing on the stack"
 	  
 let app_push bs f =
-  match bs.stack with
-    | [] -> error "Nothing on the stack"
-    | h::_ -> push bs (f h)
+  if bs.size = 0 then error "Nothing on the stack"
+  else push bs (f (bs.stack.(bs.pos)))
 
 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 = []
+  if bs.size = 0 then error "Nothing on the stack"
+  else bs.stack.(bs.pos) <- f (bs.stack.(bs.pos))
 
-let depth bs = List.length bs.stack
+let depth bs = bs.size
diff --git a/lib/bstack.mli b/lib/bstack.mli
index febf7850ed..4f8ba95c44 100644
--- a/lib/bstack.mli
+++ b/lib/bstack.mli
@@ -12,12 +12,10 @@
 
 type 'a t
 
-val create : int option -> 'a t
-val set_depth : 'a t -> int option -> unit
+val create : int -> 'a -> 'a t
 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 pop : 'a t -> unit
+val top : 'a t -> 'a
 val depth : 'a t -> int
diff --git a/lib/edit.ml b/lib/edit.ml
index 04a382a586..6ffc6c850d 100644
--- a/lib/edit.ml
+++ b/lib/edit.ml
@@ -59,9 +59,7 @@ let read e =
     | 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))
+	Some(d,Bstack.top bs,c)
 
 let mutate e f =
   match e.focus with
@@ -82,16 +80,15 @@ let undo e n =
     | 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 ()) ()
+        repeat n Bstack.pop bs;
+	if Bstack.depth bs = 1 then
+          errorlabstrm "Edit.undo" (str"Undo stack exhausted")
 
 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;
+  let bs = Bstack.create udepth b in
   Hashtbl.add e.buf d (bs,c)
 
 let delete e d =
diff --git a/lib/edit.mli b/lib/edit.mli
index 4f3b7803c1..9cf8d62b89 100644
--- a/lib/edit.mli
+++ b/lib/edit.mli
@@ -48,7 +48,7 @@ val rev_mutate : ('a,'b,'c) t -> ('c -> 'b -> 'b) -> unit
   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 create : ('a,'b,'c) t -> 'a * 'b * 'c * int -> unit
 val delete : ('a,'b,'c) t -> 'a -> unit
 
 val dom : ('a,'b,'c) t -> 'a list