michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/type_context): with the new tracing infrastructure, type_context doesn't need an io_state

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-08 14:58:08 -08:00
parent 58ab526d44
commit 7da64a768f
24 changed files with 95 additions and 89 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -541,7 +541,7 @@ static void print_simp_rules(parser & p) {
if (p.curr_is_identifier()) {
ns = p.get_name_val();
p.next();
s = get_simp_rule_sets(p.env(), p.ios(), ns);
s = get_simp_rule_sets(p.env(), p.get_options(), ns);
} else {
s = get_simp_rule_sets(p.env());
}
@ -1394,7 +1394,7 @@ static environment replace_cmd(parser & p) {
parse_expr_vector(p, to);
if (from.size() != to.size())
throw parser_error("invalid #replace command, from/to vectors have different size", pos);
tmp_type_context ctx(env, p.ios());
tmp_type_context ctx(env, p.get_options());
fun_info_manager infom(ctx);
auto r = replace(infom, e, from, to);
if (!r)
@ -1410,7 +1410,7 @@ static environment congr_cmd_core(parser & p, congr_kind kind) {
auto pos = p.pos();
expr e; level_param_names ls;
std::tie(e, ls) = parse_local_expr(p);
tmp_type_context ctx(env, p.ios());
tmp_type_context ctx(env, p.get_options());
app_builder b(ctx);
fun_info_manager infom(ctx);
congr_lemma_manager cm(b, infom);
@ -1468,7 +1468,7 @@ static environment simplify_cmd(parser & p) {
} else if (ns == name("env")) {
srss = get_simp_rule_sets(p.env());
} else {
srss = get_simp_rule_sets(p.env(), p.ios(), ns);
srss = get_simp_rule_sets(p.env(), p.get_options(), ns);
}
blast::simp::result r = blast::simplify(rel, e, srss);
@ -1506,8 +1506,8 @@ static environment normalizer_cmd(parser & p) {
static environment abstract_expr_cmd(parser & p) {
unsigned o = p.parse_small_nat();
default_type_context ctx(p.env(), p.ios());
app_builder builder(p.env(), p.ios());
default_type_context ctx(p.env(), p.get_options());
app_builder builder(p.env(), p.get_options());
fun_info_manager fun_info(ctx);
congr_lemma_manager congr_lemma(builder, fun_info);
abstract_expr_manager ae_manager(congr_lemma);

10
src/library/app_builder.cpp
View file

@ -98,8 +98,8 @@ struct app_builder::imp {
m_trans_getter(mk_trans_info_getter(m_ctx->env())) {
}
imp(environment const & env, io_state const & ios, reducible_behavior b):
imp(*new tmp_type_context(env, ios, b), true) {
imp(environment const & env, options const & o, reducible_behavior b):
imp(*new tmp_type_context(env, o, b), true) {
}
imp(tmp_type_context & ctx):
@ -676,12 +676,12 @@ struct app_builder::imp {
}
};
app_builder::app_builder(environment const & env, io_state const & ios, reducible_behavior b):
m_ptr(new imp(env, ios, b)) {
app_builder::app_builder(environment const & env, options const & o, reducible_behavior b):
m_ptr(new imp(env, o, b)) {
}
app_builder::app_builder(environment const & env, reducible_behavior b):
app_builder(env, get_dummy_ios(), b) {
app_builder(env, options(), b) {
}
app_builder::app_builder(tmp_type_context & ctx):

2
src/library/app_builder.h
View file

@ -36,7 +36,7 @@ class app_builder {
struct imp;
std::unique_ptr<imp> m_ptr;
public:
app_builder(environment const & env, io_state const & ios, reducible_behavior b = UnfoldReducible);
app_builder(environment const & env, options const & o, reducible_behavior b = UnfoldReducible);
app_builder(environment const & env, reducible_behavior b = UnfoldReducible);
app_builder(tmp_type_context & ctx);
~app_builder();

10
src/library/blast/backward/backward_rule_set.cpp
View file

@ -23,8 +23,8 @@ static std::string * g_key = nullptr;
struct brs_state {
backward_rule_set m_backward_rule_set;
name_set m_names;
void add(environment const & env, io_state const & ios, name const & cname, unsigned prio) {
default_type_context tctx(env, ios);
void add(environment const & env, options const & o, name const & cname, unsigned prio) {
default_type_context tctx(env, o);
m_backward_rule_set.insert(tctx, cname, prio);
m_names.insert(cname);
}
@ -41,7 +41,7 @@ struct brs_config {
typedef brs_entry entry;
typedef brs_state state;
static void add_entry(environment const & env, io_state const & ios, state & s, entry const & e) {
s.add(env, ios, e.m_name, e.m_priority);
s.add(env, ios.get_options(), e.m_name, e.m_priority);
}
static name const & get_class_name() {
return *g_class_name;
@ -75,12 +75,12 @@ backward_rule_set get_backward_rule_set(environment const & env) {
return brs_ext::get_state(env).m_backward_rule_set;
}
backward_rule_set get_backward_rule_sets(environment const & env, io_state const & ios, name const & ns) {
backward_rule_set get_backward_rule_sets(environment const & env, options const & o, name const & ns) {
backward_rule_set brs;
list<brs_entry> const * entries = brs_ext::get_entries(env, ns);
if (entries) {
for (auto const & e : *entries) {
default_type_context tctx(env, ios);
default_type_context tctx(env, o);
brs.insert(tctx, e.m_name, e.m_priority);
}
}

2
src/library/blast/backward/backward_rule_set.h
View file

@ -61,7 +61,7 @@ bool is_backward_rule(environment const & env, name const & n);
/** \brief Get current backward rule set */
blast::backward_rule_set get_backward_rule_set(environment const & env);
/** \brief Get backward rule set in the given namespace. */
blast::backward_rule_set get_backward_rule_sets(environment const & env, io_state const & ios, name const & ns);
blast::backward_rule_set get_backward_rule_sets(environment const & env, options const & o, name const & ns);
io_state_stream const & operator<<(io_state_stream const & out, blast::backward_rule_set const & r);

8
src/library/blast/blast.cpp
View file

@ -122,7 +122,7 @@ class blastenv {
std::vector<state::assignment_snapshot> m_stack;
public:
tctx(blastenv & benv):
type_context(benv.m_env, benv.m_ios, benv.m_tmp_local_generator),
type_context(benv.m_env, benv.m_ios.get_options(), benv.m_tmp_local_generator),
m_benv(benv) {}
virtual bool is_extra_opaque(name const & n) const override {
@ -1067,8 +1067,8 @@ scope_debug::~scope_debug() {}
and blast meta-variables are stored in the blast state */
class tmp_tctx : public tmp_type_context {
public:
tmp_tctx(environment const & env, io_state const & ios, tmp_local_generator & gen):
tmp_type_context(env, ios, gen) {}
tmp_tctx(environment const & env, options const & o, tmp_local_generator & gen):
tmp_type_context(env, o, gen) {}
/** \brief Return the type of a local constant (local or not).
\remark This method allows the customer to store the type of local constants
@ -1101,7 +1101,7 @@ public:
tmp_type_context * blastenv::mk_tmp_type_context() {
tmp_type_context * r;
if (m_tmp_ctx_pool.empty()) {
r = new tmp_tctx(m_env, m_ios, m_tmp_local_generator);
r = new tmp_tctx(m_env, m_ios.get_options(), m_tmp_local_generator);
// Design decision: in the blast tactic, we only consider the instances that were
// available in initial goal provided to the blast tactic.
// So, we only need to setup the local instances when we create a new (temporary) type context.

2
src/library/blast/grinder/intro_elim_lemmas.cpp
View file

@ -88,7 +88,7 @@ optional<name> get_intro_target(tmp_type_context & ctx, name const & c) {
}
environment add_intro_lemma(environment const & env, io_state const & ios, name const & c, unsigned prio, name const & ns, bool persistent) {
tmp_type_context ctx(env, ios);
tmp_type_context ctx(env, ios.get_options());
if (!get_intro_target(ctx, c))
throw exception(sstream() << "invalid [intro] attribute for '" << c << "', head symbol of resulting type must be a constant");
return intro_elim_ext::add_entry(env, ios, intro_elim_entry(false, prio, c), ns, persistent);

12
src/library/blast/simplifier/simp_rule_set.cpp
View file

@ -475,13 +475,13 @@ struct rrs_state {
name_set m_congr_names;
void add_simp(environment const & env, io_state const & ios, name const & cname, unsigned prio) {
tmp_type_context tctx{env, ios};
tmp_type_context tctx(env, ios.get_options());
m_sets = add_core(tctx, m_sets, cname, prio);
m_simp_names.insert(cname);
}
void add_congr(environment const & env, io_state const & ios, name const & n, unsigned prio) {
tmp_type_context tctx{env, ios};
tmp_type_context tctx(env, ios.get_options());
add_congr_core(tctx, m_sets, n, prio);
m_congr_names.insert(n);
}
@ -544,25 +544,25 @@ simp_rule_sets get_simp_rule_sets(environment const & env) {
return rrs_ext::get_state(env).m_sets;
}
simp_rule_sets get_simp_rule_sets(environment const & env, io_state const & ios, name const & ns) {
simp_rule_sets get_simp_rule_sets(environment const & env, options const & o, name const & ns) {
simp_rule_sets set;
list<rrs_entry> const * entries = rrs_ext::get_entries(env, ns);
if (entries) {
for (auto const & e : *entries) {
tmp_type_context tctx(env, ios);
tmp_type_context tctx(env, o);
set = add_core(tctx, set, e.m_name, e.m_priority);
}
}
return set;
}
simp_rule_sets get_simp_rule_sets(environment const & env, io_state const & ios, std::initializer_list<name> const & nss) {
simp_rule_sets get_simp_rule_sets(environment const & env, options const & o, std::initializer_list<name> const & nss) {
simp_rule_sets set;
for (name const & ns : nss) {
list<rrs_entry> const * entries = rrs_ext::get_entries(env, ns);
if (entries) {
for (auto const & e : *entries) {
tmp_type_context tctx(env, ios);
tmp_type_context tctx(env, o);
set = add_core(tctx, set, e.m_name, e.m_priority);
}
}

4
src/library/blast/simplifier/simp_rule_set.h
View file

@ -144,9 +144,9 @@ bool is_congr_rule(environment const & env, name const & n);
/** \brief Get current simplification rule sets */
simp_rule_sets get_simp_rule_sets(environment const & env);
/** \brief Get simplification rule sets in the given namespace. */
simp_rule_sets get_simp_rule_sets(environment const & env, io_state const & ios, name const & ns);
simp_rule_sets get_simp_rule_sets(environment const & env, options const & o, name const & ns);
/** \brief Get simplification rule sets in the given namespaces. */
simp_rule_sets get_simp_rule_sets(environment const & env, io_state const & ios, std::initializer_list<name> const & nss);
simp_rule_sets get_simp_rule_sets(environment const & env, options const & o, std::initializer_list<name> const & nss);
io_state_stream const & operator<<(io_state_stream const & out, simp_rule_sets const & s);

18
src/library/blast/simplifier/simplifier.cpp
View file

@ -188,10 +188,10 @@ class simplifier {
simp_rule_sets srss = _srss;
for (unsigned i = 0; i < ls.size(); i++) {
expr & l = ls[i];
tmp_type_context tctx(env(), ios());
blast_tmp_type_context tctx;
try {
// TODO(Leo,Daniel): should we allow the user to set the priority of local lemmas
srss = add(tctx, srss, mlocal_name(l), tctx.infer(l), l, LEAN_SIMP_DEFAULT_PRIORITY);
srss = add(*tctx, srss, mlocal_name(l), tctx->infer(l), l, LEAN_SIMP_DEFAULT_PRIORITY);
} catch (exception e) {
}
}
@ -976,9 +976,9 @@ result simplifier::fuse(expr const & e) {
/* Prove (1) == (3) using simplify with [ac] */
flet<bool> no_simplify_numerals(m_numerals, false);
auto pf_1_3 = prove(get_app_builder().mk_eq(e, e_grp),
get_simp_rule_sets(env(), ios(),
get_simp_rule_sets(env(), ios().get_options(),
{*g_simplify_prove_namespace, *g_simplify_unit_namespace,
*g_simplify_neg_namespace, *g_simplify_ac_namespace}));
*g_simplify_neg_namespace, *g_simplify_ac_namespace}));
if (!pf_1_3) {
diagnostic(env(), ios()) << ppb(e) << "\n\n =?=\n\n" << ppb(e_grp) << "\n";
throw blast_exception("Failed to prove (1) == (3) during fusion", e);
@ -986,10 +986,10 @@ result simplifier::fuse(expr const & e) {
/* Prove (4) == (5) using simplify with [som] */
auto pf_4_5 = prove(get_app_builder().mk_eq(e_grp_ls, e_fused_ls),
get_simp_rule_sets(env(), ios(),
get_simp_rule_sets(env(), ios().get_options(),
{*g_simplify_prove_namespace, *g_simplify_unit_namespace,
*g_simplify_neg_namespace, *g_simplify_ac_namespace,
*g_simplify_distrib_namespace}));
*g_simplify_neg_namespace, *g_simplify_ac_namespace,
*g_simplify_distrib_namespace}));
if (!pf_4_5) {
diagnostic(env(), ios()) << ppb(e_grp_ls) << "\n\n =?=\n\n" << ppb(e_fused_ls) << "\n";
throw blast_exception("Failed to prove (4) == (5) during fusion", e);
@ -997,9 +997,9 @@ result simplifier::fuse(expr const & e) {
/* Prove (5) == (6) using simplify with [numeral] */
flet<bool> simplify_numerals(m_numerals, true);
result r_simp_ls = simplify(e_fused_ls, get_simp_rule_sets(env(), ios(),
result r_simp_ls = simplify(e_fused_ls, get_simp_rule_sets(env(), ios().get_options(),
{*g_simplify_unit_namespace, *g_simplify_neg_namespace,
*g_simplify_ac_namespace}));
*g_simplify_ac_namespace}));
/* Prove (4) == (6) by transitivity of proofs (2) and (3) */
expr pf_4_6;

2
src/library/blast/unit/unit_preprocess.cpp
View file

@ -50,7 +50,7 @@ action_result unit_preprocess(unsigned hidx) {
return action_result::failed();
}
simp_rule_sets srss = get_simp_rule_sets(env(), ios(), *g_simplify_unit_simp_namespace);
simp_rule_sets srss = get_simp_rule_sets(env(), ios().get_options(), *g_simplify_unit_simp_namespace);
// TODO(dhs): disable contextual rewriting
auto r = simplify(get_iff_name(), h.get_type(), srss, is_propositional);

41
src/library/class_instance_resolution.cpp
View file

@ -44,8 +44,8 @@ struct cienv {
typedef std::unique_ptr<default_type_context> ti_ptr;
ti_ptr m_ti_ptr;
void reset(environment const & env, io_state const & ios, list<expr> const & ctx) {
m_ti_ptr.reset(new default_type_context(env, ios, ctx));
void reset(environment const & env, options const & o, list<expr> const & ctx) {
m_ti_ptr.reset(new default_type_context(env, o, ctx));
}
bool compatible_env(environment const & env) {
@ -53,17 +53,17 @@ struct cienv {
return env.is_descendant(curr_env) && curr_env.is_descendant(env);
}
void ensure_compatible(environment const & env, io_state const & ios, list<expr> const & ctx) {
void ensure_compatible(environment const & env, options const & o, list<expr> const & ctx) {
if (!m_ti_ptr || !compatible_env(env) || !m_ti_ptr->compatible_local_instances(ctx))
reset(env, ios, ctx);
if (!m_ti_ptr->update_options(ios.get_options()))
reset(env, o, ctx);
if (!m_ti_ptr->update_options(o))
m_ti_ptr->clear_cache();
}
optional<expr> operator()(environment const & env, io_state const & ios,
optional<expr> operator()(environment const & env, options const & o,
pos_info_provider const * pip, list<expr> const & ctx, expr const & type,
expr const & pos_ref) {
ensure_compatible(env, ios, ctx);
ensure_compatible(env, o, ctx);
type_context::scope_pos_info scope(*m_ti_ptr, pip, pos_ref);
return m_ti_ptr->mk_class_instance(type);
}
@ -71,18 +71,19 @@ struct cienv {
MK_THREAD_LOCAL_GET_DEF(cienv, get_cienv);
static optional<expr> mk_class_instance(environment const & env, io_state const & ios, list<expr> const & ctx,
static optional<expr> mk_class_instance(environment const & env, options const & o, list<expr> const & ctx,
expr const & e, pos_info_provider const * pip, expr const & pos_ref) {
return get_cienv()(env, ios, pip, ctx, e, pos_ref);
return get_cienv()(env, o, pip, ctx, e, pos_ref);
}
optional<expr> mk_class_instance(environment const & env, io_state const & ios, list<expr> const & ctx,
optional<expr> mk_class_instance(environment const & env, options const & o, list<expr> const & ctx,
expr const & e, pos_info_provider const * pip) {
return mk_class_instance(env, ios, ctx, e, pip, e);
return mk_class_instance(env, o, ctx, e, pip, e);
}
optional<expr> mk_class_instance(environment const & env, list<expr> const & ctx, expr const & e, pos_info_provider const * pip) {
return mk_class_instance(env, get_dummy_ios(), ctx, e, pip);
optional<expr> mk_class_instance(environment const & env, list<expr> const & ctx, expr const & e,
pos_info_provider const * pip) {
return mk_class_instance(env, options(), ctx, e, pip);
}
// Auxiliary class for generating a lazy-stream of instances.
@ -100,7 +101,7 @@ public:
bool is_strict):
choice_iterator(!is_strict),
m_ios(ios),
m_ti(env, ios, ctx, true),
m_ti(env, ios.get_options(), ctx, true),
m_scope_pos_info(m_ti, pip, pos_ref),
m_new_meta(new_meta),
m_new_j(new_j) {
@ -134,7 +135,7 @@ static constraint mk_class_instance_root_cnstr(environment const & env, io_state
if (use_local_instances)
ctx = _ctx.instantiate(substitution(s));
cienv & cenv = get_cienv();
cenv.ensure_compatible(env, ios, ctx.get_data());
cenv.ensure_compatible(env, ios.get_options(), ctx.get_data());
auto cls_name = cenv.m_ti_ptr->is_class(meta_type);
if (!cls_name) {
// do nothing, since type is not a class.
@ -149,7 +150,7 @@ static constraint mk_class_instance_root_cnstr(environment const & env, io_state
meta_type, pip, meta,
new_meta, new_j, is_strict)));
} else {
if (auto r = mk_class_instance(env, ios, ctx.get_data(), meta_type, pip, meta)) {
if (auto r = mk_class_instance(env, ios.get_options(), ctx.get_data(), meta_type, pip, meta)) {
constraint c = mk_eq_cnstr(new_meta, *r, new_j);
return lazy_list<constraints>(constraints(c));
} else if (is_strict) {
@ -189,15 +190,15 @@ optional<expr> mk_class_instance(environment const & env, local_context const &
return mk_class_instance(env, ctx.get_data(), type, nullptr);
}
optional<expr> mk_hset_instance(type_checker & tc, io_state const & ios, list<expr> const & ctx, expr const & type) {
optional<expr> mk_hset_instance(type_checker & tc, options const & o, list<expr> const & ctx, expr const & type) {
level lvl = sort_level(tc.ensure_type(type).first);
expr is_hset = tc.whnf(mk_app(mk_constant(get_is_trunc_is_hset_name(), {lvl}), type)).first;
return mk_class_instance(tc.env(), ios, ctx, is_hset);
return mk_class_instance(tc.env(), o, ctx, is_hset);
}
optional<expr> mk_subsingleton_instance(environment const & env, io_state const & ios, list<expr> const & ctx, expr const & type) {
optional<expr> mk_subsingleton_instance(environment const & env, options const & o, list<expr> const & ctx, expr const & type) {
cienv & cenv = get_cienv();
cenv.ensure_compatible(env, ios, ctx);
cenv.ensure_compatible(env, o, ctx);
return cenv.m_ti_ptr->mk_subsingleton_instance(type);
}

11
src/library/class_instance_resolution.h
View file

@ -12,8 +12,10 @@ Author: Leonardo de Moura
#include "library/local_context.h"
namespace lean {
optional<expr> mk_class_instance(environment const & env, io_state const & ios, list<expr> const & ctx, expr const & e, pos_info_provider const * pip = nullptr);
optional<expr> mk_class_instance(environment const & env, list<expr> const & ctx, expr const & e, pos_info_provider const * pip = nullptr);
optional<expr> mk_class_instance(environment const & env, options const & o,
list<expr> const & ctx, expr const & e, pos_info_provider const * pip = nullptr);
optional<expr> mk_class_instance(environment const & env, list<expr> const & ctx, expr const & e,
pos_info_provider const * pip = nullptr);
// Old API
@ -37,8 +39,9 @@ pair<expr, constraint> mk_class_instance_elaborator(
optional<expr> mk_class_instance(environment const & env, io_state const & ios, local_context const & ctx, expr const & type, bool use_local_instances);
optional<expr> mk_class_instance(environment const & env, local_context const & ctx, expr const & type);
optional<expr> mk_hset_instance(type_checker & tc, io_state const & ios, list<expr> const & ctx, expr const & type);
optional<expr> mk_subsingleton_instance(environment const & env, io_state const & ios, list<expr> const & ctx, expr const & type);
optional<expr> mk_hset_instance(type_checker & tc, options const & o, list<expr> const & ctx, expr const & type);
optional<expr> mk_subsingleton_instance(environment const & env, options const & o,
list<expr> const & ctx, expr const & type);
void initialize_class_instance_resolution();
void finalize_class_instance_resolution();

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

@ -50,7 +50,7 @@ optional<expr> mk_congr_subsingleton_thm(type_checker & tc, io_state const & ios
if (prop.back()) {
ss.push_back(true);
} else {
ss.push_back(static_cast<bool>(mk_subsingleton_instance(tc.env(), ios, ctx, mlocal_type(d))));
ss.push_back(static_cast<bool>(mk_subsingleton_instance(tc.env(), ios.get_options(), ctx, mlocal_type(d))));
}
codomain_deps_on.push_back(depends_on(codomain, d));
ctx = cons(d, ctx);
@ -145,7 +145,7 @@ optional<expr> mk_congr_subsingleton_thm(type_checker & tc, io_state const & ios
return none_expr();
buffer<expr> hyps;
g.get_hyps(hyps);
auto spr = mk_subsingleton_instance(tc.env(), ios, to_list(hyps), mlocal_type(new_lhs));
auto spr = mk_subsingleton_instance(tc.env(), ios.get_options(), to_list(hyps), mlocal_type(new_lhs));
if (!spr)
return none_expr();
expr new_eq = mk_local(get_unused_name(name(h, eqidx), hyps), mk_eq(tc, new_rhs, new_lhs));

2
src/library/tactic/inversion_tactic.cpp
View file

@ -55,7 +55,7 @@ optional<expr> apply_eq_rec_eq(type_checker & tc, io_state const & ios, list<exp
if (!is_local(p) || !is_eq_a_a(tc, mlocal_type(p)))
return none_expr();
expr const & A = args[0];
auto is_hset_A = mk_hset_instance(tc, ios, ctx, A);
auto is_hset_A = mk_hset_instance(tc, ios.get_options(), ctx, A);
if (!is_hset_A)
return none_expr();
levels ls = const_levels(eq_rec_fn);

9
src/library/tmp_type_context.cpp
View file

@ -16,13 +16,14 @@ void tmp_type_context::init(environment const & env, reducible_behavior b) {
}
}
tmp_type_context::tmp_type_context(environment const & env, io_state const & ios, reducible_behavior b):
type_context(env, ios) {
tmp_type_context::tmp_type_context(environment const & env, options const & o, reducible_behavior b):
type_context(env, o) {
init(env, b);
}
tmp_type_context::tmp_type_context(environment const & env, io_state const & ios, tmp_local_generator & gen, reducible_behavior b):
type_context(env, ios, gen) {
tmp_type_context::tmp_type_context(environment const & env, options const & o, tmp_local_generator & gen,
reducible_behavior b):
type_context(env, o, gen) {
init(env, b);
}

5
src/library/tmp_type_context.h
View file

@ -43,8 +43,9 @@ class tmp_type_context : public type_context {
std::vector<scope> m_scopes;
void init(environment const & env, reducible_behavior b);
public:
tmp_type_context(environment const & env, io_state const & ios, reducible_behavior b = UnfoldReducible);
tmp_type_context(environment const & env, io_state const & ios, tmp_local_generator & gen, reducible_behavior b = UnfoldReducible);
tmp_type_context(environment const & env, options const & o, reducible_behavior b = UnfoldReducible);
tmp_type_context(environment const & env, options const & o,
tmp_local_generator & gen, reducible_behavior b = UnfoldReducible);
virtual ~tmp_type_context();
/** \brief Reset the state: backtracking stack, indices and assignment. */

2
src/library/trace.h
View file

@ -32,7 +32,7 @@ public:
void activate();
};
#define LEAN_MERGE_(a,b) a##b
#define LEAN_MERGE_(a, b) a##b
#define LEAN_LABEL_(a) LEAN_MERGE_(unique_name_, a)
#define LEAN_UNIQUE_NAME LEAN_LABEL_(__LINE__)

8
src/library/type_context.cpp
View file

@ -99,7 +99,7 @@ struct type_context::ext_ctx : public extension_context {
}
};
type_context::type_context(environment const & env, io_state const & ios, tmp_local_generator * gen,
type_context::type_context(environment const & env, options const & o, tmp_local_generator * gen,
bool gen_owner, bool multiple_instances):
m_env(env),
m_ngen(*g_prefix),
@ -115,7 +115,7 @@ type_context::type_context(environment const & env, io_state const & ios, tmp_lo
// TODO(Leo): use compilation options for setting config
m_ci_max_depth = 32;
m_ci_trans_instances = true;
update_options(ios.get_options());
update_options(o);
}
type_context::~type_context() {
@ -1739,9 +1739,9 @@ type_context::scope_pos_info::~scope_pos_info() {
m_owner.m_ci_pos = m_old_pos;
}
default_type_context::default_type_context(environment const & env, io_state const & ios,
default_type_context::default_type_context(environment const & env, options const & o,
list<expr> const & insts, bool multiple_instances):
type_context(env, ios, multiple_instances),
type_context(env, o, multiple_instances),
m_not_reducible_pred(mk_not_reducible_pred(env)) {
m_ignore_if_zero = false;
m_next_uvar_idx = 0;

12
src/library/type_context.h
View file

@ -296,14 +296,14 @@ class type_context {
optional<expr> mk_class_instance_core(expr const & type);
optional<expr> check_ci_cache(expr const & type) const;
void cache_ci_result(expr const & type, expr const & inst);
type_context(environment const & env, io_state const & ios, tmp_local_generator * gen,
type_context(environment const & env, options const & o, tmp_local_generator * gen,
bool gen_owner, bool multiple_instances);
public:
type_context(environment const & env, io_state const & ios, bool multiple_instances = false):
type_context(env, ios, new tmp_local_generator(), true, multiple_instances) {}
type_context(environment const & env, io_state const & ios, tmp_local_generator & gen,
type_context(environment const & env, options const & o, bool multiple_instances = false):
type_context(env, o, new tmp_local_generator(), true, multiple_instances) {}
type_context(environment const & env, options const & o, tmp_local_generator & gen,
bool multiple_instances = false):
type_context(env, ios, &gen, false, multiple_instances) {}
type_context(env, o, &gen, false, multiple_instances) {}
virtual ~type_context();
void set_local_instances(list<expr> const & insts);
@ -551,7 +551,7 @@ class default_type_context : public type_context {
unsigned mvar_idx(expr const & m) const;
public:
default_type_context(environment const & env, io_state const & ios,
default_type_context(environment const & env, options const & o,
list<expr> const & insts = list<expr>(), bool multiple_instances = false);
virtual ~default_type_context();
virtual bool is_extra_opaque(name const & n) const { return m_not_reducible_pred(n); }

2
tests/lean/hott/class_loop.hlean
View file

@ -17,7 +17,7 @@ is_iso.mk (inverse f) f
constant a : A
set_option class.trace_instances true
set_option trace.class_instances true
definition foo := inverse (id a)

2
tests/lean/run/class7.lean
View file

@ -7,7 +7,7 @@ intro : A -> inh A
theorem inh_bool [instance] : inh Prop
:= inh.intro true
set_option class.trace_instances true
set_option trace.class_instances true
theorem inh_fun [instance] {A B : Type} [H : inh B] : inh (A → B)
:= inh.rec (λ b, inh.intro (λ a : A, b)) H

2
tests/lean/run/class8.lean
View file

@ -25,7 +25,7 @@ definition assump := eassumption
tactic_hint assump
theorem tst {A B : Type} (H : inh B) : inh (A → B → B)
set_option class.trace_instances true
set_option trace.class_instances true
theorem T1 {A B C D : Type} {P : C → Prop} (a : A) (H1 : inh B) (H2 : ∃x, P x) : inh ((A → A) × B × (D → C) × Prop) :=
have h1 [visible] : inh A, from inh.intro a,

2
tests/lean/run/mult.lean
View file

@ -6,7 +6,7 @@ attribute C [multiple_instances]
definition c1 [instance] : C := C.mk 1
definition c2 [instance] : C := C.mk 2
set_option class.trace_instances true
set_option trace.class_instances true
definition f [s : C] : nat := C.val