diff options
Diffstat (limited to 'lib/heap.ml')
-rw-r--r-- | lib/heap.ml | 134 |
1 files changed, 0 insertions, 134 deletions
diff --git a/lib/heap.ml b/lib/heap.ml deleted file mode 100644 index 97ccadeb..00000000 --- a/lib/heap.ml +++ /dev/null @@ -1,134 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*s 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) = struct - - (* Heaps are encoded as Braun trees, that are binary trees - where size r <= size l <= size r + 1 for each node Node (l, x, r) *) - - type t = - | Leaf - | Node of t * X.t * t - - type elt = X.t - - let empty = Leaf - - let rec add x = function - | Leaf -> - Node (Leaf, x, Leaf) - | Node (l, y, r) -> - if X.compare x y >= 0 then - Node (add y r, x, l) - else - Node (add x r, y, l) - - let rec extract = function - | Leaf -> - assert false - | Node (Leaf, y, r) -> - assert (r = Leaf); - y, Leaf - | Node (l, y, r) -> - let x, l = extract l in - x, Node (r, y, l) - - let is_above x = function - | Leaf -> true - | Node (_, y, _) -> X.compare x y >= 0 - - let rec replace_min x = function - | Node (l, _, r) when is_above x l && is_above x r -> - Node (l, x, r) - | Node ((Node (_, lx, _) as l), _, r) when is_above lx r -> - (* lx <= x, rx necessarily *) - Node (replace_min x l, lx, r) - | Node (l, _, (Node (_, rx, _) as r)) -> - (* rx <= x, lx necessarily *) - Node (l, rx, replace_min x r) - | Leaf | Node (Leaf, _, _) | Node (_, _, Leaf) -> - assert false - - (* merges two Braun trees [l] and [r], - with the assumption that [size r <= size l <= size r + 1] *) - let rec merge l r = match l, r with - | _, Leaf -> - l - | Node (ll, lx, lr), Node (_, ly, _) -> - if X.compare lx ly >= 0 then - Node (r, lx, merge ll lr) - else - let x, l = extract l in - Node (replace_min x r, ly, l) - | Leaf, _ -> - assert false (* contradicts the assumption *) - - let maximum = function - | Leaf -> raise EmptyHeap - | Node (_, x, _) -> x - - let remove = function - | Leaf -> - raise EmptyHeap - | Node (l, _, r) -> - merge l r - - let rec iter f = function - | Leaf -> () - | Node (l, x, r) -> iter f l; f x; iter f r - - let rec fold f h x0 = match h with - | Leaf -> - x0 - | Node (l, x, r) -> - fold f l (fold f r (f x x0)) - -end |