X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fextlib%2FhExtlib.ml;h=c16b11159c38ccde56621da9d3b9c97c611419c9;hb=57ed1abc0fddb7644c396e15dd13600eef1f928f;hp=0d7254c8bd48cd34b8374e11f6c224d3620213a8;hpb=4b5527a6ccbe73ada47f903292959ed3dde3b5c6;p=helm.git diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml index 0d7254c8b..c16b11159 100644 --- a/helm/software/components/extlib/hExtlib.ml +++ b/helm/software/components/extlib/hExtlib.ml @@ -27,7 +27,7 @@ (** PROFILING *) -let profiling_enabled = ref true ;; (* ComponentsConf.profiling *) +let profiling_enabled = ref false ;; (* ComponentsConf.profiling *) let something_profiled = ref false @@ -140,6 +140,42 @@ let flatten_map f l = List.flatten (List.map f l) ;; +let list_mapi f l = + let rec aux k = function + | [] -> [] + | h::tl -> f h k :: aux (k+1) tl + in + aux 0 l +;; + +let rec list_iter_default2 f l1 def l2 = + match l1,l2 with + | [], _ -> () + | a::ta, b::tb -> f a b; list_iter_default2 f ta def tb + | a::ta, [] -> f a def; list_iter_default2 f ta def [] +;; + +let rec list_forall_default3 f l1 l2 def l3 = + match l1,l2,l3 with + | [], [], _ -> true + | [], _, _ + | _, [], _ -> raise (Invalid_argument "list_forall_default3") + | a::ta, b::tb, c::tc -> f a b c && list_forall_default3 f ta tb def tc + | a::ta, b::tb, [] -> f a b def && list_forall_default3 f ta tb def [] +;; + +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] @@ -479,3 +515,8 @@ let chop_prefix prefix s = let touch s = try close_out(open_out s) with Sys_error _ -> () ;; + +let rec mk_list x = function + | 0 -> [] + | n -> x :: mk_list x (n-1) +;;