wenzelm@9413: (*  Title:      Pure/General/heap.ML
paulson@9095:     ID:         $Id$
wenzelm@9413:     Author:     Markus Wenzel, TU Muenchen
paulson@9095: 
wenzelm@9413: Heaps over linearly ordered types.  See also Chris Okasaki: "Purely
wenzelm@9413: Functional Data Structures" (Chapter 3), Cambridge University Press,
wenzelm@9413: 1998.
wenzelm@9413: *)
paulson@9095: 
paulson@9095: signature HEAP =
paulson@9095: sig
wenzelm@9413:   type elem
wenzelm@9413:   type T
wenzelm@9413:   val empty: T
wenzelm@9413:   val is_empty: T -> bool
wenzelm@9413:   val merge: T * T -> T
wenzelm@23179:   val insert: elem -> T -> T
wenzelm@18134:   val min: T -> elem        (*exception Empty*)
wenzelm@18134:   val delete_min: T -> T    (*exception Empty*)
paulson@9095: end;
paulson@9095: 
wenzelm@9413: functor HeapFun(type elem val ord: elem * elem -> order): HEAP =
paulson@9095: struct
wenzelm@9413: 
wenzelm@9413: 
wenzelm@9413: (* datatype heap *)
paulson@9095: 
wenzelm@9413: type elem = elem;
wenzelm@9413: datatype T = Empty | Heap of int * elem * T * T;
wenzelm@9413: 
wenzelm@9413: 
wenzelm@9413: (* empty heaps *)
paulson@9095: 
wenzelm@9413: val empty = Empty;
wenzelm@9413: 
wenzelm@9413: fun is_empty Empty = true
wenzelm@9413:   | is_empty (Heap _) = false;
wenzelm@9413: 
paulson@9095: 
wenzelm@9413: (* build heaps *)
wenzelm@9413: 
wenzelm@9413: local
wenzelm@9413: 
wenzelm@9413: fun rank Empty = 0
wenzelm@9413:   | rank (Heap (r, _, _, _)) = r;
paulson@9095: 
wenzelm@9413: fun heap x a b =
wenzelm@9413:   if rank a >= rank b then Heap (rank b + 1, x, a, b)
wenzelm@9413:   else Heap (rank a + 1, x, b, a);
wenzelm@9413: 
wenzelm@9413: in
wenzelm@9413: 
wenzelm@9413: fun merge (h, Empty) = h
wenzelm@9413:   | merge (Empty, h) = h
wenzelm@9413:   | merge (h1 as Heap (_, x1, a1, b1), h2 as Heap (_, x2, a2, b2)) =
wenzelm@9413:       (case ord (x1, x2) of
paulson@14472:         GREATER => heap x2 a2 (merge (h1, b2))
wenzelm@9413:       | _ => heap x1 a1 (merge (b1, h2)));
wenzelm@9413: 
wenzelm@23179: fun insert x h = merge (Heap (1, x, Empty, Empty), h);
paulson@9095: 
wenzelm@9413: end;
wenzelm@9413: 
wenzelm@9413: 
wenzelm@9413: (* minimum element *)
wenzelm@9413: 
wenzelm@18134: fun min Empty = raise List.Empty
wenzelm@9413:   | min (Heap (_, x, _, _)) = x;
wenzelm@9413: 
wenzelm@18134: fun delete_min Empty = raise List.Empty
wenzelm@9413:   | delete_min (Heap (_, _, a, b)) = merge (a, b);
wenzelm@9413: 
paulson@9095: end;