From 3bcbfbf348c310c89ce3e8e21ec142cdda0b6bca Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 21 Jul 2017 03:29:40 -0700 Subject: [PATCH] perf(library/compiler/elim_recursors): beta_reduce ==> head_beta_reduce This commit fixes the byte code generation performace problem exposed by #1755 --- src/library/compiler/elim_recursors.cpp | 6 +++--- src/library/compiler/lambda_lifting.cpp | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/library/compiler/elim_recursors.cpp b/src/library/compiler/elim_recursors.cpp index 0889ee36a3..da53409028 100644 --- a/src/library/compiler/elim_recursors.cpp +++ b/src/library/compiler/elim_recursors.cpp @@ -89,7 +89,7 @@ protected: expr local = locals.push_local_from_binding(e); e = instantiate(binding_body(e), local); } else { - return beta_reduce(e); + return head_beta_reduce(e); } } } @@ -218,7 +218,7 @@ protected: } /* Keep consuming lambda */ minor = consume_lambdas(minor_locals, minor); - minor = visit(beta_reduce(minor)); + minor = visit(head_beta_reduce(minor)); minor = minor_locals.mk_lambda(minor); cases_on_args.push_back(minor); } @@ -250,7 +250,7 @@ protected: return visit_recursor_app(e); } } - return compiler_step_visitor::visit_app(beta_reduce(e)); + return compiler_step_visitor::visit_app(head_beta_reduce(e)); } public: diff --git a/src/library/compiler/lambda_lifting.cpp b/src/library/compiler/lambda_lifting.cpp index 4068ee9285..30210b530c 100644 --- a/src/library/compiler/lambda_lifting.cpp +++ b/src/library/compiler/lambda_lifting.cpp @@ -189,7 +189,7 @@ class lambda_lifting_fn : public compiler_step_visitor { if (is_constant(fn) && is_cases_on_recursor(env(), const_name(fn))) { return visit_cases_on_app(e); } else { - return compiler_step_visitor::visit_app(beta_reduce(e)); + return compiler_step_visitor::visit_app(head_beta_reduce(e)); } }