# HG changeset patch
# User wenzelm
# Date 1119026011 -7200
# Node ID 0ab34b9d1b1f101ea931d3a72e8c3fce433418ce
# Parent  bc90e58bb6acc66e62789af80751e426662820e2
added map', fold;
changed join to pass key;

diff -r bc90e58bb6ac -r 0ab34b9d1b1f src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Fri Jun 17 18:33:30 2005 +0200
+++ b/src/Pure/General/table.ML	Fri Jun 17 18:33:31 2005 +0200
@@ -22,6 +22,8 @@
   val empty: 'a table
   val is_empty: 'a table -> bool
   val map: ('a -> 'b) -> 'a table -> 'b table
+  val map': (key -> 'a -> 'b) -> 'a table -> 'b table
+  val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
   val foldl: ('a * (key * 'b) -> 'a) -> 'a * 'b table -> 'a
   val dest: 'a table -> (key * 'a) list
   val keys: 'a table -> key list
@@ -35,7 +37,8 @@
   val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table
   val make: (key * 'a) list -> 'a table                                (*exception DUPS*)
   val extend: 'a table * (key * 'a) list -> 'a table                   (*exception DUPS*)
-  val join: ('a * 'a -> 'a option) -> 'a table * 'a table -> 'a table  (*exception DUPS*)
+  val join: (key -> 'a * 'a -> 'a option) ->
+    'a table * 'a table -> 'a table                                    (*exception DUPS*)
   val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table      (*exception DUPS*)
   val delete: key -> 'a table -> 'a table                              (*exception UNDEF*)
   val delete_safe: key -> 'a table -> 'a table
@@ -81,23 +84,24 @@
 
 fun map_table _ Empty = Empty
   | map_table f (Branch2 (left, (k, x), right)) =
-      Branch2 (map_table f left, (k, f x), map_table f right)
+      Branch2 (map_table f left, (k, f k x), map_table f right)
   | map_table f (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
-      Branch3 (map_table f left, (k1, f x1), map_table f mid, (k2, f x2), map_table f right);
+      Branch3 (map_table f left, (k1, f k1 x1),
+        map_table f mid, (k2, f k2 x2), map_table f right);
 
-fun foldl_table _ (x, Empty) = x
-  | foldl_table f (x, Branch2 (left, p, right)) =
-      foldl_table f (f (foldl_table f (x, left), p), right)
-  | foldl_table f (x, Branch3 (left, p1, mid, p2, right)) =
-      foldl_table f (f (foldl_table f (f (foldl_table f (x, left), p1), mid), p2), right);
+fun fold_table f Empty x = x
+  | fold_table f (Branch2 (left, p, right)) x =
+      fold_table f right (f p (fold_table f left x))
+  | fold_table f (Branch3 (left, p1, mid, p2, right)) x =
+      fold_table f right (f p2 (fold_table f mid (f p1 (fold_table f left x))));
 
-fun dest tab = rev (foldl_table (fn (rev_ps, p) => p :: rev_ps) ([], tab));
-fun keys tab = rev (foldl_table (fn (rev_ks, (k, _)) => k :: rev_ks) ([], tab));
+fun dest tab = rev (fold_table cons tab []);
+fun keys tab = rev (fold_table (cons o #1) tab []);
 
 local exception TRUE in
 
 fun exists pred tab =
-  (foldl_table (fn ((), e) => if pred e then raise TRUE else ()) ((), tab); false)
+  (fold_table (fn p => fn () => if pred p then raise TRUE else ()) tab (); false)
     handle TRUE => true;
 
 fun forall pred = not o exists (not o pred);
@@ -303,20 +307,20 @@
 
 fun join f (table1, table2) =
   let
-    fun add ((tab, dups), (key, x)) =
+    fun add (key, x) (tab, dups) =
       (case lookup (tab, key) of
         NONE => (update ((key, x), tab), dups)
       | SOME y =>
-          (case f (y, x) of
+          (case f key (y, x) of
             SOME z => (update ((key, z), tab), dups)
           | NONE => (tab, key :: dups)));
   in
-    (case foldl_table add ((table1, []), table2) of
+    (case fold_table add table2 (table1, []) of
       (table', []) => table'
     | (_, dups) => raise DUPS (rev dups))
   end;
 
-fun merge eq tabs = join (fn (y, x) => if eq (y, x) then SOME y else NONE) tabs;
+fun merge eq tabs = join (fn _ => fn (y, x) => if eq (y, x) then SOME y else NONE) tabs;
 
 
 (* tables with multiple entries per key *)
@@ -331,13 +335,15 @@
 
 fun make_multi args = foldr update_multi empty args;
 fun dest_multi tab = List.concat (map (fn (key, xs) => map (pair key) xs) (dest tab));
-fun merge_multi eq tabs = join (fn (xs, xs') => SOME (gen_merge_lists eq xs xs')) tabs;
-fun merge_multi' eq tabs = join (fn (xs, xs') => SOME (gen_merge_lists' eq xs xs')) tabs;
+fun merge_multi eq = join (fn _ => fn (xs, xs') => SOME (gen_merge_lists eq xs xs'));
+fun merge_multi' eq = join (fn _ => fn (xs, xs') => SOME (gen_merge_lists' eq xs xs'));
 
 
 (*final declarations of this structure!*)
-val map = map_table;
-val foldl = foldl_table;
+fun map f = map_table (K f);
+val map' = map_table;
+val fold = fold_table;
+fun foldl f (x, tab) = fold (fn p => fn x' => f (x', p)) tab x;
 
 end;