in eta_finxing: type_of_aux' not called on eta_fixed terms

[helm.git] / helm / software / components / cic_acic / doubleTypeInference.ml

diff --git a/helm/software/components/cic_acic/doubleTypeInference.ml b/helm/software/components/cic_acic/doubleTypeInference.ml
index 214f656c38d5db4d27f889f9b6019b3b28d4eb12..fd96270467aa746901de0ff2ba7e9d175f186197 100644 (file)
--- a/helm/software/components/cic_acic/doubleTypeInference.ml
+++ b/helm/software/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)
@@ -376,14 +358,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 +493,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 +535,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 +609,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