]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/extlib/hExtlib.ml
added filter_map
[helm.git] / helm / ocaml / 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
27 (** PROFILING *)
28
29 let profiling_enabled = true
30
31 type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b }
32 let profile =
33  if profiling_enabled then
34   function s ->
35    let total = ref 0.0 in
36    let profile f x =
37     let before = Unix.gettimeofday () in
38     try
39      let res = f x in
40      let after = Unix.gettimeofday () in
41       total := !total +. (after -. before);
42       res
43     with
44      exc ->
45       let after = Unix.gettimeofday () in
46        total := !total +. (after -. before);
47        raise exc
48    in
49    at_exit
50     (fun () ->
51       print_endline
52        ("!! TOTAL TIME SPENT IN " ^ s ^ ": " ^ string_of_float !total));
53    { profile = profile }
54  else
55   function _ -> { profile = fun f x -> f x }
56
57 (** {2 Optional values} *)
58
59 let map_option f = function None -> None | Some v -> Some (f v)
60 let unopt = function None -> failwith "unopt: None" | Some v -> v
61
62 (** {2 String processing} *)
63
64 let split ?(sep = ' ') s =
65   let pieces = ref [] in
66   let rec aux idx =
67     match (try Some (String.index_from s idx sep) with Not_found -> None) with
68     | Some pos ->
69         pieces := String.sub s idx (pos - idx) :: !pieces;
70         aux (pos + 1)
71     | None -> pieces := String.sub s idx (String.length s - idx) :: !pieces
72   in
73   aux 0;
74   List.rev !pieces
75
76 let trim_blanks s =
77   let rec find_left idx =
78     match s.[idx] with
79     | ' ' | '\t' | '\r' | '\n' -> find_left (idx + 1)
80     | _ -> idx
81   in
82   let rec find_right idx =
83     match s.[idx] with
84     | ' ' | '\t' | '\r' | '\n' -> find_right (idx - 1)
85     | _ -> idx
86   in
87   let s_len = String.length s in
88   let left, right = find_left 0, find_right (s_len - 1) in
89   String.sub s left (right - left + 1)
90
91 (** {2 List processing} *)
92
93 let rec list_uniq = function 
94   | [] -> []
95   | h::[] -> [h]
96   | h1::h2::tl when h1 = h2 -> list_uniq (h2 :: tl) 
97   | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq tl
98
99 let rec filter_map f =
100   function
101   | [] -> []
102   | hd :: tl ->
103       (match f hd with
104       | None -> filter_map f tl
105       | Some v -> v :: filter_map f tl)
106
107 (** {2 File predicates} *)
108
109 let is_dir fname =
110   try
111     (Unix.stat fname).Unix.st_kind = Unix.S_DIR
112   with Unix.Unix_error _ -> false
113
114 let is_regular fname =
115   try
116     (Unix.stat fname).Unix.st_kind = Unix.S_REG
117   with Unix.Unix_error _ -> false
118
119 let mkdir path =
120   let components = split ~sep:'/' path in
121   let rec aux where = function
122     | [] -> ()
123     | piece::tl -> 
124         let path = where ^ "/" ^ piece in
125         (try
126           Unix.mkdir path 0o755
127         with 
128         | Unix.Unix_error (Unix.EEXIST,_,_) -> ()
129         | Unix.Unix_error (e,_,_) -> 
130             raise 
131               (Failure 
132                 ("Unix.mkdir " ^ path ^ " 0o755 :" ^ (Unix.error_message e))));
133         aux path tl
134   in
135   aux "" components
136
137 (** {2 Filesystem} *)
138
139 let input_file fname =
140   let size = (Unix.stat fname).Unix.st_size in
141   let buf = Buffer.create size in
142   let ic = open_in fname in
143   Buffer.add_channel buf ic size;
144   close_in ic;
145   Buffer.contents buf
146
147 let input_all ic =
148   let size = 10240 in
149   let buf = Buffer.create size in
150   let s = String.create size in
151   (try
152     while true do
153       let bytes = input ic s 0 size in
154       if bytes = 0 then raise End_of_file
155       else Buffer.add_substring buf s 0 bytes
156     done
157   with End_of_file -> ());
158   Buffer.contents buf
159
160 let output_file ~filename ~text = 
161   let oc = open_out filename in
162   output_string oc text;
163   close_out oc
164
165 (** {2 Exception handling} *)
166
167 let finally at_end f arg =
168   let res =
169     try f arg
170     with exn -> at_end (); raise exn
171   in
172   at_end ();
173   res
174