src/Pure/General/table.ML
author wenzelm
Thu Apr 03 18:42:36 2008 +0200 (2008-04-03)
changeset 26538 d65504ffb47d
parent 25391 783e5de2a6c7
child 27508 abdab08677d8
permissions -rw-r--r--
replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm@6118
     1
(*  Title:      Pure/General/table.ML
wenzelm@5015
     2
    ID:         $Id$
berghofe@15014
     3
    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
wenzelm@5015
     4
wenzelm@16342
     5
Generic tables.  Efficient purely functional implementation using
wenzelm@16342
     6
balanced 2-3 trees.
wenzelm@5015
     7
*)
wenzelm@5015
     8
wenzelm@5015
     9
signature KEY =
wenzelm@5015
    10
sig
wenzelm@5015
    11
  type key
wenzelm@5015
    12
  val ord: key * key -> order
wenzelm@5015
    13
end;
wenzelm@5015
    14
wenzelm@5015
    15
signature TABLE =
wenzelm@5015
    16
sig
wenzelm@5015
    17
  type key
wenzelm@5015
    18
  type 'a table
wenzelm@5015
    19
  exception DUP of key
wenzelm@19031
    20
  exception SAME
berghofe@15014
    21
  exception UNDEF of key
wenzelm@5015
    22
  val empty: 'a table
wenzelm@5015
    23
  val is_empty: 'a table -> bool
wenzelm@5681
    24
  val map: ('a -> 'b) -> 'a table -> 'b table
wenzelm@16446
    25
  val map': (key -> 'a -> 'b) -> 'a table -> 'b table
wenzelm@16446
    26
  val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
haftmann@17579
    27
  val fold_map: (key * 'b -> 'a -> 'c * 'a) -> 'b table -> 'a -> 'c table * 'a
wenzelm@5015
    28
  val dest: 'a table -> (key * 'a) list
wenzelm@5681
    29
  val keys: 'a table -> key list
berghofe@8409
    30
  val min_key: 'a table -> key option
obua@15160
    31
  val max_key: 'a table -> key option
