max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/abstract_context_cache): make it fully abstract

Browse source
This commit is contained in:
Leonardo de Moura 2018-02-13 15:09:40 -08:00
parent 70b6e5c958
commit 1aeaed0cae
6 changed files with 142 additions and 47 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/library/abstract_context_cache.cpp
View file

@ -49,14 +49,14 @@ bool get_smart_unfolding(options const & o) {
return o.get_bool(*g_smart_unfolding, LEAN_DEFAULT_SMART_UNFOLDING);
}
abstract_context_cache::abstract_context_cache():
context_cacheless::context_cacheless():
m_unfold_lemmas(LEAN_DEFAULT_UNFOLD_LEMMAS),
m_nat_offset_cnstr_threshold(LEAN_DEFAULT_NAT_OFFSET_CNSTR_THRESHOLD),
m_smart_unfolding(LEAN_DEFAULT_SMART_UNFOLDING),
m_class_instance_max_depth(LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH) {
}
abstract_context_cache::abstract_context_cache(options const & o):
context_cacheless::context_cacheless(options const & o):
m_options(o),
m_unfold_lemmas(::lean::get_unfold_lemmas(o)),
m_nat_offset_cnstr_threshold(::lean::get_nat_offset_cnstr_threshold(o)),
@ -64,15 +64,15 @@ abstract_context_cache::abstract_context_cache(options const & o):
m_class_instance_max_depth(::lean::get_class_instance_max_depth(o)) {
}
abstract_context_cache::abstract_context_cache(abstract_context_cache const & c, bool):
m_options(c.m_options),
m_unfold_lemmas(c.m_unfold_lemmas),
m_nat_offset_cnstr_threshold(c.m_nat_offset_cnstr_threshold),
m_smart_unfolding(c.m_smart_unfolding),
m_class_instance_max_depth(c.m_class_instance_max_depth) {
context_cacheless::context_cacheless(abstract_context_cache const & c, bool):
m_options(c.get_options()),
m_unfold_lemmas(c.get_unfold_lemmas()),
m_nat_offset_cnstr_threshold(c.get_nat_offset_cnstr_threshold()),
m_smart_unfolding(c.get_smart_unfolding()),
m_class_instance_max_depth(c.get_class_instance_max_depth()) {
}
bool abstract_context_cache::is_transparent(type_context & ctx, transparency_mode m, declaration const & d) {
bool context_cacheless::is_transparent(type_context & ctx, transparency_mode m, declaration const & d) {
if (m == transparency_mode::None)
return false;
name const & n = d.get_name();
@ -92,7 +92,7 @@ bool abstract_context_cache::is_transparent(type_context & ctx, transparency_mod
return false;
}
optional<declaration> abstract_context_cache::get_decl(type_context & ctx, transparency_mode m, name const & n) {
optional<declaration> context_cacheless::get_decl(type_context & ctx, transparency_mode m, name const & n) {
if (auto d = ctx.env().find(n)) {
if (d->is_definition() && is_transparent(ctx, m, *d)) {
return d;
@ -101,11 +101,11 @@ optional<declaration> abstract_context_cache::get_decl(type_context & ctx, trans
return optional<declaration>();
}
projection_info const * abstract_context_cache::get_proj_info(type_context & ctx, name const & n) {
projection_info const * context_cacheless::get_proj_info(type_context & ctx, name const & n) {
return get_projection_info(ctx.env(), n);
}
bool abstract_context_cache::get_aux_recursor(type_context & ctx, name const & n) {
bool context_cacheless::get_aux_recursor(type_context & ctx, name const & n) {
return ::lean::is_aux_recursor(ctx.env(), n);
}

148
src/library/abstract_context_cache.h
View file

@ -60,9 +60,6 @@ struct app_builder_info {
In the type_context, we cache inferred types, whnf, type class instances,
to cite a few.
This class do not implement any cache, only its interface. All operations
do nothing.
This class has been added to address problems with the former `type_context_cache_manager`.
The `type_context_cache_manager` objects were stored in thread local objects.
The correctness of this cache relied on the fact we used to never reuse fresh names in the whole system.
@ -162,21 +159,8 @@ struct app_builder_info {
* A tactic that reverses local instances
*/
class abstract_context_cache {
protected:
options m_options;
bool m_unfold_lemmas;
unsigned m_nat_offset_cnstr_threshold;
unsigned m_smart_unfolding;
unsigned m_class_instance_max_depth;
optional<local_instances> m_local_instances;
bool is_transparent(type_context & ctx, transparency_mode m, declaration const & d);
public:
abstract_context_cache();
abstract_context_cache(options const &);
/* Create a "dummy" context_cache with the same configuration options.
The bool parameter is not used. It is here just to make sure we don't confuse
this constructor with the copy constructor. */
abstract_context_cache(abstract_context_cache const &, bool);
abstract_context_cache() {}
abstract_context_cache(abstract_context_cache const &) = delete;
abstract_context_cache(abstract_context_cache &&) = default;
virtual ~abstract_context_cache() {}
@ -185,11 +169,126 @@ public:
abstract_context_cache & operator=(abstract_context_cache &&) = default;
/* Cached configuration options */
options const & get_options() const { return m_options; }
bool get_unfold_lemmas() const { return m_unfold_lemmas; }
unsigned get_nat_offset_cnstr_threshold() const { return m_nat_offset_cnstr_threshold; }
unsigned get_smart_unfolding() const { return m_smart_unfolding; }
unsigned get_class_instance_max_depth() const { return m_class_instance_max_depth; }
virtual options const & get_options() const = 0;
virtual bool get_unfold_lemmas() const = 0;
virtual unsigned get_nat_offset_cnstr_threshold() const = 0;
virtual unsigned get_smart_unfolding() const = 0;
virtual unsigned get_class_instance_max_depth() const = 0;
/* 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 &) = 0;
virtual projection_info const * get_proj_info(type_context &, name const &) = 0;
virtual bool get_aux_recursor(type_context &, name const &) = 0;
/* Cache support for type_context module */
virtual optional<expr> get_infer(expr const &) = 0;
virtual void set_infer(expr const &, expr const &) = 0;
virtual bool get_equiv(transparency_mode, expr const &, expr const &) = 0;
virtual void set_equiv(transparency_mode, expr const &, expr const &) = 0;
virtual bool get_is_def_eq_failure(transparency_mode, expr const &, expr const &) = 0;
virtual void set_is_def_eq_failure(transparency_mode, expr const &, expr const &) = 0;
virtual optional<expr> get_whnf(transparency_mode, expr const &) = 0;
virtual void set_whnf(transparency_mode, expr const &, expr const &) = 0;
virtual optional<optional<expr>> get_instance(expr const &) = 0;
virtual void set_instance(expr const &, optional<expr> const &) = 0;
virtual optional<optional<expr>> get_subsingleton(expr const &) = 0;
virtual void set_subsingleton(expr const &, optional<expr> 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<local_instances> get_frozen_local_instances() const = 0;
/* Cache support for fun_info module */
virtual optional<fun_info> get_fun_info(type_context &, expr const &) = 0;
virtual void set_fun_info(type_context &, expr const &, fun_info const &) = 0;
virtual optional<fun_info> get_fun_info_nargs(type_context &, expr const &, unsigned) = 0;
virtual void set_fun_info_nargs(type_context &, expr const &, unsigned, fun_info const &) = 0;
virtual optional<unsigned> get_specialization_prefix_size(type_context &, expr const &, unsigned) = 0;
virtual void set_specialization_prefix_size(type_context &, expr const &, unsigned, unsigned) = 0;
virtual optional<ss_param_infos> get_subsingleton_info(type_context &, expr const &) = 0;
virtual void set_subsingleton_info(type_context &, expr const &, ss_param_infos const &) = 0;
virtual optional<ss_param_infos> get_subsingleton_info_nargs(type_context &, expr const &, unsigned) = 0;
virtual void set_subsingleton_info_nargs(type_context &, expr const &, unsigned, ss_param_infos const &) = 0;
virtual optional<ss_param_infos> get_specialized_subsingleton_info_nargs(type_context &, expr const &, unsigned) = 0;
virtual void set_specialization_subsingleton_info_nargs(type_context &, expr const &, unsigned, ss_param_infos const &) = 0;
/* Cache support for congr_lemma module */
virtual optional<congr_lemma> get_simp_congr_lemma(type_context &, expr const &, unsigned) = 0;
virtual void set_simp_congr_lemma(type_context &, expr const &, unsigned, congr_lemma const &) = 0;
virtual optional<congr_lemma> get_specialized_simp_congr_lemma(type_context &, expr const &, unsigned) = 0;
virtual void set_specialized_simp_congr_lemma(type_context &, expr const &, unsigned, congr_lemma const &) = 0;
virtual optional<congr_lemma> get_congr_lemma(type_context &, expr const &, unsigned) = 0;
virtual void set_congr_lemma(type_context &, expr const &, unsigned, congr_lemma const &) = 0;
virtual optional<congr_lemma> get_specialized_congr_lemma(type_context &, expr const &, unsigned) = 0;
virtual void set_specialized_congr_lemma(type_context &, expr const &, unsigned, congr_lemma const &) = 0;
virtual optional<congr_lemma> get_hcongr_lemma(type_context &, expr const &, unsigned) = 0;
virtual void set_hcongr_lemma(type_context &, expr const &, unsigned, congr_lemma const &) = 0;
/* Cache support for app_builder */
virtual optional<app_builder_info> get_app_builder_info(type_context &, expr const &, unsigned) = 0;
virtual void set_app_builder_info(type_context &, expr const &, unsigned, app_builder_info const &) = 0;
virtual optional<app_builder_info> get_app_builder_info(type_context &, expr const &, list<bool> const &) = 0;
virtual void set_app_builder_info(type_context &, expr const &, list<bool> const &, app_builder_info const &) = 0;
};
/* Dummy implementation of the abstract_context_cache interface that does not do cache anything but configuration options. */
class context_cacheless : public abstract_context_cache {
protected:
bool is_transparent(type_context & ctx, transparency_mode m, declaration const & d);
private:
options m_options;
bool m_unfold_lemmas;
unsigned m_nat_offset_cnstr_threshold;
unsigned m_smart_unfolding;
unsigned m_class_instance_max_depth;
optional<local_instances> m_local_instances;
public:
context_cacheless();
context_cacheless(options const &);
/* Faster version of `context_cacheless(c.get_options())`.
The bool parameter is not used. It is here just to make sure we don't confuse
this constructor with the copy constructor. */
context_cacheless(abstract_context_cache const &, bool);
context_cacheless(context_cacheless const &) = delete;
context_cacheless(context_cacheless &&) = default;
virtual ~context_cacheless() {}
context_cacheless & operator=(context_cacheless const &) = delete;
context_cacheless & operator=(context_cacheless &&) = default;
virtual options const & get_options() const override { return m_options; }
virtual bool get_unfold_lemmas() const override { return m_unfold_lemmas; }
virtual unsigned get_nat_offset_cnstr_threshold() const override { return m_nat_offset_cnstr_threshold; }
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<local_instances>(); }
virtual void set_frozen_local_instances(local_instances const & lis) override { m_local_instances = lis; }
virtual optional<local_instances> 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. */
@ -218,13 +317,8 @@ public:
virtual optional<optional<expr>> get_subsingleton(expr const &) { return optional<optional<expr>>(); }
virtual void set_subsingleton(expr const &, optional<expr> const &) {}
/* this method should flush the instance and subsingleton cache */
virtual void flush_instances() {}
void reset_frozen_local_instances() { m_local_instances = optional<local_instances>(); }
void set_frozen_local_instances(local_instances const & lis) { m_local_instances = lis; }
optional<local_instances> get_frozen_local_instances() const { return m_local_instances; }
/* Cache support for fun_info module */
virtual optional<fun_info> get_fun_info(type_context &, expr const &) { return optional<fun_info>(); }

10
src/library/context_cache.cpp
View file

@ -8,11 +8,11 @@ Author: Leonardo de Moura
namespace lean {
context_cache::context_cache():
abstract_context_cache() {
context_cacheless() {
}
context_cache::context_cache(options const & o):
abstract_context_cache(o) {
context_cacheless(o) {
}
context_cache::~context_cache() {
@ -24,21 +24,21 @@ optional<declaration> context_cache::get_decl(type_context & ctx, transparency_m
if (it != cache.end()) {
return it->second;
}
optional<declaration> r = abstract_context_cache::get_decl(ctx, m, n);
optional<declaration> r = context_cacheless::get_decl(ctx, m, n);
cache.insert(mk_pair(n, r));
return r;
}
projection_info const * context_cache::get_proj_info(type_context & ctx, name const & n) {
// TODO(Leo): check if we really need a cache for get_proj_info
return abstract_context_cache::get_proj_info(ctx, n);
return context_cacheless::get_proj_info(ctx, n);
}
bool context_cache::get_aux_recursor(type_context & ctx, name const & n) {
auto it = m_aux_recursor_cache.find(n);
if (it != m_aux_recursor_cache.end())
return it->second;
bool r = abstract_context_cache::get_aux_recursor(ctx, n);
bool r = context_cacheless::get_aux_recursor(ctx, n);
m_aux_recursor_cache.insert(mk_pair(n, r));
return r;
}

2
src/library/context_cache.h
View file

@ -13,7 +13,7 @@ Author: Leonardo de Moura
#include "library/abstract_context_cache.h"
namespace lean {
class context_cache : public abstract_context_cache {
class context_cache : public context_cacheless {
typedef std::unordered_map<name, optional<declaration>, name_hash> transparency_cache;
typedef std::unordered_map<name, bool, name_hash> name2bool;

2
src/library/type_context.cpp
View file

@ -2295,7 +2295,7 @@ optional<expr> type_context::mk_class_instance_at(local_context const & lctx, ex
m_cache->get_frozen_local_instances() == lctx.get_frozen_local_instances()) {
return mk_class_instance(type);
} else {
abstract_context_cache tmp_cache(*m_cache, true);
context_cacheless tmp_cache(*m_cache, true);
type_context tmp_ctx(env(), m_mctx, lctx, tmp_cache, m_transparency_mode);
auto r = tmp_ctx.mk_class_instance(type);
if (r)

3
src/library/type_context.h
View file

@ -387,10 +387,11 @@ public:
private:
typedef buffer<scope_data> scopes;
typedef abstract_context_cache cache;
typedef context_cacheless dummy_cache;
environment m_env;
metavar_context m_mctx;
local_context m_lctx;
cache m_dummy_cache; /* cache used when user does not provide a cache */
dummy_cache m_dummy_cache; /* cache used when user does not provide a cache */
cache * m_cache;
local_instances m_local_instances;
/* We only cache results when m_used_assignment is false */