X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_acic%2FdoubleTypeInference.ml;h=1ea800a6b9307ec13065fe6d5c853f01a1090ba8;hb=9e18c7f8aa6c5b905598521c769c1a2f58c13262;hp=214f656c38d5db4d27f889f9b6019b3b28d4eb12;hpb=3f00ce2e2e2f2d443e942d86c394200554ba2496;p=helm.git

diff --git a/components/cic_acic/doubleTypeInference.ml b/components/cic_acic/doubleTypeInference.ml
index 214f656c3..1ea800a6b 100644
--- a/components/cic_acic/doubleTypeInference.ml
+++ b/components/cic_acic/doubleTypeInference.ml
@@ -33,20 +33,11 @@ exception WrongUriToMutualInductiveDefinitions of string;;
 exception ListTooShort;;
 exception RelToHiddenHypothesis;;
 
-let syntactic_equality_add_time = ref 0.0;;
-let type_of_aux'_add_time = ref 0.0;;
-let number_new_type_of_aux'_double_work = ref 0;;
-let number_new_type_of_aux' = ref 0;;
-let number_new_type_of_aux'_prop = ref 0;;
-
-let double_work = ref 0;;
-
 let xxx_type_of_aux' m c t =
- let t1 = Sys.time () in
- let res,_ = CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph in
- let t2 = Sys.time () in
- type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ;
- res
+ try 
+   Some (fst (CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph))
+ with
+ | CicTypeChecker.TypeCheckerFailure _ -> None (* because eta_expansion *)
 ;;
 
 type types = {synthesized : Cic.term ; expected : Cic.term option};;
@@ -241,15 +232,6 @@ let syntactic_equality t t' =
    _ -> false
 ;;
 
-let xxx_syntactic_equality t t' =
- let t1 = Sys.time () in
- let res = syntactic_equality t t' in
- let t2 = Sys.time () in
- syntactic_equality_add_time := !syntactic_equality_add_time +. t2 -. t1 ;
- res
-;;
-
-
 let rec split l n =
  match (l,n) with
     (l,0) -> ([], l)
@@ -321,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             *)
@@ -376,14 +370,15 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
                  _,None -> ()
                | Some t,Some (_,C.Def (ct,_)) ->
                   let expected_type =
-                   R.whd context
-                    (xxx_type_of_aux' metasenv context ct)
+                    match xxx_type_of_aux' metasenv context ct with
+                    | None -> None
+                    | Some t -> Some (R.whd context t)
                   in
                    (* Maybe I am a bit too paranoid, because   *)
                    (* if the term is well-typed than t and ct  *)
                    (* are convertible. Nevertheless, I compute *)
                    (* the expected type.                       *)
-                   ignore (type_of_aux context t (Some expected_type))
+                   ignore (type_of_aux context t expected_type)
                | Some t,Some (_,C.Decl ct) ->
                   ignore (type_of_aux context t (Some ct))
                | _,_ -> assert false (* the term is not well typed!!! *)
@@ -510,11 +505,12 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
         in
         let (parameters, arguments,exp_named_subst) =
          let type_of_term =
-          xxx_type_of_aux' metasenv context term
+           match xxx_type_of_aux' metasenv context term with
+           | None -> None
+           | Some t -> Some (beta_reduce t)
          in
           match
-           R.whd context (type_of_aux context term
-            (Some (beta_reduce type_of_term)))
+           R.whd context (type_of_aux context term type_of_term)
           with
              (*CSC manca il caso dei CAST *)
              C.MutInd (uri',i',exp_named_subst) ->
@@ -551,11 +547,15 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
                 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
               in
                let expectedtype =
-                type_of_branch context parsno need_dummy outtype cons
-                  (xxx_type_of_aux' metasenv context cons)
+                 match xxx_type_of_aux' metasenv context cons with
+                 | None -> None
+                 | Some t -> 
+                     Some 
+                       (beta_reduce 
+                         (type_of_branch context parsno need_dummy outtype 
+                           cons t))
                in
-                ignore (type_of_aux context p
-                 (Some (beta_reduce expectedtype))) ;
+                ignore (type_of_aux context p expectedtype);
                 j+1
             ) 1 (List.combine pl cl)
           in
@@ -621,7 +621,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
          None ->
           (* No expected type *)
           {synthesized = synthesized' ; expected = None}, synthesized
-       | Some ty when xxx_syntactic_equality synthesized' ty ->
+       | Some ty when syntactic_equality synthesized' ty ->
           (* The expected type is synthactically equal to *)
           (* the synthesized type. Let's forget it.       *)
           {synthesized = synthesized' ; expected = None}, synthesized
@@ -629,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 =