X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fextlib%2FhExtlib.ml;h=3ee270e4e00b42fd0b012a512b11a92feef48c82;hb=ac31c84bb9bcf327554976d4296d787853fc8db5;hp=b36a4d89db2630f5d0d192454f706d86fa1054d3;hpb=4c18fa5b069a1e3216e9e3e0f18d92e778e67e41;p=helm.git diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml index b36a4d89d..3ee270e4e 100644 --- a/helm/software/components/extlib/hExtlib.ml +++ b/helm/software/components/extlib/hExtlib.ml @@ -153,6 +153,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 @@ -172,6 +194,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 = @@ -179,11 +214,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 @@ -192,13 +247,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 @@ -230,7 +285,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 @@ -314,13 +370,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 _ -> () @@ -344,32 +403,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 _ as exn -> + 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 _ -> () +;;