From f41876ee0d76202514504fb7031c0245e56926be Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 27 Oct 2005 13:51:16 +0000 Subject: [PATCH] 1. Parameter enable (default true) added to HExtlib.profile 2. profiling code commented out in cicReduction since it affects performances very badly --- helm/ocaml/cic_proof_checking/cicReduction.ml | 43 ++++++++++--------- helm/ocaml/extlib/hExtlib.ml | 4 +- helm/ocaml/extlib/hExtlib.mli | 2 +- 3 files changed, 26 insertions(+), 23 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml index 39133ac92..813a589d6 100644 --- a/helm/ocaml/cic_proof_checking/cicReduction.ml +++ b/helm/ocaml/cic_proof_checking/cicReduction.ml @@ -34,6 +34,7 @@ exception ReferenceToCurrentProof;; exception ReferenceToInductiveDefinition;; let debug = false +let profile = false let debug_print s = if debug then prerr_endline (Lazy.force s) let fdebug = ref 1;; @@ -510,13 +511,15 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; unwind_aux m t ;; -let profiler_unwind = HExtlib.profile "are_convertible.unwind" - let unwind k e ens t = -let foo () = - unwind' 0 k e ens t -in - profiler_unwind.HExtlib.profile foo () + let unwind = unwind' 0;; + +(* + let unwind = + let profiler_unwind = HExtlib.profile ~enable:profile "are_convertible.unwind" in + fun k e ens t -> + profiler_unwind.HExtlib.profile (unwind k e ens) t ;; +*) let reduce ~delta ?(subst = []) context : config -> Cic.term = let module C = Cic in @@ -798,9 +801,15 @@ module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; module U = UriManager;; -let profiler_whd = HExtlib.profile "are_convertible.whd" let whd = R.whd +(* +let whd = + let profiler_whd = HExtlib.profile ~enable:profile "are_convertible.whd" in + fun ?(delta=true) ?(subst=[]) context t -> + profiler_whd.HExtlib.profile (whd ~delta ~subst context) t +*) + (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then * fallbacks to structural equality *) let (===) x y = @@ -1020,18 +1029,8 @@ let are_convertible whd ?(subst=[]) ?(metasenv=[]) = debug_print (lazy (CicPp.ppterm t2)); debug_print (lazy (CicPp.ppterm (whd ~subst context t2))) | _ -> ()); *) - let t1' = - let foo () = -whd ?delta:(Some true) ?subst:(Some subst) context t1 - in - profiler_whd.HExtlib.profile foo () -in - let t2' = - let foo () = -whd ?delta:(Some true) ?subst:(Some subst) context t2 - in - profiler_whd.HExtlib.profile foo () -in + let t1' = whd ?delta:(Some true) ?subst:(Some subst) context t1 in + let t2' = whd ?delta:(Some true) ?subst:(Some subst) context t2 in debug t1' [t2'] "POSTWHD"; aux2 test_equality_only t1' t2' ugraph end @@ -1062,12 +1061,16 @@ let _ = are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv. let are_convertible = are_convertible whd -let profiler_other_whd = HExtlib.profile "~are_convertible.whd" +let whd = R.whd + +(* +let profiler_other_whd = HExtlib.profile ~enable:profile "~are_convertible.whd" let whd ?(delta=true) ?(subst=[]) context t = let foo () = whd ~delta ~subst context t in profiler_other_whd.HExtlib.profile foo () +*) let rec normalize ?(delta=true) ?(subst=[]) ctx term = let module C = Cic in diff --git a/helm/ocaml/extlib/hExtlib.ml b/helm/ocaml/extlib/hExtlib.ml index 9f4f2d9c9..052205da8 100644 --- a/helm/ocaml/extlib/hExtlib.ml +++ b/helm/ocaml/extlib/hExtlib.ml @@ -29,8 +29,8 @@ let profiling_enabled = true type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b } -let profile = - if profiling_enabled then +let profile ?(enable = true) = + if profiling_enabled && enable then function s -> let total = ref 0.0 in let profile f x = diff --git a/helm/ocaml/extlib/hExtlib.mli b/helm/ocaml/extlib/hExtlib.mli index 32fb59d47..376cb448a 100644 --- a/helm/ocaml/extlib/hExtlib.mli +++ b/helm/ocaml/extlib/hExtlib.mli @@ -65,5 +65,5 @@ type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b } (** @return a profiling function; [s] is used for labelling the total time at * the end of the execution *) -val profile : string -> profiler +val profile : ?enable:bool -> string -> profiler -- 2.39.2