feat(replace_visitor): add an abstract class for applying transformations on expressions

I also removed replace_using_ctx since it is subsumed by the new class.

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

src/kernel/CMakeLists.txt

@@ -2,6 +2,7 @@ add_library(kernel expr.cpp free_vars.cpp abstract.cpp instantiate.cpp
   normalizer.cpp context.cpp level.cpp object.cpp environment.cpp
   type_checker.cpp builtin.cpp occurs.cpp metavar.cpp justification.cpp
   unification_constraint.cpp printer.cpp formatter.cpp
-  kernel_exception.cpp type_checker_justification.cpp pos_info_provider.cpp)
+  kernel_exception.cpp type_checker_justification.cpp pos_info_provider.cpp
+  replace_visitor.cpp)
 
 target_link_libraries(kernel ${LEAN_LIBS})

src/kernel/replace_visitor.cpp

@@ -0,0 +1,84 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/replace_visitor.h"
+
+namespace lean {
+expr replace_visitor::visit_type(expr const & e, context const &) { lean_assert(is_type(e)); return e; }
+expr replace_visitor::visit_value(expr const & e, context const &) { lean_assert(is_value(e)); return e; }
+expr replace_visitor::visit_constant(expr const & e, context const &) { lean_assert(is_constant(e)); return e; }
+expr replace_visitor::visit_var(expr const & e, context const &) { lean_assert(is_var(e)); return e; }
+expr replace_visitor::visit_metavar(expr const & e, context const &) { lean_assert(is_metavar(e)); return e; }
+expr replace_visitor::visit_app(expr const & e, context const & ctx) {
+    lean_assert(is_app(e));
+    return update_app(e, [&](expr const & c) { return visit(c, ctx); });
+}
+expr replace_visitor::visit_eq(expr const & e, context const & ctx) {
+    lean_assert(is_eq(e));
+    return update_eq(e, [&](expr const & l, expr const & r) { return std::make_pair(visit(l, ctx), visit(r, ctx)); });
+}
+expr replace_visitor::visit_abst(expr const & e, context const & ctx) {
+    lean_assert(is_abstraction(e));
+    return update_abst(e, [&](expr const & t, expr const & b) {
+            expr new_t = visit(t, ctx);
+            expr new_b;
+            {
+                cache::mk_scope sc(m_cache);
+                new_b = visit(b, extend(ctx, abst_name(e), new_t));
+            }
+            return std::make_pair(new_t, new_b);
+        });
+}
+expr replace_visitor::visit_lambda(expr const & e, context const & ctx) {
+    lean_assert(is_lambda(e));
+    return visit_abst(e, ctx);
+}
+expr replace_visitor::visit_pi(expr const & e, context const & ctx) {
+    lean_assert(is_pi(e));
+    return visit_abst(e, ctx);
+}
+expr replace_visitor::visit_let(expr const & e, context const & ctx) {
+    lean_assert(is_let(e));
+    return update_let(e, [&](expr const & t, expr const & v, expr const & b) {
+            expr new_t = t ? visit(t, ctx) : expr();
+            expr new_v = visit(v, ctx);
+            expr new_b;
+            {
+                cache::mk_scope sc(m_cache);
+                new_b = visit(b, extend(ctx, let_name(e), new_t, new_v));
+            }
+            return std::make_tuple(new_t, new_v, new_b);
+        });
+}
+expr replace_visitor::visit(expr const & e, context const & ctx) {
+    bool shared = false;
+    if (is_shared(e)) {
+        shared = true;
+        auto it = m_cache.find(e);
+        if (it != m_cache.end())
+            return it->second;
+    }
+
+    expr r;
+    switch (e.kind()) {
+    case expr_kind::Type:      r = visit_type(e, ctx); break;
+    case expr_kind::Value:     r = visit_value(e, ctx); break;
+    case expr_kind::Constant:  r = visit_constant(e, ctx); break;
+    case expr_kind::Var:       r = visit_var(e, ctx); break;
+    case expr_kind::MetaVar:   r = visit_metavar(e, ctx); break;
+    case expr_kind::App:       r = visit_app(e, ctx); break;
+    case expr_kind::Eq:        r = visit_eq(e, ctx); break;
+    case expr_kind::Lambda:    r = visit_lambda(e, ctx); break;
+    case expr_kind::Pi:        r = visit_pi(e, ctx); break;
+    case expr_kind::Let:       r = visit_let(e, ctx); break;
+    }
+
+    if (shared)
+        m_cache.insert(std::make_pair(e, r));
+
+    return r;
+}
+}

src/kernel/replace_visitor.h

