refactor(kernel): replace_fn functional object

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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<expr> {
             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<expr> {
             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)                                                 \

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<expr> {
             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<expr> {
             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();
             }
         });
 }

src/kernel/instantiate.cpp

@@ -13,24 +13,21 @@ Author: Leonardo de Moura
 namespace lean {
 template<bool ClosedSubst>
 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<expr> {
             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<expr> {
         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);

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<expr> {
                 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();
                 }
             });
     }

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);
+    optional<expr> r = m_f(e, offset);
-    if (is_atomic(r) || !is_eqp(e, r)) {
+    if (r) {
-        save_result(e, r, offset, shared);
+        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);

src/kernel/replace_fn.h

@@ -46,7 +46,7 @@ class replace_fn {
     typedef buffer<expr>   result_stack;
 
     expr_cell_offset_map<expr>                            m_cache;
-    std::function<expr(expr const &, unsigned)>     m_f;
+    std::function<optional<expr>(expr const &, unsigned)> m_f;
     std::function<void(expr const &, expr const &)>       m_post;
     frame_stack                                           m_fs;
     result_stack                                          m_rs;

src/tests/kernel/replace.cpp

@@ -74,17 +74,17 @@ static void tst3() {
     expr d = Const("d");
     expr A = Const("A");
     expr_map<expr> trace;
-    auto proc = [&](expr const & x, unsigned offset) -> expr {
+    auto proc = [&](expr const & x, unsigned offset) -> optional<expr> {
         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));