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

fix(inductive_compiler): preserve invariant that all basic ir names are <ind_name>.<atomic>

Browse source
This commit is contained in:
Daniel Selsam 2016-10-11 18:23:54 -07:00 • committed by Leonardo de Moura
parent 8d94dfd8e8
commit ae730532c8
2 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/inductive_compiler/mutual.cpp
View file

@ -231,7 +231,7 @@ class add_mutual_inductive_decl_fn {
}
expr translate_ir(unsigned ind_idx, expr const & ir) {
name ir_name = mlocal_name(m_mut_decl.get_ind(ind_idx)) + mlocal_name(ir).replace_prefix(m_basic_prefix, name());
name ir_name = m_basic_ind_name + name(mlocal_name(ir).get_string()).append_after(ind_idx);
buffer<expr> locals;
expr ty = m_tctx.whnf(mlocal_type(ir));
while (is_pi(ty)) {

4
src/library/inductive_compiler/nested.cpp
View file

@ -197,6 +197,10 @@ class add_nested_inductive_decl_fn {
name mk_inner_name(name const & n) {
if (m_nested_decl.is_ind_name(n) || m_nested_decl.is_ir_name(n)) {
return nest(n);
} else if (!n.is_atomic()) {
// We want the atomic introduction rule name to stay at the end, but we don't want to introduce
// a new "nest_" in the beginning.
return nest(n.get_prefix() + mlocal_name(m_nested_decl.get_ind(0)) + name(n.get_string()));
} else {
// We append the ind name at the end so that we don't put the "nest_" in the beginning
return nest(n + mlocal_name(m_nested_decl.get_ind(0)));