X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_acic%2FdoubleTypeInference.ml;h=4ca88d4b96a411318a6be88d2c6c1ef4d9e6302c;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=1671b98d25321ca6492f8565715ba99d5ddfedba;hpb=6719c0e318b312b51b089fea3d69d1b7103245ea;p=helm.git diff --git a/helm/software/components/cic_acic/doubleTypeInference.ml b/helm/software/components/cic_acic/doubleTypeInference.ml index 1671b98d2..4ca88d4b9 100644 --- a/helm/software/components/cic_acic/doubleTypeInference.ml +++ b/helm/software/components/cic_acic/doubleTypeInference.ml @@ -97,64 +97,72 @@ let rec does_not_occur n = ) fl true ;; -let rec beta_reduce = +(* FG: if ~clean:true, unreferenced letins are removed *) +(* (beta-reducttion can cause unreferenced letins) *) +let rec beta_reduce ?(clean=false)= let module S = CicSubstitution in let module C = Cic in function C.Rel _ as t -> t | C.Var (uri,exp_named_subst) -> let exp_named_subst' = - List.map (function (i,t) -> i, beta_reduce t) exp_named_subst + List.map (function (i,t) -> i, beta_reduce ~clean t) exp_named_subst in C.Var (uri,exp_named_subst') | C.Meta (n,l) -> C.Meta (n, List.map - (function None -> None | Some t -> Some (beta_reduce t)) l + (function None -> None | Some t -> Some (beta_reduce ~clean t)) l ) | C.Sort _ as t -> t | C.Implicit _ -> assert false | C.Cast (te,ty) -> - C.Cast (beta_reduce te, beta_reduce ty) + C.Cast (beta_reduce ~clean te, beta_reduce ~clean ty) | C.Prod (n,s,t) -> - C.Prod (n, beta_reduce s, beta_reduce t) + C.Prod (n, beta_reduce ~clean s, beta_reduce ~clean t) | C.Lambda (n,s,t) -> - C.Lambda (n, beta_reduce s, beta_reduce t) + C.Lambda (n, beta_reduce ~clean s, beta_reduce ~clean t) | C.LetIn (n,s,ty,t) -> - C.LetIn (n, beta_reduce s, beta_reduce ty, beta_reduce t) + let t' = beta_reduce ~clean t in + if clean && does_not_occur 1 t' then + (* since [Rel 1] does not occur in typ, substituting any term *) + (* in place of [Rel 1] is equivalent to delifting once *) + CicSubstitution.subst (C.Implicit None) t' + else + C.LetIn (n, beta_reduce ~clean s, beta_reduce ~clean ty, t') | C.Appl ((C.Lambda (name,s,t))::he::tl) -> let he' = S.subst he t in if tl = [] then - beta_reduce he' + beta_reduce ~clean he' else (match he' with - C.Appl l -> beta_reduce (C.Appl (l@tl)) - | _ -> beta_reduce (C.Appl (he'::tl))) + C.Appl l -> beta_reduce ~clean (C.Appl (l@tl)) + | _ -> beta_reduce ~clean (C.Appl (he'::tl))) | C.Appl l -> - C.Appl (List.map beta_reduce l) + C.Appl (List.map (beta_reduce ~clean) l) | C.Const (uri,exp_named_subst) -> let exp_named_subst' = - List.map (function (i,t) -> i, beta_reduce t) exp_named_subst + List.map (function (i,t) -> i, beta_reduce ~clean t) exp_named_subst in C.Const (uri,exp_named_subst') | C.MutInd (uri,i,exp_named_subst) -> let exp_named_subst' = - List.map (function (i,t) -> i, beta_reduce t) exp_named_subst + List.map (function (i,t) -> i, beta_reduce ~clean t) exp_named_subst in C.MutInd (uri,i,exp_named_subst') | C.MutConstruct (uri,i,j,exp_named_subst) -> let exp_named_subst' = - List.map (function (i,t) -> i, beta_reduce t) exp_named_subst + List.map (function (i,t) -> i, beta_reduce ~clean t) exp_named_subst in C.MutConstruct (uri,i,j,exp_named_subst') | C.MutCase (sp,i,outt,t,pl) -> - C.MutCase (sp,i,beta_reduce outt,beta_reduce t, - List.map beta_reduce pl) + C.MutCase (sp,i,beta_reduce ~clean outt,beta_reduce ~clean t, + List.map (beta_reduce ~clean) pl) | C.Fix (i,fl) -> let fl' = List.map (function (name,i,ty,bo) -> - name,i,beta_reduce ty,beta_reduce bo + name,i,beta_reduce ~clean ty,beta_reduce ~clean bo ) fl in C.Fix (i,fl') @@ -162,7 +170,7 @@ let rec beta_reduce = let fl' = List.map (function (name,ty,bo) -> - name,beta_reduce ty,beta_reduce bo + name,beta_reduce ~clean ty,beta_reduce ~clean bo ) fl in C.CoFix (i,fl') @@ -339,17 +347,18 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = | C.Lambda (n,s,t) -> (* Let's visit all the subterms that will not be visited later *) let _ = type_of_aux context s None in - let expected_target_type = + let n, expected_target_type = match expectedty with - None -> None + | None -> n, None | Some expectedty' -> - let ty = + let n, ty = match R.whd context expectedty' with - C.Prod (_,_,expected_target_type) -> - beta_reduce expected_target_type + | C.Prod (n',_,expected_target_type) -> + let xtt = beta_reduce expected_target_type in + if n <> C.Anonymous then n, xtt else n', xtt | _ -> assert false in - Some ty + n, Some ty in let type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type @@ -366,8 +375,8 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = (* Checks suppressed *) type_of_aux ((Some (n,(C.Def (s,ty))))::context) t None in (* CicSubstitution.subst s t_typ *) - if does_not_occur 1 t_typ then - (* since [Rel 1] does not occur in typ, substituting any term *) + if does_not_occur 1 t_typ then + (* since [Rel 1] does not occur in typ, substituting any term *) (* in place of [Rel 1] is equivalent to delifting once *) CicSubstitution.subst (C.Implicit None) t_typ else @@ -550,7 +559,8 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = let (_,ty,_) = List.nth fl i in ty in - let synthesized' = beta_reduce synthesized in +(* FG: beta-reduction can cause unreferenced letins *) + let synthesized' = beta_reduce ~clean:true synthesized in let synthesized' = !pack_coercion metasenv context synthesized' in let types,res = match expectedty with