From 20db4edf27eae53c212e8919b33bd5a44268d259 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Feb 2018 16:01:54 -0800 Subject: [PATCH] feat(library): add persistent_context_cache --- src/library/CMakeLists.txt | 2 +- src/library/persistent_context_cache.cpp | 233 +++++++++++++++++++++++ src/library/persistent_context_cache.h | 121 ++++++++++++ 3 files changed, 355 insertions(+), 1 deletion(-) create mode 100644 src/library/persistent_context_cache.cpp create mode 100644 src/library/persistent_context_cache.h diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 65220ce7bd..fe943186f8 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -21,4 +21,4 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp messages.cpp message_builder.cpp module_mgr.cpp comp_val.cpp documentation.cpp check.cpp arith_instance.cpp parray.cpp process.cpp pipe.cpp handle.cpp profiling.cpp time_task.cpp abstract_context_cache.cpp - context_cache.cpp token.cpp) + context_cache.cpp token.cpp persistent_context_cache.cpp) diff --git a/src/library/persistent_context_cache.cpp b/src/library/persistent_context_cache.cpp new file mode 100644 index 0000000000..6536eb42f2 --- /dev/null +++ b/src/library/persistent_context_cache.cpp @@ -0,0 +1,233 @@ +/* +Copyright (c) 2018 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/persistent_context_cache.h" +#include "library/context_cache.h" + +namespace lean { +typedef std::pair> token_context_cache_pair; + +MK_THREAD_LOCAL_GET_DEF(token_context_cache_pair, get_token_context_cache_pair); + +persistent_context_cache::persistent_context_cache(token tk, options const & opts) { + token_context_cache_pair & p = get_token_context_cache_pair(); + if (p.second && p.first == tk && p.second->get_options() == opts) { + /* Reuse thread local cache */ + m_cache_ptr.swap(p.second); + m_token = mk_unique_token(); + } else { + m_cache_ptr.reset(new context_cache(opts)); + m_token = mk_unique_token(); + } +} + +persistent_context_cache::~persistent_context_cache() { + token_context_cache_pair & p = get_token_context_cache_pair(); + p.first = m_token; + m_cache_ptr.swap(p.second); +} + +options const & persistent_context_cache::get_options() const { + return m_cache_ptr->get_options(); +} + +bool persistent_context_cache::get_unfold_lemmas() const { + return m_cache_ptr->get_unfold_lemmas(); +} + +unsigned persistent_context_cache::get_nat_offset_cnstr_threshold() const { + return m_cache_ptr->get_nat_offset_cnstr_threshold(); +} + +unsigned persistent_context_cache::get_smart_unfolding() const { + return m_cache_ptr->get_smart_unfolding(); +} + +unsigned persistent_context_cache::get_class_instance_max_depth() const { + return m_cache_ptr->get_class_instance_max_depth(); +} + +optional persistent_context_cache::get_decl(type_context & ctx, transparency_mode m, name const & n) { + return m_cache_ptr->get_decl(ctx, m, n); +} + +projection_info const * persistent_context_cache::get_proj_info(type_context & ctx, name const & n) { + return m_cache_ptr->get_proj_info(ctx, n); +} + +bool persistent_context_cache::get_aux_recursor(type_context & ctx, name const & n) { + return m_cache_ptr->get_aux_recursor(ctx, n); +} + +optional persistent_context_cache::get_infer(expr const & e) { + return m_cache_ptr->get_infer(e); +} + +void persistent_context_cache::set_infer(expr const & e, expr const & t) { + return m_cache_ptr->set_infer(e, t); +} + +bool persistent_context_cache::get_equiv(transparency_mode m, expr const & e1, expr const & e2) { + return m_cache_ptr->get_equiv(m, e1, e2); +} + +void persistent_context_cache::set_equiv(transparency_mode m, expr const & e1, expr const & e2) { + return m_cache_ptr->set_equiv(m, e1, e2); +} + +bool persistent_context_cache::get_is_def_eq_failure(transparency_mode m, expr const & e1, expr const & e2) { + return m_cache_ptr->get_is_def_eq_failure(m, e1, e2); +} + +void persistent_context_cache::set_is_def_eq_failure(transparency_mode m, expr const & e1, expr const & e2) { + return m_cache_ptr->set_is_def_eq_failure(m, e1, e2); +} + +optional persistent_context_cache::get_whnf(transparency_mode m, expr const & e) { + return m_cache_ptr->get_whnf(m, e); +} + +void persistent_context_cache::set_whnf(transparency_mode m, expr const & e, expr const & r) { + return m_cache_ptr->set_whnf(m, e, r); +} + +optional> persistent_context_cache::get_instance(expr const & e) { + return m_cache_ptr->get_instance(e); +} + +void persistent_context_cache::set_instance(expr const & e, optional const & r) { + return m_cache_ptr->set_instance(e, r); +} + +optional> persistent_context_cache::get_subsingleton(expr const & e) { + return m_cache_ptr->get_subsingleton(e); +} + +void persistent_context_cache::set_subsingleton(expr const & e, optional const & r) { + return m_cache_ptr->set_subsingleton(e, r); +} + +void persistent_context_cache::flush_instances() { + return m_cache_ptr->flush_instances(); +} + +void persistent_context_cache::reset_frozen_local_instances() { + return m_cache_ptr->reset_frozen_local_instances(); +} + +void persistent_context_cache::set_frozen_local_instances(local_instances const & lis) { + return m_cache_ptr->set_frozen_local_instances(lis); +} + +optional persistent_context_cache::get_frozen_local_instances() const { + return m_cache_ptr->get_frozen_local_instances(); +} + +optional persistent_context_cache::get_fun_info(type_context & ctx, expr const & e) { + return m_cache_ptr->get_fun_info(ctx, e); +} + +void persistent_context_cache::set_fun_info(type_context & ctx, expr const & e, fun_info const & r) { + return m_cache_ptr->set_fun_info(ctx, e, r); +} + +optional persistent_context_cache::get_fun_info_nargs(type_context & ctx, expr const & e, unsigned k) { + return m_cache_ptr->get_fun_info_nargs(ctx, e, k); +} + +void persistent_context_cache::set_fun_info_nargs(type_context & ctx, expr const & e, unsigned k, fun_info const & r) { + return m_cache_ptr->set_fun_info_nargs(ctx, e, k, r); +} + +optional persistent_context_cache::get_specialization_prefix_size(type_context & ctx, expr const & e, unsigned k) { + return m_cache_ptr->get_specialization_prefix_size(ctx, e, k); +} + +void persistent_context_cache::set_specialization_prefix_size(type_context & ctx, expr const & e, unsigned k, unsigned r) { + return m_cache_ptr->set_specialization_prefix_size(ctx, e, k, r); +} + +optional persistent_context_cache::get_subsingleton_info(type_context & ctx, expr const & e) { + return m_cache_ptr->get_subsingleton_info(ctx, e); +} + +void persistent_context_cache::set_subsingleton_info(type_context & ctx, expr const & e, ss_param_infos const & r) { + return m_cache_ptr->set_subsingleton_info(ctx, e, r); +} + +optional persistent_context_cache::get_subsingleton_info_nargs(type_context & ctx, expr const & e, unsigned k) { + return m_cache_ptr->get_subsingleton_info_nargs(ctx, e, k); +} + +void persistent_context_cache::set_subsingleton_info_nargs(type_context & ctx, expr const & e, unsigned k, ss_param_infos const & r) { + return m_cache_ptr->set_subsingleton_info_nargs(ctx, e, k, r); +} + +optional persistent_context_cache::get_specialized_subsingleton_info_nargs(type_context & ctx, expr const & e, unsigned k) { + return m_cache_ptr->get_specialized_subsingleton_info_nargs(ctx, e, k); +} + +void persistent_context_cache::set_specialization_subsingleton_info_nargs(type_context & ctx, expr const & e, unsigned k, ss_param_infos const & r) { + return m_cache_ptr->set_specialization_subsingleton_info_nargs(ctx, e, k, r); +} + +optional persistent_context_cache::get_simp_congr_lemma(type_context & ctx, expr const & e, unsigned k) { + return m_cache_ptr->get_simp_congr_lemma(ctx, e, k); +} + +void persistent_context_cache::set_simp_congr_lemma(type_context & ctx, expr const & e, unsigned k, congr_lemma const & r) { + return m_cache_ptr->set_simp_congr_lemma(ctx, e, k, r); +} + +optional persistent_context_cache::get_specialized_simp_congr_lemma(type_context & ctx, expr const & e, unsigned k) { + return m_cache_ptr->get_specialized_simp_congr_lemma(ctx, e, k); +} + +void persistent_context_cache::set_specialized_simp_congr_lemma(type_context & ctx, expr const & e, unsigned k, congr_lemma const & r) { + return m_cache_ptr->set_specialized_simp_congr_lemma(ctx, e, k, r); +} + +optional persistent_context_cache::get_congr_lemma(type_context & ctx, expr const & e, unsigned k) { + return m_cache_ptr->get_congr_lemma(ctx, e, k); +} + +void persistent_context_cache::set_congr_lemma(type_context & ctx, expr const & e, unsigned k, congr_lemma const & r) { + return m_cache_ptr->set_congr_lemma(ctx, e, k, r); +} + +optional persistent_context_cache::get_specialized_congr_lemma(type_context & ctx, expr const & e, unsigned k) { + return m_cache_ptr->get_specialized_congr_lemma(ctx, e, k); +} + +void persistent_context_cache::set_specialized_congr_lemma(type_context & ctx, expr const & e, unsigned k, congr_lemma const & r) { + return m_cache_ptr->set_specialized_congr_lemma(ctx, e, k, r); +} + +optional persistent_context_cache::get_hcongr_lemma(type_context & ctx, expr const & e, unsigned k) { + return m_cache_ptr->get_hcongr_lemma(ctx, e, k); +} + +void persistent_context_cache::set_hcongr_lemma(type_context & ctx, expr const & e, unsigned k, congr_lemma const & r) { + return m_cache_ptr->set_hcongr_lemma(ctx, e, k, r); +} + +optional persistent_context_cache::get_app_builder_info(type_context & ctx, expr const & e, unsigned k) { + return m_cache_ptr->get_app_builder_info(ctx, e, k); +} + +void persistent_context_cache::set_app_builder_info(type_context & ctx, expr const & e, unsigned k, app_builder_info const & r) { + return m_cache_ptr->set_app_builder_info(ctx, e, k, r); +} + + +optional persistent_context_cache::get_app_builder_info(type_context & ctx, expr const & e, list const & m) { + return m_cache_ptr->get_app_builder_info(ctx, e, m); +} + +void persistent_context_cache::set_app_builder_info(type_context & ctx, expr const & e, list const & m, app_builder_info const & r) { + return m_cache_ptr->set_app_builder_info(ctx, e, m, r); +} +} diff --git a/src/library/persistent_context_cache.h b/src/library/persistent_context_cache.h new file mode 100644 index 0000000000..dd887b0c78 --- /dev/null +++ b/src/library/persistent_context_cache.h @@ -0,0 +1,121 @@ +/* +Copyright (c) 2018 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/token.h" +#include "library/abstract_context_cache.h" + +namespace lean { +class context_cache; + +/* + Ideally, we could have a "functional" implementation of abstract_context_cache using rb_map and rb_tree. + This "functional" implementation could be used to store the cache, for example, in tactic_state objects. + We don't use this solution for two reasons: + - rb_map (and rb_tree) are 10x slower than hashtable maps (and sets). + - The functional object would increase the size of the tactic_state object considerably. + + This class provides an alternative implementation where the tactic_state stores only a token. + This token is used to retrieve a thread local context_cache object. + See comment at abstract_context_cache for more details. +*/ +class persistent_context_cache : public abstract_context_cache { + token m_token; + std::unique_ptr m_cache_ptr; +public: + persistent_context_cache(token, options const &); + virtual ~persistent_context_cache(); + + token get_token() const { return m_token; } + + /* Cached configuration options */ + virtual options const & get_options() const override; + virtual bool get_unfold_lemmas() const override; + virtual unsigned get_nat_offset_cnstr_threshold() const override; + virtual unsigned get_smart_unfolding() const override; + virtual unsigned get_class_instance_max_depth() const override; + + /* Operations for accessing environment data more efficiently. + The default implementation provided by this class does not have any optimization. */ + + virtual optional get_decl(type_context &, transparency_mode, name const &) override; + virtual projection_info const * get_proj_info(type_context &, name const &) override; + virtual bool get_aux_recursor(type_context &, name const &) override; + + /* Cache support for type_context module */ + + virtual optional get_infer(expr const &) override; + virtual void set_infer(expr const &, expr const &) override; + + virtual bool get_equiv(transparency_mode, expr const &, expr const &) override; + virtual void set_equiv(transparency_mode, expr const &, expr const &) override; + + virtual bool get_is_def_eq_failure(transparency_mode, expr const &, expr const &) override; + virtual void set_is_def_eq_failure(transparency_mode, expr const &, expr const &) override; + + 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; + + /* this method should flush the instance and subsingleton cache */ + virtual void flush_instances() override; + + virtual void reset_frozen_local_instances() override; + virtual void set_frozen_local_instances(local_instances const & lis) override; + virtual optional get_frozen_local_instances() const override; + + /* Cache support for fun_info module */ + + virtual optional get_fun_info(type_context &, expr const &) override; + virtual void set_fun_info(type_context &, expr const &, fun_info const &) override; + + virtual optional get_fun_info_nargs(type_context &, expr const &, unsigned) override; + virtual void set_fun_info_nargs(type_context &, expr const &, unsigned, fun_info const &) override; + + virtual optional get_specialization_prefix_size(type_context &, expr const &, unsigned) override; + virtual void set_specialization_prefix_size(type_context &, expr const &, unsigned, unsigned) override; + + virtual optional get_subsingleton_info(type_context &, expr const &) override; + virtual void set_subsingleton_info(type_context &, expr const &, ss_param_infos const &) override; + + virtual optional get_subsingleton_info_nargs(type_context &, expr const &, unsigned) override; + virtual void set_subsingleton_info_nargs(type_context &, expr const &, unsigned, ss_param_infos const &) override; + + virtual optional get_specialized_subsingleton_info_nargs(type_context &, expr const &, unsigned) override; + virtual void set_specialization_subsingleton_info_nargs(type_context &, expr const &, unsigned, ss_param_infos const &) override; + + /* Cache support for congr_lemma module */ + + virtual optional get_simp_congr_lemma(type_context &, expr const &, unsigned) override; + virtual void set_simp_congr_lemma(type_context &, expr const &, unsigned, congr_lemma const &) override; + + virtual optional get_specialized_simp_congr_lemma(type_context &, expr const &, unsigned) override; + virtual void set_specialized_simp_congr_lemma(type_context &, expr const &, unsigned, congr_lemma const &) override; + + virtual optional get_congr_lemma(type_context &, expr const &, unsigned) override; + virtual void set_congr_lemma(type_context &, expr const &, unsigned, congr_lemma const &) override; + + virtual optional get_specialized_congr_lemma(type_context &, expr const &, unsigned) override; + virtual void set_specialized_congr_lemma(type_context &, expr const &, unsigned, congr_lemma const &) override; + + virtual optional get_hcongr_lemma(type_context &, expr const &, unsigned) override; + virtual void set_hcongr_lemma(type_context &, expr const &, unsigned, congr_lemma const &) override; + + /* Cache support for app_builder */ + + virtual optional get_app_builder_info(type_context &, expr const &, unsigned) override; + virtual void set_app_builder_info(type_context &, expr const &, unsigned, app_builder_info const &) override; + + virtual optional get_app_builder_info(type_context &, expr const &, list const &) override; + virtual void set_app_builder_info(type_context &, expr const &, list const &, app_builder_info const &) override; +}; +}