From 61df118339ae5071ce2c3c3df587bf99ea1caf6c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 23 Jul 2014 18:14:44 -0700 Subject: [PATCH] refactor(kernel/for_each_fn): simplify module interface Signed-off-by: Leonardo de Moura --- src/kernel/for_each_fn.cpp | 118 +++++++++++++++++++++---------------- src/kernel/for_each_fn.h | 19 +----- 2 files changed, 69 insertions(+), 68 deletions(-) diff --git a/src/kernel/for_each_fn.cpp b/src/kernel/for_each_fn.cpp index 159989a77..52afd8def 100644 --- a/src/kernel/for_each_fn.cpp +++ b/src/kernel/for_each_fn.cpp @@ -8,63 +8,77 @@ Author: Leonardo de Moura #include "kernel/for_each_fn.h" namespace lean { -void for_each_fn::apply(expr const & e, unsigned offset) { - buffer> todo; - todo.emplace_back(e, offset); - while (true) { - begin_loop: - if (todo.empty()) - break; - auto p = todo.back(); - todo.pop_back(); - expr const & e = p.first; - unsigned offset = p.second; +class for_each_fn { + std::unique_ptr m_visited; + std::function m_f; // NOLINT - switch (e.kind()) { - case expr_kind::Constant: case expr_kind::Var: - case expr_kind::Sort: - m_f(e, offset); - goto begin_loop; - default: - break; - } + void apply(expr const & e, unsigned offset) { + buffer> todo; + todo.emplace_back(e, offset); + while (true) { + begin_loop: + if (todo.empty()) + break; + auto p = todo.back(); + todo.pop_back(); + expr const & e = p.first; + unsigned offset = p.second; - if (is_shared(e)) { - expr_cell_offset p(e.raw(), offset); - if (!m_visited) - m_visited.reset(new expr_cell_offset_set()); - if (m_visited->find(p) != m_visited->end()) + switch (e.kind()) { + case expr_kind::Constant: case expr_kind::Var: + case expr_kind::Sort: + m_f(e, offset); + goto begin_loop; + default: + break; + } + + if (is_shared(e)) { + expr_cell_offset p(e.raw(), offset); + if (!m_visited) + m_visited.reset(new expr_cell_offset_set()); + if (m_visited->find(p) != m_visited->end()) + goto begin_loop; + m_visited->insert(p); + } + + if (!m_f(e, offset)) + goto begin_loop; + + switch (e.kind()) { + case expr_kind::Constant: case expr_kind::Var: + case expr_kind::Sort: + goto begin_loop; + case expr_kind::Meta: case expr_kind::Local: + todo.emplace_back(mlocal_type(e), offset); + goto begin_loop; + case expr_kind::Macro: { + unsigned i = macro_num_args(e); + while (i > 0) { + --i; + todo.emplace_back(macro_arg(e, i), offset); + } + goto begin_loop; + } + case expr_kind::App: + todo.emplace_back(app_arg(e), offset); + todo.emplace_back(app_fn(e), offset); + goto begin_loop; + case expr_kind::Lambda: case expr_kind::Pi: + todo.emplace_back(binding_body(e), offset + 1); + todo.emplace_back(binding_domain(e), offset); goto begin_loop; - m_visited->insert(p); - } - - if (!m_f(e, offset)) - goto begin_loop; - - switch (e.kind()) { - case expr_kind::Constant: case expr_kind::Var: - case expr_kind::Sort: - goto begin_loop; - case expr_kind::Meta: case expr_kind::Local: - todo.emplace_back(mlocal_type(e), offset); - goto begin_loop; - case expr_kind::Macro: { - unsigned i = macro_num_args(e); - while (i > 0) { - --i; - todo.emplace_back(macro_arg(e, i), offset); } - goto begin_loop; - } - case expr_kind::App: - todo.emplace_back(app_arg(e), offset); - todo.emplace_back(app_fn(e), offset); - goto begin_loop; - case expr_kind::Lambda: case expr_kind::Pi: - todo.emplace_back(binding_body(e), offset + 1); - todo.emplace_back(binding_domain(e), offset); - goto begin_loop; } } + +public: + for_each_fn(std::function && f):m_f(f) {} // NOLINT + for_each_fn(std::function const & f):m_f(f) {} // NOLINT + void operator()(expr const & e) { apply(e, 0); } +}; + +void for_each(expr const & e, std::function && f) { // NOLINT + return for_each_fn(f)(e); } } diff --git a/src/kernel/for_each_fn.h b/src/kernel/for_each_fn.h index c07205837..c31ac7a9a 100644 --- a/src/kernel/for_each_fn.h +++ b/src/kernel/for_each_fn.h @@ -13,10 +13,9 @@ Author: Leonardo de Moura #include "kernel/expr_sets.h" namespace lean { -/** - \brief Expression visitor. +/** \brief Expression visitor. - The argument \c F must be a lambda (function object) containing the method + The argument \c f must be a lambda (function object) containing the method bool operator()(expr const & e, unsigned offset) @@ -24,17 +23,5 @@ namespace lean { The \c offset is the number of binders under which \c e occurs. */ -class for_each_fn { - std::unique_ptr m_visited; - std::function m_f; // NOLINT - void apply(expr const & e, unsigned offset); -public: - template for_each_fn(F && f):m_f(f) {} - template for_each_fn(F const & f):m_f(f) {} - void operator()(expr const & e) { apply(e, 0); } -}; - -template void for_each(expr const & e, F && f) { - return for_each_fn(f)(e); -} +void for_each(expr const & e, std::function && f); // NOLINT }