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

chore(library/type_context): simplify cache management

Browse source
This commit is contained in:
Leonardo de Moura 2018-02-06 10:30:52 -08:00
parent da032ccc3b
commit 9e08cab381
2 changed files with 1 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/library/type_context.cpp
View file

@ -183,19 +183,7 @@ type_context_cache_ptr type_context_cache_manager::mk(environment const & env, o
m_cache_ptr->m_options = o;
return release();
}
if (!env.is_descendant(m_env) ||
get_reducibility_fingerprint(env) != m_reducibility_fingerprint ||
get_instance_fingerprint(env) != m_instance_fingerprint) {
lean_trace("type_context_cache",
bool c1 = (get_reducibility_fingerprint(env) == m_reducibility_fingerprint);
bool c2 = (get_instance_fingerprint(env) == m_instance_fingerprint);
tout() << "creating new cache, is_descendant: " << env.is_descendant(m_env)
<< ", reducibility compatibility: " << c1 << ", instance compatibility: " << c2 << "\n";);
return mk_cache(env, o, m_use_bi);
}
m_cache_ptr->m_options = o;
m_cache_ptr->m_env = env;
return release();
return mk_cache(env, o, m_use_bi);
}
void type_context_cache_manager::recycle(type_context_cache_ptr const & ptr) {
@ -203,8 +191,6 @@ void type_context_cache_manager::recycle(type_context_cache_ptr const & ptr) {
m_cache_ptr = ptr;
if (!is_eqp(ptr->m_env, m_env)) {
m_env = ptr->m_env;
m_reducibility_fingerprint = get_reducibility_fingerprint(ptr->m_env);
m_instance_fingerprint = get_instance_fingerprint(ptr->m_env);
}
if (!ptr->m_instance_fingerprint) {
ptr->m_instance_cache.clear();

2
src/library/type_context.h
View file

@ -164,8 +164,6 @@ typedef std::shared_ptr<type_context_cache> type_context_cache_ptr;
to try to reuse type_context_cache objects */
class type_context_cache_manager {
type_context_cache_ptr m_cache_ptr;
unsigned m_reducibility_fingerprint;
unsigned m_instance_fingerprint;
environment m_env;
unsigned m_max_depth;
bool m_use_bi;