max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(frontends/lean/structure_cmd): instantiate universe levels in projections to parents

Browse source
This commit is contained in:
Gabriel Ebner 2017-04-29 14:58:31 +02:00
parent 832c38d3cb
commit ca2eab3a2f
2 changed files with 21 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
src/frontends/lean/structure_cmd.cpp
View file

@ -623,21 +623,7 @@ struct structure_cmd_fn {
field_map & fmap = m_field_maps.back();
buffer<expr> args;
expr const & parent_fn = get_app_args(parent, args);
level_param_names lparams; unsigned nparams; inductive::intro_rule intro;
name const & parent_name = const_name(parent_fn);
std::tie(lparams, nparams, intro) = get_parent_info(parent_name);
expr intro_type = inductive::intro_rule_type(intro);
intro_type = instantiate_univ_params(intro_type, lparams, const_levels(parent_fn));
if (nparams != args.size()) {
throw elaborator_exception(parent,
sstream() << "invalid 'structure' header, number of argument "
"mismatch for parent structure '" << parent_name << "'");
}
for (expr const & arg : args) {
if (!is_pi(intro_type))
throw_ill_formed_parent(parent_name);
intro_type = instantiate(binding_body(intro_type), arg);
}
if (m_subobjects) {
name fname;
if (auto const & ref = m_parent_refs[i])
@ -666,8 +652,9 @@ struct structure_cmd_fn {
// by projecting our new subobject field and then obtain `A` as
// `(fun {ps : Ps} (x : base_S_name ps), A) x`.
expr base_obj = *mk_base_projections(m_env, parent_name, base_S_name, field);
auto nparams = std::get<1>(get_structure_info(m_env, base_S_name));
expr type = m_p.env().get(full_fname).get_type();
level_param_names lparams; unsigned nparams; inductive::intro_rule intro;
std::tie(lparams, nparams, intro) = get_parent_info(base_S_name);
expr type = instantiate_univ_params(m_p.env().get(full_fname).get_type(), lparams, const_levels(parent_fn));
std::function<expr(expr const &, unsigned)> pi_to_lam = [&](expr const & e, unsigned i) {
if (i == nparams + 1)
return mk_as_is(e);
@ -682,6 +669,21 @@ struct structure_cmd_fn {
subfields.emplace_back(subfield, some_expr(proj), field_kind::from_parent);
}
} else {
level_param_names lparams; unsigned nparams; inductive::intro_rule intro;
std::tie(lparams, nparams, intro) = get_parent_info(parent_name);
expr intro_type = inductive::intro_rule_type(intro);
intro_type = instantiate_univ_params(intro_type, lparams, const_levels(parent_fn));
if (nparams != args.size()) {
throw elaborator_exception(parent,
sstream() << "invalid 'structure' header, number of argument "
"mismatch for parent structure '" << parent_name << "'");
}
for (expr const & arg : args) {
if (!is_pi(intro_type))
throw_ill_formed_parent(parent_name);
intro_type = instantiate(binding_body(intro_type), arg);
}
size_t fmap_start = fmap.size();
while (is_pi(intro_type)) {
name fname = binding_name(intro_type);

3
tests/lean/run/struct_extend_univ.lean Normal file
View file

@ -0,0 +1,3 @@
universe u
class foo (α : Sort u) := (a : α)
class bar (α : Type u) extends foo α := (b : α)