diff -r 530e7a33b3dd -r 3b26cc949016 src/Pure/General/heap.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/heap.ML	Tue Jun 20 11:54:22 2000 +0200
@@ -0,0 +1,62 @@
+(* 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;