summaryrefslogtreecommitdiff
path: root/lib/deque.mli
diff options
context:
space:
mode:
Diffstat (limited to 'lib/deque.mli')
-rw-r--r--lib/deque.mli58
1 files changed, 58 insertions, 0 deletions
diff --git a/lib/deque.mli b/lib/deque.mli
new file mode 100644
index 00000000..fd644e3c
--- /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-2015 *)
+(* \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 *)