X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=c1b70df8d4e6ece7d71de3b8950914efb6d3c5f4;hb=b5ac1bf4e769c6713ede5938f719ee32be3a1fea;hp=36a25a6c227928f4fddb099195cc508a078e42d8;hpb=c0e0ae45ee6fba4118f519b9d07169ed6a7edc8c;p=helm.git diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 36a25a6c2..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,14 +157,29 @@ 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' - | C.Sort s -> - C.Sort C.Type, (*CSC manca la gestione degli universi!!! *) - 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 + if not (CicUniv.add_gt t' t ) then + assert false (* t' is fresh! an error in CicUniv *) + else + C.Sort (C.Type t'),subst,metasenv + (* TASSI: CONSTRAINT *) + | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())),subst,metasenv | C.Implicit _ -> raise (AssertFailure "21") | C.Cast (te,ty) -> let _,subst',metasenv' = @@ -208,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 @@ -261,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) @@ -308,6 +324,7 @@ and type_of_aux' metasenv context t = The easy case is when the outype is specified, that amount to a trivial check. Otherwise, we should guess a type from its instances *) + (* easy case *) let _, subst, metasenv = type_of_aux subst metasenv context @@ -445,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 @@ -456,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 [] @@ -478,9 +499,15 @@ and type_of_aux' metasenv context t = (C.Sort s1, C.Sort s2) when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *) C.Sort s2,subst,metasenv - | (C.Sort s1, C.Sort s2) -> - (*CSC manca la gestione degli universi!!! *) - C.Sort C.Type,subst,metasenv + | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> + (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *) + let t' = CicUniv.fresh() in + if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then + assert false ; (* not possible, error in CicUniv *) + C.Sort (C.Type t'),subst,metasenv + | (C.Sort _,C.Sort (C.Type t1)) -> + (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *) + C.Sort (C.Type t1),subst,metasenv | (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 @@ -489,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 @@ -504,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 @@ -522,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) @@ -548,7 +575,7 @@ and type_of_aux' metasenv context t = (match hetype with Cic.Prod (n,s,t) -> let subst,metasenv = - fo_unif_subst subst context metasenv s hety + fo_unif_subst subst context metasenv hety s in eat_prods metasenv subst context (CicMetaSubst.subst subst hete t) tl @@ -559,7 +586,6 @@ and type_of_aux' metasenv context t = eat_prods metasenv subst context hetype' tlbody_and_type in t,subst,metasenv - (* let rec aux context' args (resty,subst,metasenv) = function @@ -608,15 +634,14 @@ and type_of_aux' metasenv context t = in aux [] [] (hetype,subst,metasenv) tlbody_and_type *) - in let ty,subst',metasenv' = 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