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

fix(library/compiler/lcnf): bug, minor premise must have a lambda for each field in LCNF

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-20 16:42:57 -07:00
parent 896b45239e
commit f556e0947b
3 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/compiler/lcnf.cpp
View file

@ -132,6 +132,11 @@ public:
minor = instantiate_rev(minor, minor_fvars.size(), minor_fvars.data());
if (j < num_fields) {
minor = eta_expand(minor, num_fields - j);
for (; j < num_fields; j++) {
expr new_fvar = m_lctx.mk_local_decl(ngen(), binding_name(minor), binding_domain(minor), binding_info(minor));
minor_fvars.push_back(new_fvar);
minor = instantiate(binding_body(minor), new_fvar);
}
}
flet<cache> save_cache(m_cache, m_cache);
unsigned old_fvars_size = m_fvars.size();

5
tests/lean/lcnf_bug1.lean Normal file
View file

@ -0,0 +1,5 @@
set_option trace.compiler.lcnf true
set_option pp.binder_types false
def tst1 (a : nat) : nat :=
@nat.cases_on (λ _, nat) a 0 id

2
tests/lean/lcnf_bug1.lean.expected.out Normal file
View file

@ -0,0 +1,2 @@
[compiler.lcnf] tst1
λ a, let _x_3 := nat.cases_on a (let _x_1 := nat.has_zero.0 in _x_1) (λ a, let _x_2 := id a in _x_2) in _x_3