From 064430093888668afe1400889ced26469420df96 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
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.5