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