@@ -0,0 +1,59 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/scoped_map.h"
+#include "kernel/replace.h"
+#include "kernel/context.h"
+
+namespace lean {
+/**
+   \brief Base class for implementing operations that apply modifications
+   an expressions.
+   The default behavior is a NOOP, users must create subclasses and
+   redefine the visit_* methods.
+
+   This is a more expensive (and flexible) version of replace_fn in
+   the file kernel/replace.h
+*/
+class replace_visitor {
+protected:
+    typedef scoped_map<expr, expr, expr_hash, expr_eqp> cache;
+    cache                      m_cache;
+    context                    m_ctx;
+
+    virtual expr visit_type(expr const &, context const &);
+    virtual expr visit_value(expr const &, context const &);
+    virtual expr visit_constant(expr const &, context const &);
+    virtual expr visit_var(expr const &, context const &);
+    virtual expr visit_metavar(expr const &, context const &);
+    virtual expr visit_app(expr const &, context const &);
+    virtual expr visit_eq(expr const &, context const &);
+    virtual expr visit_abst(expr const &, context const &);
+    virtual expr visit_lambda(expr const &, context const &);
+    virtual expr visit_pi(expr const &, context const &);
+    virtual expr visit_let(expr const &, context const &);
+    virtual expr visit(expr const &, context const &);
+
+    void set_ctx(context const & ctx) {
+        if (!is_eqp(m_ctx, ctx)) {
+            m_ctx = ctx;
+            m_cache.clear();
+        }
+    }
+
+public:
+    expr operator()(expr const & e, context const & ctx = context()) {
+        set_ctx(ctx);
+        return visit(e, ctx);
+    }
+
+    void clear() {
+        m_ctx = context();
+        m_cache.clear();
+    }
+};
+}

src/library/placeholder.cpp

@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #include "kernel/occurs.h"
 #include "kernel/metavar.h"
 #include "kernel/expr_maps.h"
