From 4bed9f85b01a3205d6987a506c2cf792c28d48ed Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Oct 2013 15:25:17 -0700 Subject: [PATCH] feat(kernel/for_each): add option for disabling cache of atomic expressions Signed-off-by: Leonardo de Moura --- src/kernel/for_each.h | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/kernel/for_each.h b/src/kernel/for_each.h index c3231a4d17..406204531f 100644 --- a/src/kernel/for_each.h +++ b/src/kernel/for_each.h @@ -18,7 +18,7 @@ namespace lean { The \c offset is the number of binders under which \c e occurs. */ -template +template class for_each_fn { std::unique_ptr m_visited; F m_f; @@ -26,6 +26,17 @@ class for_each_fn { "for_each_fn: return type of m_f is not bool"); void apply(expr const & e, unsigned offset) { + if (!CacheAtomic) { + switch (e.kind()) { + case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: + case expr_kind::Var: case expr_kind::MetaVar: + m_f(e, offset); + return; + default: + break; + } + } + if (is_shared(e)) { expr_cell_offset p(e.raw(), offset); if (!m_visited)