src/Pure/table.ML
author wenzelm
Sun Dec 28 14:55:34 1997 +0100 (1997-12-28)
changeset 4485 697972696f71
parent 4482 43620c417579
permissions -rw-r--r--
tuned;
wenzelm@4482
     1
(*  Title:      Pure/table.ML
wenzelm@4482
     2
    ID:         $Id$
wenzelm@4482
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@4482
     4
wenzelm@4485
     5
Generic tables and tables indexed by strings.  No delete operation.
wenzelm@4485
     6
Implemented as balanced 2-3 trees.
wenzelm@4482
     7
*)
wenzelm@4482
     8
wenzelm@4485
     9
signature KEY =
wenzelm@4482
    10
sig
wenzelm@4482
    11
  type key
wenzelm@4482
    12
  val ord: key * key -> order
wenzelm@4482
    13
end;
wenzelm@4482
    14
wenzelm@4482
    15
signature TABLE =
wenzelm@4482
    16
sig
wenzelm@4482
    17
  type key
wenzelm@4482
    18
  type 'a table
wenzelm@4482
    19
  exception DUP of key
wenzelm@4482
    20
  exception DUPS of key list
wenzelm@4482
    21
  val empty: 'a table
wenzelm@4482
    22
  val is_empty: 'a table -> bool
wenzelm@4482
    23
  val dest: 'a table -> (key * 'a) list
wenzelm@4482
    24
  val lookup: 'a table * key -> 'a option
wenzelm@4482
    25
  val update: (key * 'a) * 'a table -> 'a table
wenzelm@4485
    26
  val update_new: (key * 'a) * 'a table -> 'a table                 (*exception DUP*)
wenzelm@4485
    27
  val make: (key * 'a) list -> 'a table                             (*exception DUPS*)
wenzelm@4485
    28
  val extend: 'a table * (key * 'a) list -> 'a table                (*exception DUPS*)
wenzelm@4485
    29
  val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table   (*exception DUPS*)
wenzelm@4482
    30
  val lookup_multi: 'a list table * key -> 'a list
wenzelm@4482
    31
  val make_multi: (key * 'a) list -> 'a list table
wenzelm@4482
    32
  val dest_multi: 'a list table -> (key * 'a) list
wenzelm@4482
    33
  val map: ('a -> 'b) -> 'a table -> 'b table
wenzelm@4482
    34
end;
wenzelm@4482
    35
wenzelm@4485
    36
functor TableFun(Key: KEY): TABLE =
wenzelm@4482
    37
struct
wenzelm@4482
    38
wenzelm@4482
    39
wenzelm@4482
    40
(* datatype table *)
wenzelm@4482
    41
wenzelm@4485
    42
type key = Key.key;
wenzelm@4482
    43
wenzelm@4482
    44
datatype 'a table =
wenzelm@4482
    45
  Empty |
wenzelm@4482
    46
  Branch2 of 'a table * (key * 'a) * 'a table |
wenzelm@4482
    47
  Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table;
wenzelm@4482
    48
wenzelm@4482
    49
exception DUP of key;
wenzelm@4482
    50
exception DUPS of key list;
wenzelm@4482
    51
wenzelm@4482
    52
wenzelm@4482
    53
val empty = Empty;
wenzelm@4482
    54
wenzelm@4482
    55
fun is_empty Empty = true
wenzelm@4482
    56
  | is_empty _ = false;
wenzelm@4482
    57
wenzelm@4482
    58
fun dest Empty = []
wenzelm@4482
    59
  | dest (Branch2 (left, p, right)) = dest left @ [p] @ dest right
wenzelm@4482
    60
  | dest (Branch3 (left, p1, mid, p2, right)) =
wenzelm@4482
    61
      dest left @ [p1] @ dest mid @ [p2] @ dest right;
wenzelm@4482
    62
wenzelm@4482
    63
wenzelm@4482
    64
(* lookup *)
wenzelm@4482
    65
wenzelm@4482
    66
fun lookup (Empty, _) = None
wenzelm@4482
    67
  | lookup (Branch2 (left, (k, x), right), key) =
wenzelm@4485
    68
      (case Key.ord (key, k) of
wenzelm@4482
    69
        LESS => lookup (left, key)
wenzelm@4482
    70
      | EQUAL => Some x
wenzelm@4482
    71
      | GREATER => lookup (right, key))
wenzelm@4482
    72
  | lookup (Branch3 (left, (k1, x1), mid, (k2, x2), right), key) =
wenzelm@4485
    73
      (case Key.ord (key, k1) of
wenzelm@4482
    74
        LESS => lookup (left, key)
wenzelm@4482
    75
      | EQUAL => Some x1
wenzelm@4482
    76
      | GREATER =>
wenzelm@4485
    77
          (case Key.ord (key, k2) of
wenzelm@4482
    78
            LESS => lookup (mid, key)
wenzelm@4482
    79
          | EQUAL => Some x2
wenzelm@4482
    80
          | GREATER => lookup (right, key)));
wenzelm@4482
    81
wenzelm@4482
    82
wenzelm@4482
    83
(* update *)
wenzelm@4482
    84
wenzelm@4485
    85
fun compare (k1, _) (k2, _) = Key.ord (k1, k2);
wenzelm@4482
    86
wenzelm@4482
    87
datatype 'a growth =
wenzelm@4482
    88
  Stay of 'a table |
wenzelm@4482
    89
  Sprout of 'a table * (key * 'a) * 'a table;
