diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /clib/heap.mli | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'clib/heap.mli')
-rw-r--r-- | clib/heap.mli | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/clib/heap.mli b/clib/heap.mli new file mode 100644 index 00000000..ab0864c7 --- /dev/null +++ b/clib/heap.mli @@ -0,0 +1,54 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** 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 + +(** {6 Functional implementation. } *) + +module Functional(X: Ordered) : S with type elt=X.t |