diff options
Diffstat (limited to 'libs')
-rw-r--r-- | libs/util.ml | 21 |
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 |