X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fextlib%2FhExtlib.ml;h=cccb467674e22415b59de320e72cbbe845812142;hb=571d199acd4e6743a48f8f64f28c62d18182d04d;hp=bf3bb2574b7608327129d235974d74f7c4d0f48f;hpb=a9be219c90cccb6c19abbbf3bdf8b806810d2d5c;p=helm.git diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml index bf3bb2574..cccb46767 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,77 @@ 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_mapi_acc f a l = + let rec aux k a res = function + | [] -> a, List.rev res + | h::tl -> let a,h = f h k a in aux (k+1) a (h::res) tl + in + aux 0 a [] 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] @@ -153,6 +225,30 @@ let rec filter_map f = | None -> filter_map f tl | Some v -> v :: filter_map f tl) +let filter_map_acc f acc l = + let acc, res = + List.fold_left + (fun (acc, res) t -> + match f acc t with + | None -> acc, res + | Some (acc, x) -> acc, x::res) + (acc,[]) l + in + acc, List.rev res +;; + +let filter_map_monad f acc l = + let acc, res = + List.fold_left + (fun (acc, res) t -> + match f acc t with + | acc, None -> acc, res + | acc, Some x -> acc, x::res) + (acc,[]) l + in + acc, List.rev res +;; + let list_rev_map_filter f l = let rec aux a = function | [] -> a @@ -184,15 +280,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 +311,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 = @@ -236,6 +347,9 @@ let is_executable fname = (stat.Unix.st_perm land 0o001 > 0) with Unix.Unix_error _ -> false +let chmod mode filename = + Unix.chmod filename mode + let mkdir path = let components = split ~sep:'/' path in let rec aux where = function @@ -244,21 +358,18 @@ let mkdir path = let path = if where = "" then piece else where ^ "/" ^ piece in (try - Unix.mkdir path 0o775 + Unix.mkdir path 0o755; chmod 0o2775 path with | Unix.Unix_error (Unix.EEXIST,_,_) -> () | Unix.Unix_error (e,_,_) -> raise (Failure - ("Unix.mkdir " ^ path ^ " 0o775 :" ^ (Unix.error_message e)))); + ("Unix.mkdir " ^ path ^ " 0o2775 :" ^ (Unix.error_message e)))); aux path tl in let where = if path.[0] = '/' then "/" else "" in aux where components -let chmod mode filename = - Unix.chmod filename mode - (** {2 Filesystem} *) let input_file fname = @@ -403,32 +514,100 @@ let finally at_end f arg = (** {2 Localized exceptions } *) -exception Localized of Token.flocation * exn +exception Localized of Stdpp.location * exn -let loc_of_floc = function - | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } -> - (loc_begin, loc_end) +let loc_of_floc floc = Stdpp.first_pos floc, Stdpp.last_pos floc;; let floc_of_loc (loc_begin, loc_end) = - let floc_begin = - { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1; - Lexing.pos_cnum = loc_begin } - in - let floc_end = { floc_begin with Lexing.pos_cnum = loc_end } in - (floc_begin, floc_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 + let x, y = loc_of_floc floc in let x = offset + x in let y = offset + y in - let flocb,floce = floc in - let floc = - { flocb with Lexing.pos_cnum = x }, { floce with Lexing.pos_cnum = y } - in + let floc = floc_of_loc (x,y) in raise (Localized (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 +;; +