diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp index ef68705483..5088d3e3a0 100644 --- a/src/library/app_builder.cpp +++ b/src/library/app_builder.cpp @@ -12,6 +12,7 @@ Author: Leonardo de Moura #include "library/trace.h" #include "library/match.h" #include "library/constants.h" +#include "library/cache_helper.h" #include "library/app_builder.h" #include "library/tmp_type_context.h" #include "library/relation_manager.h" @@ -120,24 +121,13 @@ public: environment const & env() const { return m_env; } }; -struct app_builder_cache_helper { - typedef std::unique_ptr cache_ptr; - cache_ptr m_cache_ptr[4]; - - void ensure_compatible(type_context const & ctx) { - unsigned midx = ctx.mode_idx(); - if (!m_cache_ptr[midx] || !is_eqp(ctx.env(), m_cache_ptr[midx]->env())) { - m_cache_ptr[midx].reset(new app_builder_cache(ctx.env())); - } - } -}; +typedef cache_compatibility_helper app_builder_cache_helper; MK_THREAD_LOCAL_GET_DEF(app_builder_cache_helper, get_abch); /** Return an app_builder_cache for the transparency_mode in ctx, and compatible with the environment. */ app_builder_cache & get_app_builder_cache_for(type_context const & ctx) { - get_abch().ensure_compatible(ctx); - return *get_abch().m_cache_ptr[ctx.mode_idx()].get(); + return get_abch().get_cache_for(ctx); } /** \brief Helper for creating simple applications where some arguments are inferred using diff --git a/src/library/cache_helper.h b/src/library/cache_helper.h new file mode 100644 index 0000000000..c733178ce0 --- /dev/null +++ b/src/library/cache_helper.h @@ -0,0 +1,34 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include "library/type_context.h" + +namespace lean { +/** \brief Helper class for making sure we have a cache that is compatible + with a given environment and transparency mode. */ +template +class cache_compatibility_helper { + std::unique_ptr m_cache_ptr[4]; +public: + Cache & get_cache_for(environment const & env, transparency_mode m) { + unsigned midx = static_cast(m); + if (!m_cache_ptr[midx] || !is_eqp(env, m_cache_ptr[midx]->env())) { + m_cache_ptr[midx].reset(new Cache(env)); + } + return *m_cache_ptr[midx].get(); + } + + Cache & get_cache_for(type_context const & ctx) { + return get_cache_for(ctx.env(), ctx.mode()); + } + + void clear() { + for (unsigned i = 0; i < 4; i++) m_cache_ptr[i].reset(); + } +}; +} diff --git a/src/library/fun_info.cpp b/src/library/fun_info.cpp index 6828f540cb..f7337a7f22 100644 --- a/src/library/fun_info.cpp +++ b/src/library/fun_info.cpp @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "library/trace.h" #include "library/expr_unsigned_map.h" #include "library/fun_info.h" +#include "library/cache_helper.h" namespace lean { static name * g_fun_info = nullptr; @@ -41,28 +42,19 @@ struct fun_info_cache { narg_cache m_cache_get_spec; prefix_cache m_cache_prefix; fun_info_cache(environment const & env):m_env(env) {} + environment const & env() const { return m_env; } }; -struct fun_info_cache_helper { - typedef std::unique_ptr cache_ptr; - cache_ptr m_cache_ptr; - - void ensure_compatible(environment const & env) { - if (!m_cache_ptr || !is_eqp(env, m_cache_ptr->m_env)) { - m_cache_ptr.reset(new fun_info_cache(env)); - } - } -}; +typedef cache_compatibility_helper fun_info_cache_helper; MK_THREAD_LOCAL_GET_DEF(fun_info_cache_helper, get_fich); -fun_info_cache & get_fun_info_cache_for(environment const & env) { - get_fich().ensure_compatible(env); - return *get_fich().m_cache_ptr.get(); +fun_info_cache & get_fun_info_cache_for(type_context const & ctx) { + return get_fich().get_cache_for(ctx); } void clear_fun_info_cache() { - get_fich().m_cache_ptr.reset(); + get_fich().clear(); } static list collect_deps(expr const & type, buffer const & locals) { @@ -118,7 +110,7 @@ static list get_core(type_context & ctx, } fun_info get_fun_info(type_context & ctx, expr const & e) { - fun_info_cache & cache = get_fun_info_cache_for(ctx.env()); + fun_info_cache & cache = get_fun_info_cache_for(ctx); auto it = cache.m_cache_get.find(e); if (it != cache.m_cache_get.end()) return it->second; @@ -130,7 +122,7 @@ fun_info get_fun_info(type_context & ctx, expr const & e) { } fun_info get_fun_info(type_context & ctx, expr const & e, unsigned nargs) { - fun_info_cache & cache = get_fun_info_cache_for(ctx.env()); + fun_info_cache & cache = get_fun_info_cache_for(ctx); expr_unsigned key(e, nargs); auto it = cache.m_cache_get_nargs.find(key); if (it != cache.m_cache_get_nargs.end()) @@ -230,7 +222,7 @@ unsigned get_specialization_prefix_size(type_context & ctx, expr const & fn, uns This procecure returns the size of group a) */ - fun_info_cache & cache = get_fun_info_cache_for(ctx.env()); + fun_info_cache & cache = get_fun_info_cache_for(ctx); expr_unsigned key(fn, nargs); auto it = cache.m_cache_prefix.find(key); if (it != cache.m_cache_prefix.end()) @@ -263,7 +255,7 @@ fun_info get_specialized_fun_info(type_context & ctx, expr const & a) { expr g = a; for (unsigned i = 0; i < num_rest_args; i++) g = app_fn(g); - fun_info_cache & cache = get_fun_info_cache_for(ctx.env()); + fun_info_cache & cache = get_fun_info_cache_for(ctx); expr_unsigned key(g, num_rest_args); auto it = cache.m_cache_get_spec.find(key); if (it != cache.m_cache_get_spec.end()) {