wenzelm@7061
    32
  val exists: (key * 'a -> bool) -> 'a table -> bool
wenzelm@16192
    33
  val forall: (key * 'a -> bool) -> 'a table -> bool
wenzelm@16887
    34
  val defined: 'a table -> key -> bool
wenzelm@17412
    35
  val lookup: 'a table -> key -> 'a option
wenzelm@17412
    36
  val update: (key * 'a) -> 'a table -> 'a table
wenzelm@17412
    37
  val update_new: (key * 'a) -> 'a table -> 'a table                   (*exception DUP*)
haftmann@17179
    38
  val default: key * 'a -> 'a table -> 'a table
wenzelm@15665
    39
  val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table
haftmann@20141
    40
  val map_default: (key * 'a) -> ('a -> 'a) -> 'a table -> 'a table
wenzelm@23655
    41
  val make: (key * 'a) list -> 'a table                                (*exception DUP*)
wenzelm@23655
    42
  val extend: 'a table * (key * 'a) list -> 'a table                   (*exception DUP*)
wenzelm@19031
    43
  val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
wenzelm@23655
    44
    'a table * 'a table -> 'a table                                    (*exception DUP*)
wenzelm@23655
    45
  val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table      (*exception DUP*)
wenzelm@15665
    46
  val delete: key -> 'a table -> 'a table                              (*exception UNDEF*)
wenzelm@15761
    47
  val delete_safe: key -> 'a table -> 'a table
wenzelm@16466
    48
  val member: ('b * 'a -> bool) -> 'a table -> key * 'b -> bool
wenzelm@15761
    49
  val insert: ('a * 'a -> bool) -> key * 'a -> 'a table -> 'a table    (*exception DUP*)
wenzelm@16139
    50
  val remove: ('b * 'a -> bool) -> key * 'b -> 'a table -> 'a table
wenzelm@18946
    51
  val lookup_list: 'a list table -> key -> 'a list
wenzelm@25391
    52
  val cons_list: (key * 'a) -> 'a list table -> 'a list table
wenzelm@19506
    53
  val insert_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table
wenzelm@18946
    54
  val remove_list: ('b * 'a -> bool) -> key * 'b -> 'a list table -> 'a list table
wenzelm@25391
    55
  val update_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table
wenzelm@18946
    56
  val make_list: (key * 'a) list -> 'a list table
wenzelm@18946
    57
  val dest_list: 'a list table -> (key * 'a) list
wenzelm@18946
    58
  val merge_list: ('a * 'a -> bool) ->
wenzelm@23655
    59
    'a list table * 'a list table -> 'a list table                     (*exception DUP*)
wenzelm@5015
    60
end;
wenzelm@5015
    61
wenzelm@5015
    62
functor TableFun(Key: KEY): TABLE =
wenzelm@5015
    63
struct
wenzelm@5015
    64
wenzelm@5015
    65
wenzelm@5015
    66
(* datatype table *)
wenzelm@5015
    67
wenzelm@5015
    68
type key = Key.key;
wenzelm@5015
    69
wenzelm@5015
    70
datatype 'a table =
wenzelm@5015
    71
  Empty |
wenzelm@5015
    72
  Branch2 of 'a table * (key * 'a) * 'a table |
wenzelm@5015
    73
  Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table;
wenzelm@5015
    74
wenzelm@5015
    75
exception DUP of key;
wenzelm@5015
    76
wenzelm@5015
    77
wenzelm@5681
    78
(* empty *)
wenzelm@5681
    79
wenzelm@5015
    80
val empty = Empty;
wenzelm@5015
    81
wenzelm@5015
    82
fun is_empty Empty = true
wenzelm@5015
    83
  | is_empty _ = false;
wenzelm@5015
    84
wenzelm@5681
    85
wenzelm@5681
    86
(* map and fold combinators *)
wenzelm@5681
    87
wenzelm@16657
    88
fun map_table f =
wenzelm@16657
    89
  let
wenzelm@16657
    90
    fun map Empty = Empty
wenzelm@16657
    91
      | map (Branch2 (left, (k, x), right)) =
wenzelm@16657
    92
          Branch2 (map left, (k, f k x), map right)
wenzelm@16657
    93
      | map (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
wenzelm@16657
    94
          Branch3 (map left, (k1, f k1 x1), map mid, (k2, f k2 x2), map right);
wenzelm@16657
    95
  in map end;
wenzelm@5681
    96
wenzelm@16657
    97
fun fold_table f =
wenzelm@16657
    98
  let
wenzelm@16657
    99
    fun fold Empty x = x
wenzelm@16657
   100
      | fold (Branch2 (left, p, right)) x =
wenzelm@16657
   101
          fold right (f p (fold left x))
wenzelm@16657
   102
      | fold (Branch3 (left, p1, mid, p2, right)) x =
wenzelm@16657
   103
          fold right (f p2 (fold mid (f p1 (fold left x))));
wenzelm@16657
   104
  in fold end;
wenzelm@5681
   105
wenzelm@17709
   106
fun fold_map_table f =
haftmann@17579
   107
  let
haftmann@17579
   108
    fun fold_map Empty s = (Empty, s)
haftmann@17579
   109
      | fold_map (Branch2 (left, p as (k, x), right)) s =
haftmann@17579
   110
          s
haftmann@17579
   111
          |> fold_map left
haftmann@17579
   112
          ||>> f p
haftmann@17579
   113
          ||>> fold_map right
haftmann@17579
   114
          |-> (fn ((l, e), r) => pair (Branch2 (l, (k, e), r)))
haftmann@17579
   115
      | fold_map (Branch3 (left, p1 as (k1, x1), mid, p2 as (k2, x2), right)) s =
haftmann@17579
   116
          s
haftmann@17579
   117
          |> fold_map left
haftmann@17579
   118
          ||>> f p1
haftmann@17579
   119
          ||>> fold_map mid
haftmann@17579
   120
          ||>> f p2
haftmann@17579
   121
          ||>> fold_map right
haftmann@17579
   122
          |-> (fn ((((l, e1), m), e2), r) => pair (Branch3 (l, (k1, e1), m, (k2, e2), r)))
haftmann@17579
   123
  in fold_map end;
haftmann@17579
   124
wenzelm@16446
   125
fun dest tab = rev (fold_table cons tab []);
wenzelm@16446
   126
fun keys tab = rev (fold_table (cons o #1) tab []);
wenzelm@16192
   127
wenzelm@16192
   128
local exception TRUE in
wenzelm@16192
   129
wenzelm@16192
   130
fun exists pred tab =
wenzelm@16446
   131
  (fold_table (fn p => fn () => if pred p then raise TRUE else ()) tab (); false)
wenzelm@16192
   132
    handle TRUE => true;
wenzelm@16192
   133
wenzelm@16192
   134
fun forall pred = not o exists (not o pred);
wenzelm@16192
   135
wenzelm@16192
   136
end;
wenzelm@5015
   137
skalberg@15531
   138
fun min_key Empty = NONE
wenzelm@16864
   139
  | min_key (Branch2 (Empty, (k, _), _)) = SOME k
wenzelm@16864
   140
  | min_key (Branch3 (Empty, (k, _), _, _, _)) = SOME k
wenzelm@16864
   141
  | min_key (Branch2 (left, _, _)) = min_key left
wenzelm@16864
   142
  | min_key (Branch3 (left, _, _, _, _)) = min_key left;
berghofe@8409
   143
skalberg@15531
   144
fun max_key Empty = NONE
wenzelm@16864
   145
  | max_key (Branch2 (_, (k, _), Empty)) = SOME k
wenzelm@16864
   146
  | max_key (Branch3 (_, _, _, (k, _), Empty)) = SOME k
wenzelm@16864
   147
  | max_key (Branch2 (_, _, right)) = max_key right
wenzelm@16864
   148
  | max_key (Branch3 (_, _, _, _, right)) = max_key right;
wenzelm@15665
   149
wenzelm@5015
   150
wenzelm@5015
   151
(* lookup *)
wenzelm@5015
   152
wenzelm@19031
   153
fun lookup tab key =
wenzelm@19031
   154
  let
wenzelm@19031
   155
    fun look Empty = NONE
wenzelm@19031
   156
      | look (Branch2 (left, (k, x), right)) =
wenzelm@19031
   157
          (case Key.ord (key, k) of
wenzelm@19031
   158
            LESS => look left
wenzelm@19031
   159
          | EQUAL => SOME x
wenzelm@19031
   160
          | GREATER => look right)
wenzelm@19031
   161
      | look (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
wenzelm@19031
   162
          (case Key.ord (key, k1) of
wenzelm@19031
   163
            LESS => look left
wenzelm@19031
   164
          | EQUAL => SOME x1
wenzelm@19031
   165
          | GREATER =>
wenzelm@19031
   166
              (case Key.ord (key, k2) of
wenzelm@19031
   167
                LESS => look mid
wenzelm@19031
   168
              | EQUAL => SOME x2
wenzelm@19031
   169
              | GREATER => look right));
wenzelm@19031
   170
  in look tab end;
wenzelm@5015
   171
wenzelm@19031
   172
fun defined tab key =
wenzelm@19031
   173
  let
wenzelm@19031
   174
    fun def Empty = false
wenzelm@19031
   175
      | def (Branch2 (left, (k, x), right)) =
wenzelm@19031
   176
          (case Key.ord (key, k) of
wenzelm@19031
   177
            LESS => def left
wenzelm@19031
   178
          | EQUAL => true
wenzelm@19031
   179
          | GREATER => def right)
wenzelm@19031
   180
      | def (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
wenzelm@19031
   181
          (case Key.ord (key, k1) of
wenzelm@19031
   182
            LESS => def left
wenzelm@19031
   183
          | EQUAL => true
wenzelm@19031
   184
          | GREATER =>
wenzelm@19031
   185
              (case Key.ord (key, k2) of
wenzelm@19031
   186
                LESS => def mid
wenzelm@19031
   187
              | EQUAL => true
wenzelm@19031
   188
              | GREATER => def right));
wenzelm@19031
   189
  in def tab end;
wenzelm@16887
   190
wenzelm@5015
   191
wenzelm@19031
   192
(* modify *)
wenzelm@5015
   193
wenzelm@5015
   194
datatype 'a growth =
wenzelm@5015
   195
  Stay of 'a table |
wenzelm@5015
   196
  Sprout of 'a table * (key * 'a) * 'a table;
wenzelm@5015
   197
wenzelm@15761
   198
exception SAME;
wenzelm@15761
   199
wenzelm@15665
   200
fun modify key f tab =
wenzelm@15665
   201
  let
wenzelm@15665
   202
    fun modfy Empty = Sprout (Empty, (key, f NONE), Empty)
wenzelm@15665
   203
      | modfy (Branch2 (left, p as (k, x), right)) =
wenzelm@15665
   204
          (case Key.ord (key, k) of
wenzelm@15665
   205
            LESS =>
wenzelm@15665
   206
              (case modfy left of
wenzelm@15665
   207
                Stay left' => Stay (Branch2 (left', p, right))
wenzelm@15665
   208
              | Sprout (left1, q, left2) => Stay (Branch3 (left1, q, left2, p, right)))
wenzelm@15665
   209
          | EQUAL => Stay (Branch2 (left, (k, f (SOME x)), right))
wenzelm@15665
   210
          | GREATER =>
wenzelm@15665
   211
              (case modfy right of
wenzelm@15665
   212
                Stay right' => Stay (Branch2 (left, p, right'))
wenzelm@15665
   213
              | Sprout (right1, q, right2) =>
wenzelm@15665
   214
                  Stay (Branch3 (left, p, right1, q, right2))))
wenzelm@15665
   215
      | modfy (Branch3 (left, p1 as (k1, x1), mid, p2 as (k2, x2), right)) =
wenzelm@15665
   216
          (case Key.ord (key, k1) of
wenzelm@5015
   217
            LESS =>
wenzelm@15665
   218
              (case modfy left of
wenzelm@15665
   219
                Stay left' => Stay (Branch3 (left', p1, mid, p2, right))
wenzelm@15665
   220
              | Sprout (left1, q, left2) =>
wenzelm@15665
   221
                  Sprout (Branch2 (left1, q, left2), p1, Branch2 (mid, p2, right)))
wenzelm@15665
   222
          | EQUAL => Stay (Branch3 (left, (k1, f (SOME x1)), mid, p2, right))
wenzelm@5015
   223
          | GREATER =>
wenzelm@15665
   224
              (case Key.ord (key, k2) of
wenzelm@15665
   225
                LESS =>
wenzelm@15665
   226
                  (case modfy mid of
wenzelm@15665
   227
                    Stay mid' => Stay (Branch3 (left, p1, mid', p2, right))
wenzelm@15665
   228
                  | Sprout (mid1, q, mid2) =>
wenzelm@15665
   229
                      Sprout (Branch2 (left, p1, mid1), q, Branch2 (mid2, p2, right)))
wenzelm@15665
   230
              | EQUAL => Stay (Branch3 (left, p1, mid, (k2, f (SOME x2)), right))
wenzelm@15665
   231
              | GREATER =>
wenzelm@15665
   232
                  (case modfy right of
wenzelm@15665
   233
                    Stay right' => Stay (Branch3 (left, p1, mid, p2, right'))
wenzelm@15665
   234
                  | Sprout (right1, q, right2) =>
wenzelm@15665
   235
                      Sprout (Branch2 (left, p1, mid), p2, Branch2 (right1, q, right2)))));
