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

1 files changed, 37 insertions, 25 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