tuned;
authorwenzelm
Sun Dec 28 14:55:34 1997 +0100 (1997-12-28)
changeset 4485697972696f71
parent 4484 220ccae8a590
child 4486 48e4fbc03b7c
tuned;
src/Pure/table.ML
     1.1 --- a/src/Pure/table.ML	Sun Dec 28 14:55:20 1997 +0100
     1.2 +++ b/src/Pure/table.ML	Sun Dec 28 14:55:34 1997 +0100
     1.3 @@ -2,10 +2,11 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Generic tables (lacking delete operation).  Implemented as 2-3 trees.
     1.8 +Generic tables and tables indexed by strings.  No delete operation.
     1.9 +Implemented as balanced 2-3 trees.
    1.10  *)
    1.11  
    1.12 -signature TABLE_DATA =
    1.13 +signature KEY =
    1.14  sig
    1.15    type key
    1.16    val ord: key * key -> order
    1.17 @@ -22,23 +23,23 @@
    1.18    val dest: 'a table -> (key * 'a) list
    1.19    val lookup: 'a table * key -> 'a option
    1.20    val update: (key * 'a) * 'a table -> 'a table
    1.21 -  val update_new: (key * 'a) * 'a table -> 'a table                     (*exception DUP*)
    1.22 -  val make: (key * 'a) list -> 'a table                                 (*exception DUPS*)
    1.23 -  val extend: 'a table * (key * 'a) list -> 'a table                    (*exception DUPS*)
    1.24 -  val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table       (*exception DUPS*)
    1.25 +  val update_new: (key * 'a) * 'a table -> 'a table                 (*exception DUP*)
    1.26 +  val make: (key * 'a) list -> 'a table                             (*exception DUPS*)
    1.27 +  val extend: 'a table * (key * 'a) list -> 'a table                (*exception DUPS*)
    1.28 +  val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table   (*exception DUPS*)
    1.29    val lookup_multi: 'a list table * key -> 'a list
    1.30    val make_multi: (key * 'a) list -> 'a list table
    1.31    val dest_multi: 'a list table -> (key * 'a) list
    1.32    val map: ('a -> 'b) -> 'a table -> 'b table
    1.33  end;
    1.34  
    1.35 -functor TableFun(Data: TABLE_DATA): TABLE =
    1.36 +functor TableFun(Key: KEY): TABLE =
    1.37  struct
    1.38  
    1.39  
    1.40  (* datatype table *)
    1.41  
    1.42 -type key = Data.key;
    1.43 +type key = Key.key;
    1.44  
    1.45  datatype 'a table =
    1.46    Empty |
    1.47 @@ -64,16 +65,16 @@
    1.48  
    1.49  fun lookup (Empty, _) = None
    1.50    | lookup (Branch2 (left, (k, x), right), key) =
    1.51 -      (case Data.ord (key, k) of
    1.52 +      (case Key.ord (key, k) of
    1.53          LESS => lookup (left, key)
    1.54        | EQUAL => Some x
    1.55        | GREATER => lookup (right, key))
    1.56    | lookup (Branch3 (left, (k1, x1), mid, (k2, x2), right), key) =
    1.57 -      (case Data.ord (key, k1) of
    1.58 +      (case Key.ord (key, k1) of
    1.59          LESS => lookup (left, key)
    1.60        | EQUAL => Some x1
    1.61        | GREATER =>
    1.62 -          (case Data.ord (key, k2) of
    1.63 +          (case Key.ord (key, k2) of
    1.64              LESS => lookup (mid, key)
    1.65            | EQUAL => Some x2
    1.66            | GREATER => lookup (right, key)));
    1.67 @@ -81,7 +82,7 @@
    1.68  
    1.69  (* update *)
    1.70  
    1.71 -fun compare (k1, _) (k2, _) = Data.ord (k1, k2);
    1.72 +fun compare (k1, _) (k2, _) = Key.ord (k1, k2);
    1.73  
    1.74  datatype 'a growth =
    1.75    Stay of 'a table |
    1.76 @@ -128,9 +129,8 @@
    1.77    | Sprout br => Branch2 br);
    1.78  
    1.79  fun update_new (pair as (key, _), tab) =
    1.80 -  (case lookup (tab, key) of
    1.81 -    None => update (pair, tab)
    1.82 -  | Some _ => raise DUP key);
    1.83 +  if is_none (lookup (tab, key)) then update (pair, tab)
    1.84 +  else raise DUP key;
    1.85  
    1.86  
    1.87  (* make, extend, merge tables *)
    1.88 @@ -156,13 +156,13 @@
    1.89  
    1.90  fun lookup_multi tab_key = if_none (lookup tab_key) [];
    1.91  
    1.92 -fun cons_entry ((key, entry), tab) =
    1.93 -  update ((key, entry :: lookup_multi (tab, key)), tab);
    1.94 +fun cons_entry ((key, x), tab) =
    1.95 +  update ((key, x :: lookup_multi (tab, key)), tab);
    1.96  
    1.97  fun make_multi pairs = foldr cons_entry (pairs, empty);
    1.98  
    1.99  fun dest_multi tab =
   1.100 -  flat (map (fn (key, xs) => map (pair key) xs) (dest tab));
   1.101 +  flat (map (fn (key, xs) => map (Library.pair key) xs) (dest tab));
   1.102  
   1.103  
   1.104  (* map *)
   1.105 @@ -179,8 +179,3 @@
   1.106  
   1.107  (*tables indexed by strings*)
   1.108  structure Symtab = TableFun(type key = string val ord = string_ord);
   1.109 -
   1.110 -(* FIXME demo *)
   1.111 -structure IntTab = TableFun(type key = int val ord = int_ord);
   1.112 -val make = IntTab.make o map (rpair ());
   1.113 -fun dest tab = IntTab.dest tab |> map fst;