src/Pure/General/heap.ML
 author paulson Fri, 05 Oct 2007 09:59:03 +0200 changeset 24854 0ebcd575d3c6 parent 23179 8db2b22257bd child 28581 6cd2e5d5c6d0 permissions -rw-r--r--
filtering out some package theorems
```
(*  Title:      Pure/General/heap.ML
ID:         \$Id\$
Author:     Markus Wenzel, TU Muenchen

Functional Data Structures" (Chapter 3), Cambridge University Press,
1998.
*)

signature HEAP =
sig
type elem
type T
val empty: T
val is_empty: T -> bool
val merge: T * T -> T
val insert: elem -> T -> T
val min: T -> elem        (*exception Empty*)
val delete_min: T -> T    (*exception Empty*)
end;

functor HeapFun(type elem val ord: elem * elem -> order): HEAP =
struct

(* datatype heap *)

type elem = elem;
datatype T = Empty | Heap of int * elem * T * T;

(* empty heaps *)

val empty = Empty;

fun is_empty Empty = true
| is_empty (Heap _) = false;

(* build heaps *)

local

fun rank Empty = 0
| rank (Heap (r, _, _, _)) = r;

fun heap x a b =
if rank a >= rank b then Heap (rank b + 1, x, a, b)
else Heap (rank a + 1, x, b, a);

in

fun merge (h, Empty) = h
| merge (Empty, h) = h
| merge (h1 as Heap (_, x1, a1, b1), h2 as Heap (_, x2, a2, b2)) =
(case ord (x1, x2) of
GREATER => heap x2 a2 (merge (h1, b2))
| _ => heap x1 a1 (merge (b1, h2)));

fun insert x h = merge (Heap (1, x, Empty, Empty), h);

end;

(* minimum element *)

fun min Empty = raise List.Empty
| min (Heap (_, x, _, _)) = x;

fun delete_min Empty = raise List.Empty
| delete_min (Heap (_, _, a, b)) = merge (a, b);

end;
```