wenzelm@5015
   236
wenzelm@15665
   237
  in
wenzelm@15665
   238
    (case modfy tab of
wenzelm@15665
   239
      Stay tab' => tab'
wenzelm@15665
   240
    | Sprout br => Branch2 br)
wenzelm@15665
   241
    handle SAME => tab
wenzelm@15665
   242
  end;
wenzelm@5015
   243
wenzelm@17412
   244
fun update (key, x) tab = modify key (fn _ => x) tab;
wenzelm@17412
   245
fun update_new (key, x) tab = modify key (fn NONE => x | SOME _ => raise DUP key) tab;
wenzelm@17709
   246
fun default (key, x) tab = modify key (fn NONE => x | SOME _ => raise SAME) tab;
wenzelm@15761
   247
fun map_entry key f = modify key (fn NONE => raise SAME | SOME x => f x);
haftmann@20141
   248
fun map_default (key, x) f = modify key (fn NONE => f x | SOME x => f x);
wenzelm@5015
   249
wenzelm@5015
   250
berghofe@15014
   251
(* delete *)
berghofe@15014
   252
wenzelm@15665
   253
exception UNDEF of key;
wenzelm@15665
   254
wenzelm@15665
   255
local
wenzelm@15665
   256
wenzelm@15665
   257
fun compare NONE (k2, _) = LESS
wenzelm@15665
   258
  | compare (SOME k1) (k2, _) = Key.ord (k1, k2);
