2. profiling code commented out in cicReduction since it affects performances
very badly
exception ReferenceToInductiveDefinition;;
let debug = false
exception ReferenceToInductiveDefinition;;
let debug = false
let debug_print s = if debug then prerr_endline (Lazy.force s)
let fdebug = ref 1;;
let debug_print s = if debug then prerr_endline (Lazy.force s)
let fdebug = ref 1;;
-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
let reduce ~delta ?(subst = []) context : config -> Cic.term =
let module C = Cic in
module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
module U = UriManager;;
module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
module U = UriManager;;
-let profiler_whd = HExtlib.profile "are_convertible.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 =
(* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
* fallbacks to structural equality *)
let (===) x y =
debug_print (lazy (CicPp.ppterm t2));
debug_print (lazy (CicPp.ppterm (whd ~subst context t2)))
| _ -> ()); *)
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
debug t1' [t2'] "POSTWHD";
aux2 test_equality_only t1' t2' ugraph
end
let are_convertible = are_convertible whd
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 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
let rec normalize ?(delta=true) ?(subst=[]) ctx term =
let module C = Cic in
let profiling_enabled = true
type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b }
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 =
function s ->
let total = ref 0.0 in
let profile f x =
(** @return a profiling function; [s] is used for labelling the total time at
* the end of the execution *)
(** @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