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

fix(library/compiler/csimp): missing simplification opportunity

Browse source
This commit is contained in:
Leonardo de Moura 2019-04-22 13:15:08 -07:00
parent 32f41f60d3
commit ee0851921b
1 changed files with 5 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/library/compiler/csimp.cpp
View file

@ -189,13 +189,13 @@ class csimp_fn {
if (optional<local_decl> decl = m_lctx.find_local_decl(e)) {
if (optional<expr> v = decl->get_value()) {
if (!is_join_point_name(decl->get_user_name()))
return find(*v, skip_mdata);
return find(*v, skip_mdata, use_expr2ctor);
else if (is_small_join_point(*v))
return find(*v, skip_mdata);
return find(*v, skip_mdata, use_expr2ctor);
}
}
} else if (is_mdata(e) && skip_mdata) {
return find(mdata_expr(e), true);
return find(mdata_expr(e), true, use_expr2ctor);
}
return e;
}
@ -1439,13 +1439,10 @@ class csimp_fn {
}
expr visit_proj(expr const & e, bool is_let_val) {
expr s = find(proj_expr(e));
expr s = find_ctor(proj_expr(e));
if (is_constructor_app(env(), s))
if (is_constructor_app(env(), s)) {
return proj_constructor(s, proj_idx(e).get_small_value());
if (expr const * ctor = m_expr2ctor.find(s)) {
return proj_constructor(*ctor, proj_idx(e).get_small_value());
}
if (optional<expr> r = try_inline_proj_instance(e, is_let_val)) {