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

perf(library/compiler/elim_recursors): beta_reduce ==> head_beta_reduce

Browse source 
This commit fixes the byte code generation performace problem
exposed by #1755
This commit is contained in:
Leonardo de Moura 2017-07-21 03:29:40 -07:00
parent af80c2890d
commit 3bcbfbf348
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/compiler/elim_recursors.cpp
View file

@ -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:

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

@ -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));
}
}