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

refactor(library/type_context): new type class instance cache

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-01 17:37:30 -07:00
parent ef9f9f1de0
commit 0ec22bb2cf
7 changed files with 150 additions and 79 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/frontends/lean/definition_cmds.cpp
View file

@ -342,6 +342,7 @@ environment xdefinition_cmd_core(parser & p, def_cmd_kind kind, bool is_private,
elaborator elab(p.env(), p.get_options(), metavar_context(), local_context());
buffer<expr> new_params;
elaborate_params(elab, params, new_params);
elab.set_instance_fingerprint();
replace_params(params, new_params, fn, val);
expr type;
std::tie(val, type) = elaborate_definition(p, elab, kind, fn, val, header_pos);

1
src/frontends/lean/elaborator.h
View file

@ -210,6 +210,7 @@ public:
expr mk_pi(buffer<expr> const & params, expr const & type) { return m_ctx.mk_pi(params, type); }
expr mk_lambda(buffer<expr> const & params, expr const & type) { return m_ctx.mk_lambda(params, type); }
expr infer_type(expr const & e) { return m_ctx.infer(e); }
void set_instance_fingerprint() { m_ctx.set_instance_fingerprint(); }
expr elaborate(expr const & e);
expr elaborate_type(expr const & e);
expr_pair elaborate_with_type(expr const & e, expr const & e_type);

8
src/library/arith_instance_manager.cpp
View file

@ -480,7 +480,9 @@ optional<concrete_arith_type> is_concrete_arith_type(expr const & type) {
arith_instance_info_ref cache_insert(expr_struct_map<arith_instance_info_cache_entry> & cache, type_context & tctx, expr const & type) {
auto result = cache.emplace(std::piecewise_construct,
std::forward_as_tuple<expr const &>(type),
std::forward_as_tuple<local_context const &, expr const &, level const &>(tctx.initial_lctx(), type, get_level(tctx, type)));
// TODO(dselsam): the method initial_lctx was removed
std::forward_as_tuple<local_context const &, expr const &, level const &>(tctx.lctx(), type, get_level(tctx, type)));
// std::forward_as_tuple<local_context const &, expr const &, level const &>(tctx.initial_lctx(), type, get_level(tctx, type)));
lean_assert(result.second);
return result.first->second.m_info;
}
@ -496,8 +498,8 @@ arith_instance_info_ref get_arith_instance_info_for(type_context & tctx, expr co
return cache_insert(cache, tctx, type);
} else {
arith_instance_info_cache_entry & entry = it->second;
if (tctx.compatible_local_instances(entry.m_lctx)) {
entry.m_lctx = tctx.initial_lctx();
if (false) { // tctx.compatible_local_instances(entry.m_lctx)) { // <<< This method was removed
// entry.m_lctx = tctx.initial_lctx(); // << initial_lctx was removed
return entry.m_info;
} else {
cache.erase(type);

3
src/library/compiler/compiler_step_visitor.cpp
View file

@ -11,7 +11,8 @@ Author: Leonardo de Moura
namespace lean {
compiler_step_visitor::compiler_step_visitor(environment const & env):
m_env(env),
m_ctx(env, transparency_mode::All) {
/* We don't need typeclass resolution in the compiler. */
m_ctx(env, options(), local_context::mk_with_instance_fingerprint(), transparency_mode::All) {
}
compiler_step_visitor::~compiler_step_visitor() {

12
src/library/local_context.h
View file

@ -71,7 +71,10 @@ class local_context {
unsigned m_next_idx;
name_map<local_decl> m_name2local_decl;
idx2local_decl m_idx2local_decl;
optional<unsigned> m_instance_fingerprint;
friend class type_context;
/* Return the instance fingerprint for empty local_contexts */
static unsigned get_empty_instance_fingerprint() { return 31; }
local_context remove(buffer<expr> const & locals) const;
expr mk_local_decl(name const & n, name const & ppn, expr const & type,
@ -79,6 +82,15 @@ class local_context {
public:
local_context():m_next_idx(0) {}
/* Return an empty local context with instance fingerprint set. */
static local_context mk_with_instance_fingerprint() {
local_context lctx;
lctx.m_instance_fingerprint = optional<unsigned>(get_empty_instance_fingerprint());
return lctx;
}
optional<unsigned> get_instance_fingerprint() const { return m_instance_fingerprint; }
bool empty() const { return m_idx2local_decl.empty(); }
expr mk_local_decl(expr const & type, binder_info const & bi = binder_info());

157
src/library/type_context.cpp
View file

@ -160,6 +160,10 @@ void type_context_cache_manager::recycle(type_context_cache_ptr const & ptr) {
m_reducibility_fingerprint = get_attribute_fingerprint(ptr->m_env, *g_reducibility);
m_instance_fingerprint = get_attribute_fingerprint(ptr->m_env, *g_instance);
}
if (!ptr->m_instance_fingerprint) {
ptr->m_instance_cache.clear();
ptr->m_subsingleton_cache.clear();
}
}
/* =====================
@ -187,6 +191,37 @@ bool type_context::tmp_locals::all_let_decls() const {
===================== */
MK_THREAD_LOCAL_GET_DEF(type_context_cache_manager, get_tcm);
void type_context::init_local_instances() {
m_local_instances = list<pair<name, expr>>();
m_lctx.for_each([&](local_decl const & decl) {
if (auto cls_name = is_class(decl.get_type())) {
m_local_instances = cons(mk_pair(*cls_name, decl.mk_ref()), m_local_instances);
}
});
}
void type_context::flush_instance_cache() {
lean_trace("type_context_cache", tout() << "flushing instance cache\n";);
m_cache->m_instance_fingerprint = optional<unsigned>();
m_cache->m_local_instances = list<pair<name, expr>>();
m_cache->m_instance_cache.clear();
m_cache->m_subsingleton_cache.clear();
}
void type_context::set_instance_fingerprint() {
lean_assert(!m_lctx.get_instance_fingerprint());
unsigned fingerprint = local_context::get_empty_instance_fingerprint();
m_lctx.for_each([&](local_decl const & decl) {
if (auto cls_name = is_class(decl.get_type())) {
fingerprint = hash(fingerprint, hash(cls_name->hash(), decl.get_type().hash()));
}
});
m_lctx.m_instance_fingerprint = optional<unsigned>(fingerprint);
m_cache->m_instance_fingerprint = optional<unsigned>(fingerprint);
m_cache->m_local_instances = m_local_instances;
lean_trace("type_context_cache", tout() << "set_instance_fingerprint: " << fingerprint << "\n";);
}
void type_context::init_core(transparency_mode m) {
m_used_assignment = false;
m_transparency_mode = m;
@ -194,10 +229,24 @@ void type_context::init_core(transparency_mode m) {
m_is_def_eq_depth = 0;
m_tmp_uassignment = nullptr;
m_tmp_eassignment = nullptr;
m_init_local_context = m_lctx;
m_local_instances_initialized = false;
m_unfold_pred = nullptr;
m_approximate = false;
if (auto instance_fingerprint = m_lctx.get_instance_fingerprint()) {
if (m_cache->m_instance_fingerprint == instance_fingerprint) {
lean_trace("type_context_cache", tout() << "reusing instance cache, fingerprint: " << *instance_fingerprint << "\n";);
m_local_instances = m_cache->m_local_instances;
} else {
lean_trace("type_context_cache", tout() << "incompatible fingerprints, flushing instance cache\n";);
init_local_instances();
flush_instance_cache();
m_cache->m_instance_fingerprint = m_lctx.get_instance_fingerprint();
m_cache->m_local_instances = m_local_instances;
}
} else {
init_local_instances();
flush_instance_cache();
}
lean_assert(m_cache->m_instance_fingerprint == m_lctx.get_instance_fingerprint());
}
type_context::type_context(environment const & env, options const & o, metavar_context const & mctx,
@ -228,23 +277,52 @@ type_context::~type_context() {
}
void type_context::set_env(environment const & env) {
lean_assert(m_cache->m_instance_fingerprint == m_lctx.get_instance_fingerprint());
options o = m_cache->m_options;
if (m_cache_manager) {
auto saved_local_instances = m_cache->m_local_instances;
m_cache_manager->recycle(m_cache);
m_cache = m_cache_manager->mk(env, o);
m_cache->m_local_instances = saved_local_instances;
} else {
m_cache = mk_cache(env, o, false);
}
if (m_lctx.get_instance_fingerprint()) {
m_cache->m_instance_fingerprint = m_lctx.get_instance_fingerprint();
m_cache->m_local_instances = m_local_instances;
}
lean_assert(m_cache->m_instance_fingerprint == m_lctx.get_instance_fingerprint());
}
void type_context::update_local_instances(expr const & new_local, expr const & new_type) {
if (!m_cache->m_instance_fingerprint) {
if (auto c_name = is_class(new_type)) {
m_local_instances = cons(mk_pair(*c_name, new_local), m_local_instances);
flush_instance_cache();
}
}
}
expr type_context::push_local(name const & pp_name, expr const & type, binder_info const & bi) {
return m_lctx.mk_local_decl(pp_name, type, bi);
expr local = m_lctx.mk_local_decl(pp_name, type, bi);
update_local_instances(local, type);
return local;
}
expr type_context::push_let(name const & ppn, expr const & type, expr const & value) {
expr local = m_lctx.mk_local_decl(ppn, type, value);
update_local_instances(local, type);
return local;
}
void type_context::pop_local() {
return m_lctx.pop_local_decl();
if (!m_cache->m_instance_fingerprint && m_local_instances) {
local_decl decl = *m_lctx.get_last_local_decl();
if (decl.get_name() == mlocal_name(head(m_local_instances).second)) {
m_local_instances = tail(m_local_instances);
flush_instance_cache();
}
}
m_lctx.pop_local_decl();
}
pair<local_context, expr> type_context::revert_core(buffer<expr> & to_revert, local_context const & ctx,
@ -1618,11 +1696,21 @@ bool type_context::is_def_eq_binding(expr e1, expr e2) {
}
optional<expr> type_context::mk_class_instance_at(local_context const & lctx, expr const & type) {
lean_assert(m_cache->m_instance_fingerprint == m_lctx.get_instance_fingerprint());
type_context tmp_ctx(m_cache, m_mctx, lctx, m_transparency_mode);
/* We shared the cache with tmp_ctx. So, it may be tainted with an incompatible local context. */
m_local_instances_initialized = false;
auto r = tmp_ctx.mk_class_instance(type);
if (r) m_mctx = tmp_ctx.mctx();
if (!lctx.get_instance_fingerprint() ||
lctx.get_instance_fingerprint() != m_lctx.get_instance_fingerprint()) {
/* The local instances in lctx may be different from the ones in m_lctx */
flush_instance_cache();
m_cache->m_instance_fingerprint = m_lctx.get_instance_fingerprint();
m_cache->m_local_instances = m_local_instances;
}
lean_assert(m_cache->m_instance_fingerprint == m_lctx.get_instance_fingerprint());
return r;
}
@ -2302,54 +2390,6 @@ optional<name> type_context::is_class(expr const & type) {
return is_full_class(type);
}
bool type_context::compatible_local_instances(local_context const & lctx) {
bool failed = false;
auto it = m_cache->m_local_instances;
lctx.for_each([&](local_decl const & decl) {
if (failed) return;
if (auto cname = is_class(decl.get_type())) {
if (!it) {
/* initial local context has more local instances than the ones cached at found m_local_instances */
failed = true;
return;
}
if (decl.get_name() != mlocal_name(head(it).second)) {
/* local instance in initial local constext is not compatible with the one cached at m_local_instances */
failed = true;
return;
}
it = tail(it);
}
});
return !failed && !it;
}
local_context const & type_context::initial_lctx() const {
return m_init_local_context;
}
void type_context::set_local_instances() {
m_cache->m_instance_cache.clear();
m_cache->m_subsingleton_cache.clear();
buffer<pair<name, expr>> new_instances;
m_init_local_context.for_each([&](local_decl const & decl) {
if (auto cls_name = is_class(decl.get_type())) {
new_instances.emplace_back(*cls_name, decl.mk_ref());
}
});
m_cache->m_local_instances = to_list(new_instances);
}
void type_context::init_local_instances() {
if (!m_local_instances_initialized) {
if (!compatible_local_instances(m_init_local_context)) {
set_local_instances();
}
m_local_instances_initialized = true;
}
lean_assert(m_local_instances_initialized);
}
[[ noreturn ]] static void throw_class_exception(char const * msg, expr const & m) { throw_generic_exception(msg, m); }
struct instance_synthesizer {
@ -2489,11 +2529,11 @@ struct instance_synthesizer {
list<expr> get_local_instances(name const & cname) {
buffer<expr> selected;
for (pair<name, expr> const & p : m_ctx.m_cache->m_local_instances) {
for (pair<name, expr> const & p : m_ctx.m_local_instances) {
if (p.first == cname)
selected.push_back(p.second);
}
return reverse_to_list(selected);
return to_list(selected);
}
bool mk_choice_point(expr const & mvar) {
@ -2679,7 +2719,6 @@ struct instance_synthesizer {
};
optional<expr> type_context::mk_class_instance(expr const & type) {
init_local_instances();
if (in_tmp_mode()) {
return instance_synthesizer(*this)(type);
} else {

47
src/library/type_context.h
View file

@ -80,11 +80,24 @@ class type_context_cache {
/* We use the following approach for caching type class instances.
Whenever a type_context object is initialized with a local_context,
we reset m_local_instances_initialized flag, and store a copy of the initial local_context.
Then, the first time type class resolution is invoked, we collect local_instances,
if they are equal to the ones in m_local_instances, we do nothing. Otherwise,
we reset m_local_instances with the new local_instances, and reset the cache m_local_instances. */
Whenever a type_context object is initialized with a local_context lctx
1) If lctx has an instance_fingerprint, then we compare with the instance_fingerprint
stored in this cache, if they are equal, we keep m_local_instances,
m_instance_cache and m_subsingleton_cache.
New local instances added using methods type_context::push_local and type_context::push_let will
be ignored.
2) If lctx doesn't have one, we clear m_local_instances, m_instance_cache and m_subsingleton_cache.
We also traverse lctx and collect the local instances.
The methods type_context::push_local and type_context::push_let will flush the cache
whenever new local instances are pushed into the local context.
m_instance_cache and m_subsingleton_cache are flushed before the cache is returned to the
cache manager. */
optional<unsigned> m_instance_fingerprint;
list<pair<name, expr>> m_local_instances;
instance_cache m_instance_cache;
subsingleton_cache m_subsingleton_cache;
@ -162,13 +175,12 @@ class type_context : public abstract_type_context {
m_mctx(mctx), m_tmp_uassignment_sz(usz), m_tmp_eassignment_sz(esz), m_tmp_trail_sz(tsz) {}
};
typedef buffer<scope_data> scopes;
typedef list<pair<name, expr>> local_instances;
metavar_context m_mctx;
local_context m_lctx;
bool m_local_instances_initialized;
local_context m_init_local_context;
cache_manager * m_cache_manager;
cache_ptr m_cache;
local_instances m_local_instances;
/* We only cache results when m_used_assignment is false */
bool m_used_assignment;
transparency_mode m_transparency_mode;
@ -213,6 +225,10 @@ class type_context : public abstract_type_context {
if (is_equiv_cache_target(e1, e2)) get_equiv_cache().add_equiv(e1, e2);
}
void init_local_instances();
void flush_instance_cache();
void update_local_instances(expr const & new_local, expr const & new_type);
type_context(type_context_cache_ptr const & ptr, metavar_context const & mctx, local_context const & lctx,
transparency_mode m);
public:
@ -241,6 +257,12 @@ public:
/* note: env must be a descendant of m_env */
void set_env(environment const & env);
/* Set the instance fingerprint of the current local context.
\remark After this method is invoked we cannot push local instances anymore
using the method push_local. */
void set_instance_fingerprint();
bool is_def_eq_core(level const & l1, level const & l2);
bool is_def_eq(level const & l1, level const & l2);
virtual expr whnf(expr const & e) override;
@ -285,9 +307,7 @@ public:
expr mk_pi(std::initializer_list<expr> const & locals, expr const & e);
/* Add a let-decl (aka local definition) to the local context */
expr push_let(name const & ppn, expr const & type, expr const & value) {
return m_lctx.mk_local_decl(ppn, type, value);
}
expr push_let(name const & ppn, expr const & type, expr const & value);
bool is_prop(expr const & e);
@ -489,13 +509,8 @@ private:
optional<name> constant_is_class(expr const & e);
optional<name> is_full_class(expr type);
lbool is_quick_class(expr const & type, name & result);
void set_local_instances();
void init_local_instances();
public:
bool compatible_local_instances(local_context const & lctx);
local_context const & initial_lctx() const;
/* Helper class for creating pushing local declarations into the local context m_lctx */
class tmp_locals {
type_context & m_ctx;