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

feat(library/compiler): simplify again after lambda lifting

Browse source 
Motivation: we avoid the creation of closures at join point declarations.
This commit is contained in:
Leonardo de Moura 2018-10-19 15:17:07 -07:00
parent 12d8b0e7ef
commit eb02add3de
2 changed files with 11 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/compiler/compiler.cpp
View file

@ -129,6 +129,8 @@ environment compile(environment const & env, options const & opts, names const &
trace_compiler(name({"compiler", "cse"}), ds);
ds = lambda_lifting(new_env, ds);
trace_compiler(name({"compiler", "lambda_lifting"}), ds);
ds = apply(esimp, env, ds);
trace_compiler(name({"compiler", "simp"}), ds);
ds = apply(simp_inductive, new_env, ds);
trace_compiler(name({"compiler", "simplify_inductive"}), ds);
new_env = emit_bytecode(new_env, ds);

16
src/library/compiler/lambda_lifting.cpp
View file

@ -43,7 +43,9 @@ class lambda_lifting_fn {
buffer<expr> fvars;
while (is_let(e)) {
lean_assert(!has_loose_bvars(let_type(e)));
expr new_val = visit(instantiate_rev(let_value(e), fvars.size(), fvars.data()));
bool not_root = false;
bool jp = is_join_point_name(let_name(e));
expr new_val = visit(instantiate_rev(let_value(e), fvars.size(), fvars.data()), not_root, jp);
expr new_fvar = m_lctx.mk_local_decl(ngen(), let_name(e), let_type(e), new_val);
fvars.push_back(new_fvar);
e = let_body(e);
@ -103,8 +105,8 @@ class lambda_lifting_fn {
return none_expr();
}
name next_name() {
name r(m_base_name, "_lambda");
name next_name(bool join_point) {
name r(m_base_name, join_point ? "_join_point" : "_lambda");
r = r.append_after(m_next_idx);
m_next_idx++;
return r;
@ -126,7 +128,7 @@ class lambda_lifting_fn {
return e;
}
expr visit_lambda(expr e, bool root) {
expr visit_lambda(expr e, bool root, bool join_point) {
e = visit_lambda_core(e);
if (root)
return e;
@ -135,15 +137,15 @@ class lambda_lifting_fn {
buffer<expr> fvars;
collect_fvars(e, fvars);
e = mk_lambda(fvars, e);
name new_fn = next_name();
name new_fn = next_name(join_point);
m_new_decls.push_back(comp_decl(new_fn, e));
return mk_app(mk_constant(new_fn), fvars);
}
expr visit(expr const & e, bool root = false) {
expr visit(expr const & e, bool root = false, bool join_point = false) {
switch (e.kind()) {
case expr_kind::App: return visit_app(e);
case expr_kind::Lambda: return visit_lambda(e, root);
case expr_kind::Lambda: return visit_lambda(e, root, join_point);
case expr_kind::Let: return visit_let(e);
default: return e;
}