From 2d4c0e3f1bd4b142c3187d5a4d51f0ea5745d90b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 13 Sep 2005 16:33:46 +0000 Subject: [PATCH] Enabling/disabling profiling is now controlled by a boolean (and not by a comment!!!) --- helm/ocaml/cic/cicUtil.ml | 37 +++++++++++++++++++------------------ 1 file changed, 19 insertions(+), 18 deletions(-) diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml index 7269e1f84..aa1ed1ba0 100644 --- a/helm/ocaml/cic/cicUtil.ml +++ b/helm/ocaml/cic/cicUtil.ml @@ -209,21 +209,26 @@ let rec mk_rels howmany from = | 0 -> [] | _ -> (Cic.Rel (howmany + from)) :: (mk_rels (howmany-1) from) +let profiling_enabled = false + 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 + if profiling_enabled then + 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 + else + function _ -> fun f x -> f x let id_of_annterm = function @@ -243,7 +248,3 @@ let id_of_annterm = | Cic.AMutCase (id,_,_,_,_,_) | Cic.AFix (id,_,_) | Cic.ACoFix (id,_,_) -> id - - (** WARNING: COMMENT THIS TO ENABLE PROFILING **) -let profile _ = let profile f x = f x in profile - -- 2.39.2