X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=c1b70df8d4e6ece7d71de3b8950914efb6d3c5f4;hb=7ec7262cfa317c1962164350361f82a56c5d1826;hp=e8ea0769de76416d369ba4d5f5b9ff63ee0ed945;hpb=655906d74521fa49de332f54ec34bfc9d9744151;p=helm.git diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index e8ea0769d..c1b70df8d 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -132,11 +132,12 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt | _ -> raise (AssertFailure "Prod or MutInd expected") and type_of_aux' metasenv context t = - let rec type_of_aux subst metasenv context = + let rec type_of_aux subst metasenv context t = let module C = Cic in let module S = CicSubstitution in let module U = UriManager in - function + match t with +(* function *) C.Rel n -> (try match List.nth context (n - 1) with @@ -156,11 +157,20 @@ and type_of_aux' metasenv context t = in ty,subst',metasenv' | C.Meta (n,l) -> - let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in - let subst',metasenv' = - check_metasenv_consistency n subst metasenv context canonical_context l - in - CicSubstitution.lift_meta l ty, subst', metasenv' + (try + let (canonical_context, term) = CicMetaSubst.lookup_subst n subst in + let subst,metasenv = + check_metasenv_consistency n subst metasenv context + canonical_context l + in + type_of_aux subst metasenv context (CicSubstitution.lift_meta l term) + with CicMetaSubst.SubstNotFound _ -> + let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in + let subst,metasenv = + check_metasenv_consistency n subst metasenv context + canonical_context l + in + CicSubstitution.lift_meta l ty, subst, metasenv) (* TASSI: CONSTRAINT *) | C.Sort (C.Type t) -> let t' = CicUniv.fresh() in @@ -214,7 +224,7 @@ and type_of_aux' metasenv context t = (* One-step LetIn reduction. Even faster than the previous solution. Moreover the inferred type is closer to the expected one. *) CicSubstitution.subst s inferredty,subst',metasenv' - | C.Appl (he::tl) when List.length tl > 0 -> + | C.Appl (he::((_::_) as tl)) -> let hetype,subst',metasenv' = type_of_aux subst metasenv context he in let tlbody_and_type,subst'',metasenv'' = List.fold_right @@ -267,13 +277,13 @@ and type_of_aux' metasenv context t = let no_args = count_prod arity in (* now, create a "generic" MutInd *) let metasenv,left_args = - CicMkImplicit.n_fresh_metas metasenv context no_left_params in + CicMkImplicit.n_fresh_metas metasenv subst context no_left_params in let metasenv,right_args = let no_right_params = no_args - no_left_params in if no_right_params < 0 then assert false - else CicMkImplicit.n_fresh_metas metasenv context no_right_params in + else CicMkImplicit.n_fresh_metas metasenv subst context no_right_params in let metasenv,exp_named_subst = - CicMkImplicit.fresh_subst metasenv context expl_params in + CicMkImplicit.fresh_subst metasenv subst context expl_params in let expected_type = if no_args = 0 then C.MutInd (uri,i,exp_named_subst) @@ -452,6 +462,7 @@ and type_of_aux' metasenv context t = | ((uri,t) as subst)::tl -> let typeofvar = CicSubstitution.subst_vars substs (type_of_variable uri) in +(* CSC: why was this code here? it is wrong (match CicEnvironment.get_cooked_obj ~trust:false uri with Cic.Variable (_,Some bo,_,_) -> raise @@ -463,16 +474,19 @@ and type_of_aux' metasenv context t = (RefineFailure ("Unkown variable definition " ^ UriManager.string_of_uri uri)) ) ; +*) let typeoft,metasubst',metasenv' = type_of_aux metasubst metasenv context t in - try - let metasubst'',metasenv'' = + let metasubst'',metasenv'' = + try fo_unif_subst metasubst' context metasenv' typeoft typeofvar - in - check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl - with _ -> - raise (RefineFailure "Wrong Explicit Named Substitution") + with _ -> + raise (RefineFailure + ("Wrong Explicit Named Substitution: " ^ CicMetaSubst.ppterm metasubst' typeoft ^ + " not unifiable with " ^ CicMetaSubst.ppterm metasubst' typeofvar)) + in + check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl in check_exp_named_subst_aux metasubst metasenv [] @@ -502,7 +516,7 @@ and type_of_aux' metasenv context t = * 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_sort metasenv in + CicMkImplicit.mk_implicit_sort metasenv subst in let (subst, metasenv) = fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' in @@ -517,13 +531,13 @@ and type_of_aux' metasenv context t = let rec mk_prod metasenv context = function [] -> - let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in + let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv subst context in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in metasenv,Cic.Meta (idx, irl) | (_,argty)::tl -> - let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in + let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv subst context in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in @@ -535,8 +549,8 @@ and type_of_aux' metasenv context t = (* 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) + FreshNamesGenerator.mk_fresh_name metasenv +(* (CicMetaSubst.apply_subst_metasenv subst metasenv) *) (CicMetaSubst.apply_subst_context subst context) Cic.Anonymous (CicMetaSubst.apply_subst subst argty) @@ -626,8 +640,8 @@ and type_of_aux' metasenv context t = in 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' + let substituted_metasenv = metasenv' +(* CicMetaSubst.apply_subst_metasenv subst' metasenv' *) in let cleaned_t = FreshNamesGenerator.clean_dummy_dependent_types substituted_t in