From 064430093888668afe1400889ced26469420df96 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 19 Sep 2005 09:04:14 +0000 Subject: [PATCH] CicUtil.profile made even more polymorphic. --- helm/ocaml/cic/cicUtil.ml | 7 ++++--- helm/ocaml/cic/cicUtil.mli | 3 ++- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml index aa1ed1ba0..c85c2c803 100644 --- a/helm/ocaml/cic/cicUtil.ml +++ b/helm/ocaml/cic/cicUtil.ml @@ -209,8 +209,9 @@ let rec mk_rels howmany from = | 0 -> [] | _ -> (Cic.Rel (howmany + from)) :: (mk_rels (howmany-1) from) -let profiling_enabled = false +let profiling_enabled = true +type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b } let profile = if profiling_enabled then function s -> @@ -226,9 +227,9 @@ let profile = (fun () -> print_endline ("!! TOTAL TIME SPENT IN " ^ s ^ ": " ^ string_of_float !total)); - profile + { profile = profile } else - function _ -> fun f x -> f x + function _ -> { profile = fun f x -> f x } let id_of_annterm = function diff --git a/helm/ocaml/cic/cicUtil.mli b/helm/ocaml/cic/cicUtil.mli index cad3abbee..744ac3211 100644 --- a/helm/ocaml/cic/cicUtil.mli +++ b/helm/ocaml/cic/cicUtil.mli @@ -64,4 +64,5 @@ 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 +type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b } +val profile : string -> profiler -- 2.39.2