From a2c5daededec27d7b062c49c8509452bc66c0c01 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 14 Sep 2018 13:26:24 -0700 Subject: [PATCH] feat(library/compiler/lcnf): modify LCNF format Now, the body of a let-expression is atomic. --- src/library/compiler/csimp.cpp | 4 +-- src/library/compiler/lcnf.cpp | 45 +++++++++++++++------------------- 2 files changed, 22 insertions(+), 27 deletions(-) diff --git a/src/library/compiler/csimp.cpp b/src/library/compiler/csimp.cpp index cdb19a0ed6..e114020079 100644 --- a/src/library/compiler/csimp.cpp +++ b/src/library/compiler/csimp.cpp @@ -77,7 +77,7 @@ class csimp_fn { } e = let_body(e); } - return find(visit(instantiate_rev(e, let_fvars.size(), let_fvars.data())), false); + return visit(instantiate_rev(e, let_fvars.size(), let_fvars.data())); } expr visit_lambda(expr e) { @@ -93,7 +93,7 @@ class csimp_fn { binding_fvars.push_back(new_fvar); e = binding_body(e); } - expr new_body = find(visit(instantiate_rev(e, binding_fvars.size(), binding_fvars.data())), false); + expr new_body = visit(instantiate_rev(e, binding_fvars.size(), binding_fvars.data())); new_body = m_lctx.mk_lambda(m_fvars.size() - m_fvars_init_size, m_fvars.data() + m_fvars_init_size, new_body); m_fvars.shrink(m_fvars_init_size); return m_lctx.mk_lambda(binding_fvars, new_body); diff --git a/src/library/compiler/lcnf.cpp b/src/library/compiler/lcnf.cpp index fdde045c93..c8bf63ea1d 100644 --- a/src/library/compiler/lcnf.cpp +++ b/src/library/compiler/lcnf.cpp @@ -48,19 +48,15 @@ public: return is_app_of(e, get_lc_proof_name()); } - expr mk_let_decl(expr const & e, bool root) { - if (root) { - return e; - } else { - expr type = infer_type(e); - /* Remark: we use `m_x.append_after(m_next_idx)` instead of `name(m_x, m_next_idx)` - because the resulting name is confusing during debugging: it looks like a projection application. - We should replace it with `name(m_x, m_next_idx)` when the compiler code gets more stable. */ - expr fvar = m_lctx.mk_local_decl(ngen(), m_x.append_after(m_next_idx), type, e); - m_next_idx++; - m_fvars.push_back(fvar); - return fvar; - } + expr mk_let_decl(expr const & e) { + expr type = infer_type(e); + /* Remark: we use `m_x.append_after(m_next_idx)` instead of `name(m_x, m_next_idx)` + because the resulting name is confusing during debugging: it looks like a projection application. + We should replace it with `name(m_x, m_next_idx)` when the compiler code gets more stable. */ + expr fvar = m_lctx.mk_local_decl(ngen(), m_x.append_after(m_next_idx), type, e); + m_next_idx++; + m_fvars.push_back(fvar); + return fvar; } expr eta_expand(expr e, unsigned num_extra) { @@ -153,18 +149,14 @@ public: } flet save_cache(m_cache, m_cache); unsigned m_fvars_init_size = m_fvars.size(); - expr new_minor = visit(minor, true); - if (is_lambda(new_minor) && m_fvars.size() == m_fvars_init_size) { - // create an aux let declaration to make sure we separate the cases_on binders from the result. - new_minor = mk_let_decl(new_minor, false); - } + expr new_minor = visit(minor, false); // add let-decls new_minor = m_lctx.mk_lambda(m_fvars.size() - m_fvars_init_size, m_fvars.data() + m_fvars_init_size, new_minor); m_fvars.shrink(m_fvars_init_size); new_minor = m_lctx.mk_lambda(minor_fvars, new_minor); args[i] = new_minor; } - return mk_let_decl(mk_app(fn, args), root); + return mk_let_decl(mk_app(fn, args)); } } @@ -190,7 +182,7 @@ public: if (lhs_constructor != rhs_constructor) { expr type = tc.whnf(tc.infer(mk_app(fn, args))); level lvl = sort_level(tc.ensure_type(type)); - return mk_let_decl(mk_app(mk_constant(get_lc_unreachable_name(), {lvl}), type), root); + return mk_let_decl(mk_app(mk_constant(get_lc_unreachable_name(), {lvl}), type)); } else if (args.size() < basic_arity + 1 /* major */) { return visit(eta_expand(mk_app(fn, args), basic_arity + 1 - args.size()), root); } else { @@ -253,7 +245,7 @@ public: type_checker tc(m_st, m_lctx); expr type = tc.whnf(tc.infer(mk_app(fn, args))); level lvl = sort_level(tc.ensure_type(type)); - return mk_let_decl(mk_app(mk_constant(get_lc_unreachable_name(), {lvl}), type), root); + return mk_let_decl(mk_app(mk_constant(get_lc_unreachable_name(), {lvl}), type)); } } @@ -318,7 +310,7 @@ public: for (expr & arg : args) { arg = visit(arg, false); } - return mk_let_decl(mk_app(fn, args), root); + return mk_let_decl(mk_app(fn, args)); } expr visit_app(expr const & e, bool root) { @@ -356,14 +348,14 @@ public: expr visit_proj(expr const & e, bool root) { expr v = visit(proj_expr(e), false); expr r = mk_proj(proj_idx(e), v); - return mk_let_decl(r, root); + return mk_let_decl(r); } expr visit_mdata(expr const & e, bool root) { if (is_lc_mdata(e)) { expr v = visit(mdata_expr(e), false); expr r = mk_mdata(mdata_data(e), v); - return mk_let_decl(r, root); + return mk_let_decl(r); } else { return visit(mdata_expr(e), root); } @@ -389,7 +381,10 @@ public: m_fvars.shrink(m_fvars_init_size); r = m_lctx.mk_lambda(binding_fvars, new_body); } - return mk_let_decl(r, root); + if (root) + return r; + else + return mk_let_decl(r); } expr visit_let(expr e, bool root) {