From 533f44e2246967b142eaeb76721441376dea4c2e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 16 Feb 2014 11:23:25 -0800 Subject: [PATCH] refactor(kernel/expr): for_each_fn, replace_fn, and find_fn without templates Signed-off-by: Leonardo de Moura --- src/kernel/CMakeLists.txt | 2 +- src/kernel/find_fn.h | 19 ++-- src/kernel/for_each_fn.cpp | 75 ++++++++++++++ src/kernel/for_each_fn.h | 99 ++++--------------- src/kernel/occurs.cpp | 4 +- src/kernel/replace_fn.cpp | 157 ++++++++++++++++++++++++++++++ src/kernel/replace_fn.h | 193 ++++--------------------------------- 7 files changed, 280 insertions(+), 269 deletions(-) create mode 100644 src/kernel/for_each_fn.cpp create mode 100644 src/kernel/replace_fn.cpp diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index 3e94e1e9c3..b220ecf1e9 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -1,5 +1,5 @@ add_library(kernel level.cpp diff_cnstrs.cpp expr.cpp expr_eq_fn.cpp -occurs.cpp +for_each_fn.cpp occurs.cpp replace_fn.cpp # free_vars.cpp abstract.cpp instantiate.cpp # normalizer.cpp context.cpp level.cpp object.cpp environment.cpp # type_checker.cpp kernel.cpp occurs.cpp metavar.cpp diff --git a/src/kernel/find_fn.h b/src/kernel/find_fn.h index 3fad718f06..da9db5455d 100644 --- a/src/kernel/find_fn.h +++ b/src/kernel/find_fn.h @@ -9,16 +9,16 @@ Author: Leonardo de Moura #include "kernel/expr.h" namespace lean { -template class find_fn { + template struct pred_fn { optional & m_result; - P m_p; + P m_p; pred_fn(optional & result, P const & p):m_result(result), m_p(p) {} - bool operator()(expr const & e, unsigned) { + bool operator()(expr const & e, unsigned offset) { if (m_result) { return false; // already found result, stop the search - } else if (m_p(e)) { + } else if (m_p(e, offset)) { m_result = e; return false; // stop the search } else { @@ -26,18 +26,17 @@ class find_fn { } } }; - optional m_result; - for_each_fn m_proc; + optional m_result; + for_each_fn m_proc; public: - find_fn(P const & p):m_proc(pred_fn(m_result, p)) {} + template find_fn(P const & p):m_proc(pred_fn

(m_result, p)) {} optional operator()(expr const & e) { m_proc(e); return m_result; } }; /** \brief Return a subexpression of \c e that satisfies the predicate \c p. */ -template -optional find(expr const & e, P p) { - return find_fn

(p)(e); +template optional find(expr const & e, P p) { + return find_fn(p)(e); } } diff --git a/src/kernel/for_each_fn.cpp b/src/kernel/for_each_fn.cpp new file mode 100644 index 0000000000..6b35e04b1f --- /dev/null +++ b/src/kernel/for_each_fn.cpp @@ -0,0 +1,75 @@ +/* +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/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; + + switch (e.kind()) { + case expr_kind::Constant: case expr_kind::Var: + case expr_kind::Sort: case expr_kind::Macro: + 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: case expr_kind::Macro: + goto begin_loop; + case expr_kind::Meta: case expr_kind::Local: + todo.emplace_back(mlocal_type(e), 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::Pair: + todo.emplace_back(pair_type(e), offset); + todo.emplace_back(pair_second(e), offset); + todo.emplace_back(pair_first(e), offset); + goto begin_loop; + case expr_kind::Fst: case expr_kind::Snd: + todo.emplace_back(proj_arg(e), offset); + goto begin_loop; + case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma: + todo.emplace_back(binder_body(e), offset + 1); + todo.emplace_back(binder_domain(e), offset); + goto begin_loop; + case expr_kind::Let: + todo.emplace_back(let_body(e), offset + 1); + todo.emplace_back(let_value(e), offset); + if (let_type(e)) + todo.emplace_back(*let_type(e), offset); + goto begin_loop; + } + } +} +} diff --git a/src/kernel/for_each_fn.h b/src/kernel/for_each_fn.h index a3e1a751b3..67c7740721 100644 --- a/src/kernel/for_each_fn.h +++ b/src/kernel/for_each_fn.h @@ -7,99 +7,34 @@ Author: Leonardo de Moura #pragma once #include #include +#include #include "util/buffer.h" #include "kernel/expr.h" #include "kernel/expr_sets.h" namespace lean { /** - \brief Template for implementing expression visitors. - The argument \c F must be a function object containing the method - - void operator()(expr const & e, unsigned offset) - - The \c offset is the number of binders under which \c e occurs. + \brief Expression visitor. + + The argument \c F must be a lambda (function object) containing the method + + + void operator()(expr const & e, unsigned offset) + + + The \c offset is the number of binders under which \c e occurs. */ -template class for_each_fn { - std::unique_ptr m_visited; - F m_f; - static_assert(std::is_same::type, bool>::value, - "for_each_fn: return type of m_f is not bool"); - - 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 (!CacheAtomic) { - switch (e.kind()) { - case expr_kind::Constant: case expr_kind::Var: - case expr_kind::Sort: case expr_kind::Macro: - 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: case expr_kind::Macro: - goto begin_loop; - case expr_kind::Meta: case expr_kind::Local: - todo.emplace_back(mlocal_type(e), 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::Pair: - todo.emplace_back(pair_type(e), offset); - todo.emplace_back(pair_second(e), offset); - todo.emplace_back(pair_first(e), offset); - goto begin_loop; - case expr_kind::Fst: case expr_kind::Snd: - todo.emplace_back(proj_arg(e), offset); - goto begin_loop; - case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma: - todo.emplace_back(binder_body(e), offset + 1); - todo.emplace_back(binder_domain(e), offset); - goto begin_loop; - case expr_kind::Let: - todo.emplace_back(let_body(e), offset + 1); - todo.emplace_back(let_value(e), offset); - if (let_type(e)) - todo.emplace_back(*let_type(e), offset); - goto begin_loop; - } - } - } + std::unique_ptr m_visited; + std::function m_f; + void apply(expr const & e, unsigned offset); public: - for_each_fn(F const & f):m_f(f) {} + 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); +template void for_each(expr const & e, F && f) { + return for_each_fn(f)(e); } } diff --git a/src/kernel/occurs.cpp b/src/kernel/occurs.cpp index e9fcd2792e..280965043e 100644 --- a/src/kernel/occurs.cpp +++ b/src/kernel/occurs.cpp @@ -9,10 +9,10 @@ Author: Leonardo de Moura namespace lean { bool occurs(expr const & n, expr const & m) { - return static_cast(find(m, [&](expr const & e) { return n == e; })); + return static_cast(find(m, [&](expr const & e, unsigned) { return n == e; })); } bool occurs(name const & n, expr const & m) { - return static_cast(find(m, [&](expr const & e) { return is_constant(e) && const_name(e) == n; })); + return static_cast(find(m, [&](expr const & e, unsigned) { return is_constant(e) && const_name(e) == n; })); } } diff --git a/src/kernel/replace_fn.cpp b/src/kernel/replace_fn.cpp new file mode 100644 index 0000000000..b443ee7e40 --- /dev/null +++ b/src/kernel/replace_fn.cpp @@ -0,0 +1,157 @@ +/* +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_fn.h" + +namespace lean { +bool replace_fn::is_atomic(expr const & e) { + switch (e.kind()) { + case expr_kind::Constant: case expr_kind::Sort: + case expr_kind::Macro: case expr_kind::Var: + return true; + default: + return false; + } +} + +void replace_fn::save_result(expr const & e, expr const & r, unsigned offset, bool shared) { + if (shared) + m_cache.insert(std::make_pair(expr_cell_offset(e.raw(), offset), r)); + m_post(e, r); + m_rs.push_back(r); +} + +/** + \brief Visit \c e at the given offset. Return true iff the result is on the + result stack \c m_rs. Return false iff a new frame was pushed on the stack \c m_fs. + The idea is that after the frame is processed, the result will be on the result stack. +*/ +bool replace_fn::visit(expr const & e, unsigned offset) { + bool shared = false; + if (is_shared(e)) { + expr_cell_offset p(e.raw(), offset); + auto it = m_cache.find(p); + if (it != m_cache.end()) { + m_rs.push_back(it->second); + return true; + } + shared = true; + } + + expr r = m_f(e, offset); + if (is_atomic(r) || !is_eqp(e, r)) { + save_result(e, r, offset, shared); + return true; + } else { + m_fs.emplace_back(e, offset, shared); + return false; + } +} + +/** + \brief Return true iff f.m_index == idx. + When the result is true, f.m_index is incremented. +*/ +bool replace_fn::check_index(frame & f, unsigned idx) { + if (f.m_index == idx) { + f.m_index++; + return true; + } else { + return false; + } +} + +expr const & replace_fn::rs(int i) { + lean_assert(i < 0); + return m_rs[m_rs.size() + i]; +} + +void replace_fn::pop_rs(unsigned num) { + m_rs.shrink(m_rs.size() - num); +} + +expr replace_fn::operator()(expr const & e) { + expr r; + visit(e, 0); + while (!m_fs.empty()) { + begin_loop: + check_interrupted(); + frame & f = m_fs.back(); + expr const & e = f.m_expr; + unsigned offset = f.m_offset; + switch (e.kind()) { + case expr_kind::Constant: case expr_kind::Sort: + case expr_kind::Macro: case expr_kind::Var: + lean_unreachable(); // LCOV_EXCL_LINE + case expr_kind::Meta: case expr_kind::Local: + if (check_index(f, 0) && !visit(mlocal_type(e), offset)) + goto begin_loop; + r = update_mlocal(e, rs(-1)); + pop_rs(1); + break; + case expr_kind::Pair: + if (check_index(f, 0) && !visit(pair_first(e), offset)) + goto begin_loop; + if (check_index(f, 1) && !visit(pair_second(e), offset)) + goto begin_loop; + if (check_index(f, 2) && !visit(pair_type(e), offset)) + goto begin_loop; + r = update_pair(e, rs(-3), rs(-2), rs(-1)); + pop_rs(3); + break; + case expr_kind::Fst: case expr_kind::Snd: + if (check_index(f, 0) && !visit(proj_arg(e), offset)) + goto begin_loop; + r = update_proj(e, rs(-1)); + pop_rs(1); + break; + case expr_kind::App: + if (check_index(f, 0) && !visit(app_fn(e), offset)) + goto begin_loop; + if (check_index(f, 1) && !visit(app_arg(e), offset)) + goto begin_loop; + r = update_app(e, rs(-2), rs(-1)); + pop_rs(2); + break; + case expr_kind::Sigma: case expr_kind::Pi: case expr_kind::Lambda: + if (check_index(f, 0) && !visit(binder_domain(e), offset)) + goto begin_loop; + if (check_index(f, 1) && !visit(binder_body(e), offset + 1)) + goto begin_loop; + r = update_binder(e, rs(-2), rs(-1)); + pop_rs(2); + break; + case expr_kind::Let: + if (check_index(f, 0) && let_type(e) && !visit(*let_type(e), offset)) + goto begin_loop; + if (check_index(f, 1) && !visit(let_value(e), offset)) + goto begin_loop; + if (check_index(f, 2) && !visit(let_body(e), offset + 1)) + goto begin_loop; + if (let_type(e)) { + r = update_let(e, some_expr(rs(-3)), rs(-2), rs(-1)); + pop_rs(3); + } else { + r = update_let(e, none_expr(), rs(-2), rs(-1)); + pop_rs(2); + } + break; + } + save_result(e, r, offset, f.m_shared); + m_fs.pop_back(); + } + lean_assert(m_rs.size() == 1); + r = m_rs.back(); + m_rs.pop_back(); + return r; +} + +void replace_fn::clear() { + m_cache.clear(); + m_fs.clear(); + m_rs.clear(); +} +} diff --git a/src/kernel/replace_fn.h b/src/kernel/replace_fn.h index 616e341bef..250628048f 100644 --- a/src/kernel/replace_fn.h +++ b/src/kernel/replace_fn.h @@ -35,15 +35,7 @@ public: P is a "post-processing" functional object that is applied to each pair (old, new) */ -template class replace_fn { - static_assert(std::is_same::type, expr>::value, - "replace_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"); - struct frame { expr m_expr; unsigned m_offset; @@ -54,179 +46,32 @@ class replace_fn { typedef buffer frame_stack; typedef buffer result_stack; - expr_cell_offset_map m_cache; - F m_f; - P m_post; - frame_stack m_fs; - result_stack m_rs; + expr_cell_offset_map m_cache; + std::function m_f; + std::function m_post; + frame_stack m_fs; + result_stack m_rs; - static bool is_atomic(expr const & e) { - switch (e.kind()) { - case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: - case expr_kind::Var: case expr_kind::MetaVar: - return true; - default: - return false; - } - } - - void save_result(expr const & e, expr const & r, unsigned offset, bool shared) { - if (shared) - m_cache.insert(std::make_pair(expr_cell_offset(e.raw(), offset), r)); - m_post(e, r); - m_rs.push_back(r); - } - - /** - \brief Visit \c e at the given offset. Return true iff the result is on the - result stack \c m_rs. Return false iff a new frame was pushed on the stack \c m_fs. - The idea is that after the frame is processed, the result will be on the result stack. - */ - bool visit(expr const & e, unsigned offset) { - bool shared = false; - if (is_shared(e)) { - expr_cell_offset p(e.raw(), offset); - auto it = m_cache.find(p); - if (it != m_cache.end()) { - m_rs.push_back(it->second); - return true; - } - shared = true; - } - - expr r = m_f(e, offset); - if (is_atomic(r) || !is_eqp(e, r)) { - save_result(e, r, offset, shared); - return true; - } else { - m_fs.emplace_back(e, offset, shared); - return false; - } - } - - /** - \brief Return true iff f.m_index == idx. - When the result is true, f.m_index is incremented. - */ - bool check_index(frame & f, unsigned idx) { - if (f.m_index == idx) { - f.m_index++; - return true; - } else { - return false; - } - } - - expr const & rs(int i) { - lean_assert(i < 0); - return m_rs[m_rs.size() + i]; - } - - void pop_rs(unsigned num) { - m_rs.shrink(m_rs.size() - num); - } + static bool is_atomic(expr const & e); + void save_result(expr const & e, expr const & r, unsigned offset, bool shared); + bool visit(expr const & e, unsigned offset); + bool check_index(frame & f, unsigned idx); + expr const & rs(int i); + void pop_rs(unsigned num); public: + template replace_fn(F const & f, P const & p = P()): - m_f(f), - m_post(p) { - } - - expr operator()(expr const & e) { - expr r; - visit(e, 0); - while (!m_fs.empty()) { - begin_loop: - check_interrupted(); - frame & f = m_fs.back(); - expr const & e = f.m_expr; - unsigned offset = f.m_offset; - switch (e.kind()) { - case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: case expr_kind::MetaVar: - lean_unreachable(); // LCOV_EXCL_LINE - case expr_kind::HEq: - if (check_index(f, 0) && !visit(heq_lhs(e), offset)) - goto begin_loop; - if (check_index(f, 1) && !visit(heq_rhs(e), offset)) - goto begin_loop; - r = update_heq(e, rs(-2), rs(-1)); - pop_rs(2); - break; - case expr_kind::Pair: - if (check_index(f, 0) && !visit(pair_first(e), offset)) - goto begin_loop; - if (check_index(f, 1) && !visit(pair_second(e), offset)) - goto begin_loop; - if (check_index(f, 2) && !visit(pair_type(e), offset)) - goto begin_loop; - r = update_pair(e, rs(-3), rs(-2), rs(-1)); - pop_rs(3); - break; - case expr_kind::Proj: - if (check_index(f, 0) && !visit(proj_arg(e), offset)) - goto begin_loop; - r = update_proj(e, rs(-1)); - pop_rs(1); - break; - case expr_kind::App: { - unsigned num = num_args(e); - while (f.m_index < num) { - expr const & c = arg(e, f.m_index); - f.m_index++; - if (!visit(c, offset)) - goto begin_loop; - } - r = update_app(e, num, m_rs.end() - num_args(e)); - pop_rs(num); - break; - } - case expr_kind::Sigma: case expr_kind::Pi: case expr_kind::Lambda: - if (check_index(f, 0) && !visit(abst_domain(e), offset)) - goto begin_loop; - if (check_index(f, 1) && !visit(abst_body(e), offset + 1)) - goto begin_loop; - r = update_abstraction(e, rs(-2), rs(-1)); - pop_rs(2); - break; - case expr_kind::Let: - if (check_index(f, 0) && let_type(e) && !visit(*let_type(e), offset)) - goto begin_loop; - if (check_index(f, 1) && !visit(let_value(e), offset)) - goto begin_loop; - if (check_index(f, 2) && !visit(let_body(e), offset + 1)) - goto begin_loop; - if (let_type(e)) { - r = update_let(e, some_expr(rs(-3)), rs(-2), rs(-1)); - pop_rs(3); - } else { - r = update_let(e, none_expr(), rs(-2), rs(-1)); - pop_rs(2); - } - break; - } - save_result(e, r, offset, f.m_shared); - m_fs.pop_back(); - } - lean_assert(m_rs.size() == 1); - r = m_rs.back(); - m_rs.pop_back(); - return r; - } - - void clear() { - m_cache.clear(); - m_fs.clear(); - m_rs.clear(); - } + m_f(f), m_post(p) {} + expr operator()(expr const & e); + void clear(); }; -template -expr replace(expr const & e, F f) { - return replace_fn(f)(e); +template expr replace(expr const & e, F const & f) { + return replace_fn(f)(e); } -template -expr replace(expr const & e, F f, P p) { - return replace_fn(f, p)(e); +template expr replace(expr const & e, F const & f, P const & p) { + return replace_fn(f, p)(e); } }