From 7006c84214295dc7feddba65989377da3656f4e6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 May 2016 18:48:31 -0700 Subject: [PATCH] feat(compiler/lambda_lifting): avoid unnecessary lambda lifting steps It doesn't make sense to apply lambda lifting to lambda-expressions such as (fun x, f x) since we can reduce it to `f` --- src/compiler/lambda_lifting.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/compiler/lambda_lifting.cpp b/src/compiler/lambda_lifting.cpp index 11fa31262a..ca8d951b31 100644 --- a/src/compiler/lambda_lifting.cpp +++ b/src/compiler/lambda_lifting.cpp @@ -12,6 +12,7 @@ Author: Leonardo de Moura #include "library/locals.h" #include "library/util.h" #include "library/trace.h" +#include "library/normalize.h" #include "compiler/fresh_constant.h" #include "compiler/util.h" #include "compiler/comp_irrelevant.h" @@ -23,6 +24,9 @@ class lambda_lifting_fn : public compiler_step_visitor { bool m_trusted; protected: expr declare_aux_def(expr const & value) { + expr new_value = try_eta(value); + if (!is_lambda(new_value)) + return new_value; pair ep = mk_fresh_constant(m_env); m_env = ep.first; name n = ep.second;