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

chore(library/type_context): remove "frozen local instances"

Browse source 
We will re-implement the type class resolution algorithm, and the new
implementation will not rely on a persistent cache. We will improve
performance by:
1) Using better indexing data-structures.
2) Using a local cache during the search.
This commit is contained in:
Leonardo de Moura 2018-09-07 13:17:37 -07:00
parent 425a1cea8b
commit 85465885f3
10 changed files with 18 additions and 199 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/frontends/lean/definition_cmds.cpp
View file

@ -533,7 +533,6 @@ environment single_definition_cmd_core(parser & p, decl_cmd_kind kind, cmd_meta
elaborator elab(env, p.get_options(), get_namespace(env) + local_pp_name_p(fn), metavar_context(), local_context(), recover_from_errors);
buffer<expr> new_params;
elaborate_params(elab, params, new_params);
elab.freeze_local_instances();
replace_params(params, new_params, fn, val);
auto process = [&](expr val) -> environment {

32
src/library/abstract_context_cache.h
View file

@ -10,7 +10,6 @@ Author: Leonardo de Moura
#include "kernel/declaration.h"
#include "library/projection.h"
#include "library/fun_info.h"
#include "library/local_instances.h"
namespace lean {
#define LEAN_NUM_TRANSPARENCY_MODES 5
@ -37,6 +36,11 @@ struct app_builder_info {
};
/*
==== IMPORTANT ====
THIS FILE WILL BE DELETED
THIS COMMENT DOES NOT REFLECT THE CURRENT DESIGN
===================
We have two main kinds of cache in Lean: environmental and contextual.
The environmental caches only depend on the environment, and are easier to maintain.
We usually store them in thread local storage, and before using them we compare
@ -195,19 +199,6 @@ public:
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(transparency_mode, expr const &) = 0;
@ -247,7 +238,6 @@ private:
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 &);
@ -268,10 +258,6 @@ public:
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. */
@ -293,14 +279,6 @@ public:
virtual optional<expr> get_whnf(transparency_mode, expr const &) override { return none_expr(); }
virtual void set_whnf(transparency_mode, expr const &, expr const &) override {}
virtual optional<optional<expr>> get_instance(expr const &) override { return optional<optional<expr>>(); }
virtual void set_instance(expr const &, optional<expr> const &) override {}
virtual optional<optional<expr>> get_subsingleton(expr const &) override { return optional<optional<expr>>(); }
virtual void set_subsingleton(expr const &, optional<expr> const &) override {}
virtual void flush_instances() override {}
/* Cache support for fun_info module */
virtual optional<fun_info> get_fun_info(transparency_mode, expr const &) override { return optional<fun_info>(); }

11
src/library/compiler/compiler_step_visitor.cpp
View file

@ -9,18 +9,9 @@ Author: Leonardo de Moura
#include "library/compiler/comp_irrelevant.h"
namespace lean {
/*
Remark: we don't need typeclass resolution in the compiler.
*/
static local_context mk_local_context_without_local_instances() {
local_context lctx;
lctx.freeze_local_instances(local_instances());
return lctx;
}
compiler_step_visitor::compiler_step_visitor(environment const & env, abstract_context_cache & cache):
m_env(env),
m_ctx(env, metavar_context(), mk_local_context_without_local_instances(), cache, transparency_mode::All) {
m_ctx(env, metavar_context(), local_context(), cache, transparency_mode::All) {
}
compiler_step_visitor::~compiler_step_visitor() {

21
src/library/context_cache.cpp
View file

@ -98,27 +98,6 @@ void context_cache::set_whnf(transparency_mode m, expr const & e, expr const & r
m_whnf_cache[static_cast<unsigned>(m)].insert(mk_pair(e, r));
}
optional<optional<expr>> context_cache::get_instance(expr const & e) {
return find_at<optional<expr>>(m_instance_cache, e);
}
void context_cache::set_instance(expr const & e, optional<expr> const & r) {
m_instance_cache.insert(mk_pair(e, r));
}
optional<optional<expr>> context_cache::get_subsingleton(expr const & e) {
return find_at<optional<expr>>(m_subsingleton_cache, e);
}
void context_cache::set_subsingleton(expr const & e, optional<expr> const & r) {
m_subsingleton_cache.insert(mk_pair(e, r));
}
void context_cache::flush_instances() {
m_instance_cache.clear();
m_subsingleton_cache.clear();
}
optional<fun_info> context_cache::get_fun_info(transparency_mode m, expr const & e) {
return find_at<fun_info>(m_fi_cache[static_cast<unsigned>(m)], e);
}

30
src/library/context_cache.h
View file

@ -67,28 +67,6 @@ class context_cache : public context_cacheless {
whnf_cache m_whnf_cache[LEAN_NUM_TRANSPARENCY_MODES];
name2bool m_aux_recursor_cache;
/* We use the following approach for caching type class instances.
Whenever a type_context_old object is initialized with a local_context lctx
1) If lctx has an instance_fingerprint, then we compare with the instance_fingerprint
stored in this cache, if they are equal, we keep m_local_instances,
m_instance_cache and m_subsingleton_cache.
New local instances added using methods type_context_old::push_local and type_context_old::push_let will
be ignored.
2) If lctx doesn't have one, we clear m_local_instances, m_instance_cache and m_subsingleton_cache.
We also traverse lctx and collect the local instances.
The methods type_context_old::push_local and type_context_old::push_let will flush the cache
whenever new local instances are pushed into the local context.
m_instance_cache and m_subsingleton_cache are flushed before the cache is returned to the
cache manager. */
instance_cache m_instance_cache;
subsingleton_cache m_subsingleton_cache;
/* Cache datastructures for fun_info */
typedef expr_map<fun_info> fi_cache;
@ -131,14 +109,6 @@ public:
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;
virtual void flush_instances() override;
/* Cache support for fun_info module */
virtual optional<fun_info> get_fun_info(transparency_mode, expr const &) override;

1
src/library/equations_compiler/util.cpp
View file

@ -236,7 +236,6 @@ list<expr> erase_inaccessible_annotations(list<expr> const & es) {
local_context erase_inaccessible_annotations(local_context const & lctx) {
local_context r;
r.m_next_idx = lctx.m_next_idx;
r.m_local_instances = lctx.m_local_instances;
lctx.m_idx2local_decl.for_each([&](unsigned, local_decl const & d) {
expr new_type = erase_inaccessible_annotations(d.get_type());
optional<expr> new_value;

21
src/library/local_context.cpp
View file

@ -125,17 +125,6 @@ bool depends_on(expr const & e, metavar_context const & mctx, local_context cons
return depends_on_fn(mctx, lctx, num, locals)(e);
}
void local_context::freeze_local_instances(local_instances const & lis) {
m_local_instances = lis;
lean_assert(std::all_of(lis.begin(), lis.end(), [&](local_instance const & inst) {
return m_name2local_decl.contains(local_name(inst.get_local()));
}));
}
void local_context::unfreeze_local_instances() {
m_local_instances = optional<local_instances>();
}
void local_context::insert_user_name(local_decl const & d) {
unsigned_set idxs;
if (auto existing_idxs = m_user_name2idxs.find(d.get_user_name())) {
@ -272,17 +261,8 @@ local_context local_context::remove(buffer<expr> const & locals) const {
}));
/* TODO(Leo): check whether the following loop is a performance bottleneck. */
local_context r = *this;
r.m_local_instances = m_local_instances;
for (expr const & l : locals) {
local_decl d = get_local_decl(l);
/* frozen local instances cannot be deleted */
if (m_local_instances) {
lean_assert(std::all_of(m_local_instances->begin(), m_local_instances->end(), [&](local_instance const & inst) {
return local_name(inst.get_local()) != d.get_name();
}));
}
r.m_name2local_decl.erase(local_name(l));
r.m_idx2local_decl.erase(d.get_idx());
r.erase_user_name(d);
@ -407,7 +387,6 @@ name local_context::get_unused_name(name const & suggestion) const {
local_context local_context::instantiate_mvars(metavar_context & mctx) const {
local_context r;
r.m_next_idx = m_next_idx;
r.m_local_instances = m_local_instances;
m_idx2local_decl.for_each([&](unsigned, local_decl const & d) {
expr new_type = mctx.instantiate_mvars(d.m_ptr->m_type);
optional<expr> new_value;

7
src/library/local_context.h
View file

@ -10,7 +10,6 @@ Author: Leonardo de Moura
#include "kernel/local_ctx.h"
#include "kernel/expr.h"
#include "library/formatter.h"
#include "library/local_instances.h"
#include "library/subscripted_name_set.h"
namespace lean {
@ -41,8 +40,6 @@ class metavar_context;
"freezing" local instances. */
class local_context : public local_ctx {
typedef rb_tree<unsigned, unsigned_cmp> unsigned_set;
/* frozen local instances */
optional<local_instances> m_local_instances;
/* support for user names */
subscripted_name_set m_user_names;
name_map<unsigned_set> m_user_name2idxs;
@ -61,10 +58,6 @@ class local_context : public local_ctx {
public:
local_context() {}
void freeze_local_instances(local_instances const & lis);
void unfreeze_local_instances();
optional<local_instances> get_frozen_local_instances() const { return m_local_instances; }
bool empty() const { return m_idx2local_decl.empty(); }
expr mk_local_decl(expr const & type, binder_info bi = mk_binder_info());

91
src/library/type_context.cpp
View file

@ -86,10 +86,6 @@ bool type_context_old::is_cached_failure(expr const & t, expr const & s) {
}
}
void type_context_old::freeze_local_instances() {
m_lctx.freeze_local_instances(m_local_instances);
}
void type_context_old::init_local_instances() {
m_local_instances = local_instances();
m_lctx.for_each([&](local_decl const & decl) {
@ -111,32 +107,14 @@ void type_context_old::init_local_instances() {
});
}
void type_context_old::flush_instance_cache() {
lean_trace("type_context_cache", tout() << "flushing instance cache\n";);
m_cache->reset_frozen_local_instances();
m_cache->flush_instances();
}
void type_context_old::init_core(transparency_mode m) {
m_transparency_mode = m;
m_smart_unfolding = m_cache->get_smart_unfolding();
if (auto lis = m_lctx.get_frozen_local_instances()) {
m_local_instances = *lis;
if (m_cache->get_frozen_local_instances() == lis) {
lean_trace("type_context_cache", tout() << "reusing instance cache\n";);
} else {
lean_trace("type_context_cache", tout() << "incompatible local instances, flushing instance cache\n";);
m_cache->flush_instances();
m_cache->set_frozen_local_instances(m_local_instances);
}
} else {
init_local_instances();
flush_instance_cache();
}
init_local_instances();
}
type_context_old::type_context_old(environment const & env, options const & o, metavar_context const & mctx,
local_context const & lctx, transparency_mode m):
local_context const & lctx, transparency_mode m):
m_env(env),
m_mctx(mctx), m_lctx(lctx),
m_dummy_cache(o),
@ -184,11 +162,8 @@ void type_context_old::set_env(environment const & env) {
}
void type_context_old::update_local_instances(expr const & new_local, expr const & new_type) {
if (!m_cache->get_frozen_local_instances()) {
if (auto c_name = is_class(new_type)) {
m_local_instances = local_instances(local_instance(*c_name, new_local), m_local_instances);
flush_instance_cache();
}
if (auto c_name = is_class(new_type)) {
m_local_instances = local_instances(local_instance(*c_name, new_local), m_local_instances);
}
}
@ -205,17 +180,15 @@ expr type_context_old::push_let(name const & ppn, expr const & type, expr const
}
void type_context_old::pop_local() {
if (!m_cache->get_frozen_local_instances() && m_local_instances) {
if (m_local_instances) {
optional<local_decl> decl = m_lctx.find_last_local_decl();
if (decl && decl->get_name() == local_name(head(m_local_instances).get_local())) {
m_local_instances = tail(m_local_instances);
flush_instance_cache();
}
}
m_lctx.pop_local_decl();
}
static local_decl get_local_with_smallest_idx(local_context const & lctx, buffer<expr> const & ls) {
lean_assert(!ls.empty());
lean_assert(std::all_of(ls.begin(), ls.end(), [&](expr const & l) { return (bool)lctx.find_local_decl(l); })); // NOLINT
@ -332,16 +305,6 @@ pair<local_context, expr> type_context_old::revert_core(buffer<expr> & to_revert
return ctx.get_local_decl(l1).get_idx() < ctx.get_local_decl(l2).get_idx();
});
}
/* Check whether we are trying to revert a frozen local instance. */
if (optional<local_instances> lis = m_lctx.get_frozen_local_instances()) {
for (expr const & h : to_revert) {
for (local_instance const & li : *lis) {
if (local_name(h) == local_name(li.get_local())) {
throw exception(sstream() << "failed to revert '" << h << "', it is a frozen local instance (possible solution: use tactic `tactic.unfreeze_local_instances` to reset the set of local instances)");
}
}
}
}
local_context new_ctx = ctx.remove(to_revert);
return mk_pair(new_ctx, mk_pi(ctx, to_revert, type));
}
@ -2340,17 +2303,12 @@ bool type_context_old::is_def_eq_binding(expr e1, expr e2) {
}
optional<expr> type_context_old::mk_class_instance_at(local_context const & lctx, expr const & type) {
if (m_cache->get_frozen_local_instances() &&
m_cache->get_frozen_local_instances() == lctx.get_frozen_local_instances()) {
return mk_class_instance(type);
} else {
context_cacheless tmp_cache(*m_cache, true);
type_context_old tmp_ctx(env(), m_mctx, lctx, tmp_cache, m_transparency_mode);
auto r = tmp_ctx.mk_class_instance(type);
if (r)
m_mctx = tmp_ctx.mctx();
return r;
}
context_cacheless tmp_cache(*m_cache, true);
type_context_old tmp_ctx(env(), m_mctx, lctx, tmp_cache, m_transparency_mode);
auto r = tmp_ctx.mk_class_instance(type);
if (r)
m_mctx = tmp_ctx.mctx();
return r;
}
/* Temporary hack until we can create type context objects efficiently */
@ -3700,15 +3658,9 @@ struct instance_synthesizer {
return none_expr();
}
void cache_result(expr const & type, optional<expr> const & inst) {
if (!has_expr_metavar(type))
m_ctx.m_cache->set_instance(type, inst);
}
optional<expr> ensure_no_meta(optional<expr> r) {
while (true) {
if (!r) {
cache_result(m_ctx.infer(m_main_mvar), r);
return none_expr();
}
if (!has_expr_metavar(*r)) {
@ -3718,11 +3670,6 @@ struct instance_synthesizer {
r = m_ctx.instantiate_mvars(*r);
}
if (!has_idx_metavar(*r)) {
expr type = m_ctx.infer(m_main_mvar);
if (!has_idx_metavar(type)) {
/* We only cache the result if it does not contain universe tmp metavars. */
cache_result(type, some_expr(m_ctx.instantiate_mvars(*r)));
}
return r;
}
}
@ -3735,18 +3682,6 @@ struct instance_synthesizer {
optional<expr> mk_class_instance_core(expr const & type) {
/* We do not cache results when multiple instances have to be generated. */
if (!has_expr_metavar(type)) {
if (auto r = m_ctx.m_cache->get_instance(type)) {
/* instance/failure is already cached */
lean_trace("class_instances",
scope_trace_env scope(m_ctx.env(), m_ctx);
if (*r)
tout() << "cached instance for " << type << "\n" << *(*r) << "\n";
else
tout() << "cached failure for " << type << "\n";);
return *r;
}
}
m_state = state();
m_main_mvar = m_ctx.mk_tmp_mvar(type);
m_state.m_stack = to_list(stack_entry(m_main_mvar, 0));
@ -3969,17 +3904,13 @@ optional<expr> type_context_old::mk_class_instance(expr const & type_0) {
}
optional<expr> type_context_old::mk_subsingleton_instance(expr const & type) {
if (optional<optional<expr>> r = m_cache->get_subsingleton(type))
return *r;
expr Type = whnf(infer(type));
if (!is_sort(Type)) {
m_cache->set_subsingleton(type, none_expr());
return none_expr();
}
level lvl = sort_level(Type);
expr subsingleton = mk_app(mk_constant(get_subsingleton_name(), {lvl}), type);
optional<expr> r = mk_class_instance(subsingleton);
m_cache->set_subsingleton(type, r);
return r;
}

2
src/library/type_context.h
View file

@ -18,6 +18,7 @@ Author: Leonardo de Moura
#include "library/abstract_context_cache.h"
#include "library/exception.h"
#include "library/expr_pair.h"
#include "library/local_instances.h"
namespace lean {
/* Return `f._sunfold` */
@ -538,7 +539,6 @@ private:
bool is_cached_failure(expr const & t, expr const & s);
void init_local_instances();
void flush_instance_cache();
void update_local_instances(expr const & new_local, expr const & new_type);
projection_info const * is_projection(expr const & e);