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

fix(library/equations_compiler): avoid name collision when pack_mutual is not used

Browse source
This commit is contained in:
Leonardo de Moura 2017-05-21 15:40:06 -07:00
parent 9fb7e5c931
commit 3d088eea25
4 changed files with 16 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/library/equations_compiler/equations.cpp
View file

@ -192,6 +192,17 @@ expr update_equations(expr const & eqns, buffer<expr> const & new_eqs) {
}
}
expr update_equations(expr const & eqns, equations_header const & header) {
buffer<expr> eqs;
to_equations(eqns, eqs);
if (is_wf_equations(eqns)) {
return copy_tag(eqns, mk_equations(header, eqs.size(), eqs.data(),
equations_wf_rel(eqns), equations_wf_proof(eqns)));
} else {
return copy_tag(eqns, mk_equations(header, eqs.size(), eqs.data()));
}
}
// LEGACY
expr mk_equations(unsigned num_fns, unsigned num_eqs, expr const * eqs) {
return mk_equations(equations_header(num_fns), num_eqs, eqs);

1
src/library/equations_compiler/equations.h
View file

@ -48,6 +48,7 @@ struct equations_header {
expr mk_equations(equations_header const & header, unsigned num_eqs, expr const * eqs, expr const & R, expr const & Hwf);
expr mk_equations(equations_header const & header, unsigned num_eqs, expr const * eqs);
expr update_equations(expr const & eqns, buffer<expr> const & new_eqs);
expr update_equations(expr const & eqns, equations_header const & header);
bool is_equations(expr const & e);
bool is_wf_equations(expr const & e);

4
src/library/equations_compiler/wf_rec.cpp
View file

@ -454,6 +454,10 @@ struct wf_rec_fn {
equations_header const & header = get_equations_header(eqns);
if (header.m_num_fns > 1) {
eqns = pack_mutual(eqns);
} else {
equations_header new_header = header;
new_header.m_fn_names = to_list(name(head(header.m_fn_names), "_pack"));
eqns = update_equations(eqns, new_header);
}
/* Retrieve well founded relation */

1
tests/lean/eqn_hole.lean.expected.out
View file

@ -8,4 +8,3 @@ context:
g : ℕ → ℕ,
n : ℕ
⊢ ℕ
eqn_hole.lean:6:11: error: support for well-founded recursion has not been implemented yet, use 'set_option trace.eqn_compiler true' for additional information