wenzelm@4482
    90
wenzelm@4482
    91
fun insert pair Empty = Sprout (Empty, pair, Empty)
wenzelm@4482
    92
  | insert pair (Branch2 (left, p, right)) =
wenzelm@4482
    93
      (case compare pair p of
wenzelm@4482
    94
        LESS =>
wenzelm@4482
    95
          (case insert pair left of
wenzelm@4482
    96
            Stay left' => Stay (Branch2 (left', p, right))
wenzelm@4482
    97
          | Sprout (left1, q, left2) => Stay (Branch3 (left1, q, left2, p, right)))
wenzelm@4482
    98
      | EQUAL => Stay (Branch2 (left, pair, right))
wenzelm@4482
    99
      | GREATER =>
wenzelm@4482
   100
          (case insert pair right of
wenzelm@4482
   101
            Stay right' => Stay (Branch2 (left, p, right'))
wenzelm@4482
   102
          | Sprout (right1, q, right2) =>
wenzelm@4482
   103
              Stay (Branch3 (left, p, right1, q, right2))))
wenzelm@4482
   104
  | insert pair (Branch3 (left, p1, mid, p2, right)) =
wenzelm@4482
   105
      (case compare pair p1 of
wenzelm@4482
   106
        LESS =>
wenzelm@4482
   107
          (case insert pair left of
wenzelm@4482
   108
            Stay left' => Stay (Branch3 (left', p1, mid, p2, right))
wenzelm@4482
   109
          | Sprout (left1, q, left2) =>
wenzelm@4482
   110
              Sprout (Branch2 (left1, q, left2), p1, Branch2 (mid, p2, right)))
wenzelm@4482
   111
      | EQUAL => Stay (Branch3 (left, pair, mid, p2, right))
wenzelm@4482
   112
      | GREATER =>
wenzelm@4482
   113
          (case compare pair p2 of
wenzelm@4482
   114
            LESS =>
wenzelm@4482
   115
              (case insert pair mid of
wenzelm@4482
   116
                Stay mid' => Stay (Branch3 (left, p1, mid', p2, right))
wenzelm@4482
   117
              | Sprout (mid1, q, mid2) =>
wenzelm@4482
   118
                  Sprout (Branch2 (left, p1, mid1), q, Branch2 (mid2, p2, right)))
