summaryrefslogtreecommitdiff
path: root/libs
diff options
context:
space:
mode:
Diffstat (limited to 'libs')
-rw-r--r--libs/util.ml21
1 files changed, 21 insertions, 0 deletions
diff --git a/libs/util.ml b/libs/util.ml
index 443fb1e..88b916f 100644
--- a/libs/util.ml
+++ b/libs/util.ml
@@ -1,3 +1,5 @@
+open Unix
+
(* Small things *)
let ord_couple (a, b) = if a < b then a, b else b, a
@@ -77,3 +79,22 @@ let uid =
let c = ref 0 in
fun () -> c := !c + 1; string_of_int !c
+
+(* Time heavy functions *)
+
+let times_k : (string, float) Hashtbl.t = Hashtbl.create 10
+
+let time id f =
+ let t0 = Unix.times () in
+ let result = f () in
+ let t1 = Unix.times () in
+ let t = t1.tms_utime -. t0.tms_utime in
+ let r = try Hashtbl.find times_k id with _ -> 0. in
+ Hashtbl.replace times_k id (r +. t);
+ result
+
+let show_times () =
+ Format.printf "Times:@.";
+ Hashtbl.iter
+ (fun id t -> Format.printf "%s: %f@." id t)
+ times_k