berghofe@15014
   259
berghofe@15014
   260
fun if_eq EQUAL x y = x
berghofe@15014
   261
  | if_eq _ x y = y;
berghofe@15014
   262
skalberg@15531
   263
fun del (SOME k) Empty = raise UNDEF k
skalberg@15531
   264
  | del NONE (Branch2 (Empty, p, Empty)) = (p, (true, Empty))
skalberg@15531
   265
  | del NONE (Branch3 (Empty, p, Empty, q, Empty)) =
berghofe@15014
   266
      (p, (false, Branch2 (Empty, q, Empty)))
wenzelm@15665
   267
  | del k (Branch2 (Empty, p, Empty)) = (case compare k p of
wenzelm@16002
   268
      EQUAL => (p, (true, Empty)) | _ => raise UNDEF (the k))
wenzelm@15665
   269
  | del k (Branch3 (Empty, p, Empty, q, Empty)) = (case compare k p of
berghofe@15014
   270
      EQUAL => (p, (false, Branch2 (Empty, q, Empty)))
wenzelm@15665
   271
    | _ => (case compare k q of
berghofe@15014
   272
        EQUAL => (q, (false, Branch2 (Empty, p, Empty)))
wenzelm@16002
   273
      | _ => raise UNDEF (the k)))
wenzelm@15665
   274
  | del k (Branch2 (l, p, r)) = (case compare k p of
berghofe@15014
   275
      LESS => (case del k l of
berghofe@15014
   276
        (p', (false, l')) => (p', (false, Branch2 (l', p, r)))
