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

fix(library/type_context): remove m_cache_owner field

Browse source 
This idiom creates problem if we use (even accidentally) the copy constructor.
This commit is contained in:
Leonardo de Moura 2016-06-23 14:03:46 -07:00
parent 94905a5511
commit 2b43f591c9
9 changed files with 84 additions and 80 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/frontends/lean/builtin_cmds.cpp
View file

@ -584,10 +584,10 @@ static environment unify_cmd(parser & p) {
e1 = convert_metavars(mctx, e1);
e2 = convert_metavars(mctx, e2);
tout() << e1 << " =?= " << e2 << "\n";
type_context ctx(env, p.get_options(), mctx, lctx, transparency_mode::Semireducible);
bool success = ctx.is_def_eq(e1, e2);
aux_type_context ctx(env, p.get_options(), mctx, lctx, transparency_mode::Semireducible);
bool success = ctx->is_def_eq(e1, e2);
if (success)
tout() << ctx.instantiate_mvars(e1) << " =?= " << ctx.instantiate_mvars(e2) << "\n";
tout() << ctx->instantiate_mvars(e1) << " =?= " << ctx->instantiate_mvars(e2) << "\n";
flycheck_information info(p.ios());
if (info.enabled()) {
p.display_information_pos(p.cmd_pos());
@ -680,7 +680,7 @@ static environment elab_cmd(parser & p) {
expr new_e; level_param_names ls;
std::tie(new_e, ls) = p.elaborate(e);
metavar_context mctx;
type_context ctx(p.env(), p.get_options(), mctx, p.get_local_context());
aux_type_context ctx(p.env(), p.get_options(), mctx, p.get_local_context());
auto out = regular(p.env(), p.ios(), ctx);
out << ">> " << e << "\n";
out << ">> " << new_e << "\n";

4
src/frontends/lean/old_elaborator.cpp
View file

@ -1971,8 +1971,8 @@ void old_elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name
throw_elaborator_exception("tactic failed, result contains meta-variables", r);
}
metavar_decl main_decl = *mctx.get_metavar_decl(new_ts->main());
type_context aux_ctx(env(), opts, mctx, main_decl.get_context());
r = aux_ctx.mk_lambda(new_locals, r);
aux_type_context aux_ctx(env(), opts, mctx, main_decl.get_context());
r = aux_ctx->mk_lambda(new_locals, r);
subst.assign(mvar, r);
}
}

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

