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

fix(kernel/expr): add global expressions storing Prop and Type.{1} to

Browse source 
hash-consing cache when max-sharing is enabled
This commit is contained in:
Leonardo de Moura 2015-10-02 14:54:58 -07:00
parent aadac02bec
commit d324d54d21
1 changed files with 15 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/kernel/expr.cpp
View file

@ -309,19 +309,6 @@ expr_macro::~expr_macro() {
LEAN_THREAD_VALUE(bool, g_expr_cache_enabled, true);
typedef typename std::unordered_set<expr, expr_hash, is_bi_equal_proc> expr_cache;
MK_THREAD_LOCAL_GET_DEF(expr_cache, get_expr_cache);
bool enable_expr_caching(bool f) {
bool r1 = enable_level_caching(f);
bool r2 = g_expr_cache_enabled;
lean_verify(r1 == r2);
expr_cache new_cache;
get_expr_cache().swap(new_cache);
if (f) {
clear_abstract_cache();
clear_instantiate_cache();
}
g_expr_cache_enabled = f;
return r2;
}
inline expr cache(expr const & e) {
if (g_expr_cache_enabled) {
expr_cache & cache = get_expr_cache();
@ -334,6 +321,21 @@ inline expr cache(expr const & e) {
}
return e;
}
bool enable_expr_caching(bool f) {
bool r1 = enable_level_caching(f);
bool r2 = g_expr_cache_enabled;
lean_verify(r1 == r2);
expr_cache new_cache;
get_expr_cache().swap(new_cache);
if (f) {
clear_abstract_cache();
clear_instantiate_cache();
cache(mk_Prop());
cache(mk_Type());
}
g_expr_cache_enabled = f;
return r2;
}
bool is_cached(expr const & e) {
return get_expr_cache().find(e) != get_expr_cache().end();
}