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

perf(kernel/free_vars): improve has_free_var

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-15 18:31:43 -08:00
parent ddcc8de09e
commit ce0b1d17a2
1 changed files with 11 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/kernel/free_vars.cpp
View file

@ -9,19 +9,24 @@ Author: Leonardo de Moura
#include "kernel/free_vars.h" #include "kernel/free_vars.h"
#include "kernel/expr_sets.h" #include "kernel/expr_sets.h"
#include "kernel/replace_fn.h" #include "kernel/replace_fn.h"
#include "kernel/find_fn.h" #include "kernel/for_each_fn.h"
namespace lean { namespace lean {
bool has_free_var(expr const & e, unsigned i) { bool has_free_var(expr const & e, unsigned i) {
optional<expr> r = find(e, [&](expr const & e, unsigned offset) { bool found = false;
for_each(e, [&](expr const & e, unsigned offset) {
if (found)
return false; // already found
if (closed(e))
return false; // do not search their types
if (is_var(e)) { if (is_var(e)) {
unsigned vidx = var_idx(e); unsigned vidx = var_idx(e);
return vidx >= offset && vidx - offset == i; if (vidx >= offset && vidx - offset == i)
} else { found = true;
return false;
} }
return true; // continue search
}); });
return static_cast<bool>(r); return found;
} }
expr lower_free_vars(expr const & e, unsigned s, unsigned d) { expr lower_free_vars(expr const & e, unsigned s, unsigned d) {