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