From 85465885f365cbe7e40b157f7bb5268e63bf1b53 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 7 Sep 2018 13:17:37 -0700 Subject: [PATCH] chore(library/type_context): remove "frozen local instances" We will re-implement the type class resolution algorithm, and the new implementation will not rely on a persistent cache. We will improve performance by: 1) Using better indexing data-structures. 2) Using a local cache during the search. --- src/frontends/lean/definition_cmds.cpp | 1 - src/library/abstract_context_cache.h | 32 +------ .../compiler/compiler_step_visitor.cpp | 11 +-- src/library/context_cache.cpp | 21 ----- src/library/context_cache.h | 30 ------ src/library/equations_compiler/util.cpp | 1 - src/library/local_context.cpp | 21 ----- src/library/local_context.h | 7 -- src/library/type_context.cpp | 91 +++---------------- src/library/type_context.h | 2 +- 10 files changed, 18 insertions(+), 199 deletions(-) diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index 9f0fd4d58f..1dc7dfecd5 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -533,7 +533,6 @@ environment single_definition_cmd_core(parser & p, decl_cmd_kind kind, cmd_meta elaborator elab(env, p.get_options(), get_namespace(env) + local_pp_name_p(fn), metavar_context(), local_context(), recover_from_errors); buffer new_params; elaborate_params(elab, params, new_params); - elab.freeze_local_instances(); replace_params(params, new_params, fn, val); auto process = [&](expr val) -> environment { diff --git a/src/library/abstract_context_cache.h b/src/library/abstract_context_cache.h index 8df82acefd..6768a9a84c 100644 --- a/src/library/abstract_context_cache.h +++ b/src/library/abstract_context_cache.h @@ -10,7 +10,6 @@ Author: Leonardo de Moura #include "kernel/declaration.h" #include "library/projection.h" #include "library/fun_info.h" -#include "library/local_instances.h" namespace lean { #define LEAN_NUM_TRANSPARENCY_MODES 5 @@ -37,6 +36,11 @@ struct app_builder_info { }; /* + ==== IMPORTANT ==== + THIS FILE WILL BE DELETED + THIS COMMENT DOES NOT REFLECT THE CURRENT DESIGN + =================== + We have two main kinds of cache in Lean: environmental and contextual. The environmental caches only depend on the environment, and are easier to maintain. We usually store them in thread local storage, and before using them we compare @@ -195,19 +199,6 @@ public: virtual optional get_whnf(transparency_mode, expr const &) = 0; virtual void set_whnf(transparency_mode, expr const &, expr const &) = 0; - virtual optional> get_instance(expr const &) = 0; - virtual void set_instance(expr const &, optional const &) = 0; - - virtual optional> get_subsingleton(expr const &) = 0; - virtual void set_subsingleton(expr const &, optional const &) = 0; - - /* this method should flush the instance and subsingleton cache */ - virtual void flush_instances() = 0; - - virtual void reset_frozen_local_instances() = 0; - virtual void set_frozen_local_instances(local_instances const & lis) = 0; - virtual optional get_frozen_local_instances() const = 0; - /* Cache support for fun_info module */ virtual optional get_fun_info(transparency_mode, expr const &) = 0; @@ -247,7 +238,6 @@ private: unsigned m_nat_offset_cnstr_threshold; unsigned m_smart_unfolding; unsigned m_class_instance_max_depth; - optional m_local_instances; public: context_cacheless(); context_cacheless(options const &); @@ -268,10 +258,6 @@ public: virtual unsigned get_smart_unfolding() const override { return m_smart_unfolding; } virtual unsigned get_class_instance_max_depth() const override { return m_class_instance_max_depth; } - virtual void reset_frozen_local_instances() override { m_local_instances = optional(); } - virtual void set_frozen_local_instances(local_instances const & lis) override { m_local_instances = lis; } - virtual optional get_frozen_local_instances() const override { return m_local_instances; } - /* Operations for accessing environment data more efficiently. The default implementation provided by this class does not have any optimization. */ @@ -293,14 +279,6 @@ public: virtual optional get_whnf(transparency_mode, expr const &) override { return none_expr(); } virtual void set_whnf(transparency_mode, expr const &, expr const &) override {} - virtual optional> get_instance(expr const &) override { return optional>(); } - virtual void set_instance(expr const &, optional const &) override {} - - virtual optional> get_subsingleton(expr const &) override { return optional>(); } - virtual void set_subsingleton(expr const &, optional const &) override {} - - virtual void flush_instances() override {} - /* Cache support for fun_info module */ virtual optional get_fun_info(transparency_mode, expr const &) override { return optional(); } diff --git a/src/library/compiler/compiler_step_visitor.cpp b/src/library/compiler/compiler_step_visitor.cpp index a27211ed9f..fd5585517d 100644 --- a/src/library/compiler/compiler_step_visitor.cpp +++ b/src/library/compiler/compiler_step_visitor.cpp @@ -9,18 +9,9 @@ Author: Leonardo de Moura #include "library/compiler/comp_irrelevant.h" namespace lean { -/* - Remark: we don't need typeclass resolution in the compiler. -*/ -static local_context mk_local_context_without_local_instances() { - local_context lctx; - lctx.freeze_local_instances(local_instances()); - return lctx; -} - compiler_step_visitor::compiler_step_visitor(environment const & env, abstract_context_cache & cache): m_env(env), - m_ctx(env, metavar_context(), mk_local_context_without_local_instances(), cache, transparency_mode::All) { + m_ctx(env, metavar_context(), local_context(), cache, transparency_mode::All) { } compiler_step_visitor::~compiler_step_visitor() { diff --git a/src/library/context_cache.cpp b/src/library/context_cache.cpp index c4331a6cd1..351c460e15 100644 --- a/src/library/context_cache.cpp +++ b/src/library/context_cache.cpp @@ -98,27 +98,6 @@ void context_cache::set_whnf(transparency_mode m, expr const & e, expr const & r m_whnf_cache[static_cast(m)].insert(mk_pair(e, r)); } -optional> context_cache::get_instance(expr const & e) { - return find_at>(m_instance_cache, e); -} - -void context_cache::set_instance(expr const & e, optional const & r) { - m_instance_cache.insert(mk_pair(e, r)); -} - -optional> context_cache::get_subsingleton(expr const & e) { - return find_at>(m_subsingleton_cache, e); -} - -void context_cache::set_subsingleton(expr const & e, optional const & r) { - m_subsingleton_cache.insert(mk_pair(e, r)); -} - -void context_cache::flush_instances() { - m_instance_cache.clear(); - m_subsingleton_cache.clear(); -} - optional context_cache::get_fun_info(transparency_mode m, expr const & e) { return find_at(m_fi_cache[static_cast(m)], e); } diff --git a/src/library/context_cache.h b/src/library/context_cache.h index 6da8de22ce..776092eec0 100644 --- a/src/library/context_cache.h +++ b/src/library/context_cache.h @@ -67,28 +67,6 @@ class context_cache : public context_cacheless { whnf_cache m_whnf_cache[LEAN_NUM_TRANSPARENCY_MODES]; name2bool m_aux_recursor_cache; - /* We use the following approach for caching type class instances. - - Whenever a type_context_old 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_old::push_local and type_context_old::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_old::push_local and type_context_old::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. */ - instance_cache m_instance_cache; - subsingleton_cache m_subsingleton_cache; - /* Cache datastructures for fun_info */ typedef expr_map fi_cache; @@ -131,14 +109,6 @@ public: virtual optional get_whnf(transparency_mode, expr const &) override; virtual void set_whnf(transparency_mode, expr const &, expr const &) override; - virtual optional> get_instance(expr const &) override; - virtual void set_instance(expr const &, optional const &) override; - - virtual optional> get_subsingleton(expr const &) override; - virtual void set_subsingleton(expr const &, optional const &) override; - - virtual void flush_instances() override; - /* Cache support for fun_info module */ virtual optional get_fun_info(transparency_mode, expr const &) override; diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp index d20928c6ac..c8fe3ad458 100644 --- a/src/library/equations_compiler/util.cpp +++ b/src/library/equations_compiler/util.cpp @@ -236,7 +236,6 @@ list erase_inaccessible_annotations(list const & es) { local_context erase_inaccessible_annotations(local_context const & lctx) { local_context r; r.m_next_idx = lctx.m_next_idx; - r.m_local_instances = lctx.m_local_instances; lctx.m_idx2local_decl.for_each([&](unsigned, local_decl const & d) { expr new_type = erase_inaccessible_annotations(d.get_type()); optional new_value; diff --git a/src/library/local_context.cpp b/src/library/local_context.cpp index 0c2e03028e..c4b559df09 100644 --- a/src/library/local_context.cpp +++ b/src/library/local_context.cpp @@ -125,17 +125,6 @@ bool depends_on(expr const & e, metavar_context const & mctx, local_context cons return depends_on_fn(mctx, lctx, num, locals)(e); } -void local_context::freeze_local_instances(local_instances const & lis) { - m_local_instances = lis; - lean_assert(std::all_of(lis.begin(), lis.end(), [&](local_instance const & inst) { - return m_name2local_decl.contains(local_name(inst.get_local())); - })); -} - -void local_context::unfreeze_local_instances() { - m_local_instances = optional(); -} - void local_context::insert_user_name(local_decl const & d) { unsigned_set idxs; if (auto existing_idxs = m_user_name2idxs.find(d.get_user_name())) { @@ -272,17 +261,8 @@ local_context local_context::remove(buffer const & locals) const { })); /* TODO(Leo): check whether the following loop is a performance bottleneck. */ local_context r = *this; - r.m_local_instances = m_local_instances; for (expr const & l : locals) { local_decl d = get_local_decl(l); - - /* frozen local instances cannot be deleted */ - if (m_local_instances) { - lean_assert(std::all_of(m_local_instances->begin(), m_local_instances->end(), [&](local_instance const & inst) { - return local_name(inst.get_local()) != d.get_name(); - })); - } - r.m_name2local_decl.erase(local_name(l)); r.m_idx2local_decl.erase(d.get_idx()); r.erase_user_name(d); @@ -407,7 +387,6 @@ name local_context::get_unused_name(name const & suggestion) const { local_context local_context::instantiate_mvars(metavar_context & mctx) const { local_context r; r.m_next_idx = m_next_idx; - r.m_local_instances = m_local_instances; m_idx2local_decl.for_each([&](unsigned, local_decl const & d) { expr new_type = mctx.instantiate_mvars(d.m_ptr->m_type); optional new_value; diff --git a/src/library/local_context.h b/src/library/local_context.h index 8fb13f8049..0f94005c80 100644 --- a/src/library/local_context.h +++ b/src/library/local_context.h @@ -10,7 +10,6 @@ Author: Leonardo de Moura #include "kernel/local_ctx.h" #include "kernel/expr.h" #include "library/formatter.h" -#include "library/local_instances.h" #include "library/subscripted_name_set.h" namespace lean { @@ -41,8 +40,6 @@ class metavar_context; "freezing" local instances. */ class local_context : public local_ctx { typedef rb_tree unsigned_set; - /* frozen local instances */ - optional m_local_instances; /* support for user names */ subscripted_name_set m_user_names; name_map m_user_name2idxs; @@ -61,10 +58,6 @@ class local_context : public local_ctx { public: local_context() {} - void freeze_local_instances(local_instances const & lis); - void unfreeze_local_instances(); - optional get_frozen_local_instances() const { return m_local_instances; } - bool empty() const { return m_idx2local_decl.empty(); } expr mk_local_decl(expr const & type, binder_info bi = mk_binder_info()); diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 7926007c4a..3761db7d76 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -86,10 +86,6 @@ bool type_context_old::is_cached_failure(expr const & t, expr const & s) { } } -void type_context_old::freeze_local_instances() { - m_lctx.freeze_local_instances(m_local_instances); -} - void type_context_old::init_local_instances() { m_local_instances = local_instances(); m_lctx.for_each([&](local_decl const & decl) { @@ -111,32 +107,14 @@ void type_context_old::init_local_instances() { }); } -void type_context_old::flush_instance_cache() { - lean_trace("type_context_cache", tout() << "flushing instance cache\n";); - m_cache->reset_frozen_local_instances(); - m_cache->flush_instances(); -} - void type_context_old::init_core(transparency_mode m) { m_transparency_mode = m; m_smart_unfolding = m_cache->get_smart_unfolding(); - if (auto lis = m_lctx.get_frozen_local_instances()) { - m_local_instances = *lis; - if (m_cache->get_frozen_local_instances() == lis) { - lean_trace("type_context_cache", tout() << "reusing instance cache\n";); - } else { - lean_trace("type_context_cache", tout() << "incompatible local instances, flushing instance cache\n";); - m_cache->flush_instances(); - m_cache->set_frozen_local_instances(m_local_instances); - } - } else { - init_local_instances(); - flush_instance_cache(); - } + init_local_instances(); } type_context_old::type_context_old(environment const & env, options const & o, metavar_context const & mctx, - local_context const & lctx, transparency_mode m): + local_context const & lctx, transparency_mode m): m_env(env), m_mctx(mctx), m_lctx(lctx), m_dummy_cache(o), @@ -184,11 +162,8 @@ void type_context_old::set_env(environment const & env) { } void type_context_old::update_local_instances(expr const & new_local, expr const & new_type) { - if (!m_cache->get_frozen_local_instances()) { - if (auto c_name = is_class(new_type)) { - m_local_instances = local_instances(local_instance(*c_name, new_local), m_local_instances); - flush_instance_cache(); - } + if (auto c_name = is_class(new_type)) { + m_local_instances = local_instances(local_instance(*c_name, new_local), m_local_instances); } } @@ -205,17 +180,15 @@ expr type_context_old::push_let(name const & ppn, expr const & type, expr const } void type_context_old::pop_local() { - if (!m_cache->get_frozen_local_instances() && m_local_instances) { + if (m_local_instances) { optional decl = m_lctx.find_last_local_decl(); if (decl && decl->get_name() == local_name(head(m_local_instances).get_local())) { m_local_instances = tail(m_local_instances); - flush_instance_cache(); } } m_lctx.pop_local_decl(); } - static local_decl get_local_with_smallest_idx(local_context const & lctx, buffer const & ls) { lean_assert(!ls.empty()); lean_assert(std::all_of(ls.begin(), ls.end(), [&](expr const & l) { return (bool)lctx.find_local_decl(l); })); // NOLINT @@ -332,16 +305,6 @@ pair type_context_old::revert_core(buffer & to_revert return ctx.get_local_decl(l1).get_idx() < ctx.get_local_decl(l2).get_idx(); }); } - /* Check whether we are trying to revert a frozen local instance. */ - if (optional lis = m_lctx.get_frozen_local_instances()) { - for (expr const & h : to_revert) { - for (local_instance const & li : *lis) { - if (local_name(h) == local_name(li.get_local())) { - throw exception(sstream() << "failed to revert '" << h << "', it is a frozen local instance (possible solution: use tactic `tactic.unfreeze_local_instances` to reset the set of local instances)"); - } - } - } - } local_context new_ctx = ctx.remove(to_revert); return mk_pair(new_ctx, mk_pi(ctx, to_revert, type)); } @@ -2340,17 +2303,12 @@ bool type_context_old::is_def_eq_binding(expr e1, expr e2) { } optional type_context_old::mk_class_instance_at(local_context const & lctx, expr const & type) { - if (m_cache->get_frozen_local_instances() && - m_cache->get_frozen_local_instances() == lctx.get_frozen_local_instances()) { - return mk_class_instance(type); - } else { - context_cacheless tmp_cache(*m_cache, true); - type_context_old tmp_ctx(env(), m_mctx, lctx, tmp_cache, m_transparency_mode); - auto r = tmp_ctx.mk_class_instance(type); - if (r) - m_mctx = tmp_ctx.mctx(); - return r; - } + context_cacheless tmp_cache(*m_cache, true); + type_context_old tmp_ctx(env(), m_mctx, lctx, tmp_cache, m_transparency_mode); + auto r = tmp_ctx.mk_class_instance(type); + if (r) + m_mctx = tmp_ctx.mctx(); + return r; } /* Temporary hack until we can create type context objects efficiently */ @@ -3700,15 +3658,9 @@ struct instance_synthesizer { return none_expr(); } - void cache_result(expr const & type, optional const & inst) { - if (!has_expr_metavar(type)) - m_ctx.m_cache->set_instance(type, inst); - } - optional ensure_no_meta(optional r) { while (true) { if (!r) { - cache_result(m_ctx.infer(m_main_mvar), r); return none_expr(); } if (!has_expr_metavar(*r)) { @@ -3718,11 +3670,6 @@ struct instance_synthesizer { r = m_ctx.instantiate_mvars(*r); } if (!has_idx_metavar(*r)) { - expr type = m_ctx.infer(m_main_mvar); - if (!has_idx_metavar(type)) { - /* We only cache the result if it does not contain universe tmp metavars. */ - cache_result(type, some_expr(m_ctx.instantiate_mvars(*r))); - } return r; } } @@ -3735,18 +3682,6 @@ struct instance_synthesizer { optional mk_class_instance_core(expr const & type) { /* We do not cache results when multiple instances have to be generated. */ - if (!has_expr_metavar(type)) { - if (auto r = m_ctx.m_cache->get_instance(type)) { - /* instance/failure is already cached */ - lean_trace("class_instances", - scope_trace_env scope(m_ctx.env(), m_ctx); - if (*r) - tout() << "cached instance for " << type << "\n" << *(*r) << "\n"; - else - tout() << "cached failure for " << type << "\n";); - return *r; - } - } m_state = state(); m_main_mvar = m_ctx.mk_tmp_mvar(type); m_state.m_stack = to_list(stack_entry(m_main_mvar, 0)); @@ -3969,17 +3904,13 @@ optional type_context_old::mk_class_instance(expr const & type_0) { } optional type_context_old::mk_subsingleton_instance(expr const & type) { - if (optional> r = m_cache->get_subsingleton(type)) - return *r; expr Type = whnf(infer(type)); if (!is_sort(Type)) { - m_cache->set_subsingleton(type, none_expr()); return none_expr(); } level lvl = sort_level(Type); expr subsingleton = mk_app(mk_constant(get_subsingleton_name(), {lvl}), type); optional r = mk_class_instance(subsingleton); - m_cache->set_subsingleton(type, r); return r; } diff --git a/src/library/type_context.h b/src/library/type_context.h index 5422e882b1..a06416cf79 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -18,6 +18,7 @@ Author: Leonardo de Moura #include "library/abstract_context_cache.h" #include "library/exception.h" #include "library/expr_pair.h" +#include "library/local_instances.h" namespace lean { /* Return `f._sunfold` */ @@ -538,7 +539,6 @@ private: 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); projection_info const * is_projection(expr const & e);