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

refactor(*): start process for eliminating of opaque definitions from the kernel

Browse source 
see issue #576
This commit is contained in:
Leonardo de Moura 2015-05-08 14:36:38 -07:00
parent 061e26157e
commit 57ea660963
80 changed files with 406 additions and 603 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

63
doc/lean/declarations.org
View file

@ -41,69 +41,6 @@ previous example would produce a typing error because the type checker
would be unable to unfold =id= and establish that =nat= and =id nat=
are definitionally equal.
** Opaque definitions
Opaque definitions are similar to regular definitions, but they are
only _transparent_ in the module/file where they were defined. The
idea is to allow us to prove theorems about the opaque definition =C=
in the module where it was defined. In other modules, we can only rely
on these theorems. That is, the actual definition is
hidden/encapsulated, and the module designer is free to change it
without affecting its "customers".
Actually, the opaque definition is only treated as transparent inside of
other opaque definitions/theorems in the same module.
Here is an example
#+BEGIN_SRC lean
import data.nat
opaque definition id {A : Type} (a : A) : A := a
-- The following command is type correct since it is being executed in the
-- same file where id was defined
check λ (x : nat) (y : id nat), x = y
-- The following theorem is also type correct since id is being treated as
-- transparent only in the proof by reflexivity.
theorem id_eq {A : Type} (a : A) : id a = a :=
eq.refl a
-- The following transparent definition is also type correct. It uses
-- id but it can be type checked without unfolding id.
definition id2 {A : Type} (a : A) : A :=
id a
-- The following definition is type incorrect. It only type checks if
-- we unfold id, but it is not allowed because the definition is opaque.
/-
definition buggy_def {A : Type} (a : A) : Prop :=
∀ (b : id A), a = b
-/
#+END_SRC
Theorems are always opaque, but we should be able to type check their type
in any module. The following theorem is type incorrect because we need to
unfold the opaque definition =id= to type check it.
#+BEGIN_SRC lean
import data.unit
opaque definition id {A : Type} (a : A) : A := a
/-
theorem buggy_thm (a : unit) (b : id unit) : a = b :=
unit.equal a b
-/
#+END_SRC
In contrast, the following theorem is type correct because =id= is
transparent in this example.
#+BEGIN_SRC lean
import data.unit
definition id {A : Type} (a : A) : A := a
theorem simple (a : unit) (b : id unit) : a = b :=
unit.equal a b
#+END_SRC
** Private definitions and theorems
Sometimes it is useful to hide auxiliary definitions and theorems from

5
library/logic/axioms/hilbert.lean
View file

@ -30,7 +30,7 @@ inhabited_of_nonempty (obtain w Hw, from H, nonempty.intro w)
/- the Hilbert epsilon function -/
opaque definition epsilon {A : Type} [H : nonempty A] (P : A → Prop) : A :=
definition epsilon {A : Type} [H : nonempty A] (P : A → Prop) : A :=
let u : {x | (∃y, P y) → P x} :=
strong_indefinite_description P H in
elt_of u
@ -39,7 +39,8 @@ theorem epsilon_spec_aux {A : Type} (H : nonempty A) (P : A → Prop) (Hex : ∃
P (@epsilon A H P) :=
let u : {x | (∃y, P y) → P x} :=
strong_indefinite_description P H in
has_property u Hex
have aux : (∃y, P y) → P (elt_of (strong_indefinite_description P H)), from has_property u,
aux Hex
theorem epsilon_spec {A : Type} {P : A → Prop} (Hex : ∃y, P y) :
P (@epsilon A (nonempty_of_exists Hex) P) :=

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

@ -460,7 +460,7 @@ environment end_scoped_cmd(parser & p) {
environment check_cmd(parser & p) {
expr e; level_param_names ls;
std::tie(e, ls) = parse_local_expr(p);
auto tc = mk_type_checker(p.env(), p.mk_ngen(), true);
auto tc = mk_type_checker(p.env(), p.mk_ngen());
expr type = tc->check(e, ls).first;
auto reg = p.regular_stream();
formatter fmt = reg.get_formatter();
@ -481,7 +481,7 @@ environment check_cmd(parser & p) {
class all_transparent_converter : public default_converter {
public:
all_transparent_converter(environment const & env):
default_converter(env, optional<module_idx>(), true) {
default_converter(env) {
}
virtual bool is_opaque(declaration const &) const {
return false;
@ -502,7 +502,7 @@ environment eval_cmd(parser & p) {
std::tie(e, ls) = parse_local_expr(p);
expr r;
if (whnf) {
auto tc = mk_type_checker(p.env(), p.mk_ngen(), true);
auto tc = mk_type_checker(p.env(), p.mk_ngen());
r = tc->whnf(e).first;
} else if (all_transparent) {
type_checker tc(p.env(), name_generator(),
@ -767,7 +767,7 @@ environment telescope_eq_cmd(parser & p) {
t.push_back(local);
e = instantiate(binding_body(e), local);
}
auto tc = mk_type_checker(p.env(), p.mk_ngen(), true);
auto tc = mk_type_checker(p.env(), p.mk_ngen());
buffer<expr> eqs;
mk_telescopic_eq(*tc, t, eqs);
for (expr const & eq : eqs) {

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

@ -120,7 +120,7 @@ static optional<pair<expr, expr>> apply_subst(environment const & env, local_con
constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
local_context const & _ctx, expr const & m, expr const & _e,
constraint_seq const & cs, unifier_config const & cfg,
info_manager * im, bool relax, update_type_info_fn const & fn) {
info_manager * im, update_type_info_fn const & fn) {
justification j = mk_failed_to_synthesize_jst(env, m);
auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & _s,
name_generator const & _ngen) {
@ -128,7 +128,7 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
expr e = _e;
substitution s = _s;
name_generator ngen(_ngen);
type_checker_ptr tc(mk_type_checker(env, ngen.mk_child(), relax));
type_checker_ptr tc(mk_type_checker(env, ngen.mk_child()));
constraint_seq new_cs = cs;
expr e_type = tc->infer(e, new_cs);
e_type = s.instantiate(e_type);
@ -163,8 +163,8 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
fcs.linearize(cs_buffer);
metavar_closure cls(meta);
cls.add(meta_type);
cls.mk_constraints(s, j, relax, cs_buffer);
cs_buffer.push_back(mk_eq_cnstr(meta, e, j, relax));
cls.mk_constraints(s, j, cs_buffer);
cs_buffer.push_back(mk_eq_cnstr(meta, e, j));
unifier_config new_cfg(cfg);
new_cfg.m_discard = false;
@ -182,7 +182,7 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
throw_elaborator_exception("solution contains metavariables", e);
if (im)
im->instantiate(new_s);
constraints r = cls.mk_constraints(new_s, j, relax);
constraints r = cls.mk_constraints(new_s, j);
return append(r, postponed);
};
@ -250,6 +250,6 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
}
};
bool owner = false;
return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::Epilogue), owner, j, relax);
return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::Epilogue), owner, j);
}
}

2
src/frontends/lean/calc_proof_elaborator.h
View file

@ -23,7 +23,7 @@ typedef std::function<void(expr const &)> update_type_info_fn;
constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
local_context const & ctx, expr const & m, expr const & e,
constraint_seq const & cs, unifier_config const & cfg,
info_manager * im, bool relax, update_type_info_fn const & fn);
info_manager * im, update_type_info_fn const & fn);
void initialize_calc_proof_elaborator();
void finalize_calc_proof_elaborator();

18
src/frontends/lean/coercion_elaborator.cpp
View file

@ -58,7 +58,7 @@ optional<constraints> coercion_elaborator::next() {
that considers coercions from a_type to the type assigned to \c m. */
constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom,
expr const & m, expr const & a, expr const & a_type,
justification const & j, unsigned delay_factor, bool relax) {
justification const & j, unsigned delay_factor) {
auto choice_fn = [=, &tc, &infom](expr const & meta, expr const & d_type, substitution const & s,
name_generator const & /* ngen */) {
expr new_a_type;
@ -74,10 +74,10 @@ constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom,
if (delay_factor < to_delay_factor(cnstr_group::DelayedChoice)) {
// postpone...
return lazy_list<constraints>(constraints(mk_coercion_cnstr(tc, infom, m, a, a_type, justification(),
delay_factor+1, relax)));
delay_factor+1)));
} else {
// giveup...
return lazy_list<constraints>(constraints(mk_eq_cnstr(meta, a, justification(), relax)));
return lazy_list<constraints>(constraints(mk_eq_cnstr(meta, a, justification())));
}
}
constraint_seq cs;
@ -89,7 +89,7 @@ constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom,
buffer<constraints> choices;
buffer<expr> coes;
// first alternative: no coercion
constraint_seq cs1 = cs + mk_eq_cnstr(meta, a, justification(), relax);
constraint_seq cs1 = cs + mk_eq_cnstr(meta, a, justification());
choices.push_back(cs1.to_list());
unsigned i = alts.size();
while (i > 0) {
@ -98,7 +98,7 @@ constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom,
expr coe = std::get<1>(t);
expr new_a = copy_tag(a, mk_app(coe, a));
coes.push_back(coe);
constraint_seq csi = cs + mk_eq_cnstr(meta, new_a, new_a_type_jst, relax);
constraint_seq csi = cs + mk_eq_cnstr(meta, new_a, new_a_type_jst);
choices.push_back(csi.to_list());
}
return choose(std::make_shared<coercion_elaborator>(infom, meta,
@ -109,23 +109,23 @@ constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom,
if (is_nil(coes)) {
expr new_a = a;
infom.erase_coercion_info(a);
cs += mk_eq_cnstr(meta, new_a, new_a_type_jst, relax);
cs += mk_eq_cnstr(meta, new_a, new_a_type_jst);
return lazy_list<constraints>(cs.to_list());
} else if (is_nil(tail(coes))) {
expr new_a = copy_tag(a, mk_app(head(coes), a));
infom.save_coercion_info(a, new_a);
cs += mk_eq_cnstr(meta, new_a, new_a_type_jst, relax);
cs += mk_eq_cnstr(meta, new_a, new_a_type_jst);
return lazy_list<constraints>(cs.to_list());
} else {
list<constraints> choices = map2<constraints>(coes, [&](expr const & coe) {
expr new_a = copy_tag(a, mk_app(coe, a));
constraint c = mk_eq_cnstr(meta, new_a, new_a_type_jst, relax);
constraint c = mk_eq_cnstr(meta, new_a, new_a_type_jst);
return (cs + c).to_list();
});
return choose(std::make_shared<coercion_elaborator>(infom, meta, choices, coes, false));
}
}
};
return mk_choice_cnstr(m, choice_fn, delay_factor, true, j, relax);
return mk_choice_cnstr(m, choice_fn, delay_factor, true, j);
}
}

5
src/frontends/lean/coercion_elaborator.h
View file

@ -38,14 +38,11 @@ public:
enumerate coercion functions \c f. By "not known", we mean the type is a
metavariable application.
\param relax True if opaque constants in the current module should be treated
as transparent
\see coercion_info_manager
*/
constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom,
expr const & m, expr const & a, expr const & a_type,
justification const & j, unsigned delay_factor, bool relax);
justification const & j, unsigned delay_factor);
list<expr> get_coercions_from_to(type_checker & tc, expr const & from_type, expr const & to_type, constraint_seq & cs);
}

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

