# HG changeset patch
# User haftmann
# Date 1129735177 -7200
# Node ID fbe857bedcd7cc73118ce16f2aab35caeec714be
# Parent  2b435795c9e940e6303448fc2e039c72650e9781
added join

diff -r 2b435795c9e9 -r fbe857bedcd7 src/Pure/General/alist.ML
--- a/src/Pure/General/alist.ML	Wed Oct 19 16:32:09 2005 +0200
+++ b/src/Pure/General/alist.ML	Wed Oct 19 17:19:37 2005 +0200
@@ -21,8 +21,10 @@
   val map_entry: ('a * 'b -> bool) -> 'a -> ('c -> 'c)
     -> ('b * 'c) list -> ('b * 'c) list
   val make: ('a -> 'b) -> 'a list -> ('a * 'b) list
+  val join: ('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b option) ->
+    ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list         (*exception DUP*)
   val merge: ('a * 'a -> bool) -> ('b * 'b -> bool)
-    -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception DUP*)
+    -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list      (*exception DUP*)
   val find: ('a * 'b -> bool) -> ('c * 'b) list -> 'a -> 'c list
 end;
 
@@ -73,6 +75,17 @@
 
 exception DUP;
 
+fun join eq f (xs, ys) =
+  let
+    fun add (key, x) xs =
+      (case lookup eq xs key of
+        NONE => update eq (key, x) xs
+      | SOME y =>
+          (case f key (y, x) of
+            SOME z => update eq (key, z) xs
+          | NONE => raise DUP));
+  in fold_rev add xs ys end;
+
 fun merge eq_key eq_val (xs, ys) =
   let
     fun add (x as (key, value)) ys =
@@ -82,9 +95,7 @@
             if eq_val (value, value')
             then ys
             else raise DUP;
-  in
-    fold_rev add xs ys
-  end;
+  in fold_rev add xs ys end;
 
 fun make keyfun =
   let fun keypair x = (x, keyfun x)