From: Enrico Tassi Date: Thu, 13 Apr 2006 13:06:25 +0000 (+0000) Subject: in eta_finxing: type_of_aux' not called on eta_fixed terms X-Git-Tag: 0.4.95@7852~1513 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=920e626985b94b5f6de11046c917d8012fa3d2ec;p=helm.git 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/components/cic_acic/doubleTypeInference.ml b/components/cic_acic/doubleTypeInference.ml index 214f656c3..fd9627046 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) @@ -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/components/cic_acic/doubleTypeInference.mli b/components/cic_acic/doubleTypeInference.mli index 86d8b23fa..dcc7b66bd 100644 --- a/components/cic_acic/doubleTypeInference.mli +++ b/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/components/cic_acic/eta_fixing.ml b/components/cic_acic/eta_fixing.ml index 22d26e1bd..78789179f 100644 --- a/components/cic_acic/eta_fixing.ml +++ b/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')