From ce0b1d17a247b72994f855b49fbcd5a1d308a4bb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 15 Jan 2015 18:31:43 -0800 Subject: [PATCH] perf(kernel/free_vars): improve has_free_var --- src/kernel/free_vars.cpp | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp index 830272395..315d395a6 100644 --- a/src/kernel/free_vars.cpp +++ b/src/kernel/free_vars.cpp @@ -9,19 +9,24 @@ Author: Leonardo de Moura #include "kernel/free_vars.h" #include "kernel/expr_sets.h" #include "kernel/replace_fn.h" -#include "kernel/find_fn.h" +#include "kernel/for_each_fn.h" namespace lean { bool has_free_var(expr const & e, unsigned i) { - optional 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)) { unsigned vidx = var_idx(e); - return vidx >= offset && vidx - offset == i; - } else { - return false; + if (vidx >= offset && vidx - offset == i) + found = true; } + return true; // continue search }); - return static_cast(r); + return found; } expr lower_free_vars(expr const & e, unsigned s, unsigned d) {