X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_acic%2FdoubleTypeInference.ml;h=905d1e6bc0be63568a8998ac6936f48cb59d2a78;hb=aa791b78493b604792383cf6326877d0d53e0458;hp=214f656c38d5db4d27f889f9b6019b3b28d4eb12;hpb=3f00ce2e2e2f2d443e942d86c394200554ba2496;p=helm.git diff --git a/components/cic_acic/doubleTypeInference.ml b/components/cic_acic/doubleTypeInference.ml index 214f656c3..905d1e6bc 100644 --- a/components/cic_acic/doubleTypeInference.ml +++ b/components/cic_acic/doubleTypeInference.ml @@ -33,20 +33,13 @@ 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;; +(*CSC: must alfa-conversion be considered or not? *) 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};; @@ -58,6 +51,8 @@ let rec does_not_occur n = function C.Rel m when m = n -> false | C.Rel _ +(* FG/CSC: maybe we assume the meta is guarded so we do not recur on its *) +(* explicit subsitutions (copied from the kernel) ??? *) | C.Meta _ | C.Sort _ | C.Implicit _ -> true @@ -172,84 +167,6 @@ let rec beta_reduce = C.CoFix (i,fl') ;; -(* syntactic_equality up to the *) -(* distinction between fake dependent products *) -(* and non-dependent products, alfa-conversion *) -(*CSC: must alfa-conversion be considered or not? *) -let syntactic_equality t t' = - let module C = Cic in - let rec syntactic_equality t t' = - if t = t' then true - else - match t, t' with - C.Var (uri,exp_named_subst), C.Var (uri',exp_named_subst') -> - UriManager.eq uri uri' && - syntactic_equality_exp_named_subst exp_named_subst exp_named_subst' - | C.Cast (te,ty), C.Cast (te',ty') -> - syntactic_equality te te' && - syntactic_equality ty ty' - | C.Prod (_,s,t), C.Prod (_,s',t') -> - syntactic_equality s s' && - syntactic_equality t t' - | C.Lambda (_,s,t), C.Lambda (_,s',t') -> - syntactic_equality s s' && - syntactic_equality t t' - | C.LetIn (_,s,t), C.LetIn(_,s',t') -> - syntactic_equality s s' && - syntactic_equality t t' - | C.Appl l, C.Appl l' -> - List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l' - | C.Const (uri,exp_named_subst), C.Const (uri',exp_named_subst') -> - UriManager.eq uri uri' && - syntactic_equality_exp_named_subst exp_named_subst exp_named_subst' - | C.MutInd (uri,i,exp_named_subst), C.MutInd (uri',i',exp_named_subst') -> - UriManager.eq uri uri' && i = i' && - syntactic_equality_exp_named_subst exp_named_subst exp_named_subst' - | C.MutConstruct (uri,i,j,exp_named_subst), - C.MutConstruct (uri',i',j',exp_named_subst') -> - UriManager.eq uri uri' && i = i' && j = j' && - syntactic_equality_exp_named_subst exp_named_subst exp_named_subst' - | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') -> - UriManager.eq sp sp' && i = i' && - syntactic_equality outt outt' && - syntactic_equality t t' && - List.fold_left2 - (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl' - | C.Fix (i,fl), C.Fix (i',fl') -> - i = i' && - List.fold_left2 - (fun b (_,i,ty,bo) (_,i',ty',bo') -> - b && i = i' && - syntactic_equality ty ty' && - syntactic_equality bo bo') true fl fl' - | C.CoFix (i,fl), C.CoFix (i',fl') -> - i = i' && - List.fold_left2 - (fun b (_,ty,bo) (_,ty',bo') -> - b && - syntactic_equality ty ty' && - syntactic_equality bo bo') true fl fl' - | _, _ -> false (* we already know that t != t' *) - and syntactic_equality_exp_named_subst exp_named_subst1 exp_named_subst2 = - List.fold_left2 - (fun b (_,t1) (_,t2) -> b && syntactic_equality t1 t2) true - exp_named_subst1 exp_named_subst2 - in - try - syntactic_equality t t' - with - _ -> 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 +238,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 +305,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 +440,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 +482,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 +556,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 CicUtil.alpha_equivalence synthesized' ty -> (* The expected type is synthactically equal to *) (* the synthesized type. Let's forget it. *) {synthesized = synthesized' ; expected = None}, synthesized @@ -629,8 +564,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 =