michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean): add parent classes to local context in struct definitions

Browse source 
Fixes #1066
This commit is contained in:
Sebastian Ullrich 2016-07-05 14:52:00 -07:00 committed by Leonardo de Moura
parent 3941cc1839
commit 54844e2325
2 changed files with 38 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -293,11 +293,12 @@ struct structure_cmd_fn {
return new_tmp;
}
expr update_parents(expr new_tmp) {
expr update_parents(expr new_tmp, bool inst) {
for (unsigned i = 0; i < m_parents.size(); i++) {
m_parents[i] = copy_tag(m_parents[i], expr(binding_domain(new_tmp)));
new_tmp = binding_body(new_tmp);
lean_assert(closed(new_tmp));
if (inst)
new_tmp = instantiate(new_tmp, mk_parent_expr(i));
}
return new_tmp;
}
@ -342,7 +343,7 @@ struct structure_cmd_fn {
m_params.clear();
m_params.append(ctx);
m_params.append(explicit_params);
new_tmp = update_parents(new_tmp);
new_tmp = update_parents(new_tmp, false);
m_type = new_tmp;
}
@ -471,6 +472,24 @@ struct structure_cmd_fn {
solve_constraints(cseq);
}
/** \brief Create expression of type \c m_parents[i] from corresponding fields */
expr mk_parent_expr(unsigned i) {
expr const & parent = m_parents[i];
field_map const & fmap = m_field_maps[i];
buffer<expr> parent_params;
expr const & parent_fn = get_app_args(parent, parent_params);
levels const & parent_ls = const_levels(parent_fn);
name const & parent_name = const_name(parent_fn);
auto parent_info = get_parent_info(parent_name);
name const & parent_intro_name = inductive::intro_rule_name(std::get<2>(parent_info));
expr parent_intro = mk_app(mk_constant(parent_intro_name, parent_ls), parent_params);
for (unsigned idx : fmap) {
expr const & field = m_fields[idx];
parent_intro = mk_app(parent_intro, field);
}
return parent_intro;
}
/** \brief Add params, fields and references to parent structures into parser local scope */
void add_locals() {
if (m_explicit_universe_params) {
@ -482,22 +501,8 @@ struct structure_cmd_fn {
for (expr const & field : m_fields)
m_p.add_local(field);
for (unsigned i = 0; i < m_parents.size(); i++) {
if (auto n = m_parent_refs[i]) {
expr const & parent = m_parents[i];
field_map const & fmap = m_field_maps[i];
buffer<expr> parent_params;
expr const & parent_fn = get_app_args(parent, parent_params);
levels const & parent_ls = const_levels(parent_fn);
name const & parent_name = const_name(parent_fn);
auto parent_info = get_parent_info(parent_name);
name const & parent_intro_name = inductive::intro_rule_name(std::get<2>(parent_info));
expr parent_intro = mk_app(mk_constant(parent_intro_name, parent_ls), parent_params);
for (unsigned idx : fmap) {
expr const & field = m_fields[idx];
parent_intro = mk_app(parent_intro, field);
}
m_p.add_local_expr(*n, mk_as_is(parent_intro));
}
if (auto n = m_parent_refs[i])
m_p.add_local_expr(*n, mk_as_is(mk_parent_expr(i)));
}
}
@ -552,22 +557,22 @@ struct structure_cmd_fn {
/** \brief Elaborate new fields, and copy them to m_fields */
void elaborate_new_fields(buffer<expr> & new_fields) {
expr dummy = mk_Prop();
expr tmp = Pi_as_is(m_fields, Pi(new_fields, mk_Prop(), m_p), m_p);
unsigned j = m_parents.size();
while (j > 0) {
--j;
dummy = mk_arrow(mk_as_is(m_parents[j]), dummy);
tmp = mk_arrow(mk_as_is(m_parents[j]), tmp);
}
expr tmp = Pi_as_is(m_params, Pi_as_is(m_fields, Pi(new_fields, dummy, m_p), m_p), m_p);
tmp = Pi_as_is(m_params, tmp, m_p);
level_param_names new_ls;
expr new_tmp;
std::tie(new_tmp, new_ls) = m_p.elaborate_type(tmp, list<expr>());
for (auto new_l : new_ls)
m_level_names.push_back(new_l);
new_tmp = update_locals(new_tmp, m_params);
new_tmp = update_parents(new_tmp, true);
new_tmp = update_locals(new_tmp, m_fields);
new_tmp = update_locals(new_tmp, new_fields);
new_tmp = update_parents(new_tmp);
lean_assert(new_tmp == mk_Prop());
m_fields.append(new_fields);
}

10
tests/lean/run/parent_struct_inst.lean Normal file
View file

@ -0,0 +1,10 @@
open nat
structure A [class] := (n : ℕ)
definition f [A] := A.n
structure B extends A :=
(Hf : f = 0)
example : B := ⦃B, n := 0, Hf := rfl⦄