wenzelm@4482
   119
          | EQUAL => Stay (Branch3 (left, p1, mid, pair, right))
wenzelm@4482
   120
          | GREATER =>
wenzelm@4482
   121
              (case insert pair right of
wenzelm@4482
   122
                Stay right' => Stay (Branch3 (left, p1, mid, p2, right'))
wenzelm@4482
   123
              | Sprout (right1, q, right2) =>
wenzelm@4482
   124
                  Sprout (Branch2 (left, p1, mid), p2, Branch2 (right1, q, right2)))));
wenzelm@4482
   125
wenzelm@4482
   126
fun update (pair, tab) =
wenzelm@4482
   127
  (case insert pair tab of
wenzelm@4482
   128
    Stay tab => tab
wenzelm@4482
   129
  | Sprout br => Branch2 br);
wenzelm@4482
   130
wenzelm@4482
   131
fun update_new (pair as (key, _), tab) =
wenzelm@4485
   132
  if is_none (lookup (tab, key)) then update (pair, tab)
wenzelm@4485
   133
  else raise DUP key;
wenzelm@4482
   134
wenzelm@4482
   135
wenzelm@4482
   136
(* make, extend, merge tables *)
wenzelm@4482
   137
wenzelm@4482
   138
fun add eq ((tab, dups), (key, x)) =
wenzelm@4482
   139
  (case lookup (tab, key) of
wenzelm@4482
   140
    None => (update ((key, x), tab), dups)
wenzelm@4482
   141
  | Some x' =>
wenzelm@4482
   142
      if eq (x, x') then (tab, dups)
wenzelm@4482
   143
      else (tab, dups @ [key]));
wenzelm@4482
   144
wenzelm@4482
   145
fun enter eq (tab, pairs) =
wenzelm@4482
   146
  (case foldl (add eq) ((tab, []), pairs) of
wenzelm@4482
   147
    (tab', []) => tab'
wenzelm@4482
   148
  | (_, dups) => raise DUPS dups);
wenzelm@4482
   149
wenzelm@4482
   150
fun extend tab_pairs = enter (K false) tab_pairs;
wenzelm@4482
   151
fun make pairs = extend (empty, pairs);
wenzelm@4482
   152
fun merge eq (tab1, tab2) = enter eq (tab1, dest tab2);
wenzelm@4482
   153
wenzelm@4482
   154
wenzelm@4482
   155
(* tables with multiple entries per key (preserving order) *)
wenzelm@4482
   156
wenzelm@4482
   157
fun lookup_multi tab_key = if_none (lookup tab_key) [];
wenzelm@4482
   158
wenzelm@4485
   159
fun cons_entry ((key, x), tab) =
wenzelm@4485
   160
  update ((key, x :: lookup_multi (tab, key)), tab);
wenzelm@4482
   161
wenzelm@4482
   162
fun make_multi pairs = foldr cons_entry (pairs, empty);
wenzelm@4482
   163
wenzelm@4482
   164
fun dest_multi tab =
wenzelm@4485
   165
  flat (map (fn (key, xs) => map (Library.pair key) xs) (dest tab));
wenzelm@4482
   166
wenzelm@4482
   167
wenzelm@4482
   168
(* map *)
wenzelm@4482
   169
wenzelm@4482
   170
fun map _ Empty = Empty
wenzelm@4482
   171
  | map f (Branch2 (left, (k, x), right)) =
wenzelm@4482
   172
      Branch2 (map f left, (k, f x), map f right)
wenzelm@4482
   173
  | map f (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
wenzelm@4482
   174
      Branch3 (map f left, (k1, f x1), map f mid, (k2, f x2), map f right);
wenzelm@4482
   175
wenzelm@4482
   176
wenzelm@4482
   177
end;
wenzelm@4482
   178
wenzelm@4482
   179
wenzelm@4482
   180
(*tables indexed by strings*)
wenzelm@4482
   181
structure Symtab = TableFun(type key = string val ord = string_ord);