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