From 9c5dfc387b1b643ef0f617778e5110247cab6305 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 14 May 2014 15:53:09 -0700 Subject: [PATCH] refactor(kernel/replace_visitor): remove context from replace_visitor Signed-off-by: Leonardo de Moura --- src/kernel/metavar.cpp | 18 +++++----- src/kernel/replace_visitor.cpp | 65 ++++++++++++++++------------------ src/kernel/replace_visitor.h | 50 ++++++++------------------ 3 files changed, 55 insertions(+), 78 deletions(-) diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index ddd6864c3..70bddfd88 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -141,15 +141,15 @@ protected: return map_reuse(ls, [&](level const & l) { return visit_level(l); }, [](level const & l1, level const & l2) { return is_eqp(l1, l2); }); } - virtual expr visit_sort(expr const & s, context const &) { + virtual expr visit_sort(expr const & s) { return update_sort(s, visit_level(sort_level(s))); } - virtual expr visit_constant(expr const & c, context const &) { + virtual expr visit_constant(expr const & c) { return update_constant(c, visit_levels(const_level_params(c))); } - virtual expr visit_meta(expr const & m, context const &) { + virtual expr visit_meta(expr const & m) { name const & m_name = mlocal_name(m); auto p1 = m_subst.get_expr_assignment(m_name); if (p1) { @@ -183,28 +183,28 @@ protected: } } - virtual expr visit_app(expr const & e, context const & ctx) { + virtual expr visit_app(expr const & e) { buffer args; expr const * it = &e; while (is_app(*it)) { - args.push_back(visit(app_arg(*it), ctx)); + args.push_back(visit(app_arg(*it))); it = &app_fn(*it); } expr const & f = *it; if (is_metavar(f) && m_subst.is_expr_assigned(mlocal_name(f))) { - expr new_f = visit_meta(f, ctx); + expr new_f = visit_meta(f); return apply_beta(new_f, args.size(), args.data()); } else { - args.push_back(visit(f, ctx)); + args.push_back(visit(f)); return update_rev_app(e, args); } } - virtual expr visit(expr const & e, context const & ctx) { + virtual expr visit(expr const & e) { if (!has_metavar(e)) { return e; } else { - return replace_visitor::visit(e, ctx); + return replace_visitor::visit(e); } } diff --git a/src/kernel/replace_visitor.cpp b/src/kernel/replace_visitor.cpp index 999ff6dcd..8bd1faff2 100644 --- a/src/kernel/replace_visitor.cpp +++ b/src/kernel/replace_visitor.cpp @@ -6,45 +6,42 @@ Author: Leonardo de Moura */ #include #include "util/interrupt.h" -#include "util/freset.h" #include "kernel/replace_visitor.h" namespace lean { -expr replace_visitor::visit_sort(expr const & e, context const &) { lean_assert(is_sort(e)); return e; } -expr replace_visitor::visit_var(expr const & e, context const &) { lean_assert(is_var(e)); return e; } -expr replace_visitor::visit_constant(expr const & e, context const &) { lean_assert(is_constant(e)); return e; } -expr replace_visitor::visit_mlocal(expr const & e, context const & ctx) { +expr replace_visitor::visit_sort(expr const & e) { lean_assert(is_sort(e)); return e; } +expr replace_visitor::visit_var(expr const & e) { lean_assert(is_var(e)); return e; } +expr replace_visitor::visit_constant(expr const & e) { lean_assert(is_constant(e)); return e; } +expr replace_visitor::visit_mlocal(expr const & e) { lean_assert(is_mlocal(e)); - return update_mlocal(e, visit(mlocal_type(e), ctx)); + return update_mlocal(e, visit(mlocal_type(e))); } -expr replace_visitor::visit_meta(expr const & e, context const & ctx) { return visit_mlocal(e, ctx); } -expr replace_visitor::visit_local(expr const & e, context const & ctx) { return visit_mlocal(e, ctx); } -expr replace_visitor::visit_app(expr const & e, context const & ctx) { +expr replace_visitor::visit_meta(expr const & e) { return visit_mlocal(e); } +expr replace_visitor::visit_local(expr const & e) { return visit_mlocal(e); } +expr replace_visitor::visit_app(expr const & e) { lean_assert(is_app(e)); - return update_app(e, visit(app_fn(e), ctx), visit(app_arg(e), ctx)); + return update_app(e, visit(app_fn(e)), visit(app_arg(e))); } -expr replace_visitor::visit_binder(expr const & e, context const & ctx) { +expr replace_visitor::visit_binder(expr const & e) { lean_assert(is_binder(e)); - expr new_d = visit(binder_domain(e), ctx); - freset reset(m_cache); - expr new_b = visit(binder_body(e), extend(ctx, binder_name(e), new_d)); + expr new_d = visit(binder_domain(e)); + expr new_b = visit(binder_body(e)); return update_binder(e, new_d, new_b); } -expr replace_visitor::visit_lambda(expr const & e, context const & ctx) { return visit_binder(e, ctx); } -expr replace_visitor::visit_pi(expr const & e, context const & ctx) { return visit_binder(e, ctx); } -expr replace_visitor::visit_let(expr const & e, context const & ctx) { +expr replace_visitor::visit_lambda(expr const & e) { return visit_binder(e); } +expr replace_visitor::visit_pi(expr const & e) { return visit_binder(e); } +expr replace_visitor::visit_let(expr const & e) { lean_assert(is_let(e)); - expr new_t = visit(let_type(e), ctx); - expr new_v = visit(let_value(e), ctx); - freset reset(m_cache); - expr new_b = visit(let_body(e), extend(ctx, let_name(e), new_t)); + expr new_t = visit(let_type(e)); + expr new_v = visit(let_value(e)); + expr new_b = visit(let_body(e)); return update_let(e, new_t, new_v, new_b); } -expr replace_visitor::visit_macro(expr const & e, context const & ctx) { +expr replace_visitor::visit_macro(expr const & e) { lean_assert(is_macro(e)); buffer new_args; for (unsigned i = 0; i < macro_num_args(e); i++) - new_args.push_back(visit(macro_arg(e, i), ctx)); + new_args.push_back(visit(macro_arg(e, i))); return update_macro(e, new_args.size(), new_args.data()); } expr replace_visitor::save_result(expr const & e, expr && r, bool shared) { @@ -52,7 +49,7 @@ expr replace_visitor::save_result(expr const & e, expr && r, bool shared) { m_cache.insert(std::make_pair(e, r)); return r; } -expr replace_visitor::visit(expr const & e, context const & ctx) { +expr replace_visitor::visit(expr const & e) { check_system("expression replacer"); bool shared = false; if (is_shared(e)) { @@ -63,16 +60,16 @@ expr replace_visitor::visit(expr const & e, context const & ctx) { } switch (e.kind()) { - case expr_kind::Sort: return save_result(e, visit_sort(e, ctx), shared); - case expr_kind::Macro: return save_result(e, visit_macro(e, ctx), shared); - case expr_kind::Constant: return save_result(e, visit_constant(e, ctx), shared); - case expr_kind::Var: return save_result(e, visit_var(e, ctx), shared); - case expr_kind::Meta: return save_result(e, visit_meta(e, ctx), shared); - case expr_kind::Local: return save_result(e, visit_local(e, ctx), shared); - case expr_kind::App: return save_result(e, visit_app(e, ctx), shared); - case expr_kind::Lambda: return save_result(e, visit_lambda(e, ctx), shared); - case expr_kind::Pi: return save_result(e, visit_pi(e, ctx), shared); - case expr_kind::Let: return save_result(e, visit_let(e, ctx), shared); + case expr_kind::Sort: return save_result(e, visit_sort(e), shared); + case expr_kind::Macro: return save_result(e, visit_macro(e), shared); + case expr_kind::Constant: return save_result(e, visit_constant(e), shared); + case expr_kind::Var: return save_result(e, visit_var(e), shared); + case expr_kind::Meta: return save_result(e, visit_meta(e), shared); + case expr_kind::Local: return save_result(e, visit_local(e), shared); + case expr_kind::App: return save_result(e, visit_app(e), shared); + case expr_kind::Lambda: return save_result(e, visit_lambda(e), shared); + case expr_kind::Pi: return save_result(e, visit_pi(e), shared); + case expr_kind::Let: return save_result(e, visit_let(e), shared); } lean_unreachable(); // LCOV_EXCL_LINE diff --git a/src/kernel/replace_visitor.h b/src/kernel/replace_visitor.h index 5b9a36cfb..05f671bd9 100644 --- a/src/kernel/replace_visitor.h +++ b/src/kernel/replace_visitor.h @@ -6,7 +6,6 @@ Author: Leonardo de Moura */ #pragma once #include "kernel/expr_maps.h" -#include "kernel/context.h" namespace lean { /** @@ -14,46 +13,27 @@ namespace lean { on 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 expr_map cache; cache m_cache; - context m_ctx; expr save_result(expr const & e, expr && r, bool shared); - virtual expr visit_sort(expr const &, context const &); - virtual expr visit_macro(expr const &, context const &); - virtual expr visit_constant(expr const &, context const &); - virtual expr visit_var(expr const &, context const &); - virtual expr visit_mlocal(expr const &, context const &); - virtual expr visit_meta(expr const &, context const &); - virtual expr visit_local(expr const &, context const &); - virtual expr visit_app(expr const &, context const &); - virtual expr visit_binder(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(); - } - } - + virtual expr visit_sort(expr const &); + virtual expr visit_macro(expr const &); + virtual expr visit_constant(expr const &); + virtual expr visit_var(expr const &); + virtual expr visit_mlocal(expr const &); + virtual expr visit_meta(expr const &); + virtual expr visit_local(expr const &); + virtual expr visit_app(expr const &); + virtual expr visit_binder(expr const &); + virtual expr visit_lambda(expr const &); + virtual expr visit_pi(expr const &); + virtual expr visit_let(expr const &); + virtual expr visit(expr const &); 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(); - } + expr operator()(expr const & e) { return visit(e); } + void clear() { m_cache.clear(); } }; }