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