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

fix(frontends/lean/structure_cmd): include context/section parameteres/variables that are used in explicit structure parameters

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-23 15:28:43 -08:00
parent 923fed8612
commit 7adecaf494
2 changed files with 22 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -305,21 +305,23 @@ struct structure_cmd_fn {
::lean::collect_locals(mlocal_type(v), dep_set); ::lean::collect_locals(mlocal_type(v), dep_set);
dep_set.insert(v); dep_set.insert(v);
} }
buffer<expr> all_include_vars; for (expr const & p : m_params)
sort_locals(dep_set, m_p, all_include_vars); ::lean::collect_locals(mlocal_type(p), dep_set);
buffer<expr> ctx;
sort_locals(dep_set, m_p, ctx);
expr tmp = Pi_as_is(all_include_vars, Pi(tmp_locals, m_type, m_p), m_p); expr tmp = Pi_as_is(ctx, Pi(tmp_locals, m_type, m_p), m_p);
level_param_names new_ls; level_param_names new_ls;
expr new_tmp; expr new_tmp;
std::tie(new_tmp, new_ls) = m_p.elaborate_type(tmp, list<expr>()); std::tie(new_tmp, new_ls) = m_p.elaborate_type(tmp, list<expr>());
levels new_meta_ls = map2<level>(new_ls, [](name const & n) { return mk_meta_univ(n); }); levels new_meta_ls = map2<level>(new_ls, [](name const & n) { return mk_meta_univ(n); });
new_tmp = instantiate_univ_params(new_tmp, new_ls, new_meta_ls); new_tmp = instantiate_univ_params(new_tmp, new_ls, new_meta_ls);
new_tmp = update_locals(new_tmp, all_include_vars); new_tmp = update_locals(new_tmp, ctx);
new_tmp = update_locals(new_tmp, m_params); new_tmp = update_locals(new_tmp, m_params);
buffer<expr> explicit_params; buffer<expr> explicit_params;
explicit_params.append(m_params); explicit_params.append(m_params);
m_params.clear(); m_params.clear();
m_params.append(all_include_vars); m_params.append(ctx);
m_params.append(explicit_params); m_params.append(explicit_params);
new_tmp = update_parents(new_tmp); new_tmp = update_parents(new_tmp);
m_type = new_tmp; m_type = new_tmp;

15
tests/lean/run/struct_bug1.lean Normal file
View file

@ -0,0 +1,15 @@
variable (A : Type)
structure foo (a : A) :=
(eqpr : a = a)
context
parameter (B : Type)
structure foo2 (b : B) :=
(eqpr : b = b)
check foo2
definition tst : B → Type₁ := foo2
end