# HG changeset patch
# User haftmann
# Date 1153311396 -7200
# Node ID ae2bc00408d6be13c0a3ab65c0f6f5581eb7d9ef
# Parent  4de20306a88ae4842cef0c2521624648d5b713a3
added map_default, internal restructuring

diff -r 4de20306a88a -r ae2bc00408d6 src/Pure/General/alist.ML
--- a/src/Pure/General/alist.ML	Wed Jul 19 12:12:08 2006 +0200
+++ b/src/Pure/General/alist.ML	Wed Jul 19 14:16:36 2006 +0200
@@ -20,6 +20,8 @@
     -> ('b * 'c) list -> ('b * 'c) list
   val map_entry_yield: ('a * 'b -> bool) -> 'a -> ('c -> 'd * 'c)
     -> ('b * 'c) list -> 'd option * ('b * 'c) list
+  val map_default: ('a * 'a -> bool) -> 'a * 'b -> ('b -> 'b)
+    -> ('a * 'b) list -> ('a * 'b) list
   val join: ('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b) (*exception DUP*)
     -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list      (*exception DUP*)
   val merge: ('a * 'a -> bool) -> ('b * 'b -> bool)
@@ -43,6 +45,13 @@
           else find xs (i+1);
   in find xs 0 end;
 
+fun map_index eq key f_none f_some xs =
+  let
+    val i = find_index eq xs key;
+    fun mapp 0 (x::xs) = f_some x xs
+      | mapp i (x::xs) = x :: mapp (i-1) xs;
+  in (if i = ~1 then f_none else mapp i) xs end;
+
 fun lookup _ [] _ = NONE
   | lookup eq ((key, value)::xs) key' =
       if eq (key', key) then SOME value
@@ -52,29 +61,20 @@
   | defined eq ((key, value)::xs) key' =
       eq (key', key) orelse defined eq xs key';
 
-fun update eq (x as (key, value)) xs =
-  let
-    val i = find_index eq xs key;
-    fun upd 0 (_::xs) = x :: xs
-      | upd i (x::xs) = x :: upd (i-1) xs;
-  in if i = ~1 then x::xs else upd i xs end;
+fun update eq (x as (key, value)) =
+  map_index eq key (cons x) (fn _ => cons x);
 
 fun default eq (key, value) xs =
-  if defined eq xs key then xs else (key, value)::xs;
+  if defined eq xs key then xs else (key, value) :: xs;
+
+fun delete eq key =
+  map_index eq key I (K I);
 
-fun delete eq key xs =
-  let
-    val i = find_index eq xs key;
-    fun del 0 (_::xs) = xs
-      | del i (x::xs) = x :: del (i-1) xs;
-  in if i = ~1 then xs else del i xs end;
+fun map_entry eq key f =
+  map_index eq key I (fn (key, value) => cons (key, f value));
 
-fun map_entry eq key f xs =
-  let
-    val i = find_index eq xs key;
-    fun mapp 0 ((x as (key, value))::xs) = (key, f value) :: xs
-      | mapp i (x::xs) = x :: mapp (i-1) xs;
-  in if i = ~1 then xs else mapp i xs end;
+fun map_default eq (key, value) f =
+  map_index eq key (cons (key, f value)) (fn (key, value) => cons (key, f value));
 
 fun map_entry_yield eq key f xs =
   let