From faabe59afc8e66c96a1191210ac1e97effa028fe Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 23 Jun 2005 16:37:21 +0000 Subject: [PATCH] aded prifiler factory --- helm/ocaml/cic/cicUtil.ml | 15 +++++++++++++++ helm/ocaml/cic/cicUtil.mli | 4 ++++ 2 files changed, 19 insertions(+) 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 -- 2.39.2