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