-#include "library/replace_using_ctx.h"
+#include "kernel/replace_visitor.h"
 #include "library/placeholder.h"
 
 namespace lean {
@@ -24,18 +24,33 @@ bool has_placeholder(expr const & e) {
     return occurs(mk_placholder(), e);
 }
 
-expr replace_placeholders_with_metavars(expr const & e, metavar_env & menv, expr_map<expr> * new2old) {
+class replace_placeholders_with_metavars_proc : public replace_visitor {
-    auto f = [&](expr const & e, context const & c, unsigned) -> expr {
+    metavar_env &    m_menv;
+    expr_map<expr> * m_new2old;
+protected:
+    expr visit_constant(expr const & e, context const & c) {
         if (is_placeholder(e)) {
-            return menv.mk_metavar(c);
+            return m_menv.mk_metavar(c);
         } else {
             return e;
         }
-    };
+    }
-    auto p = [&](expr const & s, expr const & t) {
+
-        if (new2old)
+    expr visit(expr const & e, context const & c) {
-            (*new2old)[t] = s;
+        expr r = replace_visitor::visit(e, c);
-    };
+        if (!is_eqp(r, e) && m_new2old)
-    return replace_using_ctx_fn<decltype(f), decltype(p)>(f, p)(e);
+            (*m_new2old)[r] = e;
+        return r;
+    }
+public:
+    replace_placeholders_with_metavars_proc(metavar_env & menv, expr_map<expr> * new2old):
+        m_menv(menv),
+        m_new2old(new2old) {
+    }
+};
+
+expr replace_placeholders_with_metavars(expr const & e, metavar_env & menv, expr_map<expr> * new2old) {
+    replace_placeholders_with_metavars_proc proc(menv, new2old);
+    return proc(e);
 }
 }

src/library/replace_using_ctx.h

@@ -1,117 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "util/scoped_map.h"
-#include "kernel/replace.h"
-
-namespace lean {
-/**
-   \brief Functional for applying <tt>F</tt> to the subexpressions of a given expression.
-
-   The signature of \c F is
-   expr const &, context const & ctx, unsigned n -> expr
-
-   F is invoked for each subexpression \c s of the input expression e.
-   In a call <tt>F(s, c, n)</tt>, \c c is the context where \c s occurs,
-   and \c n is the size of \c c.
-
-   P is a "post-processing" functional object that is applied to each
-   pair (old, new)
-*/
-template<typename F, typename P = default_replace_postprocessor>
-class replace_using_ctx_fn {
-    static_assert(std::is_same<typename std::result_of<F(expr const &, context const &, unsigned)>::type, expr>::value,
-                  "replace_using_ctx_fn: return type of F is not expr");
-    // the return type of P()(e1, e2) should be void
-    static_assert(std::is_same<typename std::result_of<decltype(std::declval<P>())(expr const &, expr const &)>::type,
-                  void>::value,
-                  "The return type of P()(e1, e2) is not void");
-    typedef scoped_map<expr, expr, expr_hash, expr_eqp> cache;
-    cache                      m_cache;
-    context                    m_ctx;
-    F                          m_f;
-    P                          m_post;
-
-    expr apply(expr const & e, context const & ctx, unsigned offset) {
-        bool shared = false;
-        if (is_shared(e)) {
-            shared = true;
-            auto it = m_cache.find(e);
-            if (it != m_cache.end())
-                return it->second;
-        }
-
-        expr r = m_f(e, ctx, offset);
-        if (is_eqp(e, r)) {
-            switch (e.kind()) {
-            case expr_kind::Type: case expr_kind::Value: case expr_kind::Constant:
-            case expr_kind::Var: case expr_kind::MetaVar:
-                break;
-            case expr_kind::App:
-                r = update_app(e, [=](expr const & c) { return apply(c, ctx, offset); });
-                break;
-            case expr_kind::Eq:
-                r = update_eq(e, [=](expr const & l, expr const & r) { return std::make_pair(apply(l, ctx, offset), apply(r, ctx, offset)); });
-                break;
-            case expr_kind::Lambda:
-            case expr_kind::Pi:
-                r = update_abst(e, [=](expr const & t, expr const & b) {
-                        expr new_t = apply(t, ctx, offset);
-                        expr new_b;
-                        {
-                            cache::mk_scope sc(m_cache);
-                            new_b = apply(b, extend(ctx, abst_name(e), new_t), offset + 1);
-                        }
-                        return std::make_pair(new_t, new_b);
-                    });
-                break;
-            case expr_kind::Let:
-                r = update_let(e, [=](expr const & t, expr const & v, expr const & b) {
-                        expr new_t = t ? apply(t, ctx, offset) : expr();
-                        expr new_v = apply(v, ctx, offset);
-                        expr new_b;
-                        {
-                            cache::mk_scope sc(m_cache);
-                            new_b  = apply(b, extend(ctx, let_name(e), new_t, new_v), offset+1);
-                        }
-                        return std::make_tuple(new_t, new_v, new_b);
-                    });
-                break;
-            }
-        }
-
-        if (shared)
-            m_cache.insert(std::make_pair(e, r));
-
-        m_post(e, r);
-        return r;
-    }
-
-    void set_ctx(context const & ctx) {
-        if (!is_eqp(m_ctx, ctx)) {
-            m_ctx = ctx;
-            m_cache.clear();
-        }
-    }
-
-public:
-    replace_using_ctx_fn(F const & f, P const & p = P()):
-        m_f(f),
-        m_post(p) {
-    }
-
-    expr operator()(expr const & e, context const & ctx = context()) {
-        set_ctx(ctx);
-        return apply(e, ctx, ctx.size());
-    }
-
-    void clear() {
-        m_ctx = context();
-        m_cache.clear();
-    }
-};
-}

src/tests/library/CMakeLists.txt

@@ -19,6 +19,3 @@ add_test(reduce ${CMAKE_CURRENT_BINARY_DIR}/reduce)
 add_executable(arith_tst arith.cpp)
 target_link_libraries(arith_tst ${EXTRA_LIBS})
 add_test(arith_tst ${CMAKE_CURRENT_BINARY_DIR}/arith_tst)
-add_executable(replace_using_ctx replace_using_ctx.cpp)
-target_link_libraries(replace_using_ctx ${EXTRA_LIBS})
-add_test(replace_using_ctx ${CMAKE_CURRENT_BINARY_DIR}/replace_using_ctx)

src/tests/library/replace_using_ctx.cpp

@@ -1,47 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "util/test.h"
-#include "kernel/context.h"
-#include "kernel/abstract.h"
-#include "library/replace_using_ctx.h"
-using namespace lean;
-
-static void tst1() {
-    expr f = Const("f");
-    expr a = Const("a");
-    expr b = Const("b");
-    expr N = Const("N");
-    expr M = Const("M");
-    expr x = Var(0);
-    context ctx1;
-    ctx1 = extend(ctx1, "x", N, a);
-    context ctx2;
-    ctx2 = extend(ctx2, "x", M, b);
-    auto proc = [](expr const & e, context const & ctx, unsigned k) -> expr {
-        if (is_var(e) && var_idx(e) < k) {
-            context_entry const & entry = ctx.lookup(var_idx(e));
-            if (entry.get_body())
-                return entry.get_body();
-        }
-        return e;
-    };
-    replace_using_ctx_fn<decltype(proc)> replacer(proc);
-    expr F1 = f(x);
-    expr F1_copy = F1;
-    lean_assert_eq(replacer(F1, ctx1), f(a));
-    lean_assert_eq(replacer(F1, ctx2), f(b));
-    lean_assert(is_eqp(replacer(F1, ctx2), replacer(F1, ctx2)));
-    expr r1 = replacer(F1, ctx2);
-    replacer.clear();
-    lean_assert(!is_eqp(r1, replacer(F1, ctx2)));
-    lean_assert(is_eqp(replacer(F1, ctx1), replacer(F1, ctx1)));
-}
-
-int main() {
-    tst1();
-    return has_violations() ? 1 : 0;
-}