diff --git a/src/kernel/abstract.cpp b/src/kernel/abstract.cpp index a5688fe1a..c96f6995a 100644 --- a/src/kernel/abstract.cpp +++ b/src/kernel/abstract.cpp @@ -13,26 +13,26 @@ Author: Leonardo de Moura namespace lean { expr abstract(expr const & e, unsigned n, expr const * s) { lean_assert(std::all_of(s, s+n, closed)); - return replace(e, [=](expr const & e, unsigned offset) -> expr { + return replace(e, [=](expr const & e, unsigned offset) -> optional { unsigned i = n; while (i > 0) { --i; if (s[i] == e) - return mk_var(offset + n - i - 1); + return some_expr(mk_var(offset + n - i - 1)); } - return e; + return none_expr(); }); } expr abstract_p(expr const & e, unsigned n, expr const * s) { lean_assert(std::all_of(s, s+n, closed)); - return replace(e, [=](expr const & e, unsigned offset) -> expr { + return replace(e, [=](expr const & e, unsigned offset) -> optional { unsigned i = n; while (i > 0) { --i; if (is_eqp(s[i], e)) - return mk_var(offset + n - i - 1); + return some_expr(mk_var(offset + n - i - 1)); } - return e; + return none_expr(); }); } #define MkBinder(FName) \ diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp index 032e34fe5..2b434818d 100644 --- a/src/kernel/free_vars.cpp +++ b/src/kernel/free_vars.cpp @@ -285,12 +285,12 @@ expr lower_free_vars(expr const & e, unsigned s, unsigned d) { return e; lean_assert(s >= d); lean_assert(!has_free_var(e, s-d, s)); - return replace(e, [=](expr const & e, unsigned offset) -> expr { + return replace(e, [=](expr const & e, unsigned offset) -> optional { if (is_var(e) && var_idx(e) >= s + offset) { lean_assert(var_idx(e) >= offset + d); - return mk_var(var_idx(e) - d); + return some_expr(mk_var(var_idx(e) - d)); } else { - return e; + return none_expr(); } }); } @@ -299,11 +299,11 @@ expr lower_free_vars(expr const & e, unsigned d) { return lower_free_vars(e, d, expr lift_free_vars(expr const & e, unsigned s, unsigned d) { if (d == 0 || closed(e)) return e; - return replace(e, [=](expr const & e, unsigned offset) -> expr { + return replace(e, [=](expr const & e, unsigned offset) -> optional { if (is_var(e) && var_idx(e) >= s + offset) { - return mk_var(var_idx(e) + d); + return some_expr(mk_var(var_idx(e) + d)); } else { - return e; + return none_expr(); } }); } diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp index c78f67c65..733f0dd91 100644 --- a/src/kernel/instantiate.cpp +++ b/src/kernel/instantiate.cpp @@ -13,24 +13,21 @@ Author: Leonardo de Moura namespace lean { template expr instantiate_core(expr const & a, unsigned s, unsigned n, expr const * subst) { - return replace(a, [=](expr const & m, unsigned offset) -> expr { + return replace(a, [=](expr const & m, unsigned offset) -> optional { if (is_var(m)) { unsigned vidx = var_idx(m); if (vidx >= offset + s) { if (vidx < offset + s + n) { if (ClosedSubst) - return subst[vidx - s - offset]; + return some_expr(subst[vidx - s - offset]); else - return lift_free_vars(subst[vidx - s - offset], offset); + return some_expr(lift_free_vars(subst[vidx - s - offset], offset)); } else { - return mk_var(vidx - n); + return some_expr(mk_var(vidx - n)); } - } else { - return m; } - } else { - return m; } + return none_expr(); }); } @@ -95,11 +92,11 @@ expr head_beta_reduce(expr const & t) { } expr beta_reduce(expr t) { - auto f = [=](expr const & m, unsigned) -> expr { + auto f = [=](expr const & m, unsigned) -> optional { if (is_head_beta(m)) - return head_beta_reduce(m); + return some_expr(head_beta_reduce(m)); else - return m; + return none_expr(); }; while (true) { expr new_t = replace_fn(f)(t); diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index 79238b880..cb5be6dc2 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -95,16 +95,16 @@ class normalizer::imp { /** \brief Convert the value \c v back into an expression in a context that contains \c k binders. */ expr reify(expr const & v, unsigned k) { - return replace(v, [&](expr const & e, unsigned DEBUG_CODE(offset)) -> expr { + return replace(v, [&](expr const & e, unsigned DEBUG_CODE(offset)) -> optional { lean_assert(offset == 0); lean_assert(!is_lambda(e) && !is_pi(e) && !is_sigma(e) && !is_let(e)); if (is_var(e)) { // de Bruijn level --> de Bruijn index - return mk_var(k - var_idx(e) - 1); + return some_expr(mk_var(k - var_idx(e) - 1)); } else if (is_closure(e)) { - return reify_closure(to_closure(e), k); + return some_expr(reify_closure(to_closure(e), k)); } else { - return e; + return none_expr(); } }); } diff --git a/src/kernel/replace_fn.cpp b/src/kernel/replace_fn.cpp index a8143c100..818b48909 100644 --- a/src/kernel/replace_fn.cpp +++ b/src/kernel/replace_fn.cpp @@ -31,9 +31,12 @@ bool replace_fn::visit(expr const & e, unsigned offset) { shared = true; } - expr r = m_f(e, offset); - if (is_atomic(r) || !is_eqp(e, r)) { - save_result(e, r, offset, shared); + optional r = m_f(e, offset); + if (r) { + save_result(e, *r, offset, shared); + return true; + } else if (is_atomic(e)) { + save_result(e, e, offset, shared); return true; } else { m_fs.emplace_back(e, offset, shared); diff --git a/src/kernel/replace_fn.h b/src/kernel/replace_fn.h index ee0bc74d7..30c119bfb 100644 --- a/src/kernel/replace_fn.h +++ b/src/kernel/replace_fn.h @@ -45,11 +45,11 @@ class replace_fn { typedef buffer frame_stack; typedef buffer result_stack; - expr_cell_offset_map m_cache; - std::function m_f; - std::function m_post; - frame_stack m_fs; - result_stack m_rs; + expr_cell_offset_map m_cache; + std::function(expr const &, unsigned)> m_f; + std::function m_post; + frame_stack m_fs; + result_stack m_rs; void save_result(expr const & e, expr const & r, unsigned offset, bool shared); bool visit(expr const & e, unsigned offset); diff --git a/src/tests/kernel/replace.cpp b/src/tests/kernel/replace.cpp index f9712a525..f7f119a07 100644 --- a/src/tests/kernel/replace.cpp +++ b/src/tests/kernel/replace.cpp @@ -74,17 +74,17 @@ static void tst3() { expr d = Const("d"); expr A = Const("A"); expr_map trace; - auto proc = [&](expr const & x, unsigned offset) -> expr { + auto proc = [&](expr const & x, unsigned offset) -> optional { if (is_var(x)) { unsigned vidx = var_idx(x); if (vidx == offset) - return c; + return some_expr(c); else if (vidx > offset) - return mk_var(vidx-1); + return some_expr(mk_var(vidx-1)); else - return x; + return none_expr(); } else { - return x; + return none_expr(); } }; replace_fn replacer(proc, tracer(trace));