let debug_print = fun _ -> ()
+let profiler = HExtlib.profile "CicRefine.fo_unif"
+
let fo_unif_subst subst context metasenv t1 t2 ugraph =
try
+let foo () =
CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
+in profiler.HExtlib.profile foo ()
with
(CicUnification.UnificationFailure msg) -> raise (RefineFailure (UnificationFailure msg))
| (CicUnification.Uncertain msg) -> raise (Uncertain msg)
try
fo_unif_subst subst context metasenv hetype hetype' ugraph
with exn ->
- debug_print (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
+ debug_print (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
(CicPp.ppterm hetype)
(CicPp.ppterm hetype')
(CicMetaSubst.ppmetasenv [] metasenv)
- (CicMetaSubst.ppsubst subst));
+ (CicMetaSubst.ppsubst subst)));
raise exn
in
try
let (t,ty,m) =
type_of_aux' metasenv context term in
- debug_print
- ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
- debug_print
- ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []);
+ debug_print (lazy
+ ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
+ debug_print (lazy
+ ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
(t,ty,m)
with
| RefineFailure msg as e ->
- debug_print ("@@@ REFINE FAILED: " ^ msg);
+ debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
raise e
| Uncertain msg as e ->
- debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);
+ debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
raise e
;; *)
+
+let profiler2 = HExtlib.profile "CicRefine"
+
+let type_of_aux' metasenv context term ugraph =
+ profiler2.HExtlib.profile (type_of_aux' metasenv context term) ugraph
+
+let typecheck metasenv uri obj =
+ profiler2.HExtlib.profile (typecheck metasenv uri) obj