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

fix(library/compiler/util): loose bvars

Browse source
This commit is contained in:
Leonardo de Moura 2019-04-17 07:57:30 -07:00
parent f12e580ac2
commit d662f312df
2 changed files with 7 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/compiler/compiler.cpp
View file

@ -205,7 +205,7 @@ environment compile(environment const & env, options const & opts, names cs) {
trace_compiler(name({"compiler", "stage1"}), ds);
environment new_env = cache_stage1(env, ds);
std::tie(new_env, ds) = specialize(new_env, ds, cfg);
// lcnf_check_let_decls(new_env, ds);
lean_assert(lcnf_check_let_decls(new_env, ds));
trace_compiler(name({"compiler", "specialize"}), ds);
ds = apply(elim_dead_let, ds);
trace_compiler(name({"compiler", "elim_dead_let"}), ds);

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

@ -600,8 +600,11 @@ class lcnf_valid_let_decls_fn {
if (is_irrelevant_type(m_st, m_lctx, new_type)) {
return some_expr(e);
}
if (optional<expr> found = visit(instantiate_rev(let_value(e), fvars.size(), fvars.data())))
expr new_val = instantiate_rev(let_value(e), fvars.size(), fvars.data());
if (optional<expr> found = visit(new_val))
return found;
expr new_fvar = m_lctx.mk_local_decl(ngen(), let_name(e), new_type, new_val);
fvars.push_back(new_fvar);
e = let_body(e);
}
return visit(instantiate_rev(e, fvars.size(), fvars.data()));
@ -632,9 +635,9 @@ optional<expr> lcnf_valid_let_decls(environment const & env, expr const & e) {
bool lcnf_check_let_decls(environment const & env, comp_decl const & d) {
if (optional<expr> v = lcnf_valid_let_decls(env, d.snd())) {
tout() << "LCNF violation at " << d.fst() << "\n" << *v << "\n";
return true;
} else {
return false;
} else {
return true;
}
}