@ -1143,15 +1143,15 @@ class definition_cmd_fn {
}
}
std::tuple<expr, expr, level_param_names> elaborate_definition(expr const & type, expr const & value, bool is_opaque) {
std::tuple<expr, expr, level_param_names> elaborate_definition(expr const & type, expr const & value) {
if (m_p.profiling()) {
std::ostringstream msg;
display_pos(msg);
msg << " elaboration time for " << m_name;
timeit timer(m_p.diagnostic_stream().get_stream(), msg.str().c_str());
return m_p.elaborate_definition(m_name, type, value, is_opaque);
return m_p.elaborate_definition(m_name, type, value);
} else {
return m_p.elaborate_definition(m_name, type, value, is_opaque);
return m_p.elaborate_definition(m_name, type, value);
}
}
@ -1161,7 +1161,7 @@ class definition_cmd_fn {
void elaborate_multi() {
lean_assert(!m_aux_decls.empty());
level_param_names new_ls;
std::tie(m_type, m_value, new_ls) = elaborate_definition(m_type, m_value, m_is_opaque);
std::tie(m_type, m_value, new_ls) = elaborate_definition(m_type, m_value);
new_ls = append(m_ls, new_ls);
lean_assert(m_aux_types.empty());
buffer<expr> aux_values;
@ -1212,7 +1212,7 @@ class definition_cmd_fn {
m_p.add_delayed_theorem(m_env, m_real_name, m_ls, type_as_is, m_value);
m_env = module::add(m_env, check(mk_axiom(m_real_name, m_ls, m_type)));
} else {
std::tie(m_type, m_value, new_ls) = elaborate_definition(type_as_is, m_value, m_is_opaque);
std::tie(m_type, m_value, new_ls) = elaborate_definition(type_as_is, m_value);
m_type = expand_abbreviations(m_env, unfold_untrusted_macros(m_env, m_type));
m_value = expand_abbreviations(m_env, unfold_untrusted_macros(m_env, m_value));
new_ls = append(m_ls, new_ls);
@ -1228,7 +1228,7 @@ class definition_cmd_fn {
}
}
} else {
std::tie(m_type, m_value, new_ls) = elaborate_definition(m_type, m_value, m_is_opaque);
std::tie(m_type, m_value, new_ls) = elaborate_definition(m_type, m_value);
new_ls = append(m_ls, new_ls);
m_type = expand_abbreviations(m_env, unfold_untrusted_macros(m_env, m_type));
m_value = expand_abbreviations(m_env, unfold_untrusted_macros(m_env, m_value));

133
src/frontends/lean/elaborator.cpp
View file

@ -68,11 +68,10 @@ struct elaborator::choice_expr_elaborator : public choice_iterator {
expr m_type;
expr m_choice;
unsigned m_idx;
bool m_relax_main_opaque;
choice_expr_elaborator(elaborator & elab, local_context const & ctx, local_context const & full_ctx,
expr const & meta, expr const & type, expr const & c, bool relax):
expr const & meta, expr const & type, expr const & c):
m_elab(elab), m_context(ctx), m_full_context(full_ctx), m_meta(meta),
m_type(type), m_choice(c), m_idx(get_num_choices(m_choice)), m_relax_main_opaque(relax) {
m_type(type), m_choice(c), m_idx(get_num_choices(m_choice)) {
}
virtual optional<constraints> next() {
@ -93,13 +92,12 @@ struct elaborator::choice_expr_elaborator : public choice_iterator {
expr r_type = m_elab.infer_type(r, new_cs);
if (!has_expr_metavar_relaxed(r_type)) {
cs = new_cs;
auto new_rcs = m_elab.ensure_has_type(r, r_type, m_type, justification(),
m_relax_main_opaque);
auto new_rcs = m_elab.ensure_has_type(r, r_type, m_type, justification());
r = new_rcs.first;
cs += new_rcs.second;
}
}
cs = mk_eq_cnstr(m_meta, r, justification(), m_relax_main_opaque) + cs;
cs = mk_eq_cnstr(m_meta, r, justification()) + cs;
return optional<constraints>(cs.to_list());
} catch (exception &) {}
}
@ -114,12 +112,10 @@ elaborator::elaborator(elaborator_context & ctx, name_generator const & ngen, bo
m_full_context(),
m_unifier_config(ctx.m_ios.get_options(), true /* use exceptions */, true /* discard */) {
m_has_sorry = has_sorry(m_ctx.m_env);
m_relax_main_opaque = false;
m_use_tactic_hints = true;
m_no_info = false;
m_in_equation_lhs = false;
m_tc[0] = mk_type_checker(ctx.m_env, m_ngen.mk_child(), false);
m_tc[1] = mk_type_checker(ctx.m_env, m_ngen.mk_child(), true);
m_tc = mk_type_checker(ctx.m_env, m_ngen.mk_child());
m_nice_mvar_names = nice_mvar_names;
}
@ -131,8 +127,6 @@ void elaborator::register_meta(expr const & meta) {
lean_assert(is_meta(meta));
name const & n = mlocal_name(get_app_fn(meta));
m_mvar2meta.insert(n, meta);
if (m_relax_main_opaque)
m_relaxed_mvars.insert(n);
}
/** \brief Convert the metavariable to the metavariable application that captures
@ -153,7 +147,7 @@ void elaborator::save_type_data(expr const & e, expr const & r) {
(is_constant(e) || is_local(e) || is_placeholder(e) || is_as_atomic(e) ||
is_consume_args(e) || is_notation_info(e))) {
if (auto p = pip()->get_pos_info(e)) {
expr t = m_tc[m_relax_main_opaque]->infer(r).first;
expr t = m_tc->infer(r).first;
m_pre_info_data.add_type_info(p->first, p->second, t);
}
}
@ -172,7 +166,7 @@ void elaborator::save_binder_type(expr const & e, expr const & r) {
void elaborator::save_extra_type_data(expr const & e, expr const & r) {
if (!m_no_info && infom() && pip()) {
if (auto p = pip()->get_pos_info(e)) {
expr t = m_tc[m_relax_main_opaque]->infer(r).first;
expr t = m_tc->infer(r).first;
m_pre_info_data.add_extra_type_info(p->first, p->second, r, t);
}
}
@ -216,7 +210,7 @@ void elaborator::save_placeholder_info(expr const & e, expr const & r) {
void elaborator::save_coercion_info(expr const & e, expr const & c) {
if (!m_no_info && infom() && pip()) {
if (auto p = pip()->get_pos_info(e)) {
expr t = m_tc[m_relax_main_opaque]->infer(c).first;
expr t = m_tc->infer(c).first;
m_pre_info_data.add_coercion_info(p->first, p->second, c, t);
}
}
@ -253,7 +247,7 @@ expr elaborator::mk_placeholder_meta(optional<name> const & suffix, optional<exp
tag g, bool is_strict, bool is_inst_implicit, constraint_seq & cs) {
if (is_inst_implicit && !m_ctx.m_ignore_instances) {
auto ec = mk_class_instance_elaborator(
env(), ios(), m_context, m_ngen.next(), suffix, m_relax_main_opaque,
env(), ios(), m_context, m_ngen.next(), suffix,
use_local_instances(), is_strict, type, g, m_unifier_config, m_ctx.m_pos_provider);
register_meta(ec.first);
cs += ec.second;
@ -299,15 +293,14 @@ expr elaborator::visit_choice(expr const & e, optional<expr> const & t, constrai
// Possible optimization: try to lookahead and discard some of the alternatives.
expr m = m_full_context.mk_meta(m_ngen, t, e.get_tag());
register_meta(m);
bool relax = m_relax_main_opaque;
local_context ctx = m_context;
local_context full_ctx = m_full_context;
auto fn = [=](expr const & meta, expr const & type, substitution const & /* s */,
name_generator const & /* ngen */) {
return choose(std::make_shared<choice_expr_elaborator>(*this, ctx, full_ctx, meta, type, e, relax));
return choose(std::make_shared<choice_expr_elaborator>(*this, ctx, full_ctx, meta, type, e));
};
justification j = mk_justification("none of the overloads is applicable", some_expr(e));
cs += mk_choice_cnstr(m, fn, to_delay_factor(cnstr_group::Basic), true, j, m_relax_main_opaque);
cs += mk_choice_cnstr(m, fn, to_delay_factor(cnstr_group::Basic), true, j);
return m;
}
@ -340,7 +333,7 @@ expr elaborator::visit_calc_proof(expr const & e, optional<expr> const & t, cons
auto fn = [=](expr const & t) { save_type_data(get_annotation_arg(e), t); };
constraint c = mk_calc_proof_cnstr(env(), ios().get_options(),
m_context, m, ecs.first, ecs.second, m_unifier_config,
im, m_relax_main_opaque, fn);
im, fn);
cs += c;
return m;
}
@ -353,8 +346,8 @@ static bool is_implicit_pi(expr const & e) {
}
/** \brief Auxiliary function for adding implicit arguments to coercions to function-class */
expr elaborator::add_implict_args(expr e, constraint_seq & cs, bool relax) {
type_checker & tc = *m_tc[relax];
expr elaborator::add_implict_args(expr e, constraint_seq & cs) {
type_checker & tc = *m_tc;
constraint_seq new_cs;
expr type = tc.whnf(tc.infer(e, new_cs), new_cs);
if (!is_implicit_pi(type))
@ -395,10 +388,10 @@ pair<expr, expr> elaborator::ensure_fun(expr f, constraint_seq & cs) {
if (!is_pi(f_type) && has_metavar(f_type)) {
constraint_seq saved_cs = cs;
expr new_f_type = whnf(f_type, cs);
if (!is_pi(new_f_type) && m_tc[m_relax_main_opaque]->is_stuck(new_f_type)) {
if (!is_pi(new_f_type) && m_tc->is_stuck(new_f_type)) {
cs = saved_cs;
// let type checker add constraint
f_type = m_tc[m_relax_main_opaque]->ensure_pi(f_type, f, cs);
f_type = m_tc->ensure_pi(f_type, f, cs);
} else {
f_type = new_f_type;
}
@ -410,14 +403,12 @@ pair<expr, expr> elaborator::ensure_fun(expr f, constraint_seq & cs) {
throw_kernel_exception(env(), f, [=](formatter const & fmt) { return pp_function_expected(fmt, f); });
} else if (is_nil(tail(coes))) {
expr old_f = f;
bool relax = m_relax_main_opaque;
f = mk_coercion_app(head(coes), f);
f = add_implict_args(f, cs, relax);
f = add_implict_args(f, cs);
f_type = infer_type(f, cs);
save_coercion_info(old_f, f);
lean_assert(is_pi(f_type));
} else {
bool relax = m_relax_main_opaque;
local_context ctx = m_context;
local_context full_ctx = m_full_context;
justification j = mk_justification(f, [=](formatter const & fmt, substitution const & subst) {
@ -429,19 +420,19 @@ pair<expr, expr> elaborator::ensure_fun(expr f, constraint_seq & cs) {
list<constraints> choices = map2<constraints>(coes, [&](expr const & coe) {
expr new_f = mk_coercion_app(coe, f);
constraint_seq cs;
new_f = add_implict_args(new_f, cs, relax);
cs += mk_eq_cnstr(meta, new_f, j, relax);
new_f = add_implict_args(new_f, cs);
cs += mk_eq_cnstr(meta, new_f, j);
return cs.to_list();
});
return choose(std::make_shared<coercion_elaborator>(*this, f, choices, coes, false));
};
f = m_full_context.mk_meta(m_ngen, none_expr(), f.get_tag());
register_meta(f);
cs += mk_choice_cnstr(f, choice_fn, to_delay_factor(cnstr_group::Basic), true, j, relax);
cs += mk_choice_cnstr(f, choice_fn, to_delay_factor(cnstr_group::Basic), true, j);
lean_assert(is_meta(f));
// let type checker add constraint
f_type = infer_type(f, cs);
f_type = m_tc[m_relax_main_opaque]->ensure_pi(f_type, f, cs);
f_type = m_tc->ensure_pi(f_type, f, cs);
lean_assert(is_pi(f_type));
}
} else {
@ -481,7 +472,7 @@ expr elaborator::apply_coercion(expr const & a, expr a_type, expr d_type) {
a_type = whnf(a_type).first;
d_type = whnf(d_type).first;
constraint_seq aux_cs;
list<expr> coes = get_coercions_from_to(*m_tc[m_relax_main_opaque], a_type, d_type, aux_cs);
list<expr> coes = get_coercions_from_to(*m_tc, a_type, d_type, aux_cs);
if (is_nil(coes)) {
erase_coercion_info(a);
return a;
@ -494,7 +485,7 @@ expr elaborator::apply_coercion(expr const & a, expr a_type, expr d_type) {
expr r = mk_coercion_app(coe, a);
expr r_type = infer_type(r).first;
try {
if (m_tc[m_relax_main_opaque]->is_def_eq(r_type, d_type).first) {
if (m_tc->is_def_eq(r_type, d_type).first) {
save_coercion_info(a, r);
return r;
}
@ -510,21 +501,17 @@ expr elaborator::apply_coercion(expr const & a, expr a_type, expr d_type) {
pair<expr, constraint_seq> elaborator::mk_delayed_coercion(
expr const & a, expr const & a_type, expr const & expected_type,
justification const & j) {
bool relax = m_relax_main_opaque;
type_checker & tc = *m_tc[relax];
type_checker & tc = *m_tc;
expr m = m_full_context.mk_meta(m_ngen, some_expr(expected_type), a.get_tag());
register_meta(m);
constraint c = mk_coercion_cnstr(tc, *this, m, a, a_type, j, to_delay_factor(cnstr_group::Basic), relax);
constraint c = mk_coercion_cnstr(tc, *this, m, a, a_type, j, to_delay_factor(cnstr_group::Basic));
return to_ecs(m, c);
}
/** \brief Given a term <tt>a : a_type</tt>, ensure it has type \c expected_type. Apply coercions if needed
\remark relax == true affects how opaque definitions in the main module are treated.
*/
pair<expr, constraint_seq> elaborator::ensure_has_type(
expr const & a, expr const & a_type, expr const & expected_type,
justification const & j, bool relax) {
expr const & a, expr const & a_type, expr const & expected_type, justification const & j) {
if (is_meta(expected_type) && has_coercions_from(a_type)) {
return mk_delayed_coercion(a, a_type, expected_type, j);
} else if (!m_in_equation_lhs && is_meta(a_type) && has_coercions_to(expected_type)) {
@ -532,7 +519,7 @@ pair<expr, constraint_seq> elaborator::ensure_has_type(
} else {
pair<bool, constraint_seq> dcs;
try {
dcs = m_tc[relax]->is_def_eq(a_type, expected_type, j);
dcs = m_tc->is_def_eq(a_type, expected_type, j);
} catch (exception&) {
dcs.first = false;
}
@ -545,7 +532,7 @@ pair<expr, constraint_seq> elaborator::ensure_has_type(
if (!is_eqp(a, new_a)) {
expr new_a_type = infer_type(new_a, cs);
try {
coercion_worked = m_tc[relax]->is_def_eq(new_a_type, expected_type, j, cs);
coercion_worked = m_tc->is_def_eq(new_a_type, expected_type, j, cs);
} catch (exception&) {
coercion_worked = false;
}
@ -554,7 +541,7 @@ pair<expr, constraint_seq> elaborator::ensure_has_type(
return to_ecs(new_a, cs);
} else if (has_metavar(a_type) || has_metavar(expected_type)) {
// rely on unification hints to solve this constraint
return to_ecs(a, mk_eq_cnstr(a_type, expected_type, j, relax));
return to_ecs(a, mk_eq_cnstr(a_type, expected_type, j));
} else {
throw unifier_exception(j, substitution());
}
@ -636,7 +623,7 @@ expr elaborator::visit_app(expr const & e, constraint_seq & cs) {
expr a_type = infer_type(a, a_cs);
expr r = mk_app(f, a, e.get_tag());
justification j = mk_app_justification(r, a, d_type, a_type);
auto new_a_cs = ensure_has_type(a, a_type, d_type, j, m_relax_main_opaque);
auto new_a_cs = ensure_has_type(a, a_type, d_type, j);
expr new_a = new_a_cs.first;
cs += f_cs + new_a_cs.second + a_cs;
return update_app(r, app_fn(r), new_a);
@ -722,7 +709,7 @@ expr elaborator::ensure_type(expr const & e, constraint_seq & cs) {
return e;
if (is_meta(t)) {
// let type checker add constraint
m_tc[m_relax_main_opaque]->ensure_sort(t, e, cs);
m_tc->ensure_sort(t, e, cs);
return e;
}
}
@ -811,7 +798,7 @@ expr elaborator::visit_typed_expr(expr const & e, constraint_seq & cs) {
expr v = visit(get_typed_expr_expr(e), v_cs);
expr v_type = infer_type(v, v_cs);
justification j = mk_type_mismatch_jst(v, v_type, t, e);
auto new_vcs = ensure_has_type(v, v_type, t, j, m_relax_main_opaque);
auto new_vcs = ensure_has_type(v, v_type, t, j);
v = new_vcs.first;
cs += t_cs + new_vcs.second + v_cs;
return v;
@ -1060,7 +1047,6 @@ static expr assign_equation_lhs_metas(type_checker & tc, expr const & eqns) {
// \remark original_eqns is eqns before elaboration
constraint elaborator::mk_equations_cnstr(expr const & m, expr const & eqns) {
bool relax = m_relax_main_opaque;
environment const & _env = env();
io_state const & _ios = ios();
justification j = mk_failed_to_synthesize_jst(_env, m);
@ -1071,15 +1057,15 @@ constraint elaborator::mk_equations_cnstr(expr const & m, expr const & eqns) {
new_eqns = solve_unassigned_mvars(new_s, new_eqns);
if (display_unassigned_mvars(new_eqns, new_s))
return lazy_list<constraints>();
type_checker_ptr tc = mk_type_checker(_env, ngen, relax);
type_checker_ptr tc = mk_type_checker(_env, ngen);
new_eqns = assign_equation_lhs_metas(*tc, new_eqns);
expr val = compile_equations(*tc, _ios, new_eqns, meta, meta_type, relax);
expr val = compile_equations(*tc, _ios, new_eqns, meta, meta_type);
justification j = mk_justification("equation compilation", some_expr(eqns));
constraint c = mk_eq_cnstr(meta, val, j, relax);
constraint c = mk_eq_cnstr(meta, val, j);
return lazy_list<constraints>(c);
};
bool owner = true;
return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::MaxDelayed), owner, j, relax);
return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::MaxDelayed), owner, j);
}
expr elaborator::visit_equations(expr const & eqns, constraint_seq & cs) {
@ -1100,7 +1086,7 @@ expr elaborator::visit_equations(expr const & eqns, constraint_seq & cs) {
expr wf = visit(mk_constant(get_well_founded_name()), cs);
wf = ::lean::mk_app(wf, *new_R);
justification j = mk_type_mismatch_jst(*new_Hwf, Hwf_type, wf, equations_wf_proof(eqns));
auto new_Hwf_cs = ensure_has_type(*new_Hwf, Hwf_type, wf, j, m_relax_main_opaque);
auto new_Hwf_cs = ensure_has_type(*new_Hwf, Hwf_type, wf, j);
new_Hwf = new_Hwf_cs.first;
cs += new_Hwf_cs.second;
}
@ -1188,7 +1174,7 @@ expr elaborator::visit_equation(expr const & eq, constraint_seq & cs) {
substitution s(subst);
return pp_def_type_mismatch(fmt, local_pp_name(lhs_fn), s.instantiate(lhs_type), s.instantiate(rhs_type));
});
pair<expr, constraint_seq> new_rhs_cs = ensure_has_type(new_rhs, rhs_type, lhs_type, j, m_relax_main_opaque);
pair<expr, constraint_seq> new_rhs_cs = ensure_has_type(new_rhs, rhs_type, lhs_type, j);
new_rhs = new_rhs_cs.first;
cs += new_rhs_cs.second;
return copy_tag(eq, mk_equation(new_lhs, new_rhs));
@ -1216,7 +1202,7 @@ expr elaborator::visit_decreasing(expr const & e, constraint_seq & cs) {
expr dec_proof = visit(decreasing_proof(e), cs);
expr f_type = mlocal_type(get_app_fn(*m_equation_lhs));
buffer<expr> ts;
type_checker & tc = *m_tc[m_relax_main_opaque];
type_checker & tc = *m_tc;
to_telescope(tc, f_type, ts, optional<binder_info>(), cs);
buffer<expr> old_args;
buffer<expr> new_args;
@ -1229,7 +1215,7 @@ expr elaborator::visit_decreasing(expr const & e, constraint_seq & cs) {
expr expected_dec_proof_type = mk_app(mk_app(*m_equation_R, new_tuple, e.get_tag()), old_tuple, e.get_tag());
expr dec_proof_type = infer_type(dec_proof, cs);
justification j = mk_type_mismatch_jst(dec_proof, dec_proof_type, expected_dec_proof_type, decreasing_proof(e));
auto new_dec_proof_cs = ensure_has_type(dec_proof, dec_proof_type, expected_dec_proof_type, j, m_relax_main_opaque);
auto new_dec_proof_cs = ensure_has_type(dec_proof, dec_proof_type, expected_dec_proof_type, j);
dec_proof = new_dec_proof_cs.first;
cs += new_dec_proof_cs.second;
return mk_decreasing(dec_app, dec_proof);
@ -1334,7 +1320,7 @@ expr elaborator::visit_structure_instance(expr const & e, constraint_seq & cs) {
S_mk = mk_app(S_mk, v, result_tag);
expr v_type = infer_type(v, cs);
justification j = mk_app_justification(S_mk, v, d_type, v_type);
auto new_v_cs = ensure_has_type(v, v_type, d_type, j, m_relax_main_opaque);
auto new_v_cs = ensure_has_type(v, v_type, d_type, j);
expr new_v = new_v_cs.first;
cs += new_v_cs.second;
S_mk = update_app(S_mk, app_fn(S_mk), new_v);
@ -1438,7 +1424,7 @@ expr elaborator::process_obtain_expr(list<obtain_struct> const & s_list, list<ex
check_R_type();
expr minor_type = whnf(binding_domain(R_type), cs);
buffer<expr> telescope;
to_telescope(*m_tc[m_relax_main_opaque], minor_type, telescope, optional<binder_info>(), cs);
to_telescope(*m_tc, minor_type, telescope, optional<binder_info>(), cs);
lean_assert(!s.is_leaf());
buffer<obtain_struct> s_buffer;
to_buffer(s.get_children(), s_buffer);
@ -1638,7 +1624,6 @@ optional<expr> elaborator::get_pre_tactic_for(expr const & mvar) {
optional<tactic> elaborator::pre_tactic_to_tactic(expr const & pre_tac) {
try {
bool relax = m_relax_main_opaque;
auto fn = [=](goal const & g, name_generator const & ngen, expr const & e, optional<expr> const & expected_type,
substitution const & subst, bool report_unassigned) {
elaborator aux_elaborator(m_ctx, ngen);
@ -1646,7 +1631,7 @@ optional<tactic> elaborator::pre_tactic_to_tactic(expr const & pre_tac) {
// We must do it otherwise, it is easy to make the system loop.
bool use_tactic_hints = false;
return aux_elaborator.elaborate_nested(g.to_context(), expected_type, e,
relax, use_tactic_hints, subst, report_unassigned);
use_tactic_hints, subst, report_unassigned);
};
return optional<tactic>(expr_to_tactic(env(), fn, pre_tac, pip()));
} catch (expr_to_tactic_exception & ex) {
@ -1813,11 +1798,10 @@ void elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name_set
return;
meta = instantiate_meta(*meta, subst);
// TODO(Leo): we are discarding constraints here
expr type = m_tc[m_relax_main_opaque]->infer(*meta).first;
expr type = m_tc->infer(*meta).first;
// first solve unassigned metavariables in type
type = solve_unassigned_mvars(subst, type, visited);
bool relax_main_opaque = m_relaxed_mvars.contains(mlocal_name(mvar));
proof_state ps = to_proof_state(*meta, type, subst, m_ngen.mk_child(), relax_main_opaque);
proof_state ps = to_proof_state(*meta, type, subst, m_ngen.mk_child());
if (auto pre_tac = get_pre_tactic_for(mvar)) {
if (is_begin_end_annotation(*pre_tac)) {
try_using_begin_end(subst, mvar, ps, *pre_tac);
@ -1924,8 +1908,7 @@ bool elaborator::display_unassigned_mvars(expr const & e, substitution const & s
expr meta = tmp_s.instantiate(*it);
expr meta_type = tmp_s.instantiate(type_checker(env()).infer(meta).first);
goal g(meta, meta_type);
bool relax = true;
proof_state ps(goals(g), s, m_ngen, constraints(), relax);
proof_state ps(goals(g), s, m_ngen, constraints());
display_unsolved_proof_state(mvar, ps, "don't know how to synthesize placeholder");
r = true;
}
@ -1982,11 +1965,10 @@ std::tuple<expr, level_param_names> elaborator::apply(substitution & s, expr con
return std::make_tuple(r, to_list(new_ps.begin(), new_ps.end()));
}
auto elaborator::operator()(list<expr> const & ctx, expr const & e, bool _ensure_type, bool relax_main_opaque)
auto elaborator::operator()(list<expr> const & ctx, expr const & e, bool _ensure_type)
-> std::tuple<expr, level_param_names> {
m_context.set_ctx(ctx);
m_full_context.set_ctx(ctx);
flet<bool> set_relax(m_relax_main_opaque, relax_main_opaque);
constraint_seq cs;
expr r = visit(e, cs);
if (_ensure_type)
@ -2000,12 +1982,10 @@ auto elaborator::operator()(list<expr> const & ctx, expr const & e, bool _ensure
return result;
}
std::tuple<expr, expr, level_param_names> elaborator::operator()(
expr const & t, expr const & v, name const & n, bool is_opaque) {
std::tuple<expr, expr, level_param_names> elaborator::operator()(expr const & t, expr const & v, name const & n) {
constraint_seq t_cs;
expr r_t = ensure_type(visit(t, t_cs), t_cs);
// Opaque definitions in the main module may treat other opaque definitions (in the main module) as transparent.
flet<bool> set_relax(m_relax_main_opaque, is_opaque);
constraint_seq v_cs;
expr r_v = visit(v, v_cs);
expr r_v_type = infer_type(r_v, v_cs);
@ -2013,7 +1993,7 @@ std::tuple<expr, expr, level_param_names> elaborator::operator()(
substitution s(subst);
return pp_def_type_mismatch(fmt, n, s.instantiate(r_t), s.instantiate(r_v_type));
});
pair<expr, constraint_seq> r_v_cs = ensure_has_type(r_v, r_v_type, r_t, j, is_opaque);
pair<expr, constraint_seq> r_v_cs = ensure_has_type(r_v, r_v_type, r_t, j);
r_v = r_v_cs.first;
constraint_seq cs = t_cs + r_v_cs.second + v_cs;
auto p = solve(cs).pull();
@ -2068,7 +2048,7 @@ static expr translate(environment const & env, list<expr> const & ctx, expr cons
/** \brief Elaborate expression \c e in context \c ctx. */
elaborate_result elaborator::elaborate_nested(list<expr> const & ctx, optional<expr> const & expected_type,
expr const & n, bool relax, bool use_tactic_hints,
expr const & n, bool use_tactic_hints,
substitution const & subst, bool report_unassigned) {
if (infom()) {
if (auto ps = get_info_tactic_proof_state()) {
@ -2084,7 +2064,6 @@ elaborate_result elaborator::elaborate_nested(list<expr> const & ctx, optional<e
m_context.set_ctx(ctx);
m_context.set_ctx(ctx);
m_full_context.set_ctx(ctx);
flet<bool> set_relax(m_relax_main_opaque, relax);
flet<bool> set_discard(m_unifier_config.m_discard, false);
flet<bool> set_use_hints(m_use_tactic_hints, use_tactic_hints);
constraint_seq cs;
@ -2104,7 +2083,7 @@ elaborate_result elaborator::elaborate_nested(list<expr> const & ctx, optional<e
display_unassigned_mvars(r, new_subst);
if (expected_type) {
justification j;
rcs = append(rcs, cls.mk_constraints(new_subst, j, relax));
rcs = append(rcs, cls.mk_constraints(new_subst, j));
}
return elaborate_result(r, new_subst, rcs);
}
@ -2112,13 +2091,13 @@ elaborate_result elaborator::elaborate_nested(list<expr> const & ctx, optional<e
static name * g_tmp_prefix = nullptr;
std::tuple<expr, level_param_names> elaborate(elaborator_context & env, list<expr> const & ctx, expr const & e,
bool relax_main_opaque, bool ensure_type, bool nice_mvar_names) {
return elaborator(env, name_generator(*g_tmp_prefix), nice_mvar_names)(ctx, e, ensure_type, relax_main_opaque);
bool ensure_type, bool nice_mvar_names) {
return elaborator(env, name_generator(*g_tmp_prefix), nice_mvar_names)(ctx, e, ensure_type);
}
std::tuple<expr, expr, level_param_names> elaborate(elaborator_context & env, name const & n, expr const & t, expr const & v,
bool is_opaque) {
return elaborator(env, name_generator(*g_tmp_prefix))(t, v, n, is_opaque);
std::tuple<expr, expr, level_param_names> elaborate(elaborator_context & env, name const & n, expr const & t,
expr const & v) {
return elaborator(env, name_generator(*g_tmp_prefix))(t, v, n);
}
void initialize_elaborator() {

32
src/frontends/lean/elaborator.h
View file

@ -32,14 +32,12 @@ class elaborator : public coercion_info_manager {
typedef std::vector<pair<expr, expr>> to_check_sorts;
elaborator_context & m_ctx;
name_generator m_ngen;
type_checker_ptr m_tc[2];
type_checker_ptr m_tc;
// mapping from metavariable ?m to the (?m l_1 ... l_n) where [l_1 ... l_n] are the local constants
// representing the context where ?m was created.
local_context m_context; // current local context: a list of local constants
local_context m_full_context; // superset of m_context, it also contains non-contextual locals.
mvar2meta m_mvar2meta;
// Set of metavariable that where created when m_relax_main_opaque flag is set to true.
name_set m_relaxed_mvars;
cache m_cache;
// The following vector contains sorts that we should check
// whether the computed universe is too specific or not.
@ -50,8 +48,6 @@ class elaborator : public coercion_info_manager {
local_tactic_hints m_local_tactic_hints;
// set of metavariables that we already reported unsolved/unassigned
name_set m_displayed_errors;
// if m_relax_main_opaque is true, then treat opaque definitions from the main module as transparent.
bool m_relax_main_opaque;
// if m_no_info is true, we do not collect information when true,
// we set is to true whenever we find no_info annotation.
bool m_no_info;
@ -82,12 +78,12 @@ class elaborator : public coercion_info_manager {
expr mk_local(name const & n, expr const & t, binder_info const & bi);
pair<expr, constraint_seq> infer_type(expr const & e) { return m_tc[m_relax_main_opaque]->infer(e); }
pair<expr, constraint_seq> whnf(expr const & e) { return m_tc[m_relax_main_opaque]->whnf(e); }
expr infer_type(expr const & e, constraint_seq & s) { return m_tc[m_relax_main_opaque]->infer(e, s); }
expr whnf(expr const & e, constraint_seq & s) { return m_tc[m_relax_main_opaque]->whnf(e, s); }
pair<expr, constraint_seq> infer_type(expr const & e) { return m_tc->infer(e); }
pair<expr, constraint_seq> whnf(expr const & e) { return m_tc->whnf(e); }
expr infer_type(expr const & e, constraint_seq & s) { return m_tc->infer(e, s); }
expr whnf(expr const & e, constraint_seq & s) { return m_tc->whnf(e, s); }
bool is_def_eq(expr const & e1, expr const & e2, justification const & j, constraint_seq & cs) {
return m_tc[m_relax_main_opaque]->is_def_eq(e1, e2, j, cs);
return m_tc->is_def_eq(e1, e2, j, cs);
}
expr mk_app(expr const & f, expr const & a, tag g) { return ::lean::mk_app(f, a, g); }
@ -118,7 +114,7 @@ class elaborator : public coercion_info_manager {
expr visit_by(expr const & e, optional<expr> const & t, constraint_seq & cs);
expr visit_by_plus(expr const & e, optional<expr> const & t, constraint_seq & cs);
expr visit_calc_proof(expr const & e, optional<expr> const & t, constraint_seq & cs);
expr add_implict_args(expr e, constraint_seq & cs, bool relax);
expr add_implict_args(expr e, constraint_seq & cs);
pair<expr, expr> ensure_fun(expr f, constraint_seq & cs);
bool has_coercions_from(expr const & a_type);
bool has_coercions_to(expr d_type);
@ -126,7 +122,7 @@ class elaborator : public coercion_info_manager {
pair<expr, constraint_seq> mk_delayed_coercion(expr const & a, expr const & a_type, expr const & expected_type,
justification const & j);
pair<expr, constraint_seq> ensure_has_type(expr const & a, expr const & a_type, expr const & expected_type,
justification const & j, bool relax);
justification const & j);
bool is_choice_app(expr const & e);
expr visit_choice_app(expr const & e, constraint_seq & cs);
@ -167,7 +163,7 @@ class elaborator : public coercion_info_manager {
expr apply(substitution & s, expr const & e, name_set & univ_params, buffer<name> & new_params);
std::tuple<expr, level_param_names> apply(substitution & s, expr const & e);
elaborate_result elaborate_nested(list<expr> const & ctx, optional<expr> const & expected_type, expr const & e,
bool relax, bool use_tactic_hints, substitution const &, bool report_unassigned);
bool use_tactic_hints, substitution const &, bool report_unassigned);
expr const & get_equation_fn(expr const & eq) const;
expr visit_equations(expr const & eqns, constraint_seq & cs);
@ -184,16 +180,14 @@ class elaborator : public coercion_info_manager {
expr visit_obtain_expr(expr const & e, constraint_seq & cs);
public:
elaborator(elaborator_context & ctx, name_generator const & ngen, bool nice_mvar_names = false);
std::tuple<expr, level_param_names> operator()(list<expr> const & ctx, expr const & e, bool _ensure_type,
bool relax_main_opaque);
std::tuple<expr, expr, level_param_names> operator()(expr const & t, expr const & v, name const & n, bool is_opaque);
std::tuple<expr, level_param_names> operator()(list<expr> const & ctx, expr const & e, bool _ensure_type);
std::tuple<expr, expr, level_param_names> operator()(expr const & t, expr const & v, name const & n);
};
std::tuple<expr, level_param_names> elaborate(elaborator_context & env, list<expr> const & ctx, expr const & e,
bool relax_main_opaque, bool ensure_type = false, bool nice_mvar_names = false);
bool ensure_type = false, bool nice_mvar_names = false);
std::tuple<expr, expr, level_param_names> elaborate(elaborator_context & env, name const & n, expr const & t, expr const & v,
bool is_opaque);
std::tuple<expr, expr, level_param_names> elaborate(elaborator_context & env, name const & n, expr const & t, expr const & v);
void initialize_elaborator();
void finalize_elaborator();
}

2
src/frontends/lean/find_cmd.cpp
View file

@ -73,7 +73,7 @@ bool match_pattern(type_checker & tc, expr const & pattern, declaration const &
cfg.m_max_steps = max_steps;
cfg.m_kind = cheap ? unifier_kind::Cheap : unifier_kind::Liberal;
cfg.m_ignore_context_check = true;
auto r = unify(tc.env(), pattern, dt, tc.mk_ngen(), true, substitution(), cfg);
auto r = unify(tc.env(), pattern, dt, tc.mk_ngen(), substitution(), cfg);
return static_cast<bool>(r.pull());
} catch (exception&) {
return false;

2
src/frontends/lean/inductive_cmd.cpp
View file

@ -113,7 +113,7 @@ struct inductive_cmd_fn {
m_u = mk_global_univ(u_name);
m_infer_result_universe = false;
m_namespace = get_namespace(m_env);
m_tc = mk_type_checker(m_env, m_p.mk_ngen(), false);
m_tc = mk_type_checker(m_env, m_p.mk_ngen());
}
[[ noreturn ]] void throw_error(char const * error_msg) { throw parser_error(error_msg, m_pos); }

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

@ -45,7 +45,7 @@ class migrate_converter : public unfold_semireducible_converter {
list<name> m_namespaces;
public:
migrate_converter(environment const & env, list<name> const & ns):
unfold_semireducible_converter(env, true, true),
unfold_semireducible_converter(env, true),
m_namespaces(ns) {
}
@ -420,7 +420,7 @@ struct migrate_cmd_fn {
m_migrate_tc = std::unique_ptr<type_checker>(new type_checker(m_env, m_ngen.mk_child(),
std::unique_ptr<converter>(new migrate_converter(m_env, get_namespaces(m_env)))));
m_tc = std::unique_ptr<type_checker>(new type_checker(m_env, m_ngen.mk_child(),
std::unique_ptr<converter>(new unfold_semireducible_converter(m_env, true, true))));
std::unique_ptr<converter>(new unfold_semireducible_converter(m_env, true))));
parse_params();
parse_from_namespace();

25
src/frontends/lean/parser.cpp
View file

@ -720,65 +720,60 @@ elaborator_context parser::mk_elaborator_context(environment const & env, local_
}
std::tuple<expr, level_param_names> parser::elaborate_relaxed(expr const & e, list<expr> const & ctx) {
bool relax = true;
bool check_unassigned = false;
bool ensure_type = false;
bool nice_mvar_names = true;
parser_pos_provider pp = get_pos_provider();
elaborator_context env = mk_elaborator_context(pp, check_unassigned);
auto r = ::lean::elaborate(env, ctx, e, relax, ensure_type, nice_mvar_names);
auto r = ::lean::elaborate(env, ctx, e, ensure_type, nice_mvar_names);
m_pre_info_manager.clear();
return r;
}
std::tuple<expr, level_param_names> parser::elaborate(expr const & e, list<expr> const & ctx) {
bool relax = false;
bool check_unassigned = true;
bool ensure_type = false;
parser_pos_provider pp = get_pos_provider();
elaborator_context env = mk_elaborator_context(pp, check_unassigned);
auto r = ::lean::elaborate(env, ctx, e, relax, ensure_type);
auto r = ::lean::elaborate(env, ctx, e, ensure_type);
m_pre_info_manager.clear();
return r;
}
std::tuple<expr, level_param_names> parser::elaborate_type(expr const & e, list<expr> const & ctx, bool clear_pre_info) {
bool relax = false;
bool check_unassigned = true;
bool ensure_type = true;
parser_pos_provider pp = get_pos_provider();
elaborator_context env = mk_elaborator_context(pp, check_unassigned);
auto r = ::lean::elaborate(env, ctx, e, relax, ensure_type);
auto r = ::lean::elaborate(env, ctx, e, ensure_type);
if (clear_pre_info)
m_pre_info_manager.clear();
return r;
}
std::tuple<expr, level_param_names> parser::elaborate_at(environment const & env, expr const & e) {
bool relax = false;
parser_pos_provider pp = get_pos_provider();
elaborator_context eenv = mk_elaborator_context(env, pp);
auto r = ::lean::elaborate(eenv, list<expr>(), e, relax);
auto r = ::lean::elaborate(eenv, list<expr>(), e);
m_pre_info_manager.clear();
return r;
}
auto parser::elaborate_definition(name const & n, expr const & t, expr const & v,
bool is_opaque)
-> std::tuple<expr, expr, level_param_names> {
auto parser::elaborate_definition(name const & n, expr const & t, expr const & v)
-> std::tuple<expr, expr, level_param_names> {
parser_pos_provider pp = get_pos_provider();
elaborator_context eenv = mk_elaborator_context(pp);
auto r = ::lean::elaborate(eenv, n, t, v, is_opaque);
auto r = ::lean::elaborate(eenv, n, t, v);
m_pre_info_manager.clear();
return r;
}
auto parser::elaborate_definition_at(environment const & env, local_level_decls const & lls,
name const & n, expr const & t, expr const & v, bool is_opaque)
name const & n, expr const & t, expr const & v)
-> std::tuple<expr, expr, level_param_names> {
parser_pos_provider pp = get_pos_provider();
elaborator_context eenv = mk_elaborator_context(env, lls, pp);
auto r = ::lean::elaborate(eenv, n, t, v, is_opaque);
auto r = ::lean::elaborate(eenv, n, t, v);
m_pre_info_manager.clear();
return r;
}
@ -1639,7 +1634,7 @@ static optional<std::string> try_file(std::string const & base, optional<unsigne
}
static std::string * g_lua_module_key = nullptr;
static void lua_module_reader(deserializer & d, module_idx, shared_environment &,
static void lua_module_reader(deserializer & d, shared_environment &,
std::function<void(asynch_update_fn const &)> &,
std::function<void(delayed_update_fn const &)> & add_delayed_update) {
name fname;

4
src/frontends/lean/parser.h
View file

@ -477,10 +477,10 @@ public:
/** \brief Elaborate \c e (making sure the result does not have metavariables). */
std::tuple<expr, level_param_names> elaborate(expr const & e) { return elaborate_at(m_env, e); }
/** \brief Elaborate the definition n : t := v */
std::tuple<expr, expr, level_param_names> elaborate_definition(name const & n, expr const & t, expr const & v, bool is_opaque);
std::tuple<expr, expr, level_param_names> elaborate_definition(name const & n, expr const & t, expr const & v);
/** \brief Elaborate the definition n : t := v in the given environment*/
std::tuple<expr, expr, level_param_names> elaborate_definition_at(environment const & env, local_level_decls const & lls,
name const & n, expr const & t, expr const & v, bool is_opaque);
name const & n, expr const & t, expr const & v);
expr mk_sorry(pos_info const & p);
bool used_sorry() const { return m_used_sorry; }

2
src/frontends/lean/server.cpp
View file

@ -767,7 +767,7 @@ bool match_type(type_checker & tc, expr const & meta, expr const & expected_type
unifier_config cfg;
cfg.m_max_steps = LEAN_FINDG_MAX_STEPS;
cfg.m_kind = unifier_kind::Cheap;
auto r = unify(tc.env(), dt, expected_type, tc.mk_ngen(), true, substitution(), cfg);
auto r = unify(tc.env(), dt, expected_type, tc.mk_ngen(), substitution(), cfg);
return static_cast<bool>(r.pull());
} catch (exception&) {
return false;

2
src/frontends/lean/structure_cmd.cpp
View file

@ -113,7 +113,7 @@ struct structure_cmd_fn {
bool m_gen_proj_mk;
structure_cmd_fn(parser & p):m_p(p), m_env(p.env()), m_ngen(p.mk_ngen()), m_namespace(get_namespace(m_env)) {
m_tc = mk_type_checker(m_env, m_p.mk_ngen(), false);
m_tc = mk_type_checker(m_env, m_p.mk_ngen());
m_infer_result_universe = false;
m_gen_eta = get_structure_eta_thm(p.get_options());
m_gen_proj_mk = get_structure_proj_mk_thm(p.get_options());

3
src/frontends/lean/theorem_queue.cpp
View file

@ -18,8 +18,7 @@ void theorem_queue::add(environment const & env, name const & n, level_param_nam
m_queue.add([=]() {
level_param_names new_ls;
expr type, value;
bool is_opaque = true; // theorems are always opaque
std::tie(type, value, new_ls) = m_parser.elaborate_definition_at(env, lls, n, t, v, is_opaque);
std::tie(type, value, new_ls) = m_parser.elaborate_definition_at(env, lls, n, t, v);
new_ls = append(ls, new_ls);
value = expand_abbreviations(env, unfold_untrusted_macros(env, value));
auto r = check(env, mk_theorem(n, new_ls, type, value));

28
src/kernel/constraint.cpp
View file

@ -16,22 +16,21 @@ struct constraint_cell {
MK_LEAN_RC()
constraint_kind m_kind;
justification m_jst;
bool m_relax_main_opaque;
constraint_cell(constraint_kind k, justification const & j, bool relax):
m_rc(1), m_kind(k), m_jst(j), m_relax_main_opaque(relax) {}
constraint_cell(constraint_kind k, justification const & j):
m_rc(1), m_kind(k), m_jst(j) {}
};
struct eq_constraint_cell : public constraint_cell {
expr m_lhs;
expr m_rhs;
eq_constraint_cell(expr const & lhs, expr const & rhs, justification const & j, bool relax):
constraint_cell(constraint_kind::Eq, j, relax),
eq_constraint_cell(expr const & lhs, expr const & rhs, justification const & j):
constraint_cell(constraint_kind::Eq, j),
m_lhs(lhs), m_rhs(rhs) {}
};
struct level_constraint_cell : public constraint_cell {
level m_lhs;
level m_rhs;
level_constraint_cell(level const & lhs, level const & rhs, justification const & j):
constraint_cell(constraint_kind::LevelEq, j, false),
constraint_cell(constraint_kind::LevelEq, j),
m_lhs(lhs), m_rhs(rhs) {}
};
struct choice_constraint_cell : public constraint_cell {
@ -40,8 +39,8 @@ struct choice_constraint_cell : public constraint_cell {
delay_factor m_delay_factor;
bool m_owner;
choice_constraint_cell(expr const & e, choice_fn const & fn, delay_factor const & f,
bool owner, justification const & j, bool relax):
constraint_cell(constraint_kind::Choice, j, relax),
bool owner, justification const & j):
constraint_cell(constraint_kind::Choice, j),
m_expr(e), m_fn(fn), m_delay_factor(f), m_owner(owner) {}
};
@ -65,16 +64,16 @@ constraint & constraint::operator=(constraint && c) { LEAN_MOVE_REF(c); }
constraint_kind constraint::kind() const { lean_assert(m_ptr); return m_ptr->m_kind; }
justification const & constraint::get_justification() const { lean_assert(m_ptr); return m_ptr->m_jst; }
constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j, bool relax_main_opaque) {
return constraint(new eq_constraint_cell(lhs, rhs, j, relax_main_opaque));
constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) {
return constraint(new eq_constraint_cell(lhs, rhs, j));
}
constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification const & j) {
return constraint(new level_constraint_cell(lhs, rhs, j));
}
constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, delay_factor const & f,
bool owner, justification const & j, bool relax_main_opaque) {
bool owner, justification const & j) {
lean_assert(is_meta(m));
return constraint(new choice_constraint_cell(m, fn, f, owner, j, relax_main_opaque));
return constraint(new choice_constraint_cell(m, fn, f, owner, j));
}
expr const & cnstr_lhs_expr(constraint const & c) {
@ -85,7 +84,6 @@ expr const & cnstr_rhs_expr(constraint const & c) {
lean_assert(is_eq_cnstr(c));
return static_cast<eq_constraint_cell*>(c.raw())->m_rhs;
}
bool relax_main_opaque(constraint const & c) { return c.raw()->m_relax_main_opaque; }
level const & cnstr_lhs_level(constraint const & c) {
lean_assert(is_level_eq_cnstr(c));
return static_cast<level_constraint_cell*>(c.raw())->m_lhs;
@ -119,13 +117,13 @@ bool cnstr_is_owner(constraint const & c) {
constraint update_justification(constraint const & c, justification const & j) {
switch (c.kind()) {
case constraint_kind::Eq:
return mk_eq_cnstr(cnstr_lhs_expr(c), cnstr_rhs_expr(c), j, relax_main_opaque(c));
return mk_eq_cnstr(cnstr_lhs_expr(c), cnstr_rhs_expr(c), j);
case constraint_kind::LevelEq:
return mk_level_eq_cnstr(cnstr_lhs_level(c), cnstr_rhs_level(c), j);
case constraint_kind::Choice:
return mk_choice_cnstr(cnstr_expr(c), cnstr_choice_fn(c),
static_cast<choice_constraint_cell*>(c.raw())->m_delay_factor,
cnstr_is_owner(c), j, relax_main_opaque(c));
cnstr_is_owner(c), j);
}
lean_unreachable(); // LCOV_EXCL_LINE
}

16
src/kernel/constraint.h
View file

@ -77,10 +77,10 @@ public:
friend bool is_eqp(constraint const & c1, constraint const & c2) { return c1.m_ptr == c2.m_ptr; }
friend void swap(constraint & l1, constraint & l2) { std::swap(l1, l2); }
friend constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j, bool relax_main_opaque);
friend constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j);
friend constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification const & j);
friend constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, delay_factor const & f, bool owner,
justification const & j, bool relax_main_opaque);
justification const & j);
constraint_cell * raw() const { return m_ptr; }
};
@ -88,10 +88,8 @@ public:
inline bool operator==(constraint const & c1, constraint const & c2) { return c1.raw() == c2.raw(); }
inline bool operator!=(constraint const & c1, constraint const & c2) { return !(c1 == c2); }
/** \brief Create a unification constraint lhs =?= rhs
If \c relax_main_opaque is true, then opaque definitions from the main module are treated as transparent.
*/
constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j, bool relax_main_opaque);
/** \brief Create a unification constraint lhs =?= rhs */
constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j);
constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification const & j);
/** \brief Create a "choice" constraint m in fn(...), where fn produces a stream of possible solutions.
@ -100,11 +98,9 @@ constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification
The variable will be assigned by the choice constraint, and the elaborator should just check whether a solution
produced by fn satisfies the other constraints or not.
\c j is a justification for the constraint.
If \c relax_main_opaque is true, then it signs that constraint was created in a context where
opaque constants of the main module can be treated as transparent.
*/
constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, delay_factor const & f,
bool owner, justification const & j, bool relax_main_opaque);
bool owner, justification const & j);
inline bool is_eq_cnstr(constraint const & c) { return c.kind() == constraint_kind::Eq; }
inline bool is_level_eq_cnstr(constraint const & c) { return c.kind() == constraint_kind::LevelEq; }
@ -116,8 +112,6 @@ constraint update_justification(constraint const & c, justification const & j);
expr const & cnstr_lhs_expr(constraint const & c);
/** \brief Return the rhs of an equality constraint. */
expr const & cnstr_rhs_expr(constraint const & c);
/** \brief Return true iff opaque definitions from the main module should be treated as transparent. */
bool relax_main_opaque(constraint const & c);
/** \brief Return the lhs of an level constraint. */
level const & cnstr_lhs_level(constraint const & c);
/** \brief Return the rhs of an level constraint. */

1
src/kernel/converter.cpp
View file

@ -35,7 +35,6 @@ struct dummy_converter : public converter {
virtual pair<bool, constraint_seq> is_def_eq(expr const &, expr const &, type_checker &, delayed_justification &) {
return mk_pair(true, constraint_seq());
}
virtual optional<module_idx> get_module_idx() const { return optional<module_idx>(); }
virtual bool is_opaque(declaration const &) const { return false; }
virtual optional<declaration> is_delta(expr const &) const { return optional<declaration>(); }
virtual bool is_stuck(expr const &, type_checker &) { return false; }

1
src/kernel/converter.h
View file

@ -18,7 +18,6 @@ protected:
extension_context & get_extension(type_checker & tc);
public:
virtual ~converter() {}
virtual optional<module_idx> get_module_idx() const = 0;
virtual bool is_opaque(declaration const & d) const = 0;
virtual optional<declaration> is_delta(expr const & e) const = 0;

20
src/kernel/declaration.cpp
View file

@ -18,7 +18,6 @@ struct declaration::cell {
optional<expr> m_value; // if none, then declaration is actually a postulate
// The following fields are only meaningful for definitions (which are not theorems)
unsigned m_weight;
unsigned m_module_idx; // module idx where it was defined
bool m_opaque;
// The following field affects the convertability checker.
// Let f be this definition, then if the following field is true,
@ -31,11 +30,11 @@ struct declaration::cell {
cell(name const & n, level_param_names const & params, expr const & t, bool is_axiom):
m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_axiom),
m_weight(0), m_module_idx(0), m_opaque(true), m_use_conv_opt(false) {}
m_weight(0), m_opaque(true), m_use_conv_opt(false) {}
cell(name const & n, level_param_names const & params, expr const & t, bool is_thm, expr const & v,
bool opaque, unsigned w, module_idx mod_idx, bool use_conv_opt):
bool opaque, unsigned w, bool use_conv_opt):
m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_thm),
m_value(v), m_weight(w), m_module_idx(mod_idx), m_opaque(opaque), m_use_conv_opt(use_conv_opt) {}
m_value(v), m_weight(w), m_opaque(opaque), m_use_conv_opt(use_conv_opt) {}
};
static declaration * g_dummy = nullptr;
@ -62,15 +61,14 @@ expr const & declaration::get_type() const { return m_ptr->m_type; }
bool declaration::is_opaque() const { return m_ptr->m_opaque; }
expr const & declaration::get_value() const { lean_assert(is_definition()); return *(m_ptr->m_value); }
unsigned declaration::get_weight() const { return m_ptr->m_weight; }
module_idx declaration::get_module_idx() const { return m_ptr->m_module_idx; }
bool declaration::use_conv_opt() const { return m_ptr->m_use_conv_opt; }
declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v,
bool opaque, unsigned weight, module_idx mod_idx, bool use_conv_opt) {
return declaration(new declaration::cell(n, params, t, false, v, opaque, weight, mod_idx, use_conv_opt));
bool opaque, unsigned weight, bool use_conv_opt) {
return declaration(new declaration::cell(n, params, t, false, v, opaque, weight, use_conv_opt));
}
declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v,
bool opaque, module_idx mod_idx, bool use_conv_opt) {
bool opaque, bool use_conv_opt) {
unsigned w = 0;
for_each(v, [&](expr const & e, unsigned) {
if (is_constant(e)) {
@ -80,10 +78,10 @@ declaration mk_definition(environment const & env, name const & n, level_param_n
}
return true;
});
return mk_definition(n, params, t, v, opaque, w+1, mod_idx, use_conv_opt);
return mk_definition(n, params, t, v, opaque, w+1, use_conv_opt);
}
declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v, module_idx mod_idx) {
return declaration(new declaration::cell(n, params, t, true, v, true, 0, mod_idx, false));
declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v) {
return declaration(new declaration::cell(n, params, t, true, v, true, 0, false));
}
declaration mk_axiom(name const & n, level_param_names const & params, expr const & t) {
return declaration(new declaration::cell(n, params, t, true));

28
src/kernel/declaration.h
View file

@ -12,21 +12,6 @@ Author: Leonardo de Moura
#include "kernel/expr.h"
namespace lean {
/**
\brief Module index. The kernel provides only basic support
for implementing a module system outside of the kernel.
We need at least the notion of module index in the kernel, because
it affects the convertability procedure.
Given an opaque definition (non-theorem) d in module m1, then d is considered
to be transparent for any other opaque definition in module m1.
*/
typedef unsigned module_idx;
/** \brief The main module is the module being currently compiled. We always assigned it the index 0. */
constexpr module_idx g_main_module_idx = 0;
constexpr module_idx g_null_module_idx = std::numeric_limits<unsigned>::max();
/** \brief Environment definitions, theorems, axioms and variable declarations. */
class declaration {
struct cell;
@ -67,14 +52,13 @@ public:
expr const & get_value() const;
bool is_opaque() const;
unsigned get_weight() const;
module_idx get_module_idx() const;
bool use_conv_opt() const;
friend declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t,
expr const & v, bool opaque, module_idx mod_idx, bool use_conv_opt);
expr const & v, bool opaque, bool use_conv_opt);
friend declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v, bool opaque,
unsigned weight, module_idx mod_idx, bool use_conv_opt);
friend declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v, module_idx mod_idx);
unsigned weight, bool use_conv_opt);
friend declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v);
friend declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
friend declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t);
};
@ -84,10 +68,10 @@ inline optional<declaration> some_declaration(declaration const & o) { return op
inline optional<declaration> some_declaration(declaration && o) { return optional<declaration>(std::forward<declaration>(o)); }
declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v,
bool opaque = false, unsigned weight = 0, module_idx mod_idx = 0, bool use_conv_opt = true);
bool opaque = false, unsigned weight = 0, bool use_conv_opt = true);
declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v,
bool opaque = false, module_idx mod_idx = 0, bool use_conv_opt = true);
declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v, module_idx mod_idx = 0);
bool opaque = false, bool use_conv_opt = true);
declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v);
declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t);

10
src/kernel/default_converter.cpp
View file

@ -14,17 +14,14 @@ Author: Leonardo de Moura
namespace lean {
static expr * g_dont_care = nullptr;
default_converter::default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize):
m_env(env), m_module_idx(mod_idx), m_memoize(memoize) {
default_converter::default_converter(environment const & env, bool memoize):
m_env(env), m_memoize(memoize) {
m_tc = nullptr;
m_jst = nullptr;
}
default_converter::default_converter(environment const & env, bool relax_main_opaque, bool memoize):
default_converter(env, relax_main_opaque ? optional<module_idx>(0) : optional<module_idx>(), memoize) {}
constraint default_converter::mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) {
return ::lean::mk_eq_cnstr(lhs, rhs, j, static_cast<bool>(m_module_idx));
return ::lean::mk_eq_cnstr(lhs, rhs, j);
}
optional<expr> default_converter::expand_macro(expr const & m) {
@ -115,7 +112,6 @@ bool default_converter::is_opaque(declaration const & d) const {
lean_assert(d.is_definition());
if (d.is_theorem()) return true; // theorems are always opaque
if (!d.is_opaque()) return false; // d is a transparent definition
if (m_module_idx && d.get_module_idx() == *m_module_idx) return false; // the opaque definitions in mod_idx are considered transparent
return true; // d is opaque
}

5
src/kernel/default_converter.h
View file

@ -17,7 +17,6 @@ namespace lean {
class default_converter : public converter {
protected:
environment m_env;
optional<module_idx> m_module_idx;
bool m_memoize;
expr_struct_map<expr> m_whnf_core_cache;
expr_struct_map<pair<expr, constraint_seq>> m_whnf_cache;
@ -73,12 +72,10 @@ protected:
pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s);
public:
default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize = true);
default_converter(environment const & env, bool relax_main_opaque, bool memoize = true);
default_converter(environment const & env, bool memoize = true);
virtual optional<declaration> is_delta(expr const & e) const;
virtual bool is_opaque(declaration const & d) const;
virtual optional<module_idx> get_module_idx() const { return m_module_idx; }
virtual bool is_stuck(expr const & e, type_checker & c);
virtual pair<expr, constraint_seq> whnf(expr const & e_prime, type_checker & c);

13
src/kernel/type_checker.cpp
View file

@ -85,7 +85,7 @@ pair<expr, expr> type_checker::open_binding_body(expr const & e) {
}
constraint type_checker::mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) {
return ::lean::mk_eq_cnstr(lhs, rhs, j, static_cast<bool>(m_conv->get_module_idx()));
return ::lean::mk_eq_cnstr(lhs, rhs, j);
}
/**
@ -422,12 +422,12 @@ type_checker::type_checker(environment const & env, name_generator const & g, st
}
type_checker::type_checker(environment const & env, name_generator const & g, bool memoize):
type_checker(env, g, std::unique_ptr<converter>(new default_converter(env, optional<module_idx>(), memoize)), memoize) {}
type_checker(env, g, std::unique_ptr<converter>(new default_converter(env, memoize)), memoize) {}
static name * g_tmp_prefix = nullptr;
type_checker::type_checker(environment const & env):
type_checker(env, name_generator(*g_tmp_prefix), std::unique_ptr<converter>(new default_converter(env, optional<module_idx>())), true) {}
type_checker(env, name_generator(*g_tmp_prefix), std::unique_ptr<converter>(new default_converter(env)), true) {}
type_checker::~type_checker() {}
@ -479,14 +479,11 @@ certified_declaration check(environment const & env, declaration const & d, name
check_name(env, d.get_name());
check_duplicated_params(env, d);
bool memoize = true;
type_checker checker1(env, g, std::unique_ptr<converter>(new default_converter(env, optional<module_idx>(), memoize)));
type_checker checker1(env, g, std::unique_ptr<converter>(new default_converter(env, memoize)));
expr sort = checker1.check(d.get_type(), d.get_univ_params()).first;
checker1.ensure_sort(sort, d.get_type());
if (d.is_definition()) {
optional<module_idx> midx;
if (d.is_opaque())
midx = optional<module_idx>(d.get_module_idx());
type_checker checker2(env, g, std::unique_ptr<converter>(new default_converter(env, midx, memoize)));
type_checker checker2(env, g, std::unique_ptr<converter>(new default_converter(env, memoize)));
expr val_type = checker2.check(d.get_value(), d.get_univ_params()).first;
if (!checker2.is_def_eq(val_type, d.get_type()).first) {
throw_kernel_exception(env, d.get_value(), [=](formatter const & fmt) {

2
src/library/class.cpp
View file

@ -187,7 +187,7 @@ environment add_instance(environment const & env, name const & n, unsigned prior
declaration d = env.get(n);
expr type = d.get_type();
name_generator ngen(*g_tmp_prefix);
auto tc = mk_type_checker(env, ngen, false);
auto tc = mk_type_checker(env, ngen);
while (true) {
type = tc->whnf(type).first;
if (!is_pi(type))

4
src/library/definitional/brec_on.cpp
View file

@ -144,7 +144,7 @@ static environment mk_below(environment const & env, name const & n, bool ibelow
bool opaque = false;
bool use_conv_opt = true;
declaration new_d = mk_definition(env, below_name, blvls, below_type, below_value,
opaque, rec_decl.get_module_idx(), use_conv_opt);
opaque, use_conv_opt);
environment new_env = module::add(env, check(env, new_d));
new_env = set_reducible(new_env, below_name, reducible_status::Reducible);
if (!ibelow)
@ -331,7 +331,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind)
bool opaque = false;
bool use_conv_opt = true;
declaration new_d = mk_definition(env, brec_on_name, blps, brec_on_type, brec_on_value,
opaque, rec_decl.get_module_idx(), use_conv_opt);
opaque, use_conv_opt);
environment new_env = module::add(env, check(env, new_d));
new_env = set_reducible(new_env, brec_on_name, reducible_status::Reducible);
if (!ind)

2
src/library/definitional/cases_on.cpp
View file

@ -180,7 +180,7 @@ environment mk_cases_on(environment const & env, name const & n) {
bool opaque = false;
bool use_conv_opt = true;
declaration new_d = mk_definition(env, cases_on_name, rec_decl.get_univ_params(), cases_on_type, cases_on_value,
opaque, rec_decl.get_module_idx(), use_conv_opt);
opaque, use_conv_opt);
environment new_env = module::add(env, check(env, new_d));
new_env = set_reducible(new_env, cases_on_name, reducible_status::Reducible);
new_env = add_unfold_c_hint(new_env, cases_on_name, cases_on_major_idx);

7
src/library/definitional/equations.cpp
View file

@ -1721,8 +1721,7 @@ class equation_compiler_fn {
public:
equation_compiler_fn(type_checker & tc, io_state const & ios, expr const & meta, expr const & meta_type,
bool /* relax */):
equation_compiler_fn(type_checker & tc, io_state const & ios, expr const & meta, expr const & meta_type):
m_tc(tc), m_ios(ios), m_meta(meta), m_meta_type(meta_type) {
get_app_args(m_meta, m_global_context);
}
@ -1746,7 +1745,7 @@ public:
};
expr compile_equations(type_checker & tc, io_state const & ios, expr const & eqns,
expr const & meta, expr const & meta_type, bool relax) {
return equation_compiler_fn(tc, ios, meta, meta_type, relax)(eqns);
expr const & meta, expr const & meta_type) {
return equation_compiler_fn(tc, ios, meta, meta_type)(eqns);
}
}

2
src/library/definitional/equations.h
View file

@ -42,7 +42,7 @@ expr mk_inaccessible(expr const & e);
bool is_inaccessible(expr const & e);
expr compile_equations(type_checker & tc, io_state const & ios, expr const & eqns,
expr const & meta, expr const & meta_type, bool relax);
expr const & meta, expr const & meta_type);
/** \brief Return true if \c e is an auxiliary macro used to store the result of mutually recursive declarations.
For example, if a set of recursive equations is defining \c n mutually recursive functions, we wrap

4
src/library/definitional/induction_on.cpp
View file

@ -32,7 +32,7 @@ environment mk_induction_on(environment const & env, name const & n) {
certified_declaration cdecl = check(new_env,
mk_definition(new_env, induction_on_name, rec_on_decl.get_univ_params(),
rec_on_decl.get_type(), rec_on_decl.get_value(),
opaque, rec_on_decl.get_module_idx(), use_conv_opt));
opaque, use_conv_opt));
new_env = module::add(new_env, cdecl);
} else {
level_param_names induction_on_univs = tail(rec_on_decl.get_univ_params());
@ -43,7 +43,7 @@ environment mk_induction_on(environment const & env, name const & n) {
certified_declaration cdecl = check(new_env,
mk_definition(new_env, induction_on_name, induction_on_univs,
induction_on_type, induction_on_value,
opaque, rec_on_decl.get_module_idx(), use_conv_opt));
opaque, use_conv_opt));
new_env = module::add(new_env, cdecl);
}
return add_protected(new_env, induction_on_name);

4
src/library/definitional/no_confusion.cpp
View file

@ -137,7 +137,7 @@ optional<environment> mk_no_confusion_type(environment const & env, name const &
bool opaque = false;
bool use_conv_opt = true;
declaration new_d = mk_definition(env, no_confusion_type_name, lps, no_confusion_type_type, no_confusion_type_value,
opaque, ind_decl.get_module_idx(), use_conv_opt);
opaque, use_conv_opt);
environment new_env = module::add(env, check(env, new_d));
new_env = set_reducible(new_env, no_confusion_type_name, reducible_status::Reducible);
return some(add_protected(new_env, no_confusion_type_name));
@ -272,7 +272,7 @@ environment mk_no_confusion(environment const & env, name const & n) {
bool opaque = false;
bool use_conv_opt = true;
declaration new_d = mk_definition(new_env, no_confusion_name, lps, no_confusion_ty, no_confusion_val,
opaque, no_confusion_type_decl.get_module_idx(), use_conv_opt);
opaque, use_conv_opt);
new_env = module::add(new_env, check(new_env, new_d));
new_env = set_reducible(new_env, no_confusion_name, reducible_status::Reducible);
return add_protected(new_env, no_confusion_name);

2
src/library/definitional/projection.cpp
View file

@ -132,7 +132,7 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
bool opaque = false;
bool use_conv_opt = false;
declaration new_d = mk_definition(env, proj_name, lvl_params, proj_type, proj_val,
opaque, rec_decl.get_module_idx(), use_conv_opt);
opaque, use_conv_opt);
new_env = module::add(new_env, check(new_env, new_d));
new_env = set_reducible(new_env, proj_name, reducible_status::Reducible);
new_env = add_unfold_c_hint(new_env, proj_name, nparams);

2
src/library/definitional/rec_on.cpp
View file

@ -58,7 +58,7 @@ environment mk_rec_on(environment const & env, name const & n) {
environment new_env = module::add(env,
check(env, mk_definition(env, rec_on_name, rec_decl.get_univ_params(),
rec_on_type, rec_on_val,
opaque, rec_decl.get_module_idx(), use_conv_opt)));
opaque, use_conv_opt)));
new_env = set_reducible(new_env, rec_on_name, reducible_status::Reducible);
new_env = add_unfold_c_hint(new_env, rec_on_name, rec_on_major_idx);
return add_protected(new_env, rec_on_name);

15
src/library/inductive_unifier_plugin.cpp
View file

@ -45,7 +45,7 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
*/
lazy_list<constraints> add_elim_meta_cnstrs(type_checker & tc, name_generator ngen, inductive::inductive_decl const & decl,
expr const & elim, buffer<expr> & args, expr const & t, justification const & j,
constraint_seq cs, bool relax) const {
constraint_seq cs) const {
lean_assert(is_constant(elim));
environment const & env = tc.env();
levels elim_lvls = const_levels(elim);
@ -75,10 +75,10 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
hint = mk_app(hint, mk_app(mk_aux_metavar_for(ngen, mtype), margs));
intro_type = tc.whnf(binding_body(intro_type), cs_intro);
}
constraint c1 = mk_eq_cnstr(meta, hint, j, relax);
constraint c1 = mk_eq_cnstr(meta, hint, j);
args[major_idx] = hint;
expr reduce_elim = tc.whnf(mk_app(elim, args), cs_intro);
constraint c2 = mk_eq_cnstr(reduce_elim, t, j, relax);
constraint c2 = mk_eq_cnstr(reduce_elim, t, j);
cs_intro = constraint_seq(c1) + constraint_seq(c2) + cs_intro;
buffer<constraint> cs_buffer;
cs_intro.linearize(cs_buffer);
@ -88,7 +88,7 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
}
lazy_list<constraints> process_elim_meta_core(type_checker & tc, name_generator const & ngen,
expr const & lhs, expr const & rhs, justification const & j, bool relax) const {
expr const & lhs, expr const & rhs, justification const & j) const {
lean_assert(inductive::is_elim_meta_app(tc, lhs));
auto dcs = tc.is_def_eq_types(lhs, rhs, j);
if (!dcs.first)
@ -101,7 +101,7 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
auto decls = *inductive::is_inductive_decl(env, it_name);
for (auto const & d : std::get<2>(decls)) {
if (inductive::inductive_decl_name(d) == it_name)
return add_elim_meta_cnstrs(tc, ngen, d, elim, args, rhs, j, cs, relax);
return add_elim_meta_cnstrs(tc, ngen, d, elim, args, rhs, j, cs);
}
lean_unreachable(); // LCOV_EXCL_LINE
}
@ -117,11 +117,10 @@ public:
expr const & lhs = cnstr_lhs_expr(c);
expr const & rhs = cnstr_rhs_expr(c);
justification const & j = c.get_justification();
bool relax = relax_main_opaque(c);
if (inductive::is_elim_meta_app(tc, lhs))
return process_elim_meta_core(tc, ngen, lhs, rhs, j, relax);
return process_elim_meta_core(tc, ngen, lhs, rhs, j);
else if (inductive::is_elim_meta_app(tc, rhs))
return process_elim_meta_core(tc, ngen, rhs, lhs, j, relax);
return process_elim_meta_core(tc, ngen, rhs, lhs, j);
else
return lazy_list<constraints>();
}

49
src/library/kernel_bindings.cpp
View file

@ -753,7 +753,6 @@ static int declaration_get_value(lua_State * L) {
throw exception("arg #1 must be a definition");
}
static int declaration_get_weight(lua_State * L) { return push_integer(L, to_declaration(L, 1).get_weight()); }
static int declaration_get_module_idx(lua_State * L) { return push_integer(L, to_declaration(L, 1).get_module_idx()); }
static int mk_constant_assumption(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs == 2)
@ -775,38 +774,37 @@ static int mk_theorem(lua_State * L) {
else
return push_declaration(L, mk_theorem(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3), to_expr(L, 4)));
}
static void get_definition_args(lua_State * L, int idx, bool & opaque, unsigned & weight, module_idx & mod_idx, bool & use_conv_opt) {
static void get_definition_args(lua_State * L, int idx, bool & opaque, unsigned & weight, bool & use_conv_opt) {
opaque = get_bool_named_param(L, idx, "opaque", opaque);
use_conv_opt = get_bool_named_param(L, idx, "use_conv_opt", use_conv_opt);
mod_idx = get_uint_named_param(L, idx, "module_idx", mod_idx);
weight = get_uint_named_param(L, idx, "weight", weight);
}
static int mk_definition(lua_State * L) {
int nargs = lua_gettop(L);
bool opaque = true; unsigned weight = 0; module_idx mod_idx = 0; bool use_conv_opt = true;
bool opaque = false; unsigned weight = 0; bool use_conv_opt = true;
if (nargs < 3) {
throw exception("mk_definition must have at least 3 arguments");
} else if (is_environment(L, 1)) {
if (nargs < 4) {
throw exception("mk_definition must have at least 4 arguments, when the first argument is an environment");
} else if (is_expr(L, 3)) {
get_definition_args(L, 5, opaque, weight, mod_idx, use_conv_opt);
get_definition_args(L, 5, opaque, weight, use_conv_opt);
return push_declaration(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), level_param_names(),
to_expr(L, 3), to_expr(L, 4), opaque, mod_idx, use_conv_opt));
to_expr(L, 3), to_expr(L, 4), opaque, use_conv_opt));
} else {
get_definition_args(L, 6, opaque, weight, mod_idx, use_conv_opt);
get_definition_args(L, 6, opaque, weight, use_conv_opt);
return push_declaration(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), to_level_param_names(L, 3),
to_expr(L, 4), to_expr(L, 5), opaque, mod_idx, use_conv_opt));
to_expr(L, 4), to_expr(L, 5), opaque, use_conv_opt));
}
} else {
if (is_expr(L, 2)) {
get_definition_args(L, 4, opaque, weight, mod_idx, use_conv_opt);
get_definition_args(L, 4, opaque, weight, use_conv_opt);
return push_declaration(L, mk_definition(to_name_ext(L, 1), level_param_names(), to_expr(L, 2),
to_expr(L, 3), opaque, weight, mod_idx, use_conv_opt));
to_expr(L, 3), opaque, weight, use_conv_opt));
} else {
get_definition_args(L, 5, opaque, weight, mod_idx, use_conv_opt);
get_definition_args(L, 5, opaque, weight, use_conv_opt);
return push_declaration(L, mk_definition(to_name_ext(L, 1), to_level_param_names(L, 2),
to_expr(L, 3), to_expr(L, 4), opaque, weight, mod_idx, use_conv_opt));
to_expr(L, 3), to_expr(L, 4), opaque, weight, use_conv_opt));
}
}
}
@ -824,7 +822,6 @@ static const struct luaL_Reg declaration_m[] = {
{"type", safe_function<declaration_get_type>},
{"value", safe_function<declaration_get_value>},
{"weight", safe_function<declaration_get_weight>},
{"module_idx", safe_function<declaration_get_module_idx>},
{0, 0}
};
@ -1481,8 +1478,7 @@ static int constraint_tostring(lua_State * L) {
static int mk_eq_cnstr(lua_State * L) {
int nargs = lua_gettop(L);
return push_constraint(L, mk_eq_cnstr(to_expr(L, 1), to_expr(L, 2),
nargs >= 3 ? to_justification(L, 3) : justification(),
nargs >= 4 && lua_toboolean(L, 4)));
nargs >= 3 ? to_justification(L, 3) : justification()));
}
static int mk_level_eq_cnstr(lua_State * L) {
int nargs = lua_gettop(L);
@ -1512,7 +1508,7 @@ static choice_fn to_choice_fn(lua_State * L, int idx) {
if (is_constraint(L, -1))
r.push_back(constraints(to_constraint(L, -1)));
else if (is_expr(L, -1))
r.push_back(constraints(mk_eq_cnstr(mvar, to_expr(L, -1), justification(), false)));
r.push_back(constraints(mk_eq_cnstr(mvar, to_expr(L, -1), justification())));
else
r.push_back(to_list_constraint_ext(L, -1));
lua_pop(L, 1);
@ -1530,19 +1526,16 @@ static int mk_choice_cnstr(lua_State * L) {
expr m = to_expr(L, 1);
choice_fn fn = to_choice_fn(L, 2);
if (nargs == 2)
return push_constraint(L, mk_choice_cnstr(m, fn, 0, false, justification(), false));
return push_constraint(L, mk_choice_cnstr(m, fn, 0, false, justification()));
else if (nargs == 3 && is_justification(L, 3))
return push_constraint(L, mk_choice_cnstr(m, fn, 0, false, to_justification(L, 3), false));
return push_constraint(L, mk_choice_cnstr(m, fn, 0, false, to_justification(L, 3)));
else if (nargs == 3)
return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), false, justification(), false));
return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), false, justification()));
else if (nargs == 4)
return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), lua_toboolean(L, 4), justification(), false));
else if (nargs == 5)
return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), lua_toboolean(L, 4),
to_justification(L, 5), false));
return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), lua_toboolean(L, 4), justification()));
else
return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), lua_toboolean(L, 4),
to_justification(L, 5), lua_toboolean(L, 6)));
to_justification(L, 5)));
}
static int constraint_expr(lua_State * L) {
@ -1796,13 +1789,9 @@ static int mk_type_checker_with_hints(lua_State * L) {
environment const & env = to_environment(L, 1);
int nargs = lua_gettop(L);
if (nargs == 1) {
return push_type_checker_ref(L, mk_type_checker(env, name_generator(*g_tmp_prefix), false));
} else if (nargs == 2 && lua_isboolean(L, 2)) {
return push_type_checker_ref(L, mk_type_checker(env, name_generator(*g_tmp_prefix), lua_toboolean(L, 2)));
} else if (nargs == 2) {
return push_type_checker_ref(L, mk_type_checker(env, to_name_generator(L, 2), false));
return push_type_checker_ref(L, mk_type_checker(env, name_generator(*g_tmp_prefix)));
} else {
return push_type_checker_ref(L, mk_type_checker(env, to_name_generator(L, 2), lua_toboolean(L, 3)));
return push_type_checker_ref(L, mk_type_checker(env, to_name_generator(L, 2)));
}
}

6
src/library/kernel_serializer.cpp
View file

@ -298,7 +298,7 @@ serializer & operator<<(serializer & s, declaration const & d) {
return s;
}
declaration read_declaration(deserializer & d, module_idx midx) {
declaration read_declaration(deserializer & d) {
char k = d.read_char();
bool has_value = (k & 1) != 0;
bool is_th_ax = (k & 8) != 0;
@ -308,12 +308,12 @@ declaration read_declaration(deserializer & d, module_idx midx) {
if (has_value) {
expr v = read_expr(d);
if (is_th_ax) {
return mk_theorem(n, ps, t, v, midx);
return mk_theorem(n, ps, t, v);
} else {
unsigned w = d.read_unsigned();
bool is_opaque = (k & 2) != 0;
bool use_conv_opt = (k & 4) != 0;
return mk_definition(n, ps, t, v, is_opaque, w, midx, use_conv_opt);
return mk_definition(n, ps, t, v, is_opaque, w, use_conv_opt);
}
} else {
if (is_th_ax)

2
src/library/kernel_serializer.h
View file

@ -27,7 +27,7 @@ expr read_expr(deserializer & d);
inline deserializer & operator>>(deserializer & d, expr & e) { e = read_expr(d); return d; }
serializer & operator<<(serializer & s, declaration const & d);
declaration read_declaration(deserializer & d, module_idx midx);
declaration read_declaration(deserializer & d);
typedef std::tuple<level_param_names, unsigned, list<inductive::inductive_decl>> inductive_decls;
serializer & operator<<(serializer & s, inductive_decls const & ds);

8
src/library/metavar_closure.cpp
View file

@ -45,10 +45,10 @@ void metavar_closure::for_each_level_mvar(std::function<void(level const &)> con
m_lvl_mvars.for_each(fn);
}
void metavar_closure::mk_constraints(substitution s, justification const & j, bool relax, buffer<constraint> & r) const {
void metavar_closure::mk_constraints(substitution s, justification const & j, buffer<constraint> & r) const {
m_expr_mvars.for_each([&](expr const & m) {
if (s.is_expr_assigned(mlocal_name(m)))
r.push_back(mk_eq_cnstr(m, s.instantiate(m), j, relax));
r.push_back(mk_eq_cnstr(m, s.instantiate(m), j));
});
m_lvl_mvars.for_each([&](level const & m) {
if (s.is_level_assigned(meta_id(m)))
@ -56,9 +56,9 @@ void metavar_closure::mk_constraints(substitution s, justification const & j, bo
});
}
constraints metavar_closure::mk_constraints(substitution s, justification const & j, bool relax) const {
constraints metavar_closure::mk_constraints(substitution s, justification const & j) const {
buffer<constraint> cs;
mk_constraints(s, j, relax, cs);
mk_constraints(s, j, cs);
return to_list(cs.begin(), cs.end());
}
}

6
src/library/metavar_closure.h
View file

@ -30,10 +30,10 @@ class metavar_closure {
void for_each_expr_mvar(std::function<void(expr const &)> const & fn) const;
void for_each_level_mvar(std::function<void(level const &)> const & fn) const;
/** \brief For each collected metavariable ?m, store in \c r constraints of the form ?m =?= s(?m)
if ?m is assigned by \c s. The constraints are justified by \c j and \c relax
if ?m is assigned by \c s. The constraints are justified by \c j
\see mk_eq_cnstr
*/
void mk_constraints(substitution s, justification const & j, bool relax, buffer<constraint> & r) const;
constraints mk_constraints(substitution s, justification const & j, bool relax) const;
void mk_constraints(substitution s, justification const & j, buffer<constraint> & r) const;
constraints mk_constraints(substitution s, justification const & j) const;
};
}

20
src/library/module.cpp
View file

@ -232,7 +232,7 @@ environment declare_quotient(environment const & env) {
return add(new_env, *g_quotient, [=](serializer &) {});
}
static void quotient_reader(deserializer &, module_idx, shared_environment & senv,
static void quotient_reader(deserializer &, shared_environment & senv,
std::function<void(asynch_update_fn const &)> &,
std::function<void(delayed_update_fn const &)> &) {
senv.update([&](environment const & env) {
@ -245,7 +245,7 @@ environment declare_hits(environment const & env) {
return add(new_env, *g_hits, [=](serializer &) {});
}
static void hits_reader(deserializer &, module_idx, shared_environment & senv,
static void hits_reader(deserializer &, shared_environment & senv,
std::function<void(asynch_update_fn const &)> &,
std::function<void(delayed_update_fn const &)> &) {
senv.update([&](environment const & env) {
@ -266,7 +266,7 @@ environment add_inductive(environment env,
});
}
static void inductive_reader(deserializer & d, module_idx, shared_environment & senv,
static void inductive_reader(deserializer & d, shared_environment & senv,
std::function<void(asynch_update_fn const &)> &,
std::function<void(delayed_update_fn const &)> &) {
inductive_decls ds = read_inductive_decls(d);
@ -282,7 +282,7 @@ environment add_inductive(environment const & env, name const & ind_name, level_
} // end of namespace module
struct import_modules_fn {
typedef std::tuple<module_idx, unsigned, delayed_update_fn> delayed_update;
typedef std::tuple<unsigned, unsigned, delayed_update_fn> delayed_update;
shared_environment m_senv;
unsigned m_num_threads;
bool m_keep_proofs;
@ -367,7 +367,7 @@ struct import_modules_fn {
module_info_ptr r = std::make_shared<module_info>();
r->m_fname = fname;
r->m_counter = 0;
r->m_module_idx = g_null_module_idx;
r->m_module_idx = 0;
m_import_counter++;
std::string new_base = dirname(fname.c_str());
std::swap(r->m_obj_code, code);
@ -407,9 +407,9 @@ struct import_modules_fn {
return mk_axiom(decl.get_name(), decl.get_univ_params(), decl.get_type());
}
void import_decl(deserializer & d, module_idx midx) {
declaration decl = read_declaration(d, midx);
lean_assert(!decl.is_definition() || decl.get_module_idx() == midx);
void import_decl(deserializer & d) {
declaration decl = read_declaration(d);
lean_assert(!decl.is_definition());
environment env = m_senv.env();
decl = unfold_untrusted_macros(env, decl);
if (decl.get_name() == get_sorry_name() && has_sorry(env))
@ -465,7 +465,7 @@ struct import_modules_fn {
if (k == g_olean_end_file) {
break;
} else if (k == *g_decl_key) {
import_decl(d, r->m_module_idx);
import_decl(d);
} else if (k == *g_glvl_key) {
import_universe(d);
} else {
@ -473,7 +473,7 @@ struct import_modules_fn {
auto it = readers.find(k);
if (it == readers.end())
throw exception(sstream() << "file '" << r->m_fname << "' has been corrupted, unknown object");
it->second(d, r->m_module_idx, m_senv, add_asynch_update, add_delayed_update);
it->second(d, m_senv, add_asynch_update, add_delayed_update);
}
obj_counter++;
}

2
src/library/module.h
View file

@ -76,7 +76,7 @@ typedef std::function<environment(environment const & env, io_state const & ios)
2- Asynchronous update using add_asynch_update.
3- Delayed update using add_delayed_update.
*/
typedef void (*module_object_reader)(deserializer & d, module_idx midx, shared_environment & senv,
typedef void (*module_object_reader)(deserializer & d, shared_environment & senv,
std::function<void(asynch_update_fn const &)> & add_asynch_update,
std::function<void(delayed_update_fn const &)> & add_delayed_update);

4
src/library/normalize.cpp
View file

@ -334,13 +334,13 @@ public:
};
expr normalize(environment const & env, expr const & e, bool eta) {
auto tc = mk_type_checker(env, true);
auto tc = mk_type_checker(env);
bool save_cnstrs = false;
return normalize_fn(*tc, save_cnstrs, eta)(e);
}
expr normalize(environment const & env, level_param_names const & ls, expr const & e, bool eta) {
auto tc = mk_type_checker(env, true);
auto tc = mk_type_checker(env);
bool save_cnstrs = false;
return normalize_fn(*tc, save_cnstrs, eta)(ls, e);
}

2
src/library/private.cpp
View file

@ -53,7 +53,7 @@ pair<environment, name> add_private_name(environment const & env, name const & n
return mk_pair(new_env, r);
}
static void private_reader(deserializer & d, module_idx, shared_environment & senv,
static void private_reader(deserializer & d, shared_environment & senv,
std::function<void(asynch_update_fn const &)> &,
std::function<void(delayed_update_fn const &)> &) {
name n, h;

2
src/library/projection.cpp
View file

@ -56,7 +56,7 @@ projection_info const * get_projection_info(environment const & env, name const
return ext.m_info.find(p);
}
static void projection_info_reader(deserializer & d, module_idx, shared_environment & senv,
static void projection_info_reader(deserializer & d, shared_environment & senv,
std::function<void(asynch_update_fn const &)> &,
std::function<void(delayed_update_fn const &)> &) {
name p, mk; unsigned nparams, i; bool inst_implicit;

2
src/library/protected.cpp
View file

@ -37,7 +37,7 @@ environment add_protected(environment const & env, name const & n) {
return module::add(new_env, *g_prt_key, [=](serializer & s) { s << n; });
}
static void protected_reader(deserializer & d, module_idx, shared_environment & senv,
static void protected_reader(deserializer & d, shared_environment & senv,
std::function<void(asynch_update_fn const &)> &,
std::function<void(delayed_update_fn const &)> &) {
name n;

35
src/library/reducible.cpp
View file

@ -86,7 +86,7 @@ static void check_declaration(environment const & env, name const & n) {
throw exception(sstream() << "invalid reducible command, '" << n << "' is not a definition");
if (d.is_theorem())
throw exception(sstream() << "invalid reducible command, '" << n << "' is a theorem");
if (d.is_opaque() && d.get_module_idx() != g_main_module_idx)
if (d.is_opaque())
throw exception(sstream() << "invalid reducible command, '" << n << "' is an opaque definition");
}
@ -105,8 +105,8 @@ bool is_at_least_quasireducible(environment const & env, name const & n) {
return r == reducible_status::Reducible || r == reducible_status::Quasireducible;
}
unfold_reducible_converter::unfold_reducible_converter(environment const & env, bool relax_main_opaque, bool memoize):
default_converter(env, relax_main_opaque, memoize) {
unfold_reducible_converter::unfold_reducible_converter(environment const & env, bool memoize):
default_converter(env, memoize) {
m_state = reducible_ext::get_state(env);
}
@ -116,8 +116,8 @@ bool unfold_reducible_converter::is_opaque(declaration const & d) const {
return default_converter::is_opaque(d);
}
unfold_quasireducible_converter::unfold_quasireducible_converter(environment const & env, bool relax_main_opaque, bool memoize):
default_converter(env, relax_main_opaque, memoize) {
unfold_quasireducible_converter::unfold_quasireducible_converter(environment const & env, bool memoize):
default_converter(env, memoize) {
m_state = reducible_ext::get_state(env);
}
@ -127,8 +127,8 @@ bool unfold_quasireducible_converter::is_opaque(declaration const & d) const {
return default_converter::is_opaque(d);
}
unfold_semireducible_converter::unfold_semireducible_converter(environment const & env, bool relax_main_opaque, bool memoize):
default_converter(env, relax_main_opaque, memoize) {
unfold_semireducible_converter::unfold_semireducible_converter(environment const & env, bool memoize):
default_converter(env, memoize) {
m_state = reducible_ext::get_state(env);
}
@ -139,29 +139,28 @@ bool unfold_semireducible_converter::is_opaque(declaration const & d) const {
}
std::unique_ptr<type_checker> mk_type_checker(environment const & env, name_generator const & ngen,
bool relax_main_opaque, reducible_behavior rb,
bool memoize) {
reducible_behavior rb, bool memoize) {
switch (rb) {
case UnfoldReducible:
return std::unique_ptr<type_checker>(new type_checker(env, ngen,
std::unique_ptr<converter>(new unfold_reducible_converter(env, relax_main_opaque, memoize))));
std::unique_ptr<converter>(new unfold_reducible_converter(env, memoize))));
case UnfoldQuasireducible:
return std::unique_ptr<type_checker>(new type_checker(env, ngen,
std::unique_ptr<converter>(new unfold_quasireducible_converter(env, relax_main_opaque, memoize))));
std::unique_ptr<converter>(new unfold_quasireducible_converter(env, memoize))));
case UnfoldSemireducible:
return std::unique_ptr<type_checker>(new type_checker(env, ngen,
std::unique_ptr<converter>(new unfold_semireducible_converter(env, relax_main_opaque, memoize))));
std::unique_ptr<converter>(new unfold_semireducible_converter(env, memoize))));
}
lean_unreachable();
}
std::unique_ptr<type_checker> mk_type_checker(environment const & env, bool relax_main_opaque, reducible_behavior rb) {
return mk_type_checker(env, name_generator(*g_tmp_prefix), relax_main_opaque, rb);
std::unique_ptr<type_checker> mk_type_checker(environment const & env, reducible_behavior rb) {
return mk_type_checker(env, name_generator(*g_tmp_prefix), rb);
}
class opaque_converter : public default_converter {
public:
opaque_converter(environment const & env): default_converter(env, true, true) {}
opaque_converter(environment const & env): default_converter(env) {}
virtual bool is_opaque(declaration const &) const { return true; }
};
@ -187,13 +186,13 @@ static int mk_opaque_type_checker(lua_State * L) {
static int mk_reducible_checker_core(lua_State * L, reducible_behavior rb) {
int nargs = lua_gettop(L);
if (nargs == 0) {
type_checker_ref r(mk_type_checker(get_global_environment(L), name_generator(), false, rb));
type_checker_ref r(mk_type_checker(get_global_environment(L), name_generator(), rb));
return push_type_checker_ref(L, r);
} else if (nargs == 1) {
type_checker_ref r(mk_type_checker(to_environment(L, 1), name_generator(), false, rb));
type_checker_ref r(mk_type_checker(to_environment(L, 1), name_generator(), rb));
return push_type_checker_ref(L, r);
} else {
type_checker_ref r(mk_type_checker(to_environment(L, 1), to_name_generator(L, 2), false, rb));
type_checker_ref r(mk_type_checker(to_environment(L, 1), to_name_generator(L, 2), rb));
return push_type_checker_ref(L, r);
}
}

11
src/library/reducible.h
View file

@ -40,7 +40,7 @@ public:
class unfold_reducible_converter : public default_converter {
reducible_state m_state;
public:
unfold_reducible_converter(environment const & env, bool relax_main_opaque, bool memoize);
unfold_reducible_converter(environment const & env, bool memoize);
virtual bool is_opaque(declaration const & d) const;
};
@ -48,7 +48,7 @@ public:
class unfold_quasireducible_converter : public default_converter {
reducible_state m_state;
public:
unfold_quasireducible_converter(environment const & env, bool relax_main_opaque, bool memoize);
unfold_quasireducible_converter(environment const & env, bool memoize);
virtual bool is_opaque(declaration const & d) const;
};
@ -56,7 +56,7 @@ public:
class unfold_semireducible_converter : public default_converter {
reducible_state m_state;
public:
unfold_semireducible_converter(environment const & env, bool relax_main_opaque, bool memoize);
unfold_semireducible_converter(environment const & env, bool memoize);
virtual bool is_opaque(declaration const & d) const;
};
@ -64,10 +64,9 @@ enum reducible_behavior { UnfoldReducible, UnfoldQuasireducible, UnfoldSemireduc
/** \brief Create a type checker that takes the "reducibility" hints into account. */
std::unique_ptr<type_checker> mk_type_checker(environment const & env, name_generator const & ngen,
bool relax_main_opaque = true, reducible_behavior r = UnfoldSemireducible,
reducible_behavior r = UnfoldSemireducible,
bool memoize = true);
std::unique_ptr<type_checker> mk_type_checker(environment const & env, bool relax_main_opaque,
reducible_behavior r = UnfoldSemireducible);
std::unique_ptr<type_checker> mk_type_checker(environment const & env, reducible_behavior r = UnfoldSemireducible);
/** \brief Create a type checker that treats all definitions as opaque. */
std::unique_ptr<type_checker> mk_opaque_type_checker(environment const & env, name_generator const & ngen);

2
src/library/scoped_ext.cpp
View file

@ -159,7 +159,7 @@ environment push_scope(environment const & env, io_state const & ios, scope_kind
return r;
}
static void namespace_reader(deserializer & d, module_idx, shared_environment &,
static void namespace_reader(deserializer & d, shared_environment &,
std::function<void(asynch_update_fn const &)> &,
std::function<void(delayed_update_fn const &)> & add_delayed_update) {
name n;

2
src/library/scoped_ext.h
View file

@ -244,7 +244,7 @@ public:
return update(env, get(env)._add_entry(env, ios, e));
}
}
static void reader(deserializer & d, module_idx, shared_environment &,
static void reader(deserializer & d, shared_environment &,
std::function<void(asynch_update_fn const &)> &,
std::function<void(delayed_update_fn const &)> & add_delayed_update) {
name n;

7
src/library/tactic/apply_tactic.cpp
View file

@ -80,8 +80,7 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const
}
bool class_inst = get_apply_class_instance(ios.get_options());
name_generator ngen = s.get_ngen();
bool relax_opaque = s.relax_main_opaque();
std::shared_ptr<type_checker> tc(mk_type_checker(env, ngen.mk_child(), relax_opaque));
std::shared_ptr<type_checker> tc(mk_type_checker(env, ngen.mk_child()));
goal g = head(gs);
goals tail_gs = tail(gs);
expr t = g.get_type();
@ -120,7 +119,7 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const
bool is_strict = false;
auto mc = mk_class_instance_elaborator(
env, ios, ctx, ngen.next(), optional<name>(),
relax_opaque, use_local_insts, is_strict,
use_local_insts, is_strict,
some_expr(binding_domain(e_t)), e.get_tag(), cfg, nullptr);
meta = mc.first;
cs.push_back(mc.second);
@ -133,7 +132,7 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const
}
}
metavar_closure cls(t);
cls.mk_constraints(s.get_subst(), justification(), relax_opaque);
cls.mk_constraints(s.get_subst(), justification());
pair<bool, constraint_seq> dcs = tc->is_def_eq(t, e_t);
if (!dcs.first) {
throw_tactic_exception_if_enabled(s, [=](formatter const & fmt) {

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

@ -22,7 +22,7 @@ tactic check_expr_tactic(elaborate_fn const & elab, expr const & e,
goal const & g = head(gs);
name_generator ngen = s.get_ngen();
expr new_e = std::get<0>(elab(g, ngen.mk_child(), e, none_expr(), s.get_subst(), false));
auto tc = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque());
auto tc = mk_type_checker(env, ngen.mk_child());
expr new_t = tc->infer(new_e).first;
auto out = regular(env, ios);
flycheck_information info(out);

33
src/library/tactic/class_instance_synth.cpp
View file

@ -99,7 +99,6 @@ struct class_instance_context {
name_generator m_ngen;
type_checker_ptr m_tc;
expr m_main_meta;
bool m_relax;
bool m_use_local_instances;
bool m_trace_instances;
bool m_conservative;
@ -107,19 +106,18 @@ struct class_instance_context {
char const * m_fname;
optional<pos_info> m_pos;
class_instance_context(environment const & env, io_state const & ios,
name const & prefix, bool relax, bool use_local_instances):
name const & prefix, bool use_local_instances):
m_ios(ios),
m_ngen(prefix),
m_relax(relax),
m_use_local_instances(use_local_instances) {
m_fname = nullptr;
m_trace_instances = get_class_trace_instances(ios.get_options());
m_max_depth = get_class_instance_max_depth(ios.get_options());
m_conservative = get_class_conservative(ios.get_options());
if (m_conservative)
m_tc = mk_type_checker(env, m_ngen.mk_child(), false, UnfoldReducible);
m_tc = mk_type_checker(env, m_ngen.mk_child(), UnfoldReducible);
else
m_tc = mk_type_checker(env, m_ngen.mk_child(), m_relax);
m_tc = mk_type_checker(env, m_ngen.mk_child());
options opts = m_ios.get_options();
opts = opts.update_if_undef(get_pp_purify_metavars_name(), false);
opts = opts.update_if_undef(get_pp_implicit_name(), true);
@ -250,8 +248,7 @@ struct class_instance_elaborator : public choice_iterator {
}
r = Fun(locals, r);
trace(meta_type, r);
bool relax = m_C->m_relax;
constraint c = mk_eq_cnstr(m_meta, r, m_jst, relax);
constraint c = mk_eq_cnstr(m_meta, r, m_jst);
return optional<constraints>(mk_constraints(c, cs));
} catch (exception &) {
return optional<constraints>();
@ -315,9 +312,7 @@ constraint mk_class_instance_cnstr(std::shared_ptr<class_instance_context> const
}
};
bool owner = false;
bool relax = C->m_relax;
return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::Basic),
owner, j, relax);
return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::Basic), owner, j);
}
pair<expr, constraint> mk_class_instance_elaborator(std::shared_ptr<class_instance_context> const & C, local_context const & ctx,
@ -362,8 +357,7 @@ constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_context>
});
metavar_closure cls(new_meta);
cls.add(meta_type);
bool relax = C->m_relax;
constraints cs = cls.mk_constraints(new_s, new_j, relax);
constraints cs = cls.mk_constraints(new_s, new_j);
return append(cs, postponed);
};
@ -430,8 +424,7 @@ constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_context>
}
};
bool owner = false;
bool relax = C->m_relax;
return mk_choice_cnstr(m, choice_fn, factor, owner, j, relax);
return mk_choice_cnstr(m, choice_fn, factor, owner, j);
}
/** \brief Create a metavariable, and attach choice constraint for generating
@ -439,10 +432,10 @@ constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_context>
*/
pair<expr, constraint> mk_class_instance_elaborator(
environment const & env, io_state const & ios, local_context const & ctx,
name const & prefix, optional<name> const & suffix, bool relax, bool use_local_instances,
name const & prefix, optional<name> const & suffix, bool use_local_instances,
bool is_strict, optional<expr> const & type, tag g, unifier_config const & cfg,
pos_info_provider const * pip) {
auto C = std::make_shared<class_instance_context>(env, ios, prefix, relax, use_local_instances);
auto C = std::make_shared<class_instance_context>(env, ios, prefix, use_local_instances);
expr m = ctx.mk_meta(C->m_ngen, suffix, type, g);
C->set_main_meta(m);
if (pip)
@ -452,9 +445,9 @@ pair<expr, constraint> mk_class_instance_elaborator(
}
optional<expr> mk_class_instance(environment const & env, io_state const & ios, local_context const & ctx,
name const & prefix, expr const & type, bool relax_opaque, bool use_local_instances,
name const & prefix, expr const & type, bool use_local_instances,
unifier_config const & cfg) {
auto C = std::make_shared<class_instance_context>(env, ios, prefix, relax_opaque, use_local_instances);
auto C = std::make_shared<class_instance_context>(env, ios, prefix, use_local_instances);
if (!is_ext_class(C->tc(), type))
return none_expr();
expr meta = ctx.mk_meta(C->m_ngen, some_expr(type), type.get_tag());
@ -482,10 +475,10 @@ optional<expr> mk_class_instance(environment const & env, io_state const & ios,
}
optional<expr> mk_class_instance(environment const & env, io_state const & ios, list<expr> const & ctx,
name const & prefix, expr const & type, bool relax_opaque, bool use_local_instances,
name const & prefix, expr const & type, bool use_local_instances,
unifier_config const & cfg) {
local_context lctx(ctx);
return mk_class_instance(env, ios, lctx, prefix, type, relax_opaque, use_local_instances, cfg);
return mk_class_instance(env, ios, lctx, prefix, type, use_local_instances, cfg);
}
optional<expr> mk_hset_instance(type_checker & tc, io_state const & ios, list<expr> const & ctx, expr const & type) {

8
src/library/tactic/class_instance_synth.h
View file

@ -19,8 +19,6 @@ class type_checker;
\param ctx Local context where placeholder is located
\param prefix Prefix for metavariables that will be created by this procedure
\param suffix If provided, then it is added to the main metavariable created by this procedure.
\param relax True if opaque constants in the current module should be treated
as transparent
\param use_local_instances If instances in the local context should be used
in the class-instance resolution
\param is_strict True if constraint should fail if not solution is found,
@ -30,17 +28,17 @@ class type_checker;
*/
pair<expr, constraint> mk_class_instance_elaborator(
environment const & env, io_state const & ios, local_context const & ctx,
name const & prefix, optional<name> const & suffix, bool relax_opaque, bool use_local_instances,
name const & prefix, optional<name> const & suffix, bool use_local_instances,
bool is_strict, optional<expr> const & type, tag g, unifier_config const & cfg,
pos_info_provider const * pip);
/** \brief Create/synthesize a term of the class instance \c type. */
optional<expr> mk_class_instance(environment const & env, io_state const & ios, local_context const & ctx,
name const & prefix, expr const & type, bool relax_opaque = true, bool use_local_instances = true,
name const & prefix, expr const & type, bool use_local_instances = true,
unifier_config const & cfg = unifier_config());
optional<expr> mk_class_instance(environment const & env, io_state const & ios, list<expr> const & ctx,
name const & prefix, expr const & type, bool relax_opaque = true, bool use_local_instances = true,
name const & prefix, expr const & type, bool use_local_instances = true,
unifier_config const & cfg = unifier_config());
/** \breif Try to synthesize an inhabitant for (is_hset type) using class instance resolution */

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

@ -23,7 +23,7 @@ tactic congruence_tactic() {
expr t = g.get_type();
substitution subst = s.get_subst();
name_generator ngen = s.get_ngen();
auto tc = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque());
auto tc = mk_type_checker(env, ngen.mk_child());
constraint_seq cs;
t = tc->whnf(t, cs);
expr lhs, rhs;

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

@ -31,7 +31,7 @@ tactic constructor_tactic(elaborate_fn const & elab, optional<unsigned> _i, opti
}
constraint_seq cs;
name_generator ngen = s.get_ngen();
auto tc = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque());
auto tc = mk_type_checker(env, ngen.mk_child());
goal const & g = head(gs);
expr t = tc->whnf(g.get_type(), cs);
buffer<expr> I_args;

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

@ -24,7 +24,7 @@ tactic contradiction_tactic() {
expr const & t = g.get_type();
substitution subst = s.get_subst();
name_generator ngen = s.get_ngen();
auto tc = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque());
auto tc = mk_type_checker(env, ngen.mk_child());
buffer<expr> hyps;
g.get_hyps(hyps);
for (expr const & h : hyps) {

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

@ -62,7 +62,7 @@ tactic exact_tactic(elaborate_fn const & elab, expr const & e, bool enforce_type
if (allow_metavars) {
buffer<goal> new_goals;
name_generator ngen = new_s.get_ngen();
auto tc = mk_type_checker(env, ngen.mk_child(), new_s.relax_main_opaque());
auto tc = mk_type_checker(env, ngen.mk_child());
for_each(*new_e, [&](expr const & m, unsigned) {
if (!has_expr_metavar(m))
return false;

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

@ -24,7 +24,7 @@ tactic exfalso_tactic() {
expr const & t = g.get_type();
substitution subst = s.get_subst();
name_generator ngen = s.get_ngen();
auto tc = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque());
auto tc = mk_type_checker(env, ngen.mk_child());
expr false_expr = mk_false(env);
expr new_meta = g.mk_meta(ngen.next(), false_expr);
goal new_goal(new_meta, false_expr);

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

@ -50,7 +50,7 @@ tactic intros_num_tactic(unsigned num, list<name> _ns) {
return proof_state_seq();
goal const & g = head(gs);
name_generator ngen = s.get_ngen();
auto tc = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque());
auto tc = mk_type_checker(env, ngen.mk_child());
expr t = g.get_type();
expr m = g.get_meta();
@ -150,7 +150,7 @@ tactic injection_tactic_core(expr const & e, unsigned num, list<name> const & id
expr t = head(gs).get_type();
constraint_seq cs;
name_generator ngen = s.get_ngen();
auto tc = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque());
auto tc = mk_type_checker(env, ngen.mk_child());
expr e_type = tc->whnf(tc->infer(e, cs), cs);
expr lhs, rhs;
if (!is_eq(e_type, lhs, rhs)) {

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

@ -21,7 +21,7 @@ tactic intros_tactic(list<name> _ns) {
}
goal const & g = head(gs);
name_generator ngen = s.get_ngen();
auto tc = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque());
auto tc = mk_type_checker(env, ngen.mk_child());
expr t = g.get_type();
expr m = g.get_meta();
bool gen_names = empty(ns);

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

@ -1096,7 +1096,7 @@ tactic inversion_tactic(name const & n, list<name> const & ids) {
goal g = head(gs);
goals tail_gs = tail(gs);
name_generator ngen = ps.get_ngen();
std::unique_ptr<type_checker> tc = mk_type_checker(env, ngen.mk_child(), ps.relax_main_opaque());
std::unique_ptr<type_checker> tc = mk_type_checker(env, ngen.mk_child());
inversion_tac tac(env, ios, ngen, *tc, ps.get_subst(), ids, ps.report_failure());
if (auto res = tac.execute(g, n, implementation_list())) {
proof_state new_s(ps, append(res->m_goals, tail_gs), res->m_subst, res->m_ngen);

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

@ -34,7 +34,7 @@ tactic let_tactic(elaborate_fn const & elab, name const & id, expr const & e) {
std::tie(new_e, new_subst, cs) = esc;
if (cs)
throw_tactic_exception_if_enabled(s, "invalid 'let' tactic, fail to resolve generated constraints");
auto tc = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque());
auto tc = mk_type_checker(env, ngen.mk_child());
expr new_e_type = tc->infer(new_e).first;
expr new_local = mk_local(ngen.next(), id, new_e_type, binder_info());
buffer<expr> hyps;

21
src/library/tactic/proof_state.cpp
View file

@ -31,8 +31,8 @@ bool get_proof_state_goal_names(options const & opts) {
}
proof_state::proof_state(goals const & gs, substitution const & s, name_generator const & ngen,
constraints const & postponed, bool relax_main_opaque, bool report_failure):
m_goals(gs), m_subst(s), m_ngen(ngen), m_postponed(postponed), m_relax_main_opaque(relax_main_opaque),
constraints const & postponed, bool report_failure):
m_goals(gs), m_subst(s), m_ngen(ngen), m_postponed(postponed),
m_report_failure(report_failure) {
if (std::any_of(gs.begin(), gs.end(),
[&](goal const & g) { return s.is_assigned(g.get_mvar()); })) {
@ -81,13 +81,12 @@ goals map_goals(proof_state const & s, std::function<optional<goal>(goal const &
});
}
proof_state to_proof_state(expr const & meta, expr const & type, substitution const & subst, name_generator ngen,
bool relax_main_opaque) {
return proof_state(goals(goal(meta, type)), subst, ngen, constraints(), relax_main_opaque);
proof_state to_proof_state(expr const & meta, expr const & type, substitution const & subst, name_generator ngen) {
return proof_state(goals(goal(meta, type)), subst, ngen, constraints());
}
proof_state to_proof_state(expr const & meta, expr const & type, name_generator ngen, bool relax_main_opaque) {
return to_proof_state(meta, type, substitution(), ngen, relax_main_opaque);
proof_state to_proof_state(expr const & meta, expr const & type, name_generator ngen) {
return to_proof_state(meta, type, substitution(), ngen);
}
proof_state apply_substitution(proof_state const & s) {
@ -180,9 +179,8 @@ static int mk_proof_state(lua_State * L) {
} else if (nargs == 3 && is_proof_state(L, 1)) {
return push_proof_state(L, proof_state(to_proof_state(L, 1), to_goals(L, 2), to_substitution(L, 3)));
} else if (nargs == 3) {
bool relax_main_opaque = true;
return push_proof_state(L, proof_state(to_goals(L, 1), to_substitution(L, 2), to_name_generator(L, 3),
constraints(), relax_main_opaque));
constraints()));
} else {
throw exception("proof_state invalid number of arguments");
}
@ -191,11 +189,10 @@ static int mk_proof_state(lua_State * L) {
static name * g_tmp_prefix = nullptr;
static int to_proof_state(lua_State * L) {
int nargs = lua_gettop(L);
bool relax_main_opaque = true;
if (nargs == 2)
return push_proof_state(L, to_proof_state(to_expr(L, 1), to_expr(L, 2), name_generator(*g_tmp_prefix), relax_main_opaque));
return push_proof_state(L, to_proof_state(to_expr(L, 1), to_expr(L, 2), name_generator(*g_tmp_prefix)));
else
return push_proof_state(L, to_proof_state(to_expr(L, 1), to_expr(L, 2), to_name_generator(L, 3), relax_main_opaque));
return push_proof_state(L, to_proof_state(to_expr(L, 1), to_expr(L, 2), to_name_generator(L, 3)));
}
static int proof_state_tostring(lua_State * L) {

17
src/library/tactic/proof_state.h
View file

@ -21,19 +21,18 @@ class proof_state {
substitution m_subst;
name_generator m_ngen;
constraints m_postponed;
bool m_relax_main_opaque;
bool m_report_failure;
format pp_core(std::function<formatter()> const & mk_fmt, options const & opts) const;
public:
proof_state(goals const & gs, substitution const & s, name_generator const & ngen, constraints const & postponed,
bool relax_main_opaque, bool report_failure = true);
bool report_failure = true);
proof_state(proof_state const & s, goals const & gs, substitution const & subst, name_generator const & ngen,
constraints const & postponed):
proof_state(gs, subst, ngen, postponed, s.relax_main_opaque(), s.report_failure()) {}
proof_state(gs, subst, ngen, postponed, s.report_failure()) {}
proof_state(proof_state const & s, goals const & gs, substitution const & subst, name_generator const & ngen):
proof_state(gs, subst, ngen, s.m_postponed, s.relax_main_opaque(), s.report_failure()) {}
proof_state(gs, subst, ngen, s.m_postponed, s.report_failure()) {}
proof_state(proof_state const & s, goals const & gs, substitution const & subst):
proof_state(s, gs, subst, s.m_ngen) {}
proof_state(proof_state const & s, goals const & gs, name_generator const & ngen):
@ -42,7 +41,7 @@ public:
proof_state(s, gs, s.m_subst) {}
proof_state(proof_state const & s, substitution const & subst, name_generator const & ngen,
constraints const & postponed):
proof_state(s.m_goals, subst, ngen, postponed, s.relax_main_opaque(), s.report_failure()) {}
proof_state(s.m_goals, subst, ngen, postponed, s.report_failure()) {}
proof_state(proof_state const & s, name_generator const & ngen, constraints const & postponed):
proof_state(s, s.m_goals, s.m_subst, ngen, postponed) {}
proof_state(proof_state const & s, substitution const & subst, name_generator const & ngen):
@ -53,14 +52,13 @@ public:
proof_state(s, subst, s.m_ngen) {}
proof_state update_report_failure(bool f) const {
return m_report_failure == f ? *this : proof_state(m_goals, m_subst, m_ngen, m_postponed, m_relax_main_opaque, f);
return m_report_failure == f ? *this : proof_state(m_goals, m_subst, m_ngen, m_postponed, f);
}
goals const & get_goals() const { return m_goals; }
substitution const & get_subst() const { return m_subst; }
name_generator const & get_ngen() const { return m_ngen; }
constraints const & get_postponed() const { return m_postponed; }
bool relax_main_opaque() const { return m_relax_main_opaque; }
bool report_failure() const { return m_report_failure; }
/** \brief Return true iff this state does not have any goals left */
@ -81,9 +79,8 @@ proof_state apply_substitution(proof_state const & s);
inline optional<proof_state> some_proof_state(proof_state const & s) { return some(s); }
inline optional<proof_state> none_proof_state() { return optional<proof_state> (); }
proof_state to_proof_state(expr const & meta, expr const & type, substitution const & subst, name_generator ngen,
bool relax_main_opaque);
proof_state to_proof_state(expr const & meta, expr const & type, name_generator ngen, bool relax_main_opaque);
proof_state to_proof_state(expr const & meta, expr const & type, substitution const & subst, name_generator ngen);
proof_state to_proof_state(expr const & meta, expr const & type, name_generator ngen);
goals map_goals(proof_state const & s, std::function<optional<goal>(goal const & g)> f);

20
src/library/tactic/rewrite_tactic.cpp
View file

@ -580,9 +580,8 @@ class rewrite_fn {
list<name> const & m_to_unfold;
bool & m_unfolded;
public:
rewriter_converter(environment const & env, bool relax_main_opaque, list<name> const & to_unfold,
bool & unfolded):
default_converter(env, relax_main_opaque),
rewriter_converter(environment const & env, list<name> const & to_unfold, bool & unfolded):
default_converter(env),
m_to_unfold(to_unfold), m_unfolded(unfolded) {}
virtual bool is_opaque(declaration const & d) const {
if (std::find(m_to_unfold.begin(), m_to_unfold.end(), d.get_name()) != m_to_unfold.end()) {
@ -596,9 +595,8 @@ class rewrite_fn {
optional<expr> reduce(expr const & e, list<name> const & to_unfold) {
bool unfolded = !to_unfold;
bool relax_main_opaque = false;
auto tc = new type_checker(m_env, m_ngen.mk_child(),
std::unique_ptr<converter>(new rewriter_converter(m_env, relax_main_opaque, to_unfold, unfolded)));
std::unique_ptr<converter>(new rewriter_converter(m_env, to_unfold, unfolded)));
constraint_seq cs;
bool use_eta = true;
expr r = normalize(*tc, e, cs, use_eta);
@ -941,7 +939,7 @@ class rewrite_fn {
bool use_local_instances = true;
bool is_strict = false;
return ::lean::mk_class_instance_elaborator(m_env, m_ios, m_ctx, m_ngen.next(), optional<name>(),
m_ps.relax_main_opaque(), use_local_instances, is_strict,
use_local_instances, is_strict,
some_expr(type), m_expr_loc.get_tag(), cfg, nullptr);
}
@ -1409,8 +1407,8 @@ class rewrite_fn {
class match_converter : public unfold_reducible_converter {
public:
match_converter(environment const & env, bool relax_main_opaque):
unfold_reducible_converter(env, relax_main_opaque, true) {}
match_converter(environment const & env):
unfold_reducible_converter(env, true) {}
virtual bool is_opaque(declaration const & d) const {
if (is_projection(m_env, d.get_name()))
return true;
@ -1424,7 +1422,7 @@ class rewrite_fn {
return mk_opaque_type_checker(m_env, m_ngen.mk_child());
} else {
return std::unique_ptr<type_checker>(new type_checker(m_env, m_ngen.mk_child(),
std::unique_ptr<converter>(new match_converter(m_env, m_ps.relax_main_opaque()))));
std::unique_ptr<converter>(new match_converter(m_env))));
}
}
@ -1476,9 +1474,9 @@ class rewrite_fn {
public:
rewrite_fn(environment const & env, io_state const & ios, elaborate_fn const & elab, proof_state const & ps):
m_env(env), m_ios(ios), m_elab(elab), m_ps(ps), m_ngen(ps.get_ngen()),
m_tc(mk_type_checker(m_env, m_ngen.mk_child(), ps.relax_main_opaque(), UnfoldQuasireducible)),
m_tc(mk_type_checker(m_env, m_ngen.mk_child(), UnfoldQuasireducible)),
m_matcher_tc(mk_matcher_tc()),
m_relaxed_tc(mk_type_checker(m_env, m_ngen.mk_child(), ps.relax_main_opaque())),
m_relaxed_tc(mk_type_checker(m_env, m_ngen.mk_child())),
m_mplugin(m_ios, *m_matcher_tc) {
m_ps = apply_substitution(m_ps);
goals const & gs = m_ps.get_goals();

3
src/library/tactic/util.cpp
View file

@ -60,8 +60,7 @@ justification mk_failed_to_synthesize_jst(environment const & env, expr const &
substitution tmp(subst);
expr new_m = instantiate_meta(m, tmp);
expr new_type = type_checker(env).infer(new_m).first;
bool relax_main_opaque = true; // this value doesn't really matter for pretty printing
proof_state ps = to_proof_state(new_m, new_type, name_generator("dontcare"), relax_main_opaque);
proof_state ps = to_proof_state(new_m, new_type, name_generator("dontcare"));
return format("failed to synthesize placeholder") + line() + ps.pp(fmt);
});
}

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

@ -11,13 +11,13 @@ Author: Leonardo de Moura
#include "library/tactic/whnf_tactic.h"
namespace lean {
tactic whnf_tactic(bool relax_main_opaque) {
tactic whnf_tactic() {
return tactic01([=](environment const & env, io_state const & ios, proof_state const & ps) {
goals const & gs = ps.get_goals();
if (empty(gs))
return none_proof_state();
name_generator ngen = ps.get_ngen();
auto tc = mk_type_checker(env, ngen.mk_child(), relax_main_opaque);
auto tc = mk_type_checker(env, ngen.mk_child());
goal g = head(gs);
goals tail_gs = tail(gs);
expr type = g.get_type();

2
src/library/tactic/whnf_tactic.h
View file

@ -8,7 +8,7 @@ Author: Leonardo de Moura
#include "library/tactic/tactic.h"
namespace lean {
tactic whnf_tactic(bool relax_main_opaque = true);
tactic whnf_tactic();
void initialize_whnf_tactic();
void finalize_whnf_tactic();
}

4
src/library/unfold_macros.cpp
View file

@ -143,11 +143,11 @@ declaration unfold_untrusted_macros(environment const & env, declaration const &
expr new_t = unfold_untrusted_macros(env, d.get_type(), trust_lvl);
if (d.is_theorem()) {
expr new_v = unfold_untrusted_macros(env, d.get_value(), trust_lvl);
return mk_theorem(d.get_name(), d.get_univ_params(), new_t, new_v, d.get_module_idx());
return mk_theorem(d.get_name(), d.get_univ_params(), new_t, new_v);
} else if (d.is_definition()) {
expr new_v = unfold_untrusted_macros(env, d.get_value(), trust_lvl);
return mk_definition(d.get_name(), d.get_univ_params(), new_t, new_v,
d.is_opaque(), d.get_weight(), d.get_module_idx(), d.use_conv_opt());
d.is_opaque(), d.get_weight(), d.use_conv_opt());
} else if (d.is_axiom()) {
return mk_axiom(d.get_name(), d.get_univ_params(), new_t);
} else if (d.is_constant_assumption()) {

192
src/library/unifier.cpp
View file

@ -329,7 +329,7 @@ struct unifier_fn {
owned_map m_owned_map; // mapping from metavariable name m to delay factor of the choice constraint that owns m
expr_map m_type_map; // auxiliary map for storing the type of the expr in choice constraints
unifier_plugin m_plugin;
type_checker_ptr m_tc[2];
type_checker_ptr m_tc;
type_checker_ptr m_flex_rigid_tc; // type checker used when solving flex rigid constraints. By default,
// only the definitions from the main module are treated as transparent.
unifier_config m_config;
@ -438,28 +438,24 @@ struct unifier_fn {
m_config(cfg), m_num_steps(0) {
switch (m_config.m_kind) {
case unifier_kind::Cheap:
m_tc[0] = mk_opaque_type_checker(env, m_ngen.mk_child());
m_tc[1] = m_tc[0];
m_flex_rigid_tc = m_tc[0];
m_tc = mk_opaque_type_checker(env, m_ngen.mk_child());
m_flex_rigid_tc = m_tc;
m_config.m_computation = false;
break;
case unifier_kind::VeryConservative:
m_tc[0] = mk_type_checker(env, m_ngen.mk_child(), false, UnfoldReducible);
m_tc[1] = m_tc[0];
m_flex_rigid_tc = m_tc[0];
m_tc = mk_type_checker(env, m_ngen.mk_child(), UnfoldReducible);
m_flex_rigid_tc = m_tc;
m_config.m_computation = false;
break;
case unifier_kind::Conservative:
m_tc[0] = mk_type_checker(env, m_ngen.mk_child(), false, UnfoldQuasireducible);
m_tc[1] = m_tc[0];
m_flex_rigid_tc = m_tc[0];
m_tc = mk_type_checker(env, m_ngen.mk_child(), UnfoldQuasireducible);
m_flex_rigid_tc = m_tc;
m_config.m_computation = false;
break;
case unifier_kind::Liberal:
m_tc[0] = mk_type_checker(env, m_ngen.mk_child(), false);
m_tc[1] = mk_type_checker(env, m_ngen.mk_child(), true);
m_tc = mk_type_checker(env, m_ngen.mk_child());
if (!cfg.m_computation)
m_flex_rigid_tc = mk_type_checker(env, m_ngen.mk_child(), false, UnfoldQuasireducible);
m_flex_rigid_tc = mk_type_checker(env, m_ngen.mk_child(), UnfoldQuasireducible);
break;
default:
lean_unreachable();
@ -556,12 +552,10 @@ struct unifier_fn {
}
/** \brief Check if \c t1 and \c t2 are definitionally equal, if they are not, set a conflict with justification \c j
\remark If relax is true then opaque definitions from the main module are treated as transparent.
*/
bool is_def_eq(expr const & t1, expr const & t2, justification const & j, bool relax) {
bool is_def_eq(expr const & t1, expr const & t2, justification const & j) {
try {
auto dcs = m_tc[relax]->is_def_eq(t1, t2, j);
auto dcs = m_tc->is_def_eq(t1, t2, j);
if (!dcs.first) {
// std::cout << "conflict: " << t1 << " =?= " << t2 << "\n";
set_conflict(j);
@ -607,37 +601,35 @@ struct unifier_fn {
/** \brief Put \c e in weak head normal form.
\remark If relax is true then opaque definitions from the main module are treated as transparent.
\remark Constraints generated in the process are stored in \c cs.
*/
expr whnf(expr const & e, bool relax, constraint_seq & cs) {
return m_tc[relax]->whnf(e, cs);
expr whnf(expr const & e, constraint_seq & cs) {
return m_tc->whnf(e, cs);
}
/** \brief Infer \c e type.
\remark Return none if an exception was throw when inferring the type.
\remark If relax is true then opaque definitions from the main module are treated as transparent.
\remark Constraints generated in the process are stored in \c cs.
*/
optional<expr> infer(expr const & e, bool relax, constraint_seq & cs) {
optional<expr> infer(expr const & e, constraint_seq & cs) {
try {
return some_expr(m_tc[relax]->infer(e, cs));
return some_expr(m_tc->infer(e, cs));
} catch (exception &) {
return none_expr();
}
}
expr whnf(expr const & e, justification const & j, bool relax, buffer<constraint> & cs) {
expr whnf(expr const & e, justification const & j, buffer<constraint> & cs) {
constraint_seq _cs;
expr r = whnf(e, relax, _cs);
expr r = whnf(e, _cs);
to_buffer(_cs, j, cs);
return r;
}
expr flex_rigid_whnf(expr const & e, justification const & j, bool relax, buffer<constraint> & cs) {
expr flex_rigid_whnf(expr const & e, justification const & j, buffer<constraint> & cs) {
if (m_config.m_computation) {
return whnf(e, j, relax, cs);
return whnf(e, j, cs);
} else {
constraint_seq _cs;
expr r = m_flex_rigid_tc->whnf(e, _cs);
@ -677,21 +669,19 @@ struct unifier_fn {
The type of lhs and rhs are inferred, and is_def_eq is invoked.
Any other constraint that contains \c m is revisited
\remark If relax is true then opaque definitions from the main module are treated as transparent.
*/
bool assign(expr const & lhs, expr const & m, buffer<expr> const & args, expr const & rhs, justification const & j, bool relax) {
bool assign(expr const & lhs, expr const & m, buffer<expr> const & args, expr const & rhs, justification const & j) {
lean_assert(is_metavar(m));
lean_assert(!in_conflict());
m_subst.assign(m, args, rhs, j);
constraint_seq cs;
auto lhs_type = infer(lhs, relax, cs);
auto rhs_type = infer(rhs, relax, cs);
auto lhs_type = infer(lhs, cs);
auto rhs_type = infer(rhs, cs);
if (lhs_type && rhs_type) {
if (!process_constraints(cs, j))
return false;
justification new_j = mk_assign_justification(m, *lhs_type, *rhs_type, j);
if (!is_def_eq(*lhs_type, *rhs_type, new_j, relax))
if (!is_def_eq(*lhs_type, *rhs_type, new_j))
return false;
} else {
set_conflict(j);
@ -754,7 +744,7 @@ struct unifier_fn {
The method returns \c Failed if \c rhs contains <tt>?m</tt>, or it contains a local constant not in <tt>{l_1, ..., l_n}</tt>.
Otherwise, it returns \c Continue.
*/
status process_metavar_eq(expr const & lhs, expr const & rhs, justification const & j, bool relax) {
status process_metavar_eq(expr const & lhs, expr const & rhs, justification const & j) {
if (!is_meta(lhs))
return Continue;
buffer<expr> locals;
@ -778,9 +768,9 @@ struct unifier_fn {
return true;
return false;
};
expr rhs_n = normalize(*m_tc[relax], rhs, is_target_fn, cs);
expr rhs_n = normalize(*m_tc, rhs, is_target_fn, cs);
if (rhs != rhs_n && process_constraints(cs))
return process_metavar_eq(lhs, rhs_n, j, relax);
return process_metavar_eq(lhs, rhs_n, j);
}
switch (status) {
case occurs_check_status::FailLocal:
@ -793,7 +783,7 @@ struct unifier_fn {
return Continue;
case occurs_check_status::Ok:
lean_assert(!m_subst.is_assigned(*m));
if (assign(lhs, *m, locals, rhs, j, relax)) {
if (assign(lhs, *m, locals, rhs, j)) {
return Solved;
} else {
return Failed;
@ -803,8 +793,7 @@ struct unifier_fn {
}
optional<declaration> is_delta(expr const & e) {
bool relax_opaque = true;
return m_tc[relax_opaque]->is_delta(e);
return m_tc->is_delta(e);
}
/** \brief Return true if lhs and rhs are of the form (f ...) where f can be expanded */
@ -827,8 +816,7 @@ struct unifier_fn {
expr rhs = rhs_jst.first;
if (lhs != cnstr_lhs_expr(c) || rhs != cnstr_rhs_expr(c)) {
return mk_pair(mk_eq_cnstr(lhs, rhs,
mk_composite1(mk_composite1(c.get_justification(), lhs_jst.second), rhs_jst.second),
relax_main_opaque(c)),
mk_composite1(mk_composite1(c.get_justification(), lhs_jst.second), rhs_jst.second)),
true);
}
} else if (is_level_eq_cnstr(c)) {
@ -849,20 +837,19 @@ struct unifier_fn {
expr const & lhs = cnstr_lhs_expr(c);
expr const & rhs = cnstr_rhs_expr(c);
justification const & jst = c.get_justification();
bool relax = relax_main_opaque(c);
if (lhs == rhs)
return Solved; // trivial constraint
// Update justification using the justification of the instantiated metavariables
if (!has_metavar(lhs) && !has_metavar(rhs)) {
return is_def_eq(lhs, rhs, jst, relax) ? Solved : Failed;
return is_def_eq(lhs, rhs, jst) ? Solved : Failed;
}
// Handle higher-order pattern matching.
status st = process_metavar_eq(lhs, rhs, jst, relax);
status st = process_metavar_eq(lhs, rhs, jst);
if (st != Continue) return st;
st = process_metavar_eq(rhs, lhs, jst, relax);
st = process_metavar_eq(rhs, lhs, jst);
if (st != Continue) return st;
return Continue;
@ -909,11 +896,11 @@ struct unifier_fn {
expr lhs = instantiate_meta(cnstr_lhs_expr(c), j);
expr rhs = instantiate_meta(cnstr_rhs_expr(c), j);
if (lhs != cnstr_lhs_expr(c) || rhs != cnstr_rhs_expr(c))
return is_def_eq(lhs, rhs, j, relax_main_opaque(c)) ? Solved : Failed;
return is_def_eq(lhs, rhs, j) ? Solved : Failed;
lhs = instantiate_meta_args(lhs, j);
rhs = instantiate_meta_args(rhs, j);
if (lhs != cnstr_lhs_expr(c) || rhs != cnstr_rhs_expr(c))
return is_def_eq(lhs, rhs, j, relax_main_opaque(c)) ? Solved : Failed;
return is_def_eq(lhs, rhs, j) ? Solved : Failed;
return Continue;
}
@ -957,7 +944,6 @@ struct unifier_fn {
expr const & lhs = cnstr_lhs_expr(c);
expr const & rhs = cnstr_rhs_expr(c);
bool relax = relax_main_opaque(c);
if (is_eq_deltas(lhs, rhs)) {
// we need to create a backtracking point for this one
@ -967,9 +953,9 @@ struct unifier_fn {
unsigned cidx = add_cnstr(c, cnstr_group::FlexFlex);
add_meta_occ(lhs, cidx);
add_meta_occ(rhs, cidx);
} else if (m_tc[relax]->may_reduce_later(lhs) ||
m_tc[relax]->may_reduce_later(rhs) ||
m_plugin->delay_constraint(*m_tc[relax], c)) {
} else if (m_tc->may_reduce_later(lhs) ||
m_tc->may_reduce_later(rhs) ||
m_plugin->delay_constraint(*m_tc, c)) {
unsigned cidx = add_cnstr(c, cnstr_group::PluginDelayed);
add_meta_occs(lhs, cidx);
add_meta_occs(rhs, cidx);
@ -1078,9 +1064,8 @@ struct unifier_fn {
// should infer it, process generated
// constraints and save the result in
// m_type_map.
bool relax = relax_main_opaque(c);
constraint_seq cs;
optional<expr> t = infer(m, relax, cs);
optional<expr> t = infer(m, cs);
if (!t) {
set_conflict(c.get_justification());
return false;
@ -1237,8 +1222,7 @@ struct unifier_fn {
return lazy_list<constraints>();
justification const & j = c.get_justification();
constraint_seq cs;
bool relax = relax_main_opaque(c);
auto fcs = m_tc[relax]->is_def_eq(f_lhs, f_rhs, j);
auto fcs = m_tc->is_def_eq(f_lhs, f_rhs, j);
if (!fcs.first)
return lazy_list<constraints>();
cs = fcs.second;
@ -1248,7 +1232,7 @@ struct unifier_fn {
if (args_lhs.size() != args_rhs.size())
return lazy_list<constraints>();
for (unsigned i = 0; i < args_lhs.size(); i++) {
auto acs = m_tc[relax]->is_def_eq(args_lhs[i], args_rhs[i], j);
auto acs = m_tc->is_def_eq(args_lhs[i], args_rhs[i], j);
if (!acs.first)
return lazy_list<constraints>();
cs = acs.second + cs;
@ -1257,9 +1241,8 @@ struct unifier_fn {
}
bool process_plugin_constraint(constraint const & c) {
bool relax = relax_main_opaque(c);
lean_assert(!is_choice_cnstr(c));
lazy_list<constraints> alts = m_plugin->solve(*m_tc[relax], c, m_ngen.mk_child());
lazy_list<constraints> alts = m_plugin->solve(*m_tc, c, m_ngen.mk_child());
alts = append(alts, process_const_const_cnstr(c));
return process_lazy_constraints(alts, c.get_justification());
}
@ -1274,10 +1257,9 @@ struct unifier_fn {
m_owned_map.erase(mlocal_name(get_app_fn(m)));
}
expr m_type;
bool relax = relax_main_opaque(c);
constraint_seq cs;
if (auto type = infer(m, relax, cs)) {
if (auto type = infer(m, cs)) {
m_type = *type;
if (!process_constraints(cs))
return false;
@ -1313,12 +1295,11 @@ struct unifier_fn {
expr lhs_fn = get_app_rev_args(lhs, lhs_args);
expr rhs_fn = get_app_rev_args(rhs, rhs_args);
declaration d = *m_env.find(const_name(lhs_fn));
bool relax = relax_main_opaque(c);
expr lhs_fn_val = instantiate_value_univ_params(d, const_levels(lhs_fn));
expr rhs_fn_val = instantiate_value_univ_params(d, const_levels(rhs_fn));
expr t = apply_beta(lhs_fn_val, lhs_args.size(), lhs_args.data());
expr s = apply_beta(rhs_fn_val, rhs_args.size(), rhs_args.data());
auto dcs = m_tc[relax]->is_def_eq(t, s, j);
auto dcs = m_tc->is_def_eq(t, s, j);
if (dcs.first) {
constraints cnstrs = dcs.second.to_list();
return process_constraints(cnstrs, extra_j);
@ -1371,7 +1352,6 @@ struct unifier_fn {
return unfold_delta(c, justification());
justification a;
bool relax = relax_main_opaque(c);
if (m_config.m_kind == unifier_kind::Liberal &&
(m_config.m_computation || module::is_definition(m_env, d.get_name()) || is_at_least_quasireducible(m_env, d.get_name()))) {
// add case_split for t =?= s
@ -1393,7 +1373,7 @@ struct unifier_fn {
unsigned i = lhs_args.size();
while (i > 0) {
--i;
if (!is_def_eq(lhs_args[i], rhs_args[i], new_j, relax))
if (!is_def_eq(lhs_args[i], rhs_args[i], new_j))
return false;
}
return true;
@ -1429,7 +1409,6 @@ struct unifier_fn {
expr const & m;
expr const & rhs;
justification j;
bool relax;
buffer<constraints> & alts; // result: alternatives
bool imitation_only; // if true, then only imitation step is used
@ -1439,12 +1418,12 @@ struct unifier_fn {
bool pattern() const { return u.m_config.m_pattern; }
type_checker & tc() {
return *u.m_tc[relax];
return *u.m_tc;
}
type_checker & restricted_tc() {
if (u.m_config.m_computation)
return *u.m_tc[relax];
return *u.m_tc;
else
return *u.m_flex_rigid_tc;
}
@ -1529,7 +1508,7 @@ struct unifier_fn {
expr const & mtype = mlocal_type(m);
constraint_seq cs;
expr new_mtype = ensure_sufficient_args(mtype, cs);
cs = cs + mk_eq_cnstr(m, mk_lambda_for(new_mtype, rhs), j, relax);
cs = cs + mk_eq_cnstr(m, mk_lambda_for(new_mtype, rhs), j);
alts.push_back(cs.to_list());
}
@ -1570,7 +1549,7 @@ struct unifier_fn {
if (tc().is_def_eq_types(marg, rhs, j, cs) &&
restricted_is_def_eq(marg, rhs, j, cs)) {
expr v = mk_lambda_for(new_mtype, mk_var(vidx));
cs = cs + mk_eq_cnstr(m, v, j, relax);
cs = cs + mk_eq_cnstr(m, v, j);
alts.push_back(cs.to_list());
}
}
@ -1610,7 +1589,7 @@ struct unifier_fn {
constraint_seq cs;
auto new_mtype = ensure_sufficient_args(mtype, cs);
expr v = mk_lambda_for(new_mtype, mk_var(vidx));
cs = cs + mk_eq_cnstr(m, v, j, relax);
cs = cs + mk_eq_cnstr(m, v, j);
alts.push_back(cs.to_list());
if (cheap())
return;
@ -1694,12 +1673,12 @@ struct unifier_fn {
if (context_check(type, locals)) {
expr maux = mk_metavar(u.m_ngen.next(), Pi(locals, type));
// std::cout << " >> " << maux << " : " << mlocal_type(maux) << "\n";
cs = mk_eq_cnstr(mk_app(maux, margs), arg, j, relax) + cs;
cs = mk_eq_cnstr(mk_app(maux, margs), arg, j) + cs;
return mk_app(maux, locals);
} else {
expr maux_type = mk_metavar(u.m_ngen.next(), Pi(locals, mk_sort(mk_meta_univ(u.m_ngen.next()))));
expr maux = mk_metavar(u.m_ngen.next(), Pi(locals, mk_app(maux_type, locals)));
cs = mk_eq_cnstr(mk_app(maux, margs), arg, j, relax) + cs;
cs = mk_eq_cnstr(mk_app(maux, margs), arg, j) + cs;
return mk_app(maux, locals);
}
}
@ -1719,7 +1698,7 @@ struct unifier_fn {
}
} catch (exception&) {}
expr v = Fun(locals, mk_app(f, sargs));
cs += mk_eq_cnstr(m, v, j, relax);
cs += mk_eq_cnstr(m, v, j);
alts.push_back(cs.to_list());
}
@ -1797,7 +1776,7 @@ struct unifier_fn {
expr binding = is_pi(rhs) ? Pi(local, B) : Fun(local, B);
locals.pop_back();
expr v = Fun(locals, binding);
cs += mk_eq_cnstr(m, v, j, relax);
cs += mk_eq_cnstr(m, v, j);
alts.push_back(cs.to_list());
} catch (exception&) {}
margs.pop_back();
@ -1805,9 +1784,9 @@ struct unifier_fn {
public:
flex_rigid_core_fn(unifier_fn & _u, expr const & _lhs, expr const & _rhs,
justification const & _j, bool _relax, buffer<constraints> & _alts,
justification const & _j, buffer<constraints> & _alts,
bool _imitation_only):
u(_u), lhs(_lhs), m(get_app_args(lhs, margs)), rhs(_rhs), j(_j), relax(_relax), alts(_alts),
u(_u), lhs(_lhs), m(get_app_args(lhs, margs)), rhs(_rhs), j(_j), alts(_alts),
imitation_only(_imitation_only) {}
void operator()() {
@ -1838,9 +1817,9 @@ struct unifier_fn {
}
};
void process_flex_rigid_core(expr const & lhs, expr const & rhs, justification const & j, bool relax,
void process_flex_rigid_core(expr const & lhs, expr const & rhs, justification const & j,
buffer<constraints> & alts, bool imitation_only) {
flex_rigid_core_fn(*this, lhs, rhs, j, relax, alts, imitation_only)();
flex_rigid_core_fn(*this, lhs, rhs, j, alts, imitation_only)();
}
/** \brief When lhs is an application (f ...), make sure that if any argument that is reducible to a
@ -1849,14 +1828,14 @@ struct unifier_fn {
\remark We store auxiliary constraints created in the reductions in \c aux. We return the new
"reduce" application.
*/
expr expose_local_args(expr const & lhs, justification const & j, bool relax, buffer<constraint> & aux) {
expr expose_local_args(expr const & lhs, justification const & j, buffer<constraint> & aux) {
buffer<expr> margs;
expr m = get_app_args(lhs, margs);
bool modified = false;
for (expr & marg : margs) {
// Make sure that if marg is reducible to a local constant, then it is replaced with it.
if (!is_local(marg)) {
expr new_marg = whnf(marg, j, relax, aux);
expr new_marg = whnf(marg, j, aux);
if (is_local(new_marg)) {
marg = new_marg;
modified = true;
@ -1866,14 +1845,14 @@ struct unifier_fn {
return modified ? mk_app(m, margs) : lhs;
}
optional<expr> expand_rhs(expr const & rhs, bool relax) {
optional<expr> expand_rhs(expr const & rhs) {
buffer<expr> args;
expr const & f = get_app_rev_args(rhs, args);
lean_assert(!is_local(f) && !is_constant(f) && !is_var(f) && !is_metavar(f));
if (is_lambda(f)) {
return some_expr(apply_beta(f, args.size(), args.data()));
} else if (is_macro(f)) {
if (optional<expr> new_f = m_tc[relax]->expand_macro(f))
if (optional<expr> new_f = m_tc->expand_macro(f))
return some_expr(mk_rev_app(*new_f, args.size(), args.data()));
}
return none_expr();
@ -1907,42 +1886,42 @@ struct unifier_fn {
}
/** \brief Process a flex rigid constraint */
bool process_flex_rigid(expr lhs, expr const & rhs, justification const & j, bool relax) {
bool process_flex_rigid(expr lhs, expr const & rhs, justification const & j) {
lean_assert(is_meta(lhs));
lean_assert(!is_meta(rhs));
if (is_app(rhs)) {
expr const & f = get_app_fn(rhs);
if (!is_local(f) && !is_constant(f)) {
if (auto new_rhs = expand_rhs(rhs, relax)) {
if (auto new_rhs = expand_rhs(rhs)) {
lean_assert(*new_rhs != rhs);
return is_def_eq(lhs, *new_rhs, j, relax);
return is_def_eq(lhs, *new_rhs, j);
} else {
return false;
}
}
} else if (is_macro(rhs)) {
if (auto new_rhs = expand_rhs(rhs, relax)) {
if (auto new_rhs = expand_rhs(rhs)) {
lean_assert(*new_rhs != rhs);
return is_def_eq(lhs, *new_rhs, j, relax);
return is_def_eq(lhs, *new_rhs, j);
} else {
return false;
}
}
buffer<constraint> aux;
lhs = expose_local_args(lhs, j, relax, aux);
lhs = expose_local_args(lhs, j, aux);
buffer<constraints> alts;
process_flex_rigid_core(lhs, rhs, j, relax, alts, false);
process_flex_rigid_core(lhs, rhs, j, alts, false);
append_auxiliary_constraints(alts, to_list(aux.begin(), aux.end()));
if (use_flex_rigid_whnf_split(lhs, rhs)) {
expr rhs_whnf = flex_rigid_whnf(rhs, j, relax, aux);
expr rhs_whnf = flex_rigid_whnf(rhs, j, aux);
if (rhs_whnf != rhs) {
if (is_meta(rhs_whnf)) {
// it become a flex-flex constraint
alts.push_back(constraints(mk_eq_cnstr(lhs, rhs_whnf, j, relax)));
alts.push_back(constraints(mk_eq_cnstr(lhs, rhs_whnf, j)));
} else {
buffer<constraints> alts2;
process_flex_rigid_core(lhs, rhs_whnf, j, relax, alts2, true);
process_flex_rigid_core(lhs, rhs_whnf, j, alts2, true);
append_auxiliary_constraints(alts2, to_list(aux.begin(), aux.end()));
alts.append(alts2);
}
@ -1975,11 +1954,10 @@ struct unifier_fn {
lean_assert(is_flex_rigid(c));
expr lhs = cnstr_lhs_expr(c);
expr rhs = cnstr_rhs_expr(c);
bool relax = relax_main_opaque(c);
if (is_meta(lhs))
return process_flex_rigid(lhs, rhs, c.get_justification(), relax);
return process_flex_rigid(lhs, rhs, c.get_justification());
else
return process_flex_rigid(rhs, lhs, c.get_justification(), relax);
return process_flex_rigid(rhs, lhs, c.get_justification());
}
void postpone(constraint const & c) {
@ -2019,9 +1997,9 @@ struct unifier_fn {
break;
if (i == min_sz) {
if (lhs_args.size() >= rhs_args.size()) {
return assign(lhs, ml, lhs_args, rhs, c.get_justification(), relax_main_opaque(c));
return assign(lhs, ml, lhs_args, rhs, c.get_justification());
} else {
return assign(rhs, mr, rhs_args, lhs, c.get_justification(), relax_main_opaque(c));
return assign(rhs, mr, rhs_args, lhs, c.get_justification());
}
} else {
discard(c);
@ -2263,7 +2241,7 @@ struct unifier_fn {
if (is_delta_cnstr(c)) {
return process_delta(c);
} else if (modified) {
return is_def_eq(cnstr_lhs_expr(c), cnstr_rhs_expr(c), c.get_justification(), relax_main_opaque(c));
return is_def_eq(cnstr_lhs_expr(c), cnstr_rhs_expr(c), c.get_justification());
} else if (auto d = is_owned(c)) {
// Metavariable in the constraint is owned by choice constraint.
// choice constraint was postponed... since c was not modifed
@ -2353,13 +2331,13 @@ unify_result_seq unify(environment const & env, unsigned num_cs, constraint con
}
unify_result_seq unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
bool relax, substitution const & s, unifier_config const & cfg) {
substitution const & s, unifier_config const & cfg) {
substitution new_s = s;
expr _lhs = new_s.instantiate(lhs);
expr _rhs = new_s.instantiate(rhs);
auto u = std::make_shared<unifier_fn>(env, 0, nullptr, ngen, new_s, cfg);
constraint_seq cs;
if (!u->m_tc[relax]->is_def_eq(_lhs, _rhs, justification(), cs) || !u->process_constraints(cs)) {
if (!u->m_tc->is_def_eq(_lhs, _rhs, justification(), cs) || !u->process_constraints(cs)) {
return unify_result_seq();
} else {
return unify(u);
@ -2485,13 +2463,13 @@ static int unify(lua_State * L) {
unify_result_seq r;
environment const & env = to_environment(L, 1);
if (is_expr(L, 2)) {
if (nargs == 7)
r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), lua_toboolean(L, 5), to_substitution(L, 6),
unifier_config(to_options(L, 7)));
else if (nargs == 6)
r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), lua_toboolean(L, 5), to_substitution(L, 6));
if (nargs == 6)
r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5),
unifier_config(to_options(L, 6)));
else if (nargs == 5)
r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5));
else
r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), lua_toboolean(L, 5));
r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4));
} else {
buffer<constraint> cs;
to_constraint_buffer(L, 2, cs);
@ -2539,7 +2517,7 @@ void initialize_unifier() {
register_bool_option(*g_unifier_nonchronological, LEAN_DEFAULT_UNIFIER_NONCHRONOLOGICAL,
"(unifier) enable/disable nonchronological backtracking in the unifier (this option is only available for debugging and benchmarking purposes, and running experiments)");
g_dont_care_cnstr = new constraint(mk_eq_cnstr(expr(), expr(), justification(), false));
g_dont_care_cnstr = new constraint(mk_eq_cnstr(expr(), expr(), justification()));
g_tmp_prefix = new name(name::mk_internal_unique_name());
}

2
src/library/unifier.h
View file

@ -77,7 +77,7 @@ typedef lazy_list<pair<substitution, constraints>> unify_result_seq;
unify_result_seq unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen,
substitution const & s = substitution(), unifier_config const & c = unifier_config());
unify_result_seq unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
bool relax_main_opaque, substitution const & s = substitution(), unifier_config const & c = unifier_config());
substitution const & s = substitution(), unifier_config const & c = unifier_config());
/**
The unifier divides the constraints in 9 groups: Simple, Basic, FlexRigid, PluginDelayed, DelayedChoice, ClassInstance,

2
src/library/update_declaration.cpp
View file

@ -31,7 +31,7 @@ static declaration update_declaration(declaration d, optional<level_param_names>
return mk_theorem(d.get_name(), _ps, _type, _value);
else
return mk_definition(d.get_name(), _ps, _type, _value, d.is_opaque(),
d.get_weight(), d.get_module_idx(), d.use_conv_opt());
d.get_weight(), d.use_conv_opt());
}
}

5
src/library/util.cpp
View file

@ -627,8 +627,7 @@ constraint instantiate_metavars(constraint const & c, substitution & s) {
case constraint_kind::Eq:
return mk_eq_cnstr(s.instantiate_all(cnstr_lhs_expr(c)),
s.instantiate_all(cnstr_rhs_expr(c)),
c.get_justification(),
relax_main_opaque(c));
c.get_justification());
case constraint_kind::LevelEq:
return mk_level_eq_cnstr(s.instantiate(cnstr_lhs_level(c)), s.instantiate(cnstr_rhs_level(c)), c.get_justification());
case constraint_kind::Choice: {
@ -642,7 +641,7 @@ constraint instantiate_metavars(constraint const & c, substitution & s) {
return mk_choice_cnstr(mk_app(mvar, args),
cnstr_choice_fn(c),
cnstr_delay_factor_core(c),
cnstr_is_owner(c), c.get_justification(), relax_main_opaque(c));
cnstr_is_owner(c), c.get_justification());
}}
lean_unreachable(); // LCOV_EXCL_LINE
}

2
src/tests/library/unifier.cpp
View file

@ -23,7 +23,7 @@ static void tst1() {
expr m = mk_metavar("m", A);
expr t1 = mk_app(f, m, m);
expr t2 = mk_app(f, a, b);
auto r = unify(env, t1, t2, ngen, false);
auto r = unify(env, t1, t2, ngen);
lean_assert(!r.pull());
}

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

@ -6,7 +6,7 @@ definition two2 : nat := succ (succ (zero))
constant f : nat → nat → nat
(*
local tc = type_checker_with_hints(get_env(), true)
local tc = type_checker_with_hints(get_env())
local plugin = whnf_match_plugin(tc)
function tst_match(p, t)
local r1, r2 = match(p, t, plugin)

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

@ -8,7 +8,7 @@ constant g : nat → nat → nat
constants a b : nat
(*
local tc = type_checker_with_hints(get_env(), true)
local tc = type_checker_with_hints(get_env())
local plugin = whnf_match_plugin(tc)
function tst_match(p, t)
local r1, r2 = match(p, t, plugin)

8
tests/lua/def1.lua
View file

@ -29,25 +29,21 @@ assert(th2:name() == name("t2"))
local d = mk_definition("d1", A, B)
assert(d:is_definition())
assert(not d:is_theorem())
assert(d:opaque())
assert(d:weight() == 0)
assert(d:module_idx() == 0)
assert(d:use_conv_opt())
assert(d:name() == name("d1"))
assert(d:value() == B)
local d2 = mk_definition("d2", A, B, nil)
local d3 = mk_definition("d3", A, B, {opaque=false, weight=100, module_idx=10, use_conv_opt=false})
local d3 = mk_definition("d3", A, B, {opaque=false, weight=100, use_conv_opt=false})
assert(not d3:opaque())
assert(d3:weight() == 100)
assert(d3:module_idx() == 10)
assert(not d3:use_conv_opt())
local env = bare_environment()
local d4 = mk_definition(env, "bool", Type, Prop)
assert(d4:weight() == 1)
local d5 = mk_definition(env, "bool", Type, Prop, {opaque=false, weight=100, module_idx=3, use_conv_opt=true})
local d5 = mk_definition(env, "bool", Type, Prop, {opaque=false, weight=100, use_conv_opt=true})
assert(not d5:opaque())
assert(d5:weight() == 1)
assert(d5:module_idx() == 3)
assert(d5:use_conv_opt())
local d6 = mk_definition("d6", {"l1", "l2"}, A, B, {opaque=true, weight=5})
assert(d6:type() == A)