berghofe@15014
   277
      | (p', (true, l')) => (p', case r of
berghofe@15014
   278
          Branch2 (rl, rp, rr) =>
berghofe@15014
   279
            (true, Branch3 (l', p, rl, rp, rr))
berghofe@15014
   280
        | Branch3 (rl, rp, rm, rq, rr) => (false, Branch2
berghofe@15014
   281
            (Branch2 (l', p, rl), rp, Branch2 (rm, rq, rr)))))
skalberg@15531
   282
    | ord => (case del (if_eq ord NONE k) r of
berghofe@15014
   283
        (p', (false, r')) => (p', (false, Branch2 (l, if_eq ord p' p, r')))
berghofe@15014
   284
      | (p', (true, r')) => (p', case l of
berghofe@15014
   285
          Branch2 (ll, lp, lr) =>
berghofe@15014
   286
            (true, Branch3 (ll, lp, lr, if_eq ord p' p, r'))
berghofe@15014
   287
        | Branch3 (ll, lp, lm, lq, lr) => (false, Branch2
berghofe@15014
   288
            (Branch2 (ll, lp, lm), lq, Branch2 (lr, if_eq ord p' p, r'))))))
wenzelm@15665
   289
  | del k (Branch3 (l, p, m, q, r)) = (case compare k q of
wenzelm@15665
   290
      LESS => (case compare k p of
berghofe@15014
   291
        LESS => (case del k l of
berghofe@15014
   292
          (p', (false, l')) => (p', (false, Branch3 (l', p, m, q, r)))
berghofe@15014
   293
        | (p', (true, l')) => (p', (false, case (m, r) of
berghofe@15014
   294
            (Branch2 (ml, mp, mr), Branch2 _) =>
berghofe@15014
   295
              Branch2 (Branch3 (l', p, ml, mp, mr), q, r)
berghofe@15014
   296
          | (Branch3 (ml, mp, mm, mq, mr), _) =>
berghofe@15014
   297
              Branch3 (Branch2 (l', p, ml), mp, Branch2 (mm, mq, mr), q, r)
berghofe@15014
   298
          | (Branch2 (ml, mp, mr), Branch3 (rl, rp, rm, rq, rr)) =>
berghofe@15014
   299
              Branch3 (Branch2 (l', p, ml), mp, Branch2 (mr, q, rl), rp,
berghofe@15014
   300
                Branch2 (rm, rq, rr)))))
skalberg@15531
   301
      | ord => (case del (if_eq ord NONE k) m of
berghofe@15014
   302
          (p', (false, m')) =>
berghofe@15014
   303
            (p', (false, Branch3 (l, if_eq ord p' p, m', q, r)))
berghofe@15014
   304
        | (p', (true, m')) => (p', (false, case (l, r) of
berghofe@15014
   305
            (Branch2 (ll, lp, lr), Branch2 _) =>
berghofe@15014
   306
              Branch2 (Branch3 (ll, lp, lr, if_eq ord p' p, m'), q, r)
berghofe@15014
   307
          | (Branch3 (ll, lp, lm, lq, lr), _) =>
berghofe@15014
   308
              Branch3 (Branch2 (ll, lp, lm), lq,
berghofe@15014
   309
                Branch2 (lr, if_eq ord p' p, m'), q, r)
berghofe@15014
   310
          | (_, Branch3 (rl, rp, rm, rq, rr)) =>
berghofe@15014
   311
              Branch3 (l, if_eq ord p' p, Branch2 (m', q, rl), rp,
berghofe@15014
   312
                Branch2 (rm, rq, rr))))))
skalberg@15531
   313
    | ord => (case del (if_eq ord NONE k) r of
berghofe@15014
   314
        (q', (false, r')) =>
berghofe@15014
   315
          (q', (false, Branch3 (l, p, m, if_eq ord q' q, r')))
berghofe@15014
   316
      | (q', (true, r')) => (q', (false, case (l, m) of
berghofe@15014
   317
          (Branch2 _, Branch2 (ml, mp, mr)) =>
berghofe@15014
   318
            Branch2 (l, p, Branch3 (ml, mp, mr, if_eq ord q' q, r'))
berghofe@15014
   319
        | (_, Branch3 (ml, mp, mm, mq, mr)) =>
berghofe@15014
   320
            Branch3 (l, p, Branch2 (ml, mp, mm), mq,
berghofe@15014
   321
              Branch2 (mr, if_eq ord q' q, r'))
berghofe@15014
   322
        | (Branch3 (ll, lp, lm, lq, lr), Branch2 (ml, mp, mr)) =>
berghofe@15014
   323
            Branch3 (Branch2 (ll, lp, lm), lq, Branch2 (lr, p, ml), mp,
berghofe@15014
   324
              Branch2 (mr, if_eq ord q' q, r'))))));
