src/Pure/General/table.ML
author wenzelm
Fri Dec 14 11:52:54 2001 +0100 (2001-12-14)
changeset 12498 3b0091bf06e8
parent 12287 7017cee2f3ac
child 14981 e73f8140af78
permissions -rw-r--r--
changed Thm.varifyT';
wenzelm@6118
     1
(*  Title:      Pure/General/table.ML
wenzelm@5015
     2
    ID:         $Id$
wenzelm@5015
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@8806
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@5015
     5
wenzelm@8806
     6
Generic tables and tables indexed by strings.  Efficient purely
wenzelm@8806
     7
functional implementation using balanced 2-3 trees.  No delete
wenzelm@8806
     8
operation (may store options instead).
wenzelm@5015
     9
*)
wenzelm@5015
    10
wenzelm@5015
    11
signature KEY =
wenzelm@5015
    12
sig
wenzelm@5015
    13
  type key
wenzelm@5015
    14
  val ord: key * key -> order
wenzelm@5015
    15
end;
wenzelm@5015
    16
wenzelm@5015
    17
signature TABLE =
wenzelm@5015
    18
sig
wenzelm@5015
    19
  type key
wenzelm@5015
    20
  type 'a table
wenzelm@5015
    21
  exception DUP of key
wenzelm@5015
    22
  exception DUPS of key list
wenzelm@5015
    23
  val empty: 'a table
wenzelm@5015
    24
  val is_empty: 'a table -> bool
wenzelm@5681
    25
  val map: ('a -> 'b) -> 'a table -> 'b table
wenzelm@5681
    26
  val foldl: ('a * (key * 'b) -> 'a) -> 'a * 'b table -> 'a
wenzelm@5015
    27
  val dest: 'a table -> (key * 'a) list
wenzelm@5681
    28
  val keys: 'a table -> key list
berghofe@8409
    29
  val min_key: 'a table -> key option
