X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fextlib%2FhExtlib.ml;h=b2092c5b35be4b91db19529f1449f818f7555868;hb=1b70a1f66be53f76e475383e86d63c2b5c1fbcaa;hp=24f0dd1967ab3f8711a5538f61058bcc13417fce;hpb=683978a2627cf1ce15673360f26806593d22f7b5;p=helm.git diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml index 24f0dd196..b2092c5b3 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,69 @@ 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 list_index p = + let rec aux n = + function + [] -> None + | he::_ when p he -> Some (n,he) + | _::tl -> aux (n + 1) tl + in + aux 0 +;; + +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 [] +;; + +exception FailureAt of int;; + +let list_forall_default3_var f l1 l2 def l3 = + let rec aux f l1 l2 def l3 i = + match l1,l2,l3 with + | [], [], _ -> true + | [], _, _ + | _, [], _ -> raise (Invalid_argument "list_forall_default3") + | a::ta, b::tb, c::tc -> + if f a b c then aux f ta tb def tc (i+1) + else raise (FailureAt i) + | a::ta, b::tb, [] -> + if f a b def then aux f ta tb def [] (i+1) + else raise (FailureAt i) + in aux f l1 l2 def l3 0 +;; + +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] @@ -184,15 +248,24 @@ let list_concat ?(sep = []) = in aux [] +let list_iter_sep ~sep f = + let rec aux = + function + | [] -> () + | [ last ] -> f last + | hd :: tl -> f hd; sep (); aux tl + in + aux + let rec list_findopt f l = - let rec aux = function + let rec aux k = function | [] -> None | x::tl -> - (match f x with - | None -> aux tl + (match f x k with + | None -> aux (succ k) tl | Some _ as rc -> rc) in - aux l + aux 0 l let split_nth n l = let rec aux acc n l = @@ -206,7 +279,13 @@ let list_last l = let l = List.rev l in try List.hd l with exn -> raise (Failure "HExtlib.list_last") ;; - + +let rec list_assoc_all a = function + | [] -> [] + | (x, y) :: tl when x = a -> y :: list_assoc_all a tl + | _ :: tl -> list_assoc_all a tl +;; + (** {2 File predicates} *) let is_dir fname = @@ -410,7 +489,7 @@ let loc_of_floc floc = Stdpp.first_pos floc, Stdpp.last_pos floc;; let floc_of_loc (loc_begin, loc_end) = Stdpp.make_loc (loc_begin, loc_end) -let dummy_floc = floc_of_loc (-1, -1) +let dummy_floc = floc_of_loc (0, 0) let raise_localized_exception ~offset floc exn = let x, y = loc_of_floc floc in @@ -422,3 +501,81 @@ let raise_localized_exception ~offset floc exn = let estimate_size x = 4 * (String.length (Marshal.to_string x [])) / 1024 +let normalize_path s = + let s = Str.global_replace (Str.regexp "//") "/" s in + let l = Str.split (Str.regexp "/") s in + let rec aux acc = function + | [] -> acc + | he::"."::tl -> aux acc (he::tl) + | he::".."::tl when he <> ".." -> aux [] (acc @ tl) + | he::tl -> aux (acc@[he]) tl + in + (if Str.string_match (Str.regexp "^/") s 0 then "/" else "") ^ + String.concat "/" (aux [] l) + ^ (if Str.string_match (Str.regexp "/$") s 0 then "/" else "") +;; + +let find_in paths path = + let rec aux = function + | [] -> raise (Failure "find_in") + | p :: tl -> + let path = normalize_path (p ^ "/" ^ path) in + try + if (Unix.stat path).Unix.st_kind = Unix.S_REG then path + else aux tl + with Unix.Unix_error _ -> + aux tl + in + try + aux paths + with Unix.Unix_error _ | Failure _ -> + raise + (Failure "find_in") +;; + +let is_prefix_of_aux d1 d2 = + let len1 = String.length d1 in + let len2 = String.length d2 in + if len2 < len1 then + false, len1, len2 + else + let pref = String.sub d2 0 len1 in + pref = d1 && (len1 = len2 || d1.[len1-1] = '/' || d2.[len1] = '/'), len1, len2 + +let is_prefix_of d1 d2 = + let b,_,_ = is_prefix_of_aux d1 d2 in b +;; + +let chop_prefix prefix s = + let b,lp,ls = is_prefix_of_aux prefix s in + if b then + String.sub s lp (ls - lp) + else + 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 = + if start > stop then [] else + 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 +;; +