src/Pure/table.ML

 (*  Title:      Pure/table.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Generic tables (lacking delete operation).  Implemented as 2-3 trees.
+Generic tables and tables indexed by strings.  No delete operation.
+Implemented as balanced 2-3 trees.
 *)
 
-signature TABLE_DATA =
+signature KEY =
 sig
   type key
   val ord: key * key -> order
 end;
 

   val empty: 'a table
   val is_empty: 'a table -> bool
   val dest: 'a table -> (key * 'a) list
   val lookup: 'a table * key -> 'a option
   val update: (key * 'a) * 'a table -> 'a table
-  val update_new: (key * 'a) * 'a table -> 'a table                     (*exception DUP*)
-  val make: (key * 'a) list -> 'a table                                 (*exception DUPS*)
-  val extend: 'a table * (key * 'a) list -> 'a table                    (*exception DUPS*)
-  val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table       (*exception DUPS*)
+  val update_new: (key * 'a) * 'a table -> 'a table                 (*exception DUP*)
+  val make: (key * 'a) list -> 'a table                             (*exception DUPS*)
+  val extend: 'a table * (key * 'a) list -> 'a table                (*exception DUPS*)
+  val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table   (*exception DUPS*)
   val lookup_multi: 'a list table * key -> 'a list
   val make_multi: (key * 'a) list -> 'a list table
   val dest_multi: 'a list table -> (key * 'a) list
   val map: ('a -> 'b) -> 'a table -> 'b table
 end;
 
-functor TableFun(Data: TABLE_DATA): TABLE =
+functor TableFun(Key: KEY): TABLE =
 struct
 
 
 (* datatype table *)
 
-type key = Data.key;
+type key = Key.key;
 
 datatype 'a table =
   Empty |
   Branch2 of 'a table * (key * 'a) * 'a table |
   Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table;

 
 (* lookup *)
 
 fun lookup (Empty, _) = None
   | lookup (Branch2 (left, (k, x), right), key) =
-      (case Data.ord (key, k) of
+      (case Key.ord (key, k) of
         LESS => lookup (left, key)
       | EQUAL => Some x
       | GREATER => lookup (right, key))
   | lookup (Branch3 (left, (k1, x1), mid, (k2, x2), right), key) =
-      (case Data.ord (key, k1) of
+      (case Key.ord (key, k1) of
         LESS => lookup (left, key)
       | EQUAL => Some x1
       | GREATER =>
-          (case Data.ord (key, k2) of
+          (case Key.ord (key, k2) of
             LESS => lookup (mid, key)
           | EQUAL => Some x2
           | GREATER => lookup (right, key)));
 
 
 (* update *)
 
-fun compare (k1, _) (k2, _) = Data.ord (k1, k2);
+fun compare (k1, _) (k2, _) = Key.ord (k1, k2);
 
 datatype 'a growth =
   Stay of 'a table |
   Sprout of 'a table * (key * 'a) * 'a table;
 

   (case insert pair tab of
     Stay tab => tab
   | Sprout br => Branch2 br);
 
 fun update_new (pair as (key, _), tab) =
-  (case lookup (tab, key) of
-    None => update (pair, tab)
-  | Some _ => raise DUP key);
+  if is_none (lookup (tab, key)) then update (pair, tab)
+  else raise DUP key;
 
 
 (* make, extend, merge tables *)
 
 fun add eq ((tab, dups), (key, x)) =

 
 (* tables with multiple entries per key (preserving order) *)
 
 fun lookup_multi tab_key = if_none (lookup tab_key) [];
 
-fun cons_entry ((key, entry), tab) =
-  update ((key, entry :: lookup_multi (tab, key)), tab);
+fun cons_entry ((key, x), tab) =
+  update ((key, x :: lookup_multi (tab, key)), tab);
 
 fun make_multi pairs = foldr cons_entry (pairs, empty);
 
 fun dest_multi tab =
-  flat (map (fn (key, xs) => map (pair key) xs) (dest tab));
+  flat (map (fn (key, xs) => map (Library.pair key) xs) (dest tab));
 
 
 (* map *)
 
 fun map _ Empty = Empty

 end;
 
 
 (*tables indexed by strings*)
 structure Symtab = TableFun(type key = string val ord = string_ord);
-
-(* FIXME demo *)
-structure IntTab = TableFun(type key = int val ord = int_ord);
-val make = IntTab.make o map (rpair ());
-fun dest tab = IntTab.dest tab |> map fst;