wenzelm@7061
    30
  val exists: (key * 'a -> bool) -> 'a table -> bool
wenzelm@5015
    31
  val lookup: 'a table * key -> 'a option
wenzelm@5015
    32
  val update: (key * 'a) * 'a table -> 'a table
wenzelm@12287
    33
  val update_new: (key * 'a) * 'a table -> 'a table                    (*exception DUP*)
wenzelm@12287
    34
  val make: (key * 'a) list -> 'a table                                (*exception DUPS*)
wenzelm@12287
    35
  val extend: 'a table * (key * 'a) list -> 'a table                   (*exception DUPS*)
wenzelm@12287
    36
  val join: ('a * 'a -> 'a option) -> 'a table * 'a table -> 'a table  (*exception DUPS*)
wenzelm@12287
    37
  val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table      (*exception DUPS*)
wenzelm@5015
    38
  val lookup_multi: 'a list table * key -> 'a list
wenzelm@8606
    39
  val update_multi: (key * 'a) * 'a list table -> 'a list table
wenzelm@5015
    40
  val make_multi: (key * 'a) list -> 'a list table
wenzelm@5015
    41
  val dest_multi: 'a list table -> (key * 'a) list
wenzelm@12287
    42
  val merge_multi: ('a * 'a -> bool) ->
wenzelm@12287
    43
    'a list table * 'a list table -> 'a list table    (*exception DUPS*)
wenzelm@12287
    44
  val merge_multi': ('a * 'a -> bool) ->
wenzelm@12287
    45
    'a list table * 'a list table -> 'a list table    (*exception DUPS*)
wenzelm@5015
    46
end;
wenzelm@5015
    47
wenzelm@5015
    48
functor TableFun(Key: KEY): TABLE =
wenzelm@5015
    49
struct
wenzelm@5015
    50
wenzelm@5015
    51
wenzelm@5015
    52
(* datatype table *)
wenzelm@5015
    53
wenzelm@5015
    54
type key = Key.key;
wenzelm@5015
    55
wenzelm@5015
    56
datatype 'a table =
wenzelm@5015
    57
  Empty |
wenzelm@5015
    58
  Branch2 of 'a table * (key * 'a) * 'a table |
wenzelm@5015
    59
  Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table;
wenzelm@5015
    60
wenzelm@5015
    61
exception DUP of key;
wenzelm@5015
    62
exception DUPS of key list;
wenzelm@5015
    63
wenzelm@5015
    64
wenzelm@5681
    65
(* empty *)
wenzelm@5681
    66
wenzelm@5015
    67
val empty = Empty;
wenzelm@5015
    68
wenzelm@5015
    69
fun is_empty Empty = true
wenzelm@5015
    70
  | is_empty _ = false;
wenzelm@5015
    71
wenzelm@5681
    72
wenzelm@5681
    73
(* map and fold combinators *)
wenzelm@5681
    74
wenzelm@5681
    75
fun map_table _ Empty = Empty
wenzelm@5681
    76
  | map_table f (Branch2 (left, (k, x), right)) =
wenzelm@5681
    77
      Branch2 (map_table f left, (k, f x), map_table f right)
wenzelm@5681
    78
  | map_table f (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
wenzelm@5681
    79
      Branch3 (map_table f left, (k1, f x1), map_table f mid, (k2, f x2), map_table f right);
wenzelm@5681
    80
wenzelm@5681
    81
fun foldl_table _ (x, Empty) = x
wenzelm@5681
    82
  | foldl_table f (x, Branch2 (left, p, right)) =
wenzelm@5681
    83
      foldl_table f (f (foldl_table f (x, left), p), right)
wenzelm@5681
    84
  | foldl_table f (x, Branch3 (left, p1, mid, p2, right)) =
wenzelm@5681
    85
      foldl_table f (f (foldl_table f (f (foldl_table f (x, left), p1), mid), p2), right);
wenzelm@5681
    86
wenzelm@5681
    87
fun dest tab = rev (foldl_table (fn (rev_ps, p) => p :: rev_ps) ([], tab));
wenzelm@5681
    88
fun keys tab = rev (foldl_table (fn (rev_ks, (k, _)) => k :: rev_ks) ([], tab));
wenzelm@7061
    89
fun exists P tab = foldl_table (fn (false, e) => P e | (b, _) => b) (false, tab);
wenzelm@5015
    90
berghofe@8409
    91
fun min_key Empty = None
berghofe@8409
    92
  | min_key (Branch2 (left, (k, _), _)) = Some (if_none (min_key left) k)
berghofe@8409
    93
  | min_key (Branch3 (left, (k, _), _, _, _)) = Some (if_none (min_key left) k);
berghofe@8409
    94
wenzelm@5015
    95
wenzelm@5015
    96
(* lookup *)
wenzelm@5015
    97
wenzelm@5015
    98
fun lookup (Empty, _) = None
wenzelm@5015
    99
  | lookup (Branch2 (left, (k, x), right), key) =
wenzelm@5015
   100
      (case Key.ord (key, k) of
wenzelm@5015
   101
        LESS => lookup (left, key)
wenzelm@5015
   102
      | EQUAL => Some x
wenzelm@5015
   103
      | GREATER => lookup (right, key))
wenzelm@5015
   104
  | lookup (Branch3 (left, (k1, x1), mid, (k2, x2), right), key) =
wenzelm@5015
   105
      (case Key.ord (key, k1) of
wenzelm@5015
   106
        LESS => lookup (left, key)
wenzelm@5015
   107
      | EQUAL => Some x1
wenzelm@5015
   108
      | GREATER =>
wenzelm@5015
   109
          (case Key.ord (key, k2) of
wenzelm@5015
   110
            LESS => lookup (mid, key)
wenzelm@5015
   111
          | EQUAL => Some x2
wenzelm@5015
   112
          | GREATER => lookup (right, key)));
wenzelm@5015
   113
wenzelm@5015
   114
wenzelm@5015
   115
(* update *)
wenzelm@5015
   116
wenzelm@5015
   117
fun compare (k1, _) (k2, _) = Key.ord (k1, k2);
wenzelm@5015
   118
wenzelm@5015
   119
datatype 'a growth =
wenzelm@5015
   120
  Stay of 'a table |
wenzelm@5015
   121
  Sprout of 'a table * (key * 'a) * 'a table;
wenzelm@5015
   122
wenzelm@5015
   123
fun insert pair Empty = Sprout (Empty, pair, Empty)
wenzelm@5015
   124
  | insert pair (Branch2 (left, p, right)) =
wenzelm@5015
   125
      (case compare pair p of
wenzelm@5015
   126
        LESS =>
wenzelm@5015
   127
          (case insert pair left of
wenzelm@5015
   128
            Stay left' => Stay (Branch2 (left', p, right))
wenzelm@5015
   129
          | Sprout (left1, q, left2) => Stay (Branch3 (left1, q, left2, p, right)))
wenzelm@5015
   130
      | EQUAL => Stay (Branch2 (left, pair, right))
wenzelm@5015
   131
      | GREATER =>
wenzelm@5015
   132
          (case insert pair right of
wenzelm@5015
   133
            Stay right' => Stay (Branch2 (left, p, right'))
wenzelm@5015
   134
          | Sprout (right1, q, right2) =>
wenzelm@5015
   135
              Stay (Branch3 (left, p, right1, q, right2))))
wenzelm@5015
   136
  | insert pair (Branch3 (left, p1, mid, p2, right)) =
wenzelm@5015
   137
      (case compare pair p1 of
wenzelm@5015
   138
        LESS =>
wenzelm@5015
   139
          (case insert pair left of
wenzelm@5015
   140
            Stay left' => Stay (Branch3 (left', p1, mid, p2, right))
wenzelm@5015
   141
          | Sprout (left1, q, left2) =>
wenzelm@5015
   142
              Sprout (Branch2 (left1, q, left2), p1, Branch2 (mid, p2, right)))
wenzelm@5015
   143
      | EQUAL => Stay (Branch3 (left, pair, mid, p2, right))
wenzelm@5015
   144
      | GREATER =>
