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

fix(library/compiler/specialize): make sure specialize generates valid LCNF

Browse source
This commit is contained in:
Leonardo de Moura 2019-04-17 07:34:42 -07:00
parent 5e9f2e4e6a
commit 32a309c566
1 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/library/compiler/specialize.cpp
View file

@ -942,8 +942,13 @@ class specialize_fn {
name y("_y");
for (unsigned i = 0; i < fvars.size(); i++) {
expr type = tc.infer(fvar_vals[i]);
expr new_fvar = m_lctx.mk_local_decl(fvar_name(fvars[i]), y.append_after(i+1), type, fvar_vals[i]).mk_ref();
new_let_decls.push_back(new_fvar);
if (is_irrelevant_type(m_st, m_lctx, type)) {
/* In LCNF, the type `ty` at `let x : ty := v in t` must not be irrelevant. */
code = replace_fvar(code, fvars[i], fvar_vals[i]);
} else {
expr new_fvar = m_lctx.mk_local_decl(fvar_name(fvars[i]), y.append_after(i+1), type, fvar_vals[i]).mk_ref();
new_let_decls.push_back(new_fvar);
}
}
code = m_lctx.mk_lambda(new_let_decls, code);
// lean_trace(name("compiler", "spec_info"), tout() << "STEP 1 " << n << "\n" << code << "\n";);