From d7d60e0067d067769b72b3d8d4b16fdae441c991 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 14 May 2008 14:58:05 +0000 Subject: [PATCH] New function map_hash. --- helm/software/components/extlib/hExtlib.ml | 12 ++++++++++++ helm/software/components/extlib/hExtlib.mli | 1 + 2 files changed, 13 insertions(+) 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 -- 2.39.2