in eta_finxing: type_of_aux' not called on eta_fixed terms

in doubletypeInference calls to type_of_aux' wrapped because of eta fixing

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

diff --git a/helm/software/components/cic_acic/doubleTypeInference.mli b/helm/software/components/cic_acic/doubleTypeInference.mli
index 86d8b23fabee6cac29723f5866a29dfb1f981d72..dcc7b66bd19f6e6821b6651b2e527f9b55cab1a7 100644 (file)
--- a/helm/software/components/cic_acic/doubleTypeInference.mli
+++ b/helm/software/components/cic_acic/doubleTypeInference.mli
@@ -6,12 +6,6 @@ exception WrongUriToMutualInductiveDefinitions of string
 exception ListTooShort
 exception RelToHiddenHypothesis
 
-val syntactic_equality_add_time: float ref
-val type_of_aux'_add_time: float ref
-val number_new_type_of_aux'_double_work: int ref
-val number_new_type_of_aux': int ref
-val number_new_type_of_aux'_prop: int ref
-
 type types = {synthesized : Cic.term ; expected : Cic.term option};;
 
 val pack_coercion : (Cic.metasenv -> Cic.context -> Cic.term -> Cic.term) ref;;

diff --git a/helm/software/components/cic_acic/eta_fixing.ml b/helm/software/components/cic_acic/eta_fixing.ml
index 22d26e1bdd19920dc4906187efc992532bef0b8c..78789179f8c739e84c7c29abdaef003cc0f67731 100644 (file)
--- a/helm/software/components/cic_acic/eta_fixing.ml
+++ b/helm/software/components/cic_acic/eta_fixing.ml
@@ -202,17 +202,14 @@ let eta_fix metasenv context t =
    | C.LetIn (n,s,t) -> 
        C.LetIn 
         (n,eta_fix' context s,eta_fix' ((Some (n,(C.Def (s,None))))::context) t)
-   | C.Appl l -> 
-       let l' =  List.map (eta_fix' context) l 
-       in 
-       (match l' with
-           [] -> assert false
-         | he::tl ->
-            let ty,_ = 
-              CicTypeChecker.type_of_aux' metasenv context he 
-               CicUniv.empty_ugraph 
-           in
-              fix_according_to_type ty he tl
+   | C.Appl [] -> assert false 
+   | C.Appl (he::tl) -> 
+       let tl' =  List.map (eta_fix' context) tl in 
+       let ty,_ = 
+         CicTypeChecker.type_of_aux' metasenv context he 
+           CicUniv.empty_ugraph 
+       in
+       fix_according_to_type ty (eta_fix' context he) tl'
 (*
          C.Const(uri,exp_named_subst)::l'' ->
            let constant_type =
@@ -224,7 +221,7 @@ let eta_fix metasenv context t =
              ) in 
            fix_according_to_type 
              constant_type (C.Const(uri,exp_named_subst)) l''
-        | _ -> C.Appl l' *))
+        | _ -> C.Appl l' *)
    | C.Const (uri,exp_named_subst) ->
        let exp_named_subst' = fix_exp_named_subst context exp_named_subst in
         C.Const (uri,exp_named_subst')