From ceeb77ec8c8bbc33f93dfcad036e69dac1652490 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 8 Mar 2017 14:48:00 -0800 Subject: [PATCH] fix(library/compiler/erase_irrelevant): erase types of irrelevant lambdas This modification makes sure we do not create unnecessary closures, and avoid artificial dependencies that may prevent destructive updates. --- src/library/compiler/erase_irrelevant.cpp | 35 +++++++++++++++++++++-- 1 file changed, 32 insertions(+), 3 deletions(-) diff --git a/src/library/compiler/erase_irrelevant.cpp b/src/library/compiler/erase_irrelevant.cpp index c584a40293..2959edf699 100644 --- a/src/library/compiler/erase_irrelevant.cpp +++ b/src/library/compiler/erase_irrelevant.cpp @@ -98,17 +98,46 @@ class erase_irrelevant_fn : public compiler_step_visitor { return *g_neutral_expr; } - expr erase_lambda_let_types(expr const & e) { + static bool is_irrelevant_lambda_let_body(expr e) { + while (true) { + if (is_lambda(e)) + e = binding_body(e); + else if (is_let(e)) + e = let_body(e); + else + return is_neutral_expr(e); + } + } + + expr erase_lambda_let_types_when_relevant(expr const & e) { if (is_lambda(e)) { return copy_tag(e, mk_lambda(binding_name(e), erase_type(binding_domain(e)), - erase_lambda_let_types(binding_body(e)))); + erase_lambda_let_types_when_relevant(binding_body(e)))); } else if (is_let(e)) { - return mk_let(let_name(e), erase_type(let_type(e)), let_value(e), erase_lambda_let_types(let_body(e))); + return mk_let(let_name(e), erase_type(let_type(e)), let_value(e), erase_lambda_let_types_when_relevant(let_body(e))); } else { return e; } } + expr erase_lambda_let_types_when_irrelevant(expr const & e) { + if (is_lambda(e)) { + return copy_tag(e, mk_lambda(binding_name(e), mk_neutral_expr(), + erase_lambda_let_types_when_irrelevant(binding_body(e)))); + } else if (is_let(e)) { + return erase_lambda_let_types_when_irrelevant(let_body(e)); + } else { + return e; + } + } + + expr erase_lambda_let_types(expr const & e) { + if (is_irrelevant_lambda_let_body(e)) + return erase_lambda_let_types_when_irrelevant(e); + else + return erase_lambda_let_types_when_relevant(e); + } + virtual expr visit_lambda(expr const & e) override { return erase_lambda_let_types(compiler_step_visitor::visit_lambda(e)); }