added map_default, internal restructuring
authorhaftmann
Wed Jul 19 14:16:36 2006 +0200 (2006-07-19)
changeset 20166ae2bc00408d6
parent 20165 4de20306a88a
child 20167 fe5fd4fd4114
added map_default, internal restructuring
src/Pure/General/alist.ML
     1.1 --- a/src/Pure/General/alist.ML	Wed Jul 19 12:12:08 2006 +0200
     1.2 +++ b/src/Pure/General/alist.ML	Wed Jul 19 14:16:36 2006 +0200
     1.3 @@ -20,6 +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 map_default: ('a * 'a -> bool) -> 'a * 'b -> ('b -> 'b)
     1.8 +    -> ('a * 'b) list -> ('a * 'b) list
     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 @@ -43,6 +45,13 @@
    1.13            else find xs (i+1);
    1.14    in find xs 0 end;
    1.15  
    1.16 +fun map_index eq key f_none f_some xs =
    1.17 +  let
    1.18 +    val i = find_index eq xs key;
    1.19 +    fun mapp 0 (x::xs) = f_some x xs
    1.20 +      | mapp i (x::xs) = x :: mapp (i-1) xs;
    1.21 +  in (if i = ~1 then f_none else mapp i) xs end;
    1.22 +
    1.23  fun lookup _ [] _ = NONE
    1.24    | lookup eq ((key, value)::xs) key' =
    1.25        if eq (key', key) then SOME value
    1.26 @@ -52,29 +61,20 @@
    1.27    | defined eq ((key, value)::xs) key' =
    1.28        eq (key', key) orelse defined eq xs key';
    1.29  
    1.30 -fun update eq (x as (key, value)) xs =
    1.31 -  let
    1.32 -    val i = find_index eq xs key;
    1.33 -    fun upd 0 (_::xs) = x :: xs
    1.34 -      | upd i (x::xs) = x :: upd (i-1) xs;
    1.35 -  in if i = ~1 then x::xs else upd i xs end;
    1.36 +fun update eq (x as (key, value)) =
    1.37 +  map_index eq key (cons x) (fn _ => cons x);
    1.38  
    1.39  fun default eq (key, value) xs =
    1.40 -  if defined eq xs key then xs else (key, value)::xs;
    1.41 +  if defined eq xs key then xs else (key, value) :: xs;
    1.42 +
    1.43 +fun delete eq key =
    1.44 +  map_index eq key I (K I);
    1.45  
    1.46 -fun delete eq key xs =
    1.47 -  let
    1.48 -    val i = find_index eq xs key;
    1.49 -    fun del 0 (_::xs) = xs
    1.50 -      | del i (x::xs) = x :: del (i-1) xs;
    1.51 -  in if i = ~1 then xs else del i xs end;
    1.52 +fun map_entry eq key f =
    1.53 +  map_index eq key I (fn (key, value) => cons (key, f value));
    1.54  
    1.55 -fun map_entry eq key f xs =
    1.56 -  let
    1.57 -    val i = find_index eq xs key;
    1.58 -    fun mapp 0 ((x as (key, value))::xs) = (key, f value) :: xs
    1.59 -      | mapp i (x::xs) = x :: mapp (i-1) xs;
    1.60 -  in if i = ~1 then xs else mapp i xs end;
    1.61 +fun map_default eq (key, value) f =
    1.62 +  map_index eq key (cons (key, f value)) (fn (key, value) => cons (key, f value));
    1.63  
    1.64  fun map_entry_yield eq key f xs =
    1.65    let