Added a Deque module to CLib (to be used in CoqIDE).

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

3 files changed, 156 insertions, 0 deletions

diff --git a/lib/clib.mllib b/lib/clib.mllib
index 36059fad38..6ffbd25b13 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -1,6 +1,7 @@
 Coq_config
 Segmenttree
 Unicodetable
+Deque
 Util
 Serialize
 Xml_utils
diff --git a/lib/deque.ml b/lib/deque.ml
new file mode 100644
index 0000000000..f895e63686
--- /dev/null
+++ b/lib/deque.ml
@@ -0,0 +1,97 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+exception Empty
+
+type 'a t = {
+  face : 'a list;
+  rear : 'a list;
+  lenf : int;
+  lenr : int;
+}
+
+let rec split i accu l = match l with
+| [] ->
+  if i = 0 then (accu, []) else invalid_arg "split"
+| t :: q ->
+  if i = 0 then (accu, l)
+  else split (pred i) (t :: accu) q
+
+let balance q =
+  let avg = (q.lenf + q.lenr) / 2 in
+  let dif = q.lenf + q.lenr - avg in
+  if q.lenf > succ (2 * q.lenr) then
+    let (ff, fr) = split avg [] q.face in
+    { face = List.rev ff ; rear = q.rear @ List.rev fr; lenf = avg; lenr = dif }
+  else if q.lenr > succ (2 * q.lenf) then
+    let (rf, rr) = split avg [] q.rear in
+    { face = q.face @ List.rev rr ; rear = List.rev rf; lenf = dif; lenr = avg }
+  else q
+
+let empty = {
+  face = [];
+  rear = [];
+  lenf = 0;
+  lenr = 0;
+}
+
+let lcons x q =
+  balance { q with lenf = succ q.lenf; face = x :: q.face }
+
+let lhd q = match q.face with
+| [] ->
+  begin match q.rear with
+  | [] -> raise Empty
+  | t :: _ -> t
+  end
+| t :: _ -> t
+
+let ltl q = match q.face with
+| [] ->
+  begin match q.rear with
+  | [] -> raise Empty
+  | t :: _ -> empty
+  end
+| t :: r -> balance { q with lenf = pred q.lenf; face = r }
+
+let rcons x q =
+  balance { q with lenr = succ q.lenr; rear = x :: q.rear }
+
+let rhd q = match q.rear with
+| [] ->
+  begin match q.face with
+  | [] -> raise Empty
+  | t :: r -> t
+  end
+| t :: _ -> t
+
+let rtl q = match q.rear with
+| [] ->
+  begin match q.face with
+  | [] -> raise Empty
+  | t :: r -> empty
+  end
+| t :: r ->
+  balance { q with lenr = pred q.lenr; rear = r }
+
+let rev q = {
+  face = q.rear;
+  rear = q.face;
+  lenf = q.lenr;
+  lenr = q.lenf;
+}
+
+let length q = q.lenf + q.lenr
+
+let is_empty q = length q = 0
+
+let filter f q =
+  let fold (accu, len) x = if f x then (x :: accu, succ len) else (accu, len) in
+  let (rf, lenf) = List.fold_left fold ([], 0) q.face in
+  let (rr, lenr) = List.fold_left fold ([], 0) q.rear in
+  balance { face = List.rev rf; rear = List.rev rr; lenf = lenf; lenr = lenr }
diff --git a/lib/deque.mli b/lib/deque.mli
new file mode 100644
index 0000000000..b65dcc4bd1
--- /dev/null
+++ b/lib/deque.mli
@@ -0,0 +1,58 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** * Purely functional, double-ended queues *)
+
+(** This module implements the banker's deque, from Okasaki. Most operations are
+    amortized O(1). *)
+
+type +'a t
+
+exception Empty
+
+(** {5 Constructor} *)
+
+val empty : 'a t
+
+(** The empty deque. *)
+
+(** {5 Left-side operations} *)
+
+val lcons : 'a -> 'a t -> 'a t
+(** Pushes an element on the left side of the deque. *)
+
+val lhd : 'a t -> 'a
+(** Returns the leftmost element in the deque. Raises [Empty] when empty. *)
+
+val ltl : 'a t -> 'a t
+(** Returns the left-tail of the deque. Raises [Empty] when empty. *)
+
+(** {5 Right-side operations} *)
+
+val rcons : 'a -> 'a t -> 'a t
+(** Same as [lcons] but on the right side. *)
+
+val rhd : 'a t -> 'a
+(** Same as [lhd] but on the right side. *)
+
+val rtl : 'a t -> 'a t
+(** Same as [ltl] but on the right side. *)
+
+(** {5 Operations} *)
+
+val rev : 'a t -> 'a t
+(** Reverse deque. *)
+
+val length : 'a t -> int
+(** Length of a deque. *)
+
+val is_empty : 'a t -> bool
+(** Emptyness of a deque. *)
+
+val filter : ('a -> bool) -> 'a t -> 'a t
+(** Filters the deque *)