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