X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=fbbb10a6eefecebf6af669bf81e41be57330d8c1;hb=b38de2d3fa8bbe346c59c18bbeb889f29e493f63;hp=60b6129b1c2db4ca806e4460872e95db635f525d;hpb=5bb1c1ed4a30a99751414b7519efb5c58283d649;p=helm.git diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 60b6129b1..fbbb10a6e 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -163,13 +163,13 @@ and type_of_aux' metasenv context t = | C.Meta (n,l) -> let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in let subst',metasenv' = - check_metasenv_consistency subst metasenv context canonical_context l + check_metasenv_consistency n subst metasenv context canonical_context l in CicSubstitution.lift_meta l ty, subst', metasenv' | C.Sort s -> C.Sort C.Type, (*CSC manca la gestione degli universi!!! *) subst,metasenv - | C.Implicit -> raise (Impossible 21) + | C.Implicit _ -> raise (Impossible 21) | C.Cast (te,ty) -> let _,subst',metasenv' = type_of_aux subst metasenv context ty in @@ -389,7 +389,9 @@ and type_of_aux' metasenv context t = (* check_metasenv_consistency checks that the "canonical" context of a metavariable is consitent - up to relocation via the relocation list l - with the actual context *) - and check_metasenv_consistency subst metasenv context canonical_context l = + and check_metasenv_consistency + metano subst metasenv context canonical_context l + = let module C = Cic in let module R = CicReduction in let module S = CicSubstitution in @@ -417,7 +419,7 @@ and type_of_aux' metasenv context t = | Some t,Some (_,C.Def (ct,_)) -> (try CicUnification.fo_unif_subst subst context metasenv t ct - with _ -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct)))) + with e -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with CicUnification.AssertFailure msg -> msg | _ -> (Printexc.to_string e))))) | Some t,Some (_,C.Decl ct) -> let inferredty,subst',metasenv' = type_of_aux subst metasenv context t @@ -425,9 +427,12 @@ and type_of_aux' metasenv context t = (try CicUnification.fo_unif_subst subst' context metasenv' inferredty ct - with _ -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct)))) + with e -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with CicUnification.AssertFailure msg -> msg | _ -> (Printexc.to_string e))))) | None, Some _ -> - raise (NotRefinable "The local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context") + raise (NotRefinable (sprintf + "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" + (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) + (CicMetaSubst.ppcontext subst canonical_context))) ) (subst,metasenv) l lifted_canonical_context and check_exp_named_subst metasubst metasenv context = @@ -461,8 +466,9 @@ and type_of_aux' metasenv context t = and sort_of_prod subst metasenv context (name,s) (t1, t2) = let module C = Cic in + let context_for_t2 = (Some (name,C.Decl s))::context in let t1'' = CicMetaSubst.whd subst context t1 in - let t2'' = CicMetaSubst.whd subst ((Some (name,C.Decl s))::context) t2 in + let t2'' = CicMetaSubst.whd subst context_for_t2 t2 in match (t1'', t2'') with (C.Sort s1, C.Sort s2) when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *) @@ -470,20 +476,23 @@ and type_of_aux' metasenv context t = | (C.Sort s1, C.Sort s2) -> (*CSC manca la gestione degli universi!!! *) C.Sort C.Type,subst,metasenv - | (C.Meta _,_) | (_,C.Meta _) -> + | (C.Meta _, C.Sort _) -> t2'',subst,metasenv + | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) -> (* TODO how can we force the meta to become a sort? If we don't we * brake the invariant that refine produce only well typed terms *) (* TODO if we check the non meta term and if it is a sort then we are * likely to know the exact value of the result e.g. if the rhs is a * Sort (Prop | Set | CProp) then the result is the rhs *) - let (metasenv, idx) = CicMkImplicit.mk_implicit metasenv context in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context + let (metasenv,idx) = + CicMkImplicit.mk_implicit_sort metasenv in + let (subst, metasenv) = + CicUnification.fo_unif_subst subst context_for_t2 metasenv + (C.Meta (idx,[])) t2'' in - C.Meta (idx, irl), subst, metasenv + t2'',subst,metasenv | (_,_) -> raise (NotRefinable (sprintf - "Two types were expected, found %s (that reduces to %s) and %s (that reducecs to %s)" + "Two types were expected, found %s (that reduces to %s) and %s (that reduces to %s)" (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2) (CicPp.ppterm t2''))) @@ -499,14 +508,33 @@ and type_of_aux' metasenv context t = | Some t -> Some (CicMetaSubst.lift subst 1 t) ) args in let argty' = CicMetaSubst.lift subst (List.length args) argty in - let context'' = Some (Cic.Anonymous, Cic.Decl argty') :: context' in + let name = + (* The name must be fresh for (context'@context). *) + (* Nevertheless, argty is well-typed only in context. *) + (* Thus I generate a name (name_hint) in context and *) + (* then I generate a name --- using the hint name_hint *) + (* --- that is fresh in (context'@context). *) + let name_hint = + FreshNamesGenerator.mk_fresh_name + (CicMetaSubst.apply_subst_metasenv subst metasenv) + (CicMetaSubst.apply_subst_context subst context) + Cic.Anonymous + (CicMetaSubst.apply_subst subst argty) + in + (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *) + FreshNamesGenerator.mk_fresh_name + [] (context'@context) name_hint (Cic.Sort Cic.Prop) + in + let context'' = Some (name, Cic.Decl argty') :: context' in let (metasenv, idx) = - CicMkImplicit.mk_implicit metasenv (context'' @ context) in + CicMkImplicit.mk_implicit_type metasenv (context'' @ context) in let irl = - (Some (Cic.Rel 1))::args'@(CicMkImplicit.identity_relocation_list_for_metavariable ~start:2 context) + (Some (Cic.Rel 1))::args' @ + (CicMkImplicit.identity_relocation_list_for_metavariable ~start:2 + context) in let newmeta = Cic.Meta (idx, irl) in - let prod = Cic.Prod (Cic.Anonymous, argty, newmeta) in + let prod = Cic.Prod (name, argty, newmeta) in let (_, subst, metasenv) = type_of_aux subst metasenv context prod in let (subst, metasenv) = CicUnification.fo_unif_subst subst context metasenv resty prod @@ -520,9 +548,42 @@ and type_of_aux' metasenv context t = let ty,subst',metasenv' = type_of_aux [] metasenv context t in - (CicMetaSubst.apply_subst subst' t, - CicMetaSubst.apply_subst subst' ty, - CicMetaSubst.apply_subst_metasenv subst' metasenv') + let substituted_t = CicMetaSubst.apply_subst subst' t in + let substituted_ty = CicMetaSubst.apply_subst subst' ty in + let substituted_metasenv = + CicMetaSubst.apply_subst_metasenv subst' metasenv' + in + let cleaned_t = + FreshNamesGenerator.clean_dummy_dependent_types substituted_t in + let cleaned_ty = + FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in + let cleaned_metasenv = + List.map + (function (n,context,ty) -> + let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in + let context' = + List.map + (function + None -> None + | Some (n, Cic.Decl t) -> + Some (n, + Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t)) + | Some (n, Cic.Def (bo,ty)) -> + let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in + let ty' = + match ty with + None -> None + | Some ty -> + Some (FreshNamesGenerator.clean_dummy_dependent_types ty) + in + Some (n, Cic.Def (bo',ty')) + ) context + in + (n,context',ty') + ) substituted_metasenv + in + (cleaned_t,cleaned_ty,cleaned_metasenv) + ;; (* DEBUGGING ONLY *)