1. Parameter enable (default true) added to HExtlib.profile

2. profiling code commented out in cicReduction since it affects performances
   very badly

diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml
index 39133ac92a4beb9ce9a5bbd87c4ca2f27387fc79..813a589d603d7c2025d9cfb97686d10573e5064c 100644 (file)
--- 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 9f4f2d9c904bef51d1c3121eeeec90aad4ca050e..052205da823f3a524375eb32304fa1947af3c305 100644 (file)
--- 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 32fb59d473942a2f4ac61a72b07dacd391c4a18e..376cb448ab204d19a50873b6fa69ad8fcb765d7c 100644 (file)
--- 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