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

feat(library/type_context): cache failures at is_def_eq

Browse source
This commit is contained in:
Daniel Selsam 2016-12-12 13:26:56 -08:00 • committed by Leonardo de Moura
parent 13ae8b07b3
commit fc7410633f
2 changed files with 31 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/library/type_context.cpp
View file

@ -204,6 +204,26 @@ bool type_context::tmp_locals::all_let_decls() const {
===================== */
MK_THREAD_LOCAL_GET_DEF(type_context_cache_manager, get_tcm);
void type_context::cache_failure(expr const & t, expr const & s) {
if (t.hash() <= s.hash())
get_failure_cache().insert(mk_pair(t, s));
else
get_failure_cache().insert(mk_pair(s, t));
}
bool type_context::is_cached_failure(expr const & t, expr const & s) {
type_context_cache::failure_cache fcache = get_failure_cache();
if (t.hash() < s.hash()) {
return fcache.find(mk_pair(t, s)) != fcache.end();
} else if (t.hash() > s.hash()) {
return fcache.find(mk_pair(s, t)) != fcache.end();
} else {
return
fcache.find(mk_pair(t, s)) != fcache.end() ||
fcache.find(mk_pair(s, t)) != fcache.end();
}
}
void type_context::init_local_instances() {
m_local_instances = list<pair<name, expr>>();
m_lctx.for_each([&](local_decl const & decl) {
@ -2632,13 +2652,15 @@ bool type_context::is_def_eq_core_core(expr const & t, expr const & s) {
if (is_local(t_n) && is_local(s_n) && mlocal_name(t_n) == mlocal_name(s_n))
return true;
if (is_app(t_n) && is_app(s_n)) {
if (is_app(t_n) && is_app(s_n) && !is_cached_failure(t_n, s_n)) {
scope s(*this);
if (is_def_eq_core(get_app_fn(t_n), get_app_fn(s_n)) &&
is_def_eq_args(t_n, s_n) &&
process_postponed(s)) {
s.commit();
return true;
} else if (!has_expr_metavar(t_n) && !has_expr_metavar(s_n)) {
cache_failure(t_n, s_n);
}
}

8
src/library/type_context.h
View file

@ -42,6 +42,8 @@ class type_context_cache {
typedef expr_struct_map<expr> whnf_cache;
typedef expr_struct_map<optional<expr>> instance_cache;
typedef expr_struct_map<optional<expr>> subsingleton_cache;
typedef std::unordered_set<expr_pair, expr_pair_hash, expr_pair_eq> failure_cache;
environment m_env;
options m_options;
name_map<projection_info> m_proj_info;
@ -77,6 +79,8 @@ class type_context_cache {
equiv_manager m_equiv_manager[4];
failure_cache m_failure_cache[4];
whnf_cache m_whnf_cache[4];
name2bool m_aux_recursor_cache;
@ -275,6 +279,10 @@ class type_context : public abstract_type_context {
if (is_equiv_cache_target(e1, e2)) get_equiv_cache().add_equiv(e1, e2);
}
type_context_cache::failure_cache & get_failure_cache() { return m_cache->m_failure_cache[static_cast<unsigned>(m_transparency_mode)]; }
void cache_failure(expr const & t, expr const & s);
bool is_cached_failure(expr const & t, expr const & s);
void init_local_instances();
void flush_instance_cache();
void update_local_instances(expr const & new_local, expr const & new_type);