diff options
Diffstat (limited to 'lib/heap.mli')
-rw-r--r-- | lib/heap.mli | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/lib/heap.mli b/lib/heap.mli new file mode 100644 index 00000000..c865461e --- /dev/null +++ b/lib/heap.mli @@ -0,0 +1,54 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: heap.mli,v 1.1.2.1 2004/07/16 19:30:30 herbelin Exp $ *) + +(* Heaps *) + +module type Ordered = sig + type t + val compare : t -> t -> int +end + +module type S =sig + + (* Type of functional heaps *) + type t + + (* Type of elements *) + type elt + + (* The empty heap *) + val empty : t + + (* [add x h] returns a new heap containing the elements of [h], plus [x]; + complexity $O(log(n))$ *) + val add : elt -> t -> t + + (* [maximum h] returns the maximum element of [h]; raises [EmptyHeap] + when [h] is empty; complexity $O(1)$ *) + val maximum : t -> elt + + (* [remove h] returns a new heap containing the elements of [h], except + the maximum of [h]; raises [EmptyHeap] when [h] is empty; + complexity $O(log(n))$ *) + val remove : t -> t + + (* usual iterators and combinators; elements are presented in + arbitrary order *) + val iter : (elt -> unit) -> t -> unit + + val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a + +end + +exception EmptyHeap + +(*S Functional implementation. *) + +module Functional(X: Ordered) : S with type elt=X.t |