max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/tactic/user_attribute): make sure it compiles when using older versions of g++

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-12 10:51:25 -07:00
parent 5e3e54e208
commit af78fd0a3c
2 changed files with 9 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/tactic/user_attribute.cpp
View file

@ -49,6 +49,7 @@ private:
struct entry {
unsigned m_fingerprint;
vm_obj m_val;
entry(unsigned f, vm_obj const & val):m_fingerprint(f), m_val(val) {}
};
name_hash_map<entry> m_cache;
@ -58,6 +59,10 @@ public:
if (it != m_cache.end()) {
if (it->second.m_fingerprint == attr.get_fingerprint(env))
return it->second.m_val;
lean_trace("user_attributes_cache", tout() << "cached result for [" << attr.get_name() << "] "
<< "has been found, but cache fingerprint does not match\n";);
} else {
lean_trace("user_attributes_cache", tout() << "no cached result for [" << attr.get_name() << "]\n";);
}
lean_trace("user_attributes_cache", tout() << "recomputing cache for [" << attr.get_name() << "]\n";);
@ -66,7 +71,8 @@ public:
auto cached = invoke(cache_handler, to_vm_list(to_list(instances), [&](const name & inst) {
return to_obj(env.get(inst));
}));
return m_cache[attr.get_name()] = entry {attr.get_fingerprint(env), cached};
m_cache.erase(attr.get_name());
m_cache.insert(mk_pair(attr.get_name(), entry(attr.get_fingerprint(env), cached)));
return cached;
}
};

2
tests/lean/caching_user_attribute.lean.expected.out
View file

@ -1,3 +1,4 @@
[user_attributes_cache] no cached result for [foo]
[user_attributes_cache] recomputing cache for [foo]
eq.refl
eq.mp
@ -5,6 +6,7 @@ eq.mp
eq.refl
eq.mp
[user_attributes_cache] cached result for [foo] has been found, but cache fingerprint does not match
[user_attributes_cache] recomputing cache for [foo]
eq.refl
eq.mpr