From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 23 Jun 2005 16:37:21 +0000 (+0000)
Subject: aded prifiler factory
X-Git-Tag: INDEXING_NO_PROOFS~91
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=faabe59afc8e66c96a1191210ac1e97effa028fe;p=helm.git

aded prifiler factory
---

diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml
index 289d6d983..81055e681 100644
--- 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 60c14f8a6..39316586e 100644
--- 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