module Bstack et Edit

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

1 files changed, 44 insertions, 0 deletions

diff --git a/lib/bstack.ml b/lib/bstack.ml
new file mode 100644
index 0000000000..c67f51092c
--- /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