From 34b6e08c53e9fe5cac7c426188c6043ca48d0df2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 21 Sep 2005 16:52:11 +0000 Subject: [PATCH] More profiling code. --- helm/ocaml/cic_unification/cicRefine.ml | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index b0bc8c623..0b63f6a8c 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 = CicUtil.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.CicUtil.profile foo () with (CicUnification.UnificationFailure msg) -> raise (RefineFailure (UnificationFailure msg)) | (CicUnification.Uncertain msg) -> raise (Uncertain msg) @@ -1083,3 +1087,11 @@ let type_of_aux' metasenv context term = debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg)); raise e ;; *) + +let profiler2 = CicUtil.profile "CicRefine" + +let type_of_aux' metasenv context term ugraph = + profiler2.CicUtil.profile (type_of_aux' metasenv context term) ugraph + +let typecheck metasenv uri obj = + profiler2.CicUtil.profile (typecheck metasenv uri) obj -- 2.39.2