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;