From 0ec22bb2cff756f7482a47551adb133a12dc38f2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 1 Sep 2016 17:37:30 -0700 Subject: [PATCH] refactor(library/type_context): new type class instance cache --- src/frontends/lean/definition_cmds.cpp | 1 + src/frontends/lean/elaborator.h | 1 + src/library/arith_instance_manager.cpp | 8 +- .../compiler/compiler_step_visitor.cpp | 3 +- src/library/local_context.h | 12 ++ src/library/type_context.cpp | 157 +++++++++++------- src/library/type_context.h | 47 ++++-- 7 files changed, 150 insertions(+), 79 deletions(-) diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index c66fc50da4..0779ad4da0 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -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 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); diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 1f054a1394..59acf4e032 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -210,6 +210,7 @@ public: expr mk_pi(buffer const & params, expr const & type) { return m_ctx.mk_pi(params, type); } expr mk_lambda(buffer 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); diff --git a/src/library/arith_instance_manager.cpp b/src/library/arith_instance_manager.cpp index 5c00b62341..3133f78470 100644 --- a/src/library/arith_instance_manager.cpp +++ b/src/library/arith_instance_manager.cpp @@ -480,7 +480,9 @@ optional is_concrete_arith_type(expr const & type) { arith_instance_info_ref cache_insert(expr_struct_map & cache, type_context & tctx, expr const & type) { auto result = cache.emplace(std::piecewise_construct, std::forward_as_tuple(type), - std::forward_as_tuple(tctx.initial_lctx(), type, get_level(tctx, type))); + // TODO(dselsam): the method initial_lctx was removed + std::forward_as_tuple(tctx.lctx(), type, get_level(tctx, type))); +// std::forward_as_tuple(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); diff --git a/src/library/compiler/compiler_step_visitor.cpp b/src/library/compiler/compiler_step_visitor.cpp index aefa05b0de..485709a788 100644 --- a/src/library/compiler/compiler_step_visitor.cpp +++ b/src/library/compiler/compiler_step_visitor.cpp @@ -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() { diff --git a/src/library/local_context.h b/src/library/local_context.h index 6980d1c500..90a67a30ab 100644 --- a/src/library/local_context.h +++ b/src/library/local_context.h @@ -71,7 +71,10 @@ class local_context { unsigned m_next_idx; name_map m_name2local_decl; idx2local_decl m_idx2local_decl; + optional 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 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(get_empty_instance_fingerprint()); + return lctx; + } + + optional 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()); diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index dadc1bd3dd..79c00b7d93 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -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>(); + 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(); + m_cache->m_local_instances = list>(); + 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(fingerprint); + m_cache->m_instance_fingerprint = optional(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 type_context::revert_core(buffer & to_revert, local_context const & ctx, @@ -1618,11 +1696,21 @@ bool type_context::is_def_eq_binding(expr e1, expr e2) { } optional 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 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> 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 get_local_instances(name const & cname) { buffer selected; - for (pair const & p : m_ctx.m_cache->m_local_instances) { + for (pair 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 type_context::mk_class_instance(expr const & type) { - init_local_instances(); if (in_tmp_mode()) { return instance_synthesizer(*this)(type); } else { diff --git a/src/library/type_context.h b/src/library/type_context.h index 6686e8933a..897c512333 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -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 m_instance_fingerprint; list> 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 scopes; - + typedef list> 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 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 constant_is_class(expr const & e); optional 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;