berghofe@15014
   325
wenzelm@15665
   326
in
wenzelm@15665
   327
wenzelm@15761
   328
fun delete key tab = snd (snd (del (SOME key) tab));
wenzelm@15761
   329
fun delete_safe key tab = delete key tab handle UNDEF _ => tab;
berghofe@15014
   330
wenzelm@15665
   331
end;
wenzelm@15665
   332
berghofe@15014
   333
wenzelm@19031
   334
(* membership operations *)
wenzelm@16466
   335
wenzelm@16466
   336
fun member eq tab (key, x) =
wenzelm@17412
   337
  (case lookup tab key of
wenzelm@16466
   338
    NONE => false
wenzelm@16466
   339
  | SOME y => eq (x, y));
wenzelm@15761
   340
wenzelm@15761
   341
fun insert eq (key, x) =
wenzelm@15761
   342
  modify key (fn NONE => x | SOME y => if eq (x, y) then raise SAME else raise DUP key);
wenzelm@15761
   343
wenzelm@15761
   344
fun remove eq (key, x) tab =
wenzelm@17412
   345
  (case lookup tab key of
wenzelm@15761
   346
    NONE => tab
wenzelm@15761
   347
  | SOME y => if eq (x, y) then delete key tab else tab);
wenzelm@15761
   348
