From c1e451151a65da8157af04915015b9e372e73e72 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 23 Oct 2013 15:01:33 -0700 Subject: [PATCH] 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 --- src/kernel/CMakeLists.txt | 3 +- src/kernel/replace_visitor.cpp | 84 +++++++++++++++++ src/kernel/replace_visitor.h | 59 ++++++++++++ src/library/placeholder.cpp | 35 +++++-- src/library/replace_using_ctx.h | 117 ------------------------ src/tests/library/CMakeLists.txt | 3 - src/tests/library/replace_using_ctx.cpp | 47 ---------- 7 files changed, 170 insertions(+), 178 deletions(-) create mode 100644 src/kernel/replace_visitor.cpp create mode 100644 src/kernel/replace_visitor.h delete mode 100644 src/library/replace_using_ctx.h delete mode 100644 src/tests/library/replace_using_ctx.cpp diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index 467470678..f5a0853b3 100644 --- a/src/kernel/CMakeLists.txt +++ b/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}) diff --git a/src/kernel/replace_visitor.cpp b/src/kernel/replace_visitor.cpp new file mode 100644 index 000000000..88e67a90a --- /dev/null +++ b/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; +} +} diff --git a/src/kernel/replace_visitor.h b/src/kernel/replace_visitor.h new file mode 100644 index 000000000..b46185759 --- /dev/null +++ b/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 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(); + } +}; +} diff --git a/src/library/placeholder.cpp b/src/library/placeholder.cpp index 2d07ebab1..2e6fdcd09 100644 --- a/src/library/placeholder.cpp +++ b/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 * new2old) { - auto f = [&](expr const & e, context const & c, unsigned) -> expr { +class replace_placeholders_with_metavars_proc : public replace_visitor { + metavar_env & m_menv; + expr_map * 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) - (*new2old)[t] = s; - }; - return replace_using_ctx_fn(f, p)(e); + } + + expr visit(expr const & e, context const & c) { + expr r = replace_visitor::visit(e, c); + if (!is_eqp(r, e) && m_new2old) + (*m_new2old)[r] = e; + return r; + } +public: + replace_placeholders_with_metavars_proc(metavar_env & menv, expr_map * new2old): + m_menv(menv), + m_new2old(new2old) { + } +}; + +expr replace_placeholders_with_metavars(expr const & e, metavar_env & menv, expr_map * new2old) { + replace_placeholders_with_metavars_proc proc(menv, new2old); + return proc(e); } } diff --git a/src/library/replace_using_ctx.h b/src/library/replace_using_ctx.h deleted file mode 100644 index ebce5f19d..000000000 --- a/src/library/replace_using_ctx.h +++ /dev/null @@ -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 F 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 F(s, c, n), \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 -class replace_using_ctx_fn { - static_assert(std::is_same::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())(expr const &, expr const &)>::type, - void>::value, - "The return type of P()(e1, e2) is not void"); - typedef scoped_map 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(); - } -}; -} diff --git a/src/tests/library/CMakeLists.txt b/src/tests/library/CMakeLists.txt index 49577ff77..1540ea3e6 100644 --- a/src/tests/library/CMakeLists.txt +++ b/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) diff --git a/src/tests/library/replace_using_ctx.cpp b/src/tests/library/replace_using_ctx.cpp deleted file mode 100644 index d7f26ce07..000000000 --- a/src/tests/library/replace_using_ctx.cpp +++ /dev/null @@ -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 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; -}