]> matita.cs.unibo.it Git - helm.git/commitdiff
implemented the first bunch of useful functions
authorStefano Zacchiroli <zack@upsilon.cc>
Mon, 26 Sep 2005 08:55:16 +0000 (08:55 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Mon, 26 Sep 2005 08:55:16 +0000 (08:55 +0000)
helm/ocaml/extlib/Makefile
helm/ocaml/extlib/hExtlib.ml
helm/ocaml/extlib/hExtlib.mli

index 7035415203dbe4f9d6bd453e9b4895fb3e8cad32..936bf3b21184aff18a0352decea262bf6781371f 100644 (file)
@@ -1,5 +1,5 @@
 PACKAGE = extlib
-REQUIRES = mysql
+REQUIRES = unix mysql
 PREDICATES =
 
 INTERFACE_FILES = \
index 6e1f3564a4759c91c2942d22dd4d20c4dc81e17b..b8bee56568f08d36bb9816bf295f9b2e0649a0db 100644 (file)
@@ -1,4 +1,4 @@
-(* Copyright (C) 2000, HELM Team.
+(* Copyright (C) 2005, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -54,3 +54,108 @@ let profile =
  else
   function _ -> { profile = fun f x -> f x }
 
+(** {2 Optional values} *)
+
+let map_option f = function None -> None | Some v -> Some (f v)
+let unopt = function None -> failwith "unopt: None" | Some v -> v
+
+(** {2 String processing} *)
+
+let split ?(sep = ' ') s =
+  let pieces = ref [] in
+  let rec aux idx =
+    match (try Some (String.index_from s idx sep) with Not_found -> None) with
+    | Some pos ->
+        pieces := String.sub s idx (pos - idx) :: !pieces;
+        aux (pos + 1)
+    | None -> pieces := String.sub s idx (String.length s - idx) :: !pieces
+  in
+  aux 0;
+  List.rev !pieces
+
+let trim_blanks s =
+  let rec find_left idx =
+    match s.[idx] with
+    | ' ' | '\t' | '\r' | '\n' -> find_left (idx + 1)
+    | _ -> idx
+  in
+  let rec find_right idx =
+    match s.[idx] with
+    | ' ' | '\t' | '\r' | '\n' -> find_right (idx - 1)
+    | _ -> idx
+  in
+  let s_len = String.length s in
+  let left, right = find_left 0, find_right (s_len - 1) in
+  String.sub s left (right - left + 1)
+
+(*   let rex = Pcre.regexp "^\\s*(.*?)\\s*$" in
+  fun s -> (Pcre.extract ~rex s).(1) *)
+
+(** {2 File predicates} *)
+
+let is_dir fname =
+  try
+    (Unix.stat fname).Unix.st_kind = Unix.S_DIR
+  with Unix.Unix_error _ -> false
+
+let is_regular fname =
+  try
+    (Unix.stat fname).Unix.st_kind = Unix.S_REG
+  with Unix.Unix_error _ -> false
+
+let mkdir path =
+  let components = split ~sep:'/' path in
+  let rec aux where = function
+    | [] -> ()
+    | piece::tl -> 
+        let path = where ^ "/" ^ piece in
+        (try
+          Unix.mkdir path 0o755
+        with 
+        | Unix.Unix_error (Unix.EEXIST,_,_) -> ()
+        | Unix.Unix_error (e,_,_) -> 
+            raise 
+              (Failure 
+                ("Unix.mkdir " ^ path ^ " 0o755 :" ^ (Unix.error_message e))));
+        aux path tl
+  in
+  aux "" components
+
+(** {2 Filesystem} *)
+
+let input_file fname =
+  let size = (Unix.stat fname).Unix.st_size in
+  let buf = Buffer.create size in
+  let ic = open_in fname in
+  Buffer.add_channel buf ic size;
+  close_in ic;
+  Buffer.contents buf
+
+let input_all ic =
+  let size = 10240 in
+  let buf = Buffer.create size in
+  let s = String.create size in
+  (try
+    while true do
+      let bytes = input ic s 0 size in
+      if bytes = 0 then raise End_of_file
+      else Buffer.add_substring buf s 0 bytes
+    done
+  with End_of_file -> ());
+  Buffer.contents buf
+
+let output_file ~filename ~text = 
+  let oc = open_out filename in
+  output_string oc text;
+  close_out oc
+
+(** {2 Exception handling} *)
+
+let finally at_end f arg =
+  let res =
+    try f arg
+    with exn -> at_end (); raise exn
+  in
+  at_end ();
+  res
+
index 05a8b7d29b6085d8fa947ca29c925f6b43e8d7a7..ad055315e077faf337f0d937fb2b516eada03eab 100644 (file)
@@ -1,4 +1,4 @@
-(* Copyright (C) 2004, HELM Team.
+(* Copyright (C) 2005, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
  * http://helm.cs.unibo.it/
  *)
 
-(** profile s
- * returns a profiling function; [s] is used for labelling the total time at
-   the end of the execution *)
+(** {2 Optional values} *)
+
+val map_option: ('a -> 'b) -> 'a option -> 'b option
+val unopt: 'a option -> 'a  (** @raise Failure *)
+
+(** {2 Filesystem} *)
+
+val is_dir: string -> bool  (** @return true if file is a directory *)
+val is_regular: string -> bool  (** @return true if file is a regular file *)
+val mkdir: string -> unit (** create dir and parents. @raise Failure *)
+
+(** {2 File I/O} *)
+
+val input_file: string -> string  (** read all the contents of file to string *)
+val input_all: in_channel -> string (** read all the contents of a channel *)
+val output_file: filename:string -> text:string -> unit (** other way round *)
+
+(** {2 Exception handling} *)
+
+val finally: (unit -> unit) -> ('a -> 'b) -> 'a -> 'b
+
+(** {2 String processing} *)
+
+val split: ?sep:char -> string -> string list (** @param sep defaults to ' ' *)
+val trim_blanks: string -> string (** strip heading and trailing blanks *)
+
+(** {2 Debugging & Profiling} *)
+
 type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b }
+
+  (** @return a profiling function; [s] is used for labelling the total time at
+   * the end of the execution *)
 val profile : string -> profiler
+