New function map_hash.

diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml
index fe587e297c50b5631d992852e12b2ae9bc84486c..cdf26c5c7d2af6bf082a3a7b4e22b6b166ed45b4 100644 (file)
--- a/helm/software/components/extlib/hExtlib.ml
+++ b/helm/software/components/extlib/hExtlib.ml
@@ -148,6 +148,18 @@ let list_mapi f l =
      aux 0 l
 ;;
 
+let sharing_map f l =
+  let unchanged = ref true in
+  let rec aux b = function
+    | [] as t -> unchanged := b; t
+    | he::tl ->
+        let he1 = f he in
+        he1 :: aux (b && he1 == he) tl
+  in
+  let l1 = aux true l in
+  if !unchanged then l else l1
+;;
+        
 let rec list_uniq ?(eq=(=)) = function 
   | [] -> []
   | h::[] -> [h]

diff --git a/helm/software/components/extlib/hExtlib.mli b/helm/software/components/extlib/hExtlib.mli
index 5600bfbc7e7c1c9b28c5f71480aad42180e2f2df..6316fa11cc2a36497183288188873871284b203b 100644 (file)
--- a/helm/software/components/extlib/hExtlib.mli
+++ b/helm/software/components/extlib/hExtlib.mli
@@ -91,6 +91,7 @@ val list_findopt: ('a -> 'b option) -> 'a list -> 'b option
 val flatten_map: ('a -> 'b list) -> 'a list -> 'b list
 val list_last: 'a list -> 'a
 val list_mapi: ('a -> int -> 'b) -> 'a list -> 'b list
+val sharing_map: ('a -> 'a) -> 'a list -> 'a list
 
   (** split_nth n l
    * @returns two list, the first contains at least n elements, the second the