feat(library): add persistent_context_cache
This commit is contained in:
Leonardo de Moura
parent
1aeaed0cae
commit
20db4edf27
3 changed files with 355 additions and 1 deletions
|
|
@ -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)
|
||||
|
|
|
|||
233
src/library/persistent_context_cache.cpp
Normal file
233
src/library/persistent_context_cache.cpp
Normal file
|
|
@ -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, std::unique_ptr<context_cache>> 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<declaration> 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<expr> 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<expr> 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<optional<expr>> 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<expr> const & r) {
|
||||
return m_cache_ptr->set_instance(e, r);
|
||||
}
|
||||
|
||||
optional<optional<expr>> 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<expr> 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<local_instances> persistent_context_cache::get_frozen_local_instances() const {
|
||||
return m_cache_ptr->get_frozen_local_instances();
|
||||
}
|
||||
|
||||
optional<fun_info> 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<fun_info> 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<unsigned> 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<ss_param_infos> 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<ss_param_infos> 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<ss_param_infos> 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<congr_lemma> 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<congr_lemma> 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<congr_lemma> 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<congr_lemma> 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<congr_lemma> 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<app_builder_info> 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<app_builder_info> persistent_context_cache::get_app_builder_info(type_context & ctx, expr const & e, list<bool> 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<bool> const & m, app_builder_info const & r) {
|
||||
return m_cache_ptr->set_app_builder_info(ctx, e, m, r);
|
||||
}
|
||||
}
|
||||
121
src/library/persistent_context_cache.h
Normal file
121
src/library/persistent_context_cache.h
Normal file
|
|
@ -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 <memory>
|
||||
#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<context_cache> 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<declaration> 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<expr> 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<expr> get_whnf(transparency_mode, expr const &) override;
|
||||
virtual void set_whnf(transparency_mode, expr const &, expr const &) override;
|
||||
|
||||
virtual optional<optional<expr>> get_instance(expr const &) override;
|
||||
virtual void set_instance(expr const &, optional<expr> const &) override;
|
||||
|
||||
virtual optional<optional<expr>> get_subsingleton(expr const &) override;
|
||||
virtual void set_subsingleton(expr const &, optional<expr> 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<local_instances> get_frozen_local_instances() const override;
|
||||
|
||||
/* Cache support for fun_info module */
|
||||
|
||||
virtual optional<fun_info> get_fun_info(type_context &, expr const &) override;
|
||||
virtual void set_fun_info(type_context &, expr const &, fun_info const &) override;
|
||||
|
||||
virtual optional<fun_info> 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<unsigned> 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<ss_param_infos> get_subsingleton_info(type_context &, expr const &) override;
|
||||
virtual void set_subsingleton_info(type_context &, expr const &, ss_param_infos const &) override;
|
||||
|
||||
virtual optional<ss_param_infos> 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<ss_param_infos> 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<congr_lemma> 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<congr_lemma> 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<congr_lemma> 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<congr_lemma> 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<congr_lemma> 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<app_builder_info> 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<app_builder_info> get_app_builder_info(type_context &, expr const &, list<bool> const &) override;
|
||||
virtual void set_app_builder_info(type_context &, expr const &, list<bool> const &, app_builder_info const &) override;
|
||||
};
|
||||
}
|
||||
Loading…
Add table
Reference in a new issue