max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(compiler/lambda_lifting): avoid unnecessary lambda lifting steps

Browse source 
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`
This commit is contained in:
Leonardo de Moura 2016-05-03 18:48:31 -07:00
parent 3dac0f6bb6
commit 7006c84214
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/compiler/lambda_lifting.cpp
View file

@ -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<environment, name> ep = mk_fresh_constant(m_env);
m_env = ep.first;
name n = ep.second;