]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/extlib/hExtlib.ml
list_iter2_default_value moved to HExtlib. 1 euro to the first one that will
[helm.git] / helm / software / components / extlib / hExtlib.ml
1 (* Copyright (C) 2005, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 (* $Id$ *)
27
28 (** PROFILING *)
29
30 let profiling_enabled = ref false ;; (* ComponentsConf.profiling *)
31
32 let something_profiled = ref false
33
34 let _ = 
35   if !something_profiled then
36     at_exit 
37       (fun _ -> 
38         prerr_endline 
39          (Printf.sprintf "!! %39s ---------- --------- --------- ---------" 
40            (String.make 39 '-'));
41         prerr_endline 
42          (Printf.sprintf "!! %-39s %10s %9s %9s %9s" 
43            "function" "#calls" "total" "max" "average"))
44
45 let profiling_printings = ref (fun _ -> true)
46 let set_profiling_printings f = profiling_printings := f
47
48 type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b }
49 let profile ?(enable = true) s =
50  if !profiling_enabled && enable then
51    let total = ref 0.0 in
52    let calls = ref 0 in
53    let max = ref 0.0 in
54    let profile f x =
55     if not !profiling_enabled then f x else
56     let before = Unix.gettimeofday () in
57     try
58      incr calls;
59      let res = f x in
60      let after = Unix.gettimeofday () in
61      let delta = after -. before in
62       total := !total +. delta;
63       if delta > !max then max := delta;
64       res
65     with
66      exc ->
67       let after = Unix.gettimeofday () in
68       let delta = after -. before in
69        total := !total +. delta;
70        if delta > !max then max := delta;
71        raise exc
72    in
73    at_exit
74     (fun () ->
75       if !profiling_printings s && !calls <> 0 then
76        begin
77         something_profiled := true;
78         prerr_endline
79          (Printf.sprintf "!! %-39s %10d %9.4f %9.4f %9.4f" 
80          s !calls !total !max (!total /. (float_of_int !calls)))
81        end);
82    { profile = profile }
83  else
84    { profile = fun f x -> f x }
85
86 (** {2 Optional values} *)
87
88 let map_option f = function None -> None | Some v -> Some (f v)
89 let iter_option f = function None -> () | Some v -> f v
90 let unopt = function None -> failwith "unopt: None" | Some v -> v
91
92 (** {2 String processing} *)
93
94 let split ?(sep = ' ') s =
95   let pieces = ref [] in
96   let rec aux idx =
97     match (try Some (String.index_from s idx sep) with Not_found -> None) with
98     | Some pos ->
99         pieces := String.sub s idx (pos - idx) :: !pieces;
100         aux (pos + 1)
101     | None -> pieces := String.sub s idx (String.length s - idx) :: !pieces
102   in
103   aux 0;
104   List.rev !pieces
105
106 let trim_blanks s =
107   let rec find_left idx =
108     match s.[idx] with
109     | ' ' | '\t' | '\r' | '\n' -> find_left (idx + 1)
110     | _ -> idx
111   in
112   let rec find_right idx =
113     match s.[idx] with
114     | ' ' | '\t' | '\r' | '\n' -> find_right (idx - 1)
115     | _ -> idx
116   in
117   let s_len = String.length s in
118   let left, right = find_left 0, find_right (s_len - 1) in
119   String.sub s left (right - left + 1)
120
121 (** {2 Char processing} *)
122
123 let is_alpha c =
124   let code = Char.code c in 
125   (code >= 65 && code <= 90) || (code >= 97 && code <= 122)
126
127 let is_digit c =
128   let code = Char.code c in 
129   code >= 48 && code <= 57
130
131 let is_blank c =
132   let code = Char.code c in 
133   code = 9 || code = 10 || code = 13 || code = 32
134
135 let is_alphanum c = is_alpha c || is_digit c
136
137 (** {2 List processing} *)
138
139 let flatten_map f l =
140   List.flatten (List.map f l)
141 ;;
142
143 let list_mapi f l =
144   let rec aux k = function
145     | [] -> []
146     | h::tl -> f h k :: aux (k+1) tl
147   in
148      aux 0 l
149 ;;
150
151 let rec list_iter_default2 f l1 def l2 = 
152   match l1,l2 with
153     | [], _ -> ()
154     | a::ta, b::tb -> f a b; list_iter_default2 f ta def tb 
155     | a::ta, [] -> f a def; list_iter_default2 f ta def [] 
156 ;;
157
158 let sharing_map f l =
159   let unchanged = ref true in
160   let rec aux b = function
161     | [] as t -> unchanged := b; t
162     | he::tl ->
163         let he1 = f he in
164         he1 :: aux (b && he1 == he) tl
165   in
166   let l1 = aux true l in
167   if !unchanged then l else l1
168 ;;
169         
170 let rec list_uniq ?(eq=(=)) = function 
171   | [] -> []
172   | h::[] -> [h]
173   | h1::h2::tl when eq h1 h2 -> list_uniq ~eq (h2 :: tl) 
174   | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq ~eq tl
175
176 let rec filter_map f =
177   function
178   | [] -> []
179   | hd :: tl ->
180       (match f hd with
181       | None -> filter_map f tl
182       | Some v -> v :: filter_map f tl)
183
184 let list_rev_map_filter f l =
185    let rec aux a = function
186       | []       -> a
187       | hd :: tl -> 
188          begin match f hd with
189             | None   -> aux a tl
190             | Some b -> aux (b :: a) tl 
191          end
192    in 
193    aux [] l
194
195 let list_rev_map_filter_fold f v l =
196    let rec aux v a = function
197       | []       -> v, a
198       | hd :: tl -> 
199          begin match f v hd with
200             | v, None   -> aux v a tl
201             | v, Some b -> aux v (b :: a) tl 
202          end
203    in 
204    aux v [] l
205
206 let list_concat ?(sep = []) =
207   let rec aux acc =
208     function
209     | [] -> []
210     | [ last ] -> List.flatten (List.rev (last :: acc))
211     | hd :: tl -> aux ([sep; hd] @ acc) tl
212   in
213   aux []
214   
215 let rec list_findopt f l = 
216   let rec aux = function 
217     | [] -> None 
218     | x::tl -> 
219         (match f x with
220         | None -> aux tl
221         | Some _ as rc -> rc)
222   in
223   aux l
224
225 let split_nth n l =
226   let rec aux acc n l =
227     match n, l with
228     | 0, _ -> List.rev acc, l
229     | n, [] -> raise (Failure "HExtlib.split_nth")
230     | n, hd :: tl -> aux (hd :: acc) (n - 1) tl in
231   aux [] n l
232
233 let list_last l =
234   let l = List.rev l in 
235   try List.hd l with exn -> raise (Failure "HExtlib.list_last")
236 ;;
237   
238 (** {2 File predicates} *)
239
240 let is_dir fname =
241   try
242     (Unix.stat fname).Unix.st_kind = Unix.S_DIR
243   with Unix.Unix_error _ -> false
244
245 let writable_dir path =
246   try
247     let file = path ^ "/prova_matita" in
248     let oc = open_out file in
249     close_out oc;
250     Sys.remove file;
251     true
252   with Sys_error _ -> false
253
254
255 let is_regular fname =
256   try
257     (Unix.stat fname).Unix.st_kind = Unix.S_REG
258   with Unix.Unix_error _ -> false
259
260 let is_executable fname =
261   try
262     let stat = (Unix.stat fname) in
263     stat.Unix.st_kind = Unix.S_REG &&
264     (stat.Unix.st_perm land 0o001 > 0)
265   with Unix.Unix_error _ -> false
266
267 let chmod mode filename =
268    Unix.chmod filename mode
269
270 let mkdir path =
271   let components = split ~sep:'/' path in
272   let rec aux where = function
273     | [] -> ()
274     | piece::tl -> 
275         let path =
276           if where = "" then piece else where ^ "/" ^ piece in
277         (try
278           Unix.mkdir path 0o755; chmod 0o2775 path 
279         with 
280         | Unix.Unix_error (Unix.EEXIST,_,_) -> ()
281         | Unix.Unix_error (e,_,_) -> 
282             raise 
283               (Failure 
284                 ("Unix.mkdir " ^ path ^ " 0o2775 :" ^ (Unix.error_message e))));
285         aux path tl
286   in
287   let where = if path.[0] = '/' then "/" else "" in
288   aux where components
289
290 (** {2 Filesystem} *)
291
292 let input_file fname =
293   let size = (Unix.stat fname).Unix.st_size in
294   let buf = Buffer.create size in
295   let ic = open_in fname in
296   Buffer.add_channel buf ic size;
297   close_in ic;
298   Buffer.contents buf
299
300 let input_all ic =
301   let size = 10240 in
302   let buf = Buffer.create size in
303   let s = String.create size in
304   (try
305     while true do
306       let bytes = input ic s 0 size in
307       if bytes = 0 then raise End_of_file
308       else Buffer.add_substring buf s 0 bytes
309     done
310   with End_of_file -> ());
311   Buffer.contents buf
312
313 let output_file ~filename ~text = 
314   let oc = open_out filename in
315   output_string oc text;
316   close_out oc;
317   chmod 0o664 filename
318
319 let blank_split s =
320   let len = String.length s in
321   let buf = Buffer.create 0 in
322   let rec aux acc i =
323     if i >= len
324     then begin
325       if Buffer.length buf > 0
326       then List.rev (Buffer.contents buf :: acc)
327       else List.rev acc
328     end else begin
329       if is_blank s.[i] then
330         if Buffer.length buf > 0 then begin
331           let s = Buffer.contents buf in
332           Buffer.clear buf;
333           aux (s :: acc) (i + 1)
334         end else
335           aux acc (i + 1)
336       else begin
337         Buffer.add_char buf s.[i];
338         aux acc (i + 1)
339       end
340     end
341   in
342   aux [] 0
343
344   (* Rules: * "~name" -> home dir of "name"
345    * "~" -> value of $HOME if defined, home dir of the current user otherwise *)
346 let tilde_expand s =
347   let get_home login = (Unix.getpwnam login).Unix.pw_dir in
348   let expand_one s =
349     let len = String.length s in
350     if len > 0 && s.[0] = '~' then begin
351       let login_len = ref 1 in
352       while !login_len < len && is_alphanum (s.[!login_len]) do
353         incr login_len
354       done;
355       let login = String.sub s 1 (!login_len - 1) in
356       try
357         let home =
358           if login = "" then
359             try Sys.getenv "HOME" with Not_found -> get_home (Unix.getlogin ())
360           else
361             get_home login
362         in
363         home ^ String.sub s !login_len (len - !login_len)
364       with Not_found | Invalid_argument _ -> s
365     end else
366       s
367   in
368   String.concat " " (List.map expand_one (blank_split s))
369   
370 let find ?(test = fun _ -> true) path = 
371   let rec aux acc todo = 
372     match todo with
373     | [] -> acc
374     | path :: tl ->
375         try
376           let handle = Unix.opendir path in
377           let dirs = ref [] in
378           let matching_files = ref [] in 
379           (try 
380             while true do 
381               match Unix.readdir handle with
382               | "." | ".." -> ()
383               | entry ->
384                   let qentry = path ^ "/" ^ entry in
385                   (try
386                     if is_dir qentry then
387                       dirs := qentry :: !dirs
388                     else if test qentry then
389                       matching_files := qentry :: !matching_files;
390                   with Unix.Unix_error _ -> ())
391             done
392           with End_of_file -> Unix.closedir handle);
393           aux (!matching_files @ acc) (!dirs @ tl)
394         with Unix.Unix_error _ -> aux acc tl
395   in
396   aux [] [path]
397
398 let safe_remove fname = if Sys.file_exists fname then Sys.remove fname
399
400 let is_dir_empty d =
401  try
402   let od = Unix.opendir d in
403   let rec aux () =
404    let name = Unix.readdir od in
405    if name <> "." && name <> ".." then false else aux () in
406   let res = try aux () with End_of_file -> true in
407    Unix.closedir od;
408    res
409  with
410   Unix.Unix_error _ -> true (* raised by Unix.opendir, we hope :-) *)
411
412 let safe_rmdir d = try Unix.rmdir d with Unix.Unix_error _ -> ()
413
414 let rec rmdir_descend d = 
415   if is_dir_empty d then
416     begin
417       safe_rmdir d;
418       rmdir_descend (Filename.dirname d)
419     end
420
421
422 (** {2 Exception handling} *)
423
424 let finally at_end f arg =
425   let res =
426     try f arg
427     with exn -> at_end (); raise exn
428   in
429   at_end ();
430   res
431
432 (** {2 Localized exceptions } *)
433
434 exception Localized of Stdpp.location * exn
435
436 let loc_of_floc floc = Stdpp.first_pos floc, Stdpp.last_pos floc;;
437
438 let floc_of_loc (loc_begin, loc_end) =
439  Stdpp.make_loc (loc_begin, loc_end)
440
441 let dummy_floc = floc_of_loc (-1, -1)
442
443 let raise_localized_exception ~offset floc exn =
444  let x, y = loc_of_floc floc in
445  let x = offset + x in
446  let y = offset + y in
447  let floc = floc_of_loc (x,y) in
448   raise (Localized (floc, exn))
449
450 let estimate_size x = 
451   4 * (String.length (Marshal.to_string x [])) / 1024
452
453 let normalize_path s = 
454   let s = Str.global_replace (Str.regexp "//") "/" s in
455   let l = Str.split (Str.regexp "/") s in
456   let rec aux acc = function
457     | [] -> acc
458     | he::"."::tl -> aux acc (he::tl)
459     | he::".."::tl when he <> ".." -> aux [] (acc @ tl)
460     | he::tl -> aux (acc@[he]) tl
461   in
462   (if Str.string_match (Str.regexp "^/") s 0 then "/" else "") ^
463   String.concat "/" (aux [] l)
464   ^ (if Str.string_match (Str.regexp "/$") s 0 then "/" else "")
465 ;;
466
467 let find_in paths path =
468    let rec aux = function
469    | [] -> raise (Failure "find_in")
470    | p :: tl ->
471       let path = normalize_path (p ^ "/" ^ path) in
472        try
473          if (Unix.stat path).Unix.st_kind = Unix.S_REG then path
474          else aux tl
475        with Unix.Unix_error _ -> 
476                aux tl
477    in
478    try
479      aux paths
480    with Unix.Unix_error _ | Failure _ -> 
481      raise 
482        (Failure "find_in")
483 ;;
484
485 let is_prefix_of_aux d1 d2 = 
486   let len1 = String.length d1 in
487   let len2 = String.length d2 in
488   if len2 < len1 then 
489     false, len1, len2
490   else
491     let pref = String.sub d2 0 len1 in
492     pref = d1 && (len1 = len2 || d1.[len1-1] = '/' || d2.[len1] = '/'), len1, len2
493
494 let is_prefix_of d1 d2 =
495   let b,_,_ = is_prefix_of_aux d1 d2 in b
496 ;;
497
498 let chop_prefix prefix s =
499   let b,lp,ls = is_prefix_of_aux prefix s in
500   if b then
501     String.sub s lp (ls - lp)
502   else 
503     s
504 ;;
505
506 let touch s =
507   try close_out(open_out s) with Sys_error _ -> ()
508 ;;