# HG changeset patch
# User wenzelm
# Date 883317334 -3600
# Node ID 697972696f71ff7f922090914307b03af7df284b
# Parent  220ccae8a59030a7d096c4bb7bfb59f41e40bab4
tuned;

diff -r 220ccae8a590 -r 697972696f71 src/Pure/table.ML
--- a/src/Pure/table.ML	Sun Dec 28 14:55:20 1997 +0100
+++ b/src/Pure/table.ML	Sun Dec 28 14:55:34 1997 +0100
@@ -2,10 +2,11 @@
     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
@@ -22,23 +23,23 @@
   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 |
@@ -64,16 +65,16 @@
 
 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)));
@@ -81,7 +82,7 @@
 
 (* update *)
 
-fun compare (k1, _) (k2, _) = Data.ord (k1, k2);
+fun compare (k1, _) (k2, _) = Key.ord (k1, k2);
 
 datatype 'a growth =
   Stay of 'a table |
@@ -128,9 +129,8 @@
   | 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 *)
@@ -156,13 +156,13 @@
 
 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 *)
@@ -179,8 +179,3 @@
 
 (*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;