AList.join now with 'DUP' exception
authorhaftmann
Tue Jul 18 13:27:59 2006 +0200 (2006-07-18)
changeset 201427f5bb7f8b9b9
parent 20141 cf8129ebcdd3
child 20143 54e493016486
AList.join now with 'DUP' exception
src/Pure/General/alist.ML
     1.1 --- a/src/Pure/General/alist.ML	Tue Jul 18 08:48:11 2006 +0200
     1.2 +++ b/src/Pure/General/alist.ML	Tue Jul 18 13:27:59 2006 +0200
     1.3 @@ -20,8 +20,8 @@
     1.4      -> ('b * 'c) list -> ('b * 'c) list
     1.5    val map_entry_yield: ('a * 'b -> bool) -> 'a -> ('c -> 'd * 'c)
     1.6      -> ('b * 'c) list -> 'd option * ('b * 'c) list
     1.7 -  val join: ('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b option) ->
     1.8 -    ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list         (*exception DUP*)
     1.9 +  val join: ('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b) (*exception DUP*)
    1.10 +    -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list      (*exception DUP*)
    1.11    val merge: ('a * 'a -> bool) -> ('b * 'b -> bool)
    1.12      -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list      (*exception DUP*)
    1.13    val make: ('a -> 'b) -> 'a list -> ('a * 'b) list
    1.14 @@ -94,14 +94,11 @@
    1.15      fun add (y as (key, value)) xs =
    1.16        (case lookup eq xs key of
    1.17          NONE => cons y xs
    1.18 -      | SOME value' =>
    1.19 -          (case f key (value', value) of
    1.20 -            SOME value'' => update eq (key, value'') xs
    1.21 -          | NONE => raise DUP));
    1.22 +      | SOME value' => update eq (key, f key (value', value)) xs);
    1.23    in fold_rev add ys xs end;
    1.24  
    1.25  fun merge eq_key eq_val =
    1.26 -  join eq_key (K (fn (yx as (_, x)) => if eq_val yx then SOME x else NONE));
    1.27 +  join eq_key (K (fn (yx as (_, x)) => if eq_val yx then x else raise DUP));
    1.28  
    1.29  fun make keyfun =
    1.30    let fun keypair x = (x, keyfun x)