src/Pure/General/heap.ML
author wenzelm
Thu Jul 19 23:18:48 2007 +0200 (2007-07-19)
changeset 23863 8f3099589cfa
parent 23179 8db2b22257bd
child 28581 6cd2e5d5c6d0
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      Pure/General/heap.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Heaps over linearly ordered types.  See also Chris Okasaki: "Purely
     6 Functional Data Structures" (Chapter 3), Cambridge University Press,
     7 1998.
     8 *)
     9 
    10 signature HEAP =
    11 sig
    12   type elem
    13   type T
    14   val empty: T
    15   val is_empty: T -> bool
    16   val merge: T * T -> T
    17   val insert: elem -> T -> T
    18   val min: T -> elem        (*exception Empty*)
    19   val delete_min: T -> T    (*exception Empty*)
    20 end;
    21 
    22 functor HeapFun(type elem val ord: elem * elem -> order): HEAP =
    23 struct
    24 
    25 
    26 (* datatype heap *)
    27 
    28 type elem = elem;
    29 datatype T = Empty | Heap of int * elem * T * T;
    30 
    31 
    32 (* empty heaps *)
    33 
    34 val empty = Empty;
    35 
    36 fun is_empty Empty = true
    37   | is_empty (Heap _) = false;
    38 
    39 
    40 (* build heaps *)
    41 
    42 local
    43 
    44 fun rank Empty = 0
    45   | rank (Heap (r, _, _, _)) = r;
    46 
    47 fun heap x a b =
    48   if rank a >= rank b then Heap (rank b + 1, x, a, b)
    49   else Heap (rank a + 1, x, b, a);
    50 
    51 in
    52 
    53 fun merge (h, Empty) = h
    54   | merge (Empty, h) = h
    55   | merge (h1 as Heap (_, x1, a1, b1), h2 as Heap (_, x2, a2, b2)) =
    56       (case ord (x1, x2) of
    57         GREATER => heap x2 a2 (merge (h1, b2))
    58       | _ => heap x1 a1 (merge (b1, h2)));
    59 
    60 fun insert x h = merge (Heap (1, x, Empty, Empty), h);
    61 
    62 end;
    63 
    64 
    65 (* minimum element *)
    66 
    67 fun min Empty = raise List.Empty
    68   | min (Heap (_, x, _, _)) = x;
    69 
    70 fun delete_min Empty = raise List.Empty
    71   | delete_min (Heap (_, _, a, b)) = merge (a, b);
    72 
    73 end;