aded prifiler factory

diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml
index 289d6d9838595eeafb59c7c9624a0fea6dd97015..81055e68178099bd41523c9e870b07d83be84194 100644 (file)
--- a/helm/ocaml/cic/cicUtil.ml
+++ b/helm/ocaml/cic/cicUtil.ml
@@ -290,3 +290,18 @@ let rec mk_rels howmany from =
   | 0 -> []
   | _ -> (Cic.Rel (howmany + from)) :: (mk_rels (howmany-1) from)
 
+let profile =
+ function s ->
+  let total = ref 0.0 in
+  let profile f x =
+   let before = Unix.gettimeofday () in
+   let res = f x in
+   let after = Unix.gettimeofday () in
+    total := !total +. (after -. before);
+    res
+  in
+  at_exit
+   (fun () ->
+     print_endline
+      ("!! TOTAL TIME SPENT IN " ^ s ^ ": " ^ string_of_float !total));
+  profile

diff --git a/helm/ocaml/cic/cicUtil.mli b/helm/ocaml/cic/cicUtil.mli
index 60c14f8a6c03e5e0d9736a3a22c9275eda047ed0..39316586e2360ec2fa702dfe52e33732cc381ee2 100644 (file)
--- a/helm/ocaml/cic/cicUtil.mli
+++ b/helm/ocaml/cic/cicUtil.mli
@@ -75,3 +75,7 @@ val select: term:Cic.term -> context:Cic.term -> (int * Cic.term) list
  * creates a list of [howmany] rels starting from [from] in decreasing order *)
 val mk_rels : int -> int -> Cic.term list
 
+(** profile s
+ * returns a profiling function; [s] is used for labelling the total time at
+   the end of the execution *)
+val profile : string -> ('a -> 'b) -> 'a -> 'b