From: Claudio Sacerdoti Coen Date: Tue, 3 Feb 2004 13:04:33 +0000 (+0000) Subject: eat_prods reimplemented to generalize the output type of the application X-Git-Tag: V_0_2_3~99 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5bb1c1ed4a30a99751414b7519efb5c58283d649;p=helm.git eat_prods reimplemented to generalize the output type of the application a bit more (when it is a metavariable). --- diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index a6506d5ca..60b6129b1 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -25,6 +25,8 @@ open Printf +exception RefineFailure of string;; + exception Impossible of int;; exception NotRefinable of string;; exception Uncertain of string;; @@ -33,7 +35,6 @@ exception WrongUriToVariable of string;; exception ListTooShort;; exception WrongUriToMutualInductiveDefinitions of string;; exception RelToHiddenHypothesis;; -exception MetasenvInconsistency;; exception WrongArgumentNumber;; let fdebug = ref 0;; @@ -416,7 +417,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 MetasenvInconsistency) + 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)))) | Some t,Some (_,C.Decl ct) -> let inferredty,subst',metasenv' = type_of_aux subst metasenv context t @@ -424,9 +425,9 @@ and type_of_aux' metasenv context t = (try CicUnification.fo_unif_subst subst' context metasenv' inferredty ct - with _ -> raise MetasenvInconsistency) - | _, _ -> - raise MetasenvInconsistency + 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)))) + | None, Some _ -> + raise (NotRefinable "The local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context") ) (subst,metasenv) l lifted_canonical_context and check_exp_named_subst metasubst metasenv context = @@ -482,41 +483,46 @@ and type_of_aux' metasenv context t = C.Meta (idx, irl), subst, metasenv | (_,_) -> raise (NotRefinable (sprintf - "Two types were expected, found %s of type %s and %s of type %s" + "Two types were expected, found %s (that reduces to %s) and %s (that reducecs to %s)" (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2) (CicPp.ppterm t2''))) and eat_prods subst metasenv context hetype tlbody_and_type = - (* TODO to be reviewed *) - List.fold_left - (fun (resty, subst, metasenv) (arg, argty) -> - let context' = Some (Cic.Anonymous, Cic.Decl argty) :: context in - let (metasenv, idx) = CicMkImplicit.mk_implicit metasenv context' in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context' - in - let newmeta = Cic.Meta (idx, irl) in - let prod = Cic.Prod (Cic.Anonymous, 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 - in - (CicMetaSubst.subst subst arg newmeta, subst, metasenv)) - (hetype, subst, metasenv) tlbody_and_type + let rec aux context' args (resty,subst,metasenv) = + function + [] -> resty,subst,metasenv + | (arg,argty)::tl -> + let args' = + List.map + (function + None -> assert false + | 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 (metasenv, idx) = + CicMkImplicit.mk_implicit metasenv (context'' @ context) in + let irl = + (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 (_, subst, metasenv) = type_of_aux subst metasenv context prod in + let (subst, metasenv) = + CicUnification.fo_unif_subst subst context metasenv resty prod + in + aux context'' (Some arg :: args) + (CicMetaSubst.subst subst arg newmeta, subst, metasenv) tl + in + aux [] [] (hetype,subst,metasenv) tlbody_and_type in let ty,subst',metasenv' = type_of_aux [] metasenv context t in - (* we get rid of the metavariables that have been instantiated *) - let metasenv'' = - List.filter - (function (i,_,_) -> not (List.exists (function (j,_) -> j=i) subst')) - metasenv' - in (CicMetaSubst.apply_subst subst' t, CicMetaSubst.apply_subst subst' ty, - CicMetaSubst.apply_subst_metasenv subst' metasenv'') + CicMetaSubst.apply_subst_metasenv subst' metasenv') ;; (* DEBUGGING ONLY *)