X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=b450d25021d35ab496f4bc87a7831c343d833411;hb=0ab691fe2f45a742c2aa83446a120675910b03d9;hp=a5221c22976f3d3c337121cbb116e82b7a0bb88c;hpb=e82e30cc9885f2acdf03801c637aaacfd8c81d71;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index a5221c229..b450d2502 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -40,9 +40,13 @@ exception AssertFailure of string;;
 
 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)
@@ -873,11 +877,11 @@ and type_of_aux' metasenv context t ugraph =
       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
@@ -1070,16 +1074,24 @@ let type_of_aux' metasenv context term =
  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