src/Pure/General/heap.ML
 author paulson Tue, 20 Jun 2000 11:54:22 +0200 changeset 9095 3b26cc949016 child 9413 ba209591a8d4 permissions -rw-r--r--
new module for heaps
```
(* Source code from
*   Purely Functional Data Structures (Chapter 3)
*   Chris Okasaki
*   Cambridge University Press, 1998
*
* Copyright (c) 1998 Cambridge University Press
ID:         \$Id\$
*)

signature ORDERED =
(* a totally ordered type and its comparison functions *)
sig
type T

val eq  : T * T -> bool
val lt  : T * T -> bool
val leq : T * T -> bool
end;

signature HEAP =
sig
structure Elem : ORDERED

type Heap

val empty     : Heap
val isEmpty   : Heap -> bool

val insert    : Elem.T * Heap -> Heap
val merge     : Heap * Heap -> Heap

val findMin   : Heap -> Elem.T   (* raises Empty if heap is empty *)
val deleteMin : Heap -> Heap     (* raises Empty if heap is empty *)
end;

functor LeftistHeap (Element : ORDERED) : HEAP =
struct
structure Elem = Element

datatype Heap = E | T of int * Elem.T * Heap * Heap

fun rank E = 0
| rank (T (r,_,_,_)) = r
fun makeT (x, a, b) = if rank a >= rank b then T (rank b + 1, x, a, b)
else T (rank a + 1, x, b, a)

val empty = E
fun isEmpty E = true | isEmpty _ = false

fun merge (h, E) = h
| merge (E, h) = h
| merge (h1 as T (_, x, a1, b1), h2 as T (_, y, a2, b2)) =
if Elem.leq (x, y) then makeT (x, a1, merge (b1, h2))
else makeT (y, a2, merge (h1, b2))

fun insert (x, h) = merge (T (1, x, E, E), h)

fun findMin E = raise List.Empty
| findMin (T (_, x, a, b)) = x
fun deleteMin E = raise List.Empty
| deleteMin (T (_, x, a, b)) = merge (a, b)
end;
```