michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/blast/expr): improve performance of abstract_lrefs

Browse source
This commit is contained in:
Leonardo de Moura 2015-09-28 16:42:55 -07:00
parent 885f5745c4
commit 913d4526cd
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/library/blast/expr.cpp
View file

@ -559,8 +559,12 @@ expr instantiate_value_univ_params(declaration const & d, levels const & ls) {
} }
expr abstract_lrefs(expr const & e, unsigned n, expr const * subst) { expr abstract_lrefs(expr const & e, unsigned n, expr const * subst) {
if (!has_lref(e))
return e;
lean_assert(std::all_of(subst, subst+n, [](expr const & e) { return closed(e) && is_lref(e); })); lean_assert(std::all_of(subst, subst+n, [](expr const & e) { return closed(e) && is_lref(e); }));
return blast::replace(e, [=](expr const & m, unsigned offset) -> optional<expr> { return blast::replace(e, [=](expr const & m, unsigned offset) -> optional<expr> {
if (!has_lref(m))
return some_expr(m); // skip: m does not contain lref's
if (is_lref(m)) { if (is_lref(m)) {
unsigned i = n; unsigned i = n;
while (i > 0) { while (i > 0) {