michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(kernel/replace_fn): add use_cache flag to replace function

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-05 10:49:18 -08:00
parent 2ffdbba8b0
commit bc8bb1dbd3
2 changed files with 12 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/kernel/replace_fn.cpp
View file

@ -84,6 +84,7 @@ class replace_fn {
frame_stack m_fs;
result_stack m_rs;
replace_cache_ref m_cache;
bool m_use_cache;
void save_result(expr const & e, expr const & r, unsigned offset, bool shared) {
if (shared)
@ -98,7 +99,7 @@ class replace_fn {
*/
bool visit(expr const & e, unsigned offset) {
bool shared = false;
if (is_shared(e)) {
if (m_use_cache && is_shared(e)) {
if (auto r = m_cache->find(e, offset)) {
m_rs.push_back(*r);
return true;
@ -143,7 +144,7 @@ class replace_fn {
public:
template<typename F>
replace_fn(F const & f):m_f(f) {}
replace_fn(F const & f, bool use_cache):m_f(f), m_use_cache(use_cache) {}
expr operator()(expr const & e) {
expr r;
@ -205,6 +206,7 @@ public:
class replace_rec_fn {
replace_cache_ref m_cache;
std::function<optional<expr>(expr const &, unsigned)> m_f;
bool m_use_cache;
expr save_result(expr const & e, unsigned offset, expr const & r, bool shared) {
if (shared)
@ -214,7 +216,7 @@ class replace_rec_fn {
expr apply(expr const & e, unsigned offset) {
bool shared = false;
if (is_shared(e)) {
if (m_use_cache && is_shared(e)) {
if (auto r = m_cache->find(e, offset))
return *r;
shared = true;
@ -254,15 +256,15 @@ class replace_rec_fn {
}
public:
template<typename F>
replace_rec_fn(F const & f):m_f(f) {}
replace_rec_fn(F const & f, bool use_cache):m_f(f), m_use_cache(use_cache) {}
expr operator()(expr const & e) { return apply(e, 0); }
};
expr replace(expr const & e, std::function<optional<expr>(expr const &, unsigned)> const & f) {
expr replace(expr const & e, std::function<optional<expr>(expr const &, unsigned)> const & f, bool use_cache) {
if (get_weight(e) < LEAN_REPLACE_SMALL_TERM_THRESHOLD)
return replace_rec_fn(f)(e);
return replace_rec_fn(f, use_cache)(e);
else
return replace_fn(f)(e);
return replace_fn(f, use_cache)(e);
}
}

6
src/kernel/replace_fn.h
View file

@ -20,8 +20,8 @@ namespace lean {
bindings operators that enclosing \c s. The replaces only visits children of \c e
if f return none_expr.
*/
expr replace(expr const & e, std::function<optional<expr>(expr const &, unsigned)> const & f);
inline expr replace(expr const & e, std::function<optional<expr>(expr const &)> const & f) {
return replace(e, [&](expr const & e, unsigned) { return f(e); });
expr replace(expr const & e, std::function<optional<expr>(expr const &, unsigned)> const & f, bool use_cache = true);
inline expr replace(expr const & e, std::function<optional<expr>(expr const &)> const & f, bool use_cache = true) {
return replace(e, [&](expr const & e, unsigned) { return f(e); }, use_cache);
}
}