wenzelm@5015
   145
          (case compare pair p2 of
wenzelm@5015
   146
            LESS =>
wenzelm@5015
   147
              (case insert pair mid of
wenzelm@5015
   148
                Stay mid' => Stay (Branch3 (left, p1, mid', p2, right))
wenzelm@5015
   149
              | Sprout (mid1, q, mid2) =>
wenzelm@5015
   150
                  Sprout (Branch2 (left, p1, mid1), q, Branch2 (mid2, p2, right)))
wenzelm@5015
   151
          | EQUAL => Stay (Branch3 (left, p1, mid, pair, right))
wenzelm@5015
   152
          | GREATER =>
wenzelm@5015
   153
              (case insert pair right of
wenzelm@5015
   154
                Stay right' => Stay (Branch3 (left, p1, mid, p2, right'))
wenzelm@5015
   155
              | Sprout (right1, q, right2) =>
wenzelm@5015
   156
                  Sprout (Branch2 (left, p1, mid), p2, Branch2 (right1, q, right2)))));
wenzelm@5015
   157
wenzelm@5015
   158
fun update (pair, tab) =
wenzelm@5015
   159
  (case insert pair tab of
wenzelm@5015
   160
    Stay tab => tab
wenzelm@5015
   161
  | Sprout br => Branch2 br);
wenzelm@5015
   162
wenzelm@5015
   163
fun update_new (pair as (key, _), tab) =
wenzelm@5015
   164
  if is_none (lookup (tab, key)) then update (pair, tab)
wenzelm@5015
   165
  else raise DUP key;
wenzelm@5015
   166
wenzelm@5015
   167
wenzelm@12287
   168
(* extend and make *)
wenzelm@5015
   169
wenzelm@12287
   170
fun extend (table, pairs) =
wenzelm@12287
   171
  let
wenzelm@12287
   172
    fun add ((tab, dups), (key, x)) =
wenzelm@12287
   173
      (case lookup (tab, key) of
wenzelm@12287
   174
        None => (update ((key, x), tab), dups)
wenzelm@12287
   175
      | _ => (tab, key :: dups));
wenzelm@12287
   176
  in
wenzelm@12287
   177
    (case foldl add ((table, []), pairs) of
wenzelm@12287
   178
      (table', []) => table'
wenzelm@12287
   179
    | (_, dups) => raise DUPS (rev dups))
wenzelm@12287
   180
  end;
wenzelm@12287
   181
wenzelm@12287
   182
fun make pairs = extend (empty, pairs);
wenzelm@12287
   183
wenzelm@5015
   184
wenzelm@12287
   185
(* join and merge *)
wenzelm@5015
   186
wenzelm@12287
   187
fun join f (table1, table2) =
wenzelm@12287
   188
  let
wenzelm@12287
   189
    fun add ((tab, dups), (key, x)) =
wenzelm@12287
   190
      (case lookup (tab, key) of
wenzelm@12287
   191
        None => (update ((key, x), tab), dups)
wenzelm@12287
   192
      | Some y =>
wenzelm@12287
   193
          (case f (y, x) of
wenzelm@12287
   194
            Some z => (update ((key, z), tab), dups)
wenzelm@12287
   195
          | None => (tab, key :: dups)));
wenzelm@12287
   196
  in
wenzelm@12287
   197
    (case foldl_table add ((table1, []), table2) of
wenzelm@12287
   198
      (table', []) => table'
wenzelm@12287
   199
    | (_, dups) => raise DUPS (rev dups))
wenzelm@12287
   200
  end;
wenzelm@12287
   201
wenzelm@12287
   202
fun merge eq tabs = join (fn (y, x) => if eq (y, x) then Some y else None) tabs;
wenzelm@5015
   203
wenzelm@5015
   204
wenzelm@5015
   205
(* tables with multiple entries per key (preserving order) *)
wenzelm@5015
   206
wenzelm@5015
   207
fun lookup_multi tab_key = if_none (lookup tab_key) [];
wenzelm@12287
   208
fun update_multi ((key, x), tab) = update ((key, x :: lookup_multi (tab, key)), tab);
wenzelm@5015
   209
wenzelm@8606
   210
fun make_multi pairs = foldr update_multi (pairs, empty);
wenzelm@12287
   211
fun dest_multi tab = flat (map (fn (key, xs) => map (Library.pair key) xs) (dest tab));
wenzelm@12287
   212
fun merge_multi eq tabs = join (fn (xs, xs') => Some (gen_merge_lists eq xs xs')) tabs;
wenzelm@12287
   213
fun merge_multi' eq tabs = join (fn (xs, xs') => Some (gen_merge_lists' eq xs xs')) tabs;
wenzelm@5015
   214
wenzelm@5015
   215
wenzelm@5681
   216
(*final declarations of this structure!*)
wenzelm@5681
   217
val map = map_table;
wenzelm@5681
   218
val foldl = foldl_table;
wenzelm@5015
   219
wenzelm@5015
   220
end;
wenzelm@5015
   221
wenzelm@5015
   222
wenzelm@5015
   223
(*tables indexed by strings*)
wenzelm@5015
   224
structure Symtab = TableFun(type key = string val ord = string_ord);