diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/inductiveops.ml | 41 | ||||
| -rw-r--r-- | pretyping/inductiveops.mli | 2 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 10 | ||||
| -rw-r--r-- | pretyping/retyping.mli | 2 | ||||
| -rw-r--r-- | pretyping/typing.ml | 2 | ||||
| -rw-r--r-- | pretyping/vnorm.ml | 3 |
6 files changed, 48 insertions, 12 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 7e4d37b2e..0b7cd89f2 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -451,9 +451,44 @@ let arity_of_case_predicate env (ind,params) dep k = (* Inferring the sort of parameters of a polymorphic inductive type knowing the sort of the conclusion *) -let type_of_inductive_knowing_conclusion env ((mib,mip),u) conclty = - let subst = Inductive.make_inductive_subst mib u in - subst_univs_constr subst mip.mind_arity.mind_user_arity + +(* Compute the inductive argument types: replace the sorts + that appear in the type of the inductive by the sort of the + conclusion, and the other ones by fresh universes. *) +let rec instantiate_universes env evdref scl is = function + | (_,Some _,_ as d)::sign, exp -> + d :: instantiate_universes env evdref scl is (sign, exp) + | d::sign, None::exp -> + d :: instantiate_universes env evdref scl is (sign, exp) + | (na,None,ty)::sign, Some u::exp -> + let ctx,_ = Reduction.dest_arity env ty in + let s = + (* Does the sort of parameter [u] appear in (or equal) + the sort of inductive [is] ? *) + if univ_depends u is then + scl (* constrained sort: replace by scl *) + else + (* unconstriained sort: replace by fresh universe *) + let evm, s = Evd.new_sort_variable Evd.univ_flexible !evdref in + evdref := evm; s + in + (na,None,mkArity(ctx,s)):: instantiate_universes env evdref scl is (sign, exp) + | sign, [] -> sign (* Uniform parameters are exhausted *) + | [], _ -> assert false + +let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty = + match mip.mind_arity with + | RegularArity s -> + let subst = Inductive.make_inductive_subst mib u in + sigma, subst_univs_constr subst s.mind_user_arity + | TemplateArity ar -> + let _,scl = Reduction.dest_arity env conclty in + let ctx = List.rev mip.mind_arity_ctxt in + let evdref = ref sigma in + let ctx = + instantiate_universes + env evdref scl ar.template_level (ctx,ar.template_param_levels) in + !evdref, mkArity (List.rev ctx,scl) (***********************************************) (* Guard condition *) diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 39451ec05..34ddce72b 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -142,7 +142,7 @@ i*) (********************) val type_of_inductive_knowing_conclusion : - env -> Inductive.mind_specif puniverses -> types -> types + env -> evar_map -> Inductive.mind_specif puniverses -> types -> evar_map * types (********************) val control_only_guard : env -> types -> unit diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 31487125a..ccb9420fd 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -190,7 +190,7 @@ let retype ?(polyprop=true) sigma = with Reduction.NotArity -> retype_error NotAnArity) | Const cst -> let t = constant_type_in env cst in - (try Typeops.type_of_constant_knowing_parameters env t argtyps + (try Typeops.type_of_constant_type_knowing_parameters env t argtyps with Reduction.NotArity -> retype_error NotAnArity) | Var id -> type_of_var env id | Construct cstr -> type_of_constructor env cstr @@ -211,13 +211,13 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty = match kind_of_term c with | Ind (ind,u) -> let spec = Inductive.lookup_mind_specif env ind in - type_of_inductive_knowing_conclusion env (spec,u) conclty + type_of_inductive_knowing_conclusion env sigma (spec,u) conclty | Const cst -> let t = constant_type_in env cst in (* TODO *) - Typeops.type_of_constant_knowing_parameters env t [||] - | Var id -> type_of_var env id - | Construct cstr -> type_of_constructor env cstr + sigma, Typeops.type_of_constant_type_knowing_parameters env t [||] + | Var id -> sigma, type_of_var env id + | Construct cstr -> sigma, type_of_constructor env cstr | _ -> assert false (* Profiling *) diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index fc1dd3564..b8b458555 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -41,4 +41,4 @@ val type_of_global_reference_knowing_parameters : env -> evar_map -> constr -> constr array -> types val type_of_global_reference_knowing_conclusion : - env -> evar_map -> constr -> types -> types + env -> evar_map -> constr -> types -> evar_map * types diff --git a/pretyping/typing.ml b/pretyping/typing.ml index bd559ddd5..cc473bd86 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -27,7 +27,7 @@ let meta_type evd mv = let constant_type_knowing_parameters env cst jl = let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in - type_of_constant_knowing_parameters env (constant_type_in env cst) paramstyp + type_of_constant_type_knowing_parameters env (constant_type_in env cst) paramstyp let inductive_type_knowing_parameters env (ind,u) jl = let mspec = lookup_mind_specif env ind in diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 16eeaa293..2cf730f11 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -98,7 +98,8 @@ let construct_of_constr_block = construct_of_constr false let constr_type_of_idkey env idkey = match idkey with | ConstKey cst -> - mkConst cst, (Environ.lookup_constant cst env).const_type + let const_type = (Environ.lookup_constant cst env).const_type in + mkConst cst, Typeops.type_of_constant_type env const_type | VarKey id -> let (_,_,ty) = lookup_named id env in mkVar id, ty |