From ee0851921bfaead21d1c6409af1d0de322c1b987 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 22 Apr 2019 13:15:08 -0700 Subject: [PATCH] fix(library/compiler/csimp): missing simplification opportunity --- src/library/compiler/csimp.cpp | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/src/library/compiler/csimp.cpp b/src/library/compiler/csimp.cpp index d45151506f..c4e71cd22f 100644 --- a/src/library/compiler/csimp.cpp +++ b/src/library/compiler/csimp.cpp @@ -189,13 +189,13 @@ class csimp_fn { if (optional decl = m_lctx.find_local_decl(e)) { if (optional 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 r = try_inline_proj_instance(e, is_let_val)) {