wenzelm@15761
   349
wenzelm@19031
   350
(* simultaneous modifications *)
wenzelm@19031
   351
wenzelm@23655
   352
fun extend (table, args) = fold update_new args table;
wenzelm@19031
   353
wenzelm@19031
   354
fun make entries = extend (empty, entries);
wenzelm@5015
   355
wenzelm@12287
   356
fun join f (table1, table2) =
wenzelm@23655
   357
  let fun add (key, y) tab = modify key (fn NONE => y | SOME x => f key (x, y)) tab;
wenzelm@23655
   358
  in fold_table add table2 table1 end;
wenzelm@12287
   359
wenzelm@19031
   360
fun merge eq = join (fn key => fn xy => if eq xy then raise SAME else raise DUP key);
wenzelm@5015
   361
wenzelm@5015
   362
wenzelm@19031
   363
(* list tables *)
wenzelm@15761
   364
wenzelm@18946
   365
fun lookup_list tab key = these (lookup tab key);
wenzelm@25391
   366
wenzelm@25391
   367
fun cons_list (key, x) tab = modify key (fn NONE => [x] | SOME xs => x :: xs) tab;
wenzelm@5015
   368
wenzelm@20124
   369
fun insert_list eq (key, x) =
wenzelm@20124
   370
  modify key (fn NONE => [x] | SOME xs => if Library.member eq xs x then raise SAME else x :: xs);
wenzelm@25391
   371
wenzelm@18946
   372
fun remove_list eq (key, x) tab =
wenzelm@15761
   373
  map_entry key (fn xs => (case Library.remove eq x xs of [] => raise UNDEF key | ys => ys)) tab
wenzelm@15761
   374
  handle UNDEF _ => delete key tab;
wenzelm@5015
   375
wenzelm@25391
   376
fun update_list eq (key, x) =
wenzelm@25391
   377
  modify key (fn NONE => [x] | SOME [] => [x] | SOME (xs as y :: _) =>
wenzelm@25391
   378
    if eq (x, y) then raise SAME else Library.update eq x xs);
wenzelm@25391
   379
wenzelm@25391
   380
fun make_list args = fold_rev cons_list args empty;
wenzelm@19482
   381
fun dest_list tab = maps (fn (key, xs) => map (pair key) xs) (dest tab);
wenzelm@19031
   382
fun merge_list eq = join (fn _ => Library.merge eq);
wenzelm@5015
   383
wenzelm@5015
   384
wenzelm@5681
   385
(*final declarations of this structure!*)
wenzelm@16446
   386
fun map f = map_table (K f);
wenzelm@16446
   387
val map' = map_table;
wenzelm@16446
   388
val fold = fold_table;
haftmann@17579
   389
val fold_map = fold_map_table;
wenzelm@5015
   390
wenzelm@5015
   391
end;
wenzelm@5015
   392
wenzelm@16342
   393
structure Inttab = TableFun(type key = int val ord = int_ord);
wenzelm@16687
   394
structure Symtab = TableFun(type key = string val ord = fast_string_ord);