From d044e9f47e4e8b4e5d3e7662f52334651daf0fff Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 8 Jul 2020 09:39:25 -0700 Subject: [PATCH] chore: remove instance cache If the missing cache generates perf problems in the future, we should add the cache at `MetaM`. cc @Kha --- src/kernel/instantiate.cpp | 69 ++------------------------------------ src/kernel/instantiate.h | 5 --- 2 files changed, 2 insertions(+), 72 deletions(-) diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp index d7f1ded2a9..0e19256f71 100644 --- a/src/kernel/instantiate.cpp +++ b/src/kernel/instantiate.cpp @@ -6,15 +6,10 @@ Author: Leonardo de Moura */ #include #include -#include #include "kernel/replace_fn.h" #include "kernel/declaration.h" #include "kernel/instantiate.h" -#ifndef LEAN_INST_UNIV_CACHE_SIZE -#define LEAN_INST_UNIV_CACHE_SIZE 1023 -#endif - namespace lean { expr instantiate(expr const & a, unsigned s, unsigned n, expr const * subst) { if (s >= get_loose_bvar_range(a) || n == 0) @@ -233,62 +228,12 @@ expr instantiate_lparams(expr const & e, names const & lps, levels const & ls) { }); } -class instantiate_univ_cache { - typedef std::tuple entry; - unsigned m_capacity; - std::vector> m_cache; -public: - instantiate_univ_cache(unsigned capacity):m_capacity(capacity) { - if (m_capacity == 0) - m_capacity++; - } - - optional is_cached(constant_info const & d, levels const & ls) { - if (m_cache.empty()) - return none_expr(); - lean_assert(m_cache.size() == m_capacity); - unsigned idx = d.get_name().hash() % m_capacity; - if (auto it = m_cache[idx]) { - constant_info info_c; levels ls_c; expr r_c; - std::tie(info_c, ls_c, r_c) = *it; - if (!is_eqp(info_c, d)) - return none_expr(); - if (ls == ls_c) - return some_expr(r_c); - else - return none_expr(); - } - return none_expr(); - } - - void save(constant_info const & d, levels const & ls, expr const & r) { - if (m_cache.empty()) - m_cache.resize(m_capacity); - lean_assert(m_cache.size() == m_capacity); - unsigned idx = d.get_name().hash() % m_cache.size(); - m_cache[idx] = entry(d, ls, r); - } - - void clear() { - m_cache.clear(); - lean_assert(m_cache.empty()); - } -}; - -MK_THREAD_LOCAL_GET(instantiate_univ_cache, get_type_univ_cache, LEAN_INST_UNIV_CACHE_SIZE); -MK_THREAD_LOCAL_GET(instantiate_univ_cache, get_value_univ_cache, LEAN_INST_UNIV_CACHE_SIZE); - expr instantiate_type_lparams(constant_info const & info, levels const & ls) { if (info.get_num_lparams() != length(ls)) lean_panic("#universes mismatch at instantiateTypeLevelParams"); if (is_nil(ls) || !has_param_univ(info.get_type())) return info.get_type(); - instantiate_univ_cache & cache = get_type_univ_cache(); - if (auto r = cache.is_cached(info, ls)) - return *r; - expr r = instantiate_lparams(info.get_type(), info.get_lparams(), ls); - cache.save(info, ls, r); - return r; + return instantiate_lparams(info.get_type(), info.get_lparams(), ls); } expr instantiate_value_lparams(constant_info const & info, levels const & ls) { @@ -298,12 +243,7 @@ expr instantiate_value_lparams(constant_info const & info, levels const & ls) { lean_panic("definition/theorem expected at instantiateValueLevelParams"); if (is_nil(ls) || !has_param_univ(info.get_value())) return info.get_value(); - instantiate_univ_cache & cache = get_value_univ_cache(); - if (auto r = cache.is_cached(info, ls)) - return *r; - expr r = instantiate_lparams(info.get_value(), info.get_lparams(), ls); - cache.save(info, ls, r); - return r; + return instantiate_lparams(info.get_value(), info.get_lparams(), ls); } extern "C" object * lean_instantiate_type_lparams(b_obj_arg info, b_obj_arg ls) { @@ -313,9 +253,4 @@ extern "C" object * lean_instantiate_type_lparams(b_obj_arg info, b_obj_arg ls) extern "C" object * lean_instantiate_value_lparams(b_obj_arg info, b_obj_arg ls) { return instantiate_value_lparams(TO_REF(constant_info, info), TO_REF(levels, ls)).steal(); } - -void clear_instantiate_cache() { - get_type_univ_cache().clear(); - get_value_univ_cache().clear(); -} } diff --git a/src/kernel/instantiate.h b/src/kernel/instantiate.h index d00d8347e4..ac07bdde7e 100644 --- a/src/kernel/instantiate.h +++ b/src/kernel/instantiate.h @@ -42,9 +42,4 @@ expr instantiate_type_lparams(constant_info const & info, levels const & ls); /** \brief Instantiate the universe level parameters of the value of the given constant. \pre d.get_num_lparams() == length(ls) */ expr instantiate_value_lparams(constant_info const & info, levels const & ls); - -/** \brief Clear thread local caches used by instantiate_value_lparams and instantiate_type_lparams. - We clear the caches whenever we enable expression caching (aka max sharing). - We do that because the cache may still contain expressions that are not maximally shared. */ -void clear_instantiate_cache(); }