From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 14 May 2008 14:58:05 +0000 (+0000)
Subject: New function map_hash.
X-Git-Tag: make_still_working~5215
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d7d60e0067d067769b72b3d8d4b16fdae441c991;p=helm.git

New function map_hash.
---

diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml
index fe587e297..cdf26c5c7 100644
--- 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 5600bfbc7..6316fa11c 100644
--- 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