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