@ -11,7 +11,7 @@ Author: Leonardo de Moura
namespace lean {
compiler_step_visitor::compiler_step_visitor(environment const & env):
m_env(env),
m_ctx(m_env, options(), m_mctx, m_lctx, transparency_mode::All) {
m_ctx(env, transparency_mode::All) {
}
compiler_step_visitor::~compiler_step_visitor() {

6
src/library/compiler/compiler_step_visitor.h
View file

@ -13,10 +13,8 @@ namespace lean {
Types are ignored during compilation steps. */
class compiler_step_visitor : public replace_visitor {
protected:
environment m_env;
local_context m_lctx;
metavar_context m_mctx;
type_context m_ctx;
environment m_env;
aux_type_context m_ctx;
expr visit_lambda_let(expr const & e);
protected:

16
src/library/compiler/elim_recursors.cpp
View file

@ -41,7 +41,7 @@ protected:
typedef rb_map<unsigned, local_decl, unsigned_rev_cmp> idx2decls;
void collect_locals(expr const & e, idx2decls & r) {
local_context const & lctx = m_ctx.lctx();
local_context const & lctx = ctx().lctx();
for_each(e, [&](expr const & e, unsigned) {
if (is_local_decl_ref(e)) {
local_decl d = *lctx.get_local_decl(e);
@ -109,7 +109,7 @@ protected:
buffer<expr> abst_locals;
aux = abstract_locals(aux, abst_locals);
/* Create expr (rec_fn) for representing recursive calls. */
expr aux_decl_type = m_ctx.infer(aux);
expr aux_decl_type = ctx().infer(aux);
name aux_decl_name = mk_fresh_name(m_env, m_prefix, "_rec", m_idx);
expr rec_fn = mk_rec_fn_macro(aux_decl_name, aux_decl_type);
/* Create new locals for aux.
@ -132,23 +132,23 @@ protected:
These parameters are fixed in recursive calls. */
rec_fn = mk_app(rec_fn, aux_decl_params);
/* Create locals for indices and major premise */
expr aux_body_type = m_ctx.infer(aux_body);
expr aux_body_type = ctx().infer(aux_body);
buffer<expr> indices;
for (unsigned i = 0; i < nindices; i++) {
aux_body_type = m_ctx.whnf(aux_body_type);
aux_body_type = ctx().whnf(aux_body_type);
lean_assert(is_pi(aux_body_type));
expr index = locals.push_local_from_binding(aux_body_type);
indices.push_back(index);
aux_body_type = instantiate(binding_body(aux_body_type), index);
}
aux_body_type = m_ctx.whnf(aux_body_type);
aux_body_type = ctx().whnf(aux_body_type);
lean_assert(is_pi(aux_body_type));
expr major = locals.push_local_from_binding(aux_body_type);
/* Make sure result is eta-expanded */
buffer<expr> extra_args; /* to make sure result is eta-expanded */
aux_body_type = instantiate(binding_body(aux_body_type), major);
while (true) {
aux_body_type = m_ctx.whnf(aux_body_type);
aux_body_type = ctx().whnf(aux_body_type);
if (!is_pi(aux_body_type))
break;
expr new_arg = locals.push_local_from_binding(aux_body_type);
@ -182,11 +182,11 @@ protected:
minor = instantiate(binding_body(minor), minor_local);
/* Check if minor_local is recursive data */
type_context::tmp_locals aux_locals(m_ctx);
expr minor_local_type = m_ctx.whnf(ctx().infer(minor_local));
expr minor_local_type = ctx().whnf(ctx().infer(minor_local));
// tout() << ">>> minor_local_type: " << minor_local_type << "\n";
while (is_pi(minor_local_type)) {
expr aux_local = aux_locals.push_local_from_binding(minor_local_type);
minor_local_type = m_ctx.whnf(instantiate(binding_body(minor_local_type), aux_local));
minor_local_type = ctx().whnf(instantiate(binding_body(minor_local_type), aux_local));
}
if (is_constant(get_app_fn(minor_local_type), I_name)) {
/* Recursive data, we must update minor_recs */

2
src/library/compiler/lambda_lifting.cpp
View file

@ -43,7 +43,7 @@ class lambda_lifting_fn : public compiler_step_visitor {
typedef rb_map<unsigned, local_decl, unsigned_rev_cmp> idx2decls;
void collect_locals(expr const & e, idx2decls & r) {
local_context const & lctx = m_ctx.lctx();
local_context const & lctx = ctx().lctx();
for_each(e, [&](expr const & e, unsigned) {
if (is_local_decl_ref(e)) {
local_decl d = *lctx.get_local_decl(e);

4
src/library/tactic/tactic_state.cpp
View file

@ -88,7 +88,7 @@ format tactic_state::pp_goal(formatter_factory const & fmtf, expr const & g) con
metavar_decl decl = *mctx().get_metavar_decl(g);
local_context const & lctx = decl.get_context();
metavar_context mctx_tmp = mctx();
type_context ctx(env(), get_options(), mctx_tmp, lctx, transparency_mode::All);
aux_type_context ctx(env(), get_options(), mctx_tmp, lctx, transparency_mode::All);
formatter fmt = fmtf(env(), get_options(), ctx);
format r = lctx.pp(fmt);
unsigned indent = get_pp_indent(get_options());
@ -236,7 +236,7 @@ vm_obj tactic_format_result(vm_obj const & o) {
metavar_context mctx = s.mctx();
expr r = mctx.instantiate_mvars(s.main());
metavar_decl main_decl = *mctx.get_metavar_decl(s.main());
type_context ctx(s.env(), s.get_options(), mctx, main_decl.get_context(), transparency_mode::All);
aux_type_context ctx(s.env(), s.get_options(), mctx, main_decl.get_context(), transparency_mode::All);
formatter_factory const & fmtf = get_global_ios().get_formatter_factory();
formatter fmt = fmtf(s.env(), s.get_options(), ctx);
return mk_tactic_success(to_obj(fmt(r)), s);

82
src/library/type_context.cpp
View file

@ -184,29 +184,21 @@ void type_context::init_core(transparency_mode m) {
m_is_def_eq_depth = 0;
m_tmp_uassignment = nullptr;
m_tmp_eassignment = nullptr;
m_cache->m_init_local_context = m_lctx;
if (!m_cache->m_frozen_mode) {
m_cache.m_init_local_context = m_lctx;
if (!m_cache.m_frozen_mode) {
/* default type class resolution mode */
m_cache->m_local_instances_initialized = false;
m_cache.m_local_instances_initialized = false;
}
m_unfold_pred = nullptr;
}
type_context::type_context(metavar_context & mctx, local_context const & lctx, type_context_cache & cache,
transparency_mode m):
m_mctx(mctx), m_lctx(lctx), m_cache(&cache), m_cache_owner(false) {
init_core(m);
}
type_context::type_context(environment const & env, options const & opts, metavar_context & mctx, local_context const & lctx,
transparency_mode m):
m_mctx(mctx), m_lctx(lctx), m_cache(new type_context_cache(env, opts)), m_cache_owner(true) {
m_mctx(mctx), m_lctx(lctx), m_cache(cache) {
init_core(m);
}
type_context::~type_context() {
if (m_cache_owner)
delete m_cache;
}
expr type_context::push_local(name const & pp_name, expr const & type, binder_info const & bi) {
@ -387,7 +379,7 @@ expr type_context::mk_pi(std::initializer_list<expr> const & locals, expr const
-------------------- */
optional<declaration> type_context::is_transparent(transparency_mode m, name const & n) {
return m_cache->is_transparent(m, n);
return m_cache.is_transparent(m, n);
}
optional<declaration> type_context::is_transparent(name const & n) {
@ -431,7 +423,7 @@ optional<expr> type_context::reduce_projection(expr const & e) {
expr const & f = get_app_fn(e);
if (!is_constant(f))
return none_expr();
projection_info const * info = m_cache->m_proj_info.find(const_name(f));
projection_info const * info = m_cache.m_proj_info.find(const_name(f));
if (!info)
return none_expr();
buffer<expr> args;
@ -471,7 +463,7 @@ bool type_context::should_unfold_macro(expr const & e) {
return
m_transparency_mode == transparency_mode::All ||
m_in_is_def_eq ||
m_cache->should_unfold_macro(e);
m_cache.should_unfold_macro(e);
}
optional<expr> type_context::expand_macro(expr const & e) {
@ -628,7 +620,7 @@ expr type_context::infer_core(expr const & e) {
lean_assert(!is_var(e));
lean_assert(closed(e));
auto & cache = m_cache->m_infer_cache;
auto & cache = m_cache.m_infer_cache;
auto it = cache.find(e);
if (it != cache.end())
return it->second;
@ -2087,17 +2079,17 @@ optional<name> type_context::is_class(expr const & type) {
bool type_context::compatible_local_instances(bool frozen_only) {
unsigned i = 0;
bool failed = false;
m_cache->m_init_local_context.for_each([&](local_decl const & decl) {
m_cache.m_init_local_context.for_each([&](local_decl const & decl) {
if (failed) return;
if (frozen_only && !m_cache->m_init_local_context.is_frozen(decl.get_name()))
if (frozen_only && !m_cache.m_init_local_context.is_frozen(decl.get_name()))
return;
if (auto cname = is_class(decl.get_type())) {
if (i == m_cache->m_local_instances.size()) {
if (i == m_cache.m_local_instances.size()) {
/* initial local context has more local instances than the ones cached at found m_local_instances */
failed = true;
return;
}
if (decl.get_name() != mlocal_name(m_cache->m_local_instances[i].second)) {
if (decl.get_name() != mlocal_name(m_cache.m_local_instances[i].second)) {
/* local instance in initial local constext is not compatible with the one cached at m_local_instances */
failed = true;
return;
@ -2105,35 +2097,35 @@ bool type_context::compatible_local_instances(bool frozen_only) {
i++;
}
});
return i == m_cache->m_local_instances.size();
return i == m_cache.m_local_instances.size();
}
void type_context::set_local_instances() {
m_cache->m_instance_cache.clear();
m_cache->m_subsingleton_cache.clear();
m_cache->m_local_instances.clear();
m_cache->m_init_local_context.for_each([&](local_decl const & decl) {
m_cache.m_instance_cache.clear();
m_cache.m_subsingleton_cache.clear();
m_cache.m_local_instances.clear();
m_cache.m_init_local_context.for_each([&](local_decl const & decl) {
if (auto cls_name = is_class(decl.get_type())) {
m_cache->m_local_instances.emplace_back(*cls_name, decl.mk_ref());
m_cache.m_local_instances.emplace_back(*cls_name, decl.mk_ref());
}
});
}
void type_context::init_local_instances() {
if (m_cache->m_frozen_mode) {
lean_assert(m_cache->m_local_instances_initialized);
if (m_cache.m_frozen_mode) {
lean_assert(m_cache.m_local_instances_initialized);
/* Check if the local instances are really compatible.
See comment at type_context_cache. */
lean_cond_assert("type_context", compatible_local_instances(true));
} else if (!m_cache->m_local_instances_initialized) {
} else if (!m_cache.m_local_instances_initialized) {
/* default type class resolution mode */
bool frozen_only = false;
if (!compatible_local_instances(frozen_only)) {
set_local_instances();
}
m_cache->m_local_instances_initialized = true;
m_cache.m_local_instances_initialized = true;
}
lean_assert(m_cache->m_local_instances_initialized);
lean_assert(m_cache.m_local_instances_initialized);
}
[[ noreturn ]] static void throw_class_exception(char const * msg, expr const & m) { throw_generic_exception(msg, m); }
@ -2196,12 +2188,12 @@ struct instance_synthesizer {
auto out = tout();
if (!m_displayed_trace_header && m_choices.size() == 1) {
out << tclass("class_instances");
if (m_ctx.m_cache->m_pip) {
if (auto fname = m_ctx.m_cache->m_pip->get_file_name()) {
if (m_ctx.m_cache.m_pip) {
if (auto fname = m_ctx.m_cache.m_pip->get_file_name()) {
out << fname << ":";
}
if (m_ctx.m_cache->m_ci_pos)
out << m_ctx.m_cache->m_ci_pos->first << ":" << m_ctx.m_cache->m_ci_pos->second << ":";
if (m_ctx.m_cache.m_ci_pos)
out << m_ctx.m_cache.m_ci_pos->first << ":" << m_ctx.m_cache.m_ci_pos->second << ":";
}
out << " class-instance resolution trace" << endl;
m_displayed_trace_header = true;
@ -2274,7 +2266,7 @@ struct instance_synthesizer {
list<expr> get_local_instances(name const & cname) {
buffer<expr> selected;
for (pair<name, expr> const & p : m_ctx.m_cache->m_local_instances) {
for (pair<name, expr> const & p : m_ctx.m_cache.m_local_instances) {
if (p.first == cname)
selected.push_back(p.second);
}
@ -2283,7 +2275,7 @@ struct instance_synthesizer {
bool mk_choice_point(expr const & mvar) {
lean_assert(is_metavar(mvar));
if (m_choices.size() > m_ctx.m_cache->m_ci_max_depth) {
if (m_choices.size() > m_ctx.m_cache.m_ci_max_depth) {
throw_class_exception("maximum class-instance resolution depth has been reached "
"(the limit can be increased by setting option 'class.instance_max_depth') "
"(the class-instance resolution trace can be visualized "
@ -2306,7 +2298,7 @@ struct instance_synthesizer {
if (!cname)
return false;
r.m_local_instances = get_local_instances(*cname);
if (m_ctx.m_cache->m_ci_trans_instances && toplevel_choice) {
if (m_ctx.m_cache.m_ci_trans_instances && toplevel_choice) {
// we only use transitive instances in the top-level
r.m_trans_instances = get_class_derived_trans_instances(env(), *cname);
}
@ -2418,7 +2410,7 @@ struct instance_synthesizer {
}
void cache_result(expr const & type, optional<expr> const & inst) {
m_ctx.m_cache->m_instance_cache.insert(mk_pair(type, inst));
m_ctx.m_cache.m_instance_cache.insert(mk_pair(type, inst));
}
optional<expr> ensure_no_meta(optional<expr> r) {
@ -2437,8 +2429,8 @@ struct instance_synthesizer {
optional<expr> mk_class_instance_core(expr const & type) {
/* We do not cache results when multiple instances have to be generated. */
auto it = m_ctx.m_cache->m_instance_cache.find(type);
if (it != m_ctx.m_cache->m_instance_cache.end()) {
auto it = m_ctx.m_cache.m_instance_cache.find(type);
if (it != m_ctx.m_cache.m_instance_cache.end()) {
/* instance/failure is already cached */
lean_trace("class_instances",
if (it->second)
@ -2478,12 +2470,12 @@ optional<expr> type_context::mk_class_instance(expr const & type) {
}
optional<expr> type_context::mk_subsingleton_instance(expr const & type) {
auto it = m_cache->m_subsingleton_cache.find(type);
if (it != m_cache->m_subsingleton_cache.end())
auto it = m_cache.m_subsingleton_cache.find(type);
if (it != m_cache.m_subsingleton_cache.end())
return it->second;
expr Type = whnf(infer(type));
if (!is_sort(Type)) {
m_cache->m_subsingleton_cache.insert(mk_pair(type, none_expr()));
m_cache.m_subsingleton_cache.insert(mk_pair(type, none_expr()));
return none_expr();
}
level lvl = sort_level(Type);
@ -2493,7 +2485,7 @@ optional<expr> type_context::mk_subsingleton_instance(expr const & type) {
else
subsingleton = whnf(mk_app(mk_constant(get_is_trunc_is_prop_name(), {lvl}), type));
auto r = mk_class_instance(subsingleton);
m_cache->m_subsingleton_cache.insert(mk_pair(type, r));
m_cache.m_subsingleton_cache.insert(mk_pair(type, r));
return r;
}

40
src/library/type_context.h
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#pragma once
#include <vector>
#include <unordered_map>
#include "util/flet.h"
#include "kernel/environment.h"
#include "kernel/abstract_type_context.h"
#include "kernel/expr_maps.h"
@ -145,8 +146,7 @@ class type_context : public abstract_type_context {
metavar_context & m_mctx;
local_context m_lctx;
cache * m_cache;
bool m_cache_owner;
cache & m_cache;
/* We only cache results when m_used_assignment is false */
bool m_used_assignment;
transparency_mode m_transparency_mode;
@ -179,13 +179,10 @@ class type_context : public abstract_type_context {
public:
type_context(metavar_context & mctx, local_context const & lctx, type_context_cache & cache,
transparency_mode m = transparency_mode::Reducible);
/* Constructor for creating a type_context with a temporary type_context_cache object. */
type_context(environment const & env, options const & opts, metavar_context & mctx, local_context const & lctx,
transparency_mode m = transparency_mode::Reducible);
virtual ~type_context();
virtual environment const & env() const override { return m_cache->m_env; }
options const & get_options() const { return m_cache->m_options; }
virtual environment const & env() const override { return m_cache.m_env; }
options const & get_options() const { return m_cache.m_options; }
local_context const & lctx() const { return m_lctx; }
bool is_def_eq(level const & l1, level const & l2);
@ -243,6 +240,12 @@ public:
transparency_mode mode() const { return m_transparency_mode; }
unsigned mode_idx() const { return static_cast<unsigned>(mode()); }
struct transparency_scope : public flet<transparency_mode> {
transparency_scope(type_context & ctx, transparency_mode m):
flet<transparency_mode>(ctx.m_transparency_mode, m) {
}
};
/* --------------------------
Temporary assignment mode.
It is used when performing type class resolution and matching.
@ -460,21 +463,32 @@ public:
/** Auxiliary object for automating the creation of temporary type_context objects */
class aux_type_context {
metavar_context m_mctx;
type_context m_ctx;
type_context_cache m_cache;
metavar_context m_mctx;
type_context m_ctx;
public:
aux_type_context(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,
transparency_mode m = transparency_mode::Reducible):
m_cache(env, opts),
m_mctx(mctx),
m_ctx(m_mctx, lctx, m_cache, m) {}
aux_type_context(environment const & env, options const & opts, local_context const & lctx,
transparency_mode m = transparency_mode::Reducible):
m_ctx(env, opts, m_mctx, lctx, m) {}
m_cache(env, opts),
m_ctx(m_mctx, lctx, m_cache, m) {}
aux_type_context(environment const & env, options const & opts,
transparency_mode m = transparency_mode::Reducible):
m_ctx(env, opts, m_mctx, local_context(), m) {}
m_cache(env, opts),
m_ctx(m_mctx, local_context(), m_cache, m) {}
aux_type_context(environment const & env, transparency_mode m = transparency_mode::Reducible):
m_ctx(env, options(), m_mctx, local_context(), m) {}
m_cache(env, options()),
m_ctx(m_mctx, local_context(), m_cache, m) {}
type_context & get() { return m_ctx; }
operator type_context&() { return m_ctx; }
operator type_context() { return m_ctx; }
type_context * operator->() { return &m_ctx; }
};