From da971c367f15b855e7a4af88829f1daaadc3bd3c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 16 May 2006 08:23:42 +0000 Subject: [PATCH] more profiling and less assertions --- .../components/cic_acic/doubleTypeInference.ml | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/helm/software/components/cic_acic/doubleTypeInference.ml b/helm/software/components/cic_acic/doubleTypeInference.ml index fd9627046..1ea800a6b 100644 --- a/helm/software/components/cic_acic/doubleTypeInference.ml +++ b/helm/software/components/cic_acic/doubleTypeInference.ml @@ -303,6 +303,18 @@ let type_of_mutual_inductive_constr uri i j = let pack_coercion = ref (fun _ _ _ -> assert false);; +let profiler_for_find = HExtlib.profile "CicHash ADD" ;; + +let cic_CicHash_add a b c = + profiler_for_find.HExtlib.profile (Cic.CicHash.add a b) c +;; + +let profiler_for_find1 = HExtlib.profile "CicHash MEM" ;; + +let cic_CicHash_mem a b = + profiler_for_find1.HExtlib.profile (Cic.CicHash.mem a) b +;; + (* type_of_aux' is just another name (with a different scope) for type_of_aux *) let rec type_of_aux' subterms_to_types metasenv context t expectedty = (* Coscoy's double type-inference algorithm *) @@ -617,8 +629,8 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = {synthesized = synthesized' ; expected = Some expectedty'}, expectedty' in - assert (not (Cic.CicHash.mem subterms_to_types t)); - Cic.CicHash.add subterms_to_types t types ; +(* assert (not (cic_CicHash_mem subterms_to_types t));*) + cic_CicHash_add subterms_to_types t types ; res and visit_exp_named_subst context uri exp_named_subst = -- 2.39.2