X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fextlib%2FhExtlib.ml;h=6af86f9cd4d4ac0b620d004976ea6a83fc951a6e;hb=01001c883a8151edba81cd03a6f254d24a81c867;hp=3ee270e4e00b42fd0b012a512b11a92feef48c82;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git

diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml
index 3ee270e4e..6af86f9cd 100644
--- a/helm/software/components/extlib/hExtlib.ml
+++ b/helm/software/components/extlib/hExtlib.ml
@@ -27,7 +27,7 @@
 
 (** PROFILING *)
 
-let profiling_enabled = false ;; (* ComponentsConf.profiling *)
+let profiling_enabled = ref false ;; (* ComponentsConf.profiling *)
 
 let something_profiled = ref false
 
@@ -47,11 +47,12 @@ let set_profiling_printings f = profiling_printings := f
 
 type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b }
 let profile ?(enable = true) s =
- if profiling_enabled && enable then
+ if !profiling_enabled && enable then
    let total = ref 0.0 in
    let calls = ref 0 in
    let max = ref 0.0 in
    let profile f x =
+    if not !profiling_enabled then f x else
     let before = Unix.gettimeofday () in
     try
      incr calls;
@@ -139,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]
@@ -444,7 +481,7 @@ let find_in paths path =
        try
          if (Unix.stat path).Unix.st_kind = Unix.S_REG then path
          else aux tl
-       with Unix.Unix_error _ as exn -> 
+       with Unix.Unix_error _ -> 
                aux tl
    in
    try
@@ -478,3 +515,24 @@ 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)
+;;
+
+let list_seq start stop =
+  let rec aux pos =
+    if pos = stop then []
+    else pos :: (aux (pos+1))
+  in
+    aux start
+;;
+
+let rec list_skip n l =
+  match n,l with
+  | 0,_ -> l
+  | n,_::l -> list_skip (n-1) l
+  | _, [] -> assert false
+;;
+