X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fextlib%2FhExtlib.ml;h=c2de58f810fe99728b5b13253135c12934e02bec;hb=ba5c1c83e77e701ef11625687ec27931bc4bb944;hp=bf725122c260e31f0b8c4595e36f9af2833db2fb;hpb=cfea6dbbb5f488f85e4cd7069d5c9179a2ed0b2d;p=helm.git diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml index bf725122c..c2de58f81 100644 --- a/helm/software/components/extlib/hExtlib.ml +++ b/helm/software/components/extlib/hExtlib.ml @@ -27,7 +27,7 @@ (** PROFILING *) -let profiling_enabled = 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; @@ -135,6 +136,10 @@ let is_alphanum c = is_alpha c || is_digit c (** {2 List processing} *) +let flatten_map f l = + List.flatten (List.map f l) +;; + let rec list_uniq ?(eq=(=)) = function | [] -> [] | h::[] -> [h] @@ -149,6 +154,28 @@ let rec filter_map f = | None -> filter_map f tl | Some v -> v :: filter_map f tl) +let list_rev_map_filter f l = + let rec aux a = function + | [] -> a + | hd :: tl -> + begin match f hd with + | None -> aux a tl + | Some b -> aux (b :: a) tl + end + in + aux [] l + +let list_rev_map_filter_fold f v l = + let rec aux v a = function + | [] -> v, a + | hd :: tl -> + begin match f v hd with + | v, None -> aux v a tl + | v, Some b -> aux v (b :: a) tl + end + in + aux v [] l + let list_concat ?(sep = []) = let rec aux acc = function @@ -168,6 +195,19 @@ let rec list_findopt f l = in aux l +let split_nth n l = + let rec aux acc n l = + match n, l with + | 0, _ -> List.rev acc, l + | n, [] -> raise (Failure "HExtlib.split_nth") + | n, hd :: tl -> aux (hd :: acc) (n - 1) tl in + aux [] n l + +let list_last l = + let l = List.rev l in + try List.hd l with exn -> raise (Failure "HExtlib.list_last") +;; + (** {2 File predicates} *) let is_dir fname = @@ -175,11 +215,31 @@ let is_dir fname = (Unix.stat fname).Unix.st_kind = Unix.S_DIR with Unix.Unix_error _ -> false +let writable_dir path = + try + let file = path ^ "/prova_matita" in + let oc = open_out file in + close_out oc; + Sys.remove file; + true + with Sys_error _ -> false + + let is_regular fname = try (Unix.stat fname).Unix.st_kind = Unix.S_REG with Unix.Unix_error _ -> false +let is_executable fname = + try + let stat = (Unix.stat fname) in + stat.Unix.st_kind = Unix.S_REG && + (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 @@ -188,13 +248,13 @@ let mkdir path = let path = if where = "" then piece else where ^ "/" ^ piece in (try - Unix.mkdir path 0o755 + Unix.mkdir path 0o755; chmod 0o2775 path with | Unix.Unix_error (Unix.EEXIST,_,_) -> () | Unix.Unix_error (e,_,_) -> raise (Failure - ("Unix.mkdir " ^ path ^ " 0o755 :" ^ (Unix.error_message e)))); + ("Unix.mkdir " ^ path ^ " 0o2775 :" ^ (Unix.error_message e)))); aux path tl in let where = if path.[0] = '/' then "/" else "" in @@ -226,7 +286,8 @@ let input_all ic = let output_file ~filename ~text = let oc = open_out filename in output_string oc text; - close_out oc + close_out oc; + chmod 0o664 filename let blank_split s = let len = String.length s in @@ -310,13 +371,16 @@ let find ?(test = fun _ -> true) path = let safe_remove fname = if Sys.file_exists fname then Sys.remove fname let is_dir_empty d = - let od = Unix.opendir d in - let rec aux () = - let name = Unix.readdir od in - if name <> "." && name <> ".." then false else aux () in - let res = try aux () with End_of_file -> true in - Unix.closedir od; - res + try + let od = Unix.opendir d in + let rec aux () = + let name = Unix.readdir od in + if name <> "." && name <> ".." then false else aux () in + let res = try aux () with End_of_file -> true in + Unix.closedir od; + res + with + Unix.Unix_error _ -> true (* raised by Unix.opendir, we hope :-) *) let safe_rmdir d = try Unix.rmdir d with Unix.Unix_error _ -> () @@ -340,32 +404,78 @@ 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 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 _ -> () +;;