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

feat(kernel/for_each): add option for disabling cache of atomic expressions

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-10-25 15:25:17 -07:00
parent ce10bfeaf6
commit 4bed9f85b0
1 changed files with 12 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/kernel/for_each.h
View file

@ -18,7 +18,7 @@ namespace lean {
</code> </code>
The \c offset is the number of binders under which \c e occurs. The \c offset is the number of binders under which \c e occurs.
*/ */
template<typename F> template<typename F, bool CacheAtomic = false>
class for_each_fn { class for_each_fn {
std::unique_ptr<expr_cell_offset_set> m_visited; std::unique_ptr<expr_cell_offset_set> m_visited;
F m_f; F m_f;
@ -26,6 +26,17 @@ class for_each_fn {
"for_each_fn: return type of m_f is not bool"); "for_each_fn: return type of m_f is not bool");
void apply(expr const & e, unsigned offset) { 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)) { if (is_shared(e)) {
expr_cell_offset p(e.raw(), offset); expr_cell_offset p(e.raw(), offset);
if (!m_visited) if (!m_visited)