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

fix(*): make sure elaborator and type_checker use the same "rules" for treating opaque definitions

Browse source 
This is a big change because we have to store in constraints whether we can use the "relaxed" rules or not.
The "relaxed" case says that when type checking the value of an opaque definition we can treat other opaque definitions in the same module as transparent.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-27 12:01:06 -07:00
parent 83d38674c9
commit faee08591f
29 changed files with 303 additions and 214 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -86,7 +86,7 @@ environment check_cmd(parser & p) {
level_param_names ls = to_level_param_names(collect_univ_params(e));
level_param_names new_ls;
std::tie(e, new_ls) = p.elaborate_relaxed(e, ctx);
auto tc = mk_type_checker_with_hints(p.env(), p.mk_ngen());
auto tc = mk_type_checker_with_hints(p.env(), p.mk_ngen(), true);
expr type = tc->check(e, append(ls, new_ls));
auto reg = p.regular_stream();
formatter const & fmt = reg.get_formatter();
@ -270,7 +270,7 @@ environment opaque_hint_cmd(parser & p) {
if (p.curr_is_token(g_module)) {
found = true;
p.next();
env = set_main_module_opaque_defs(env, hiding);
env = set_hide_main_opaque(env, hiding);
} else {
name c = p.check_constant_next("invalid 'opaque_hint', constant expected");
found = true;

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

@ -271,11 +271,11 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
std::tie(type, new_ls) = p.elaborate_type(type);
env = module::add(env, check(env, mk_axiom(real_n, append(ls, new_ls), type)));
} else {
std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value);
std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value, modifiers.m_is_opaque);
env = module::add(env, check(env, mk_theorem(real_n, append(ls, new_ls), type, value)));
}
} else {
std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value);
std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value, modifiers.m_is_opaque);
env = module::add(env, check(env, mk_definition(env, real_n, append(ls, new_ls), type, value, modifiers.m_is_opaque)));
}
if (real_n != n)

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

@ -131,7 +131,7 @@ class elaborator {
local_decls<level> m_lls;
io_state m_ios;
name_generator m_ngen;
type_checker_ptr m_tc;
type_checker_ptr m_tc[2];
substitution m_subst;
expr_map<expr> m_cache; // (pointer equality) cache for Type and Constants (this is a trick to make sure we get the
// same universe metavariable for different occurrences of the same Type/Constant
@ -148,6 +148,7 @@ class elaborator {
name_set m_displayed_errors; // set of metavariables that we already reported unsolved/unassigned
bool m_check_unassigned; // if true if display error messages if elaborated term still contains metavariables
bool m_use_local_instances; // if true class-instance resolution will use the local context
bool m_relax_main_opaque; // if true, then treat opaque definitions from the main module as transparent
// Set m_ctx to ctx, and make sure m_ctx_buffer and m_ctx_domain_buffer reflect the contents of the new ctx
void set_ctx(context const & ctx) {
@ -173,12 +174,14 @@ class elaborator {
lean_assert(m_main.m_accumulated.is_none());
m_old_ctx = m_main.m_ctx;
m_main.set_ctx(ctx);
m_main.m_tc->push();
m_main.m_tc[0]->push();
m_main.m_tc[1]->push();
m_main.m_subst = s;
}
~scope() {
m_main.set_ctx(m_old_ctx);
m_main.m_tc->pop();
m_main.m_tc[0]->pop();
m_main.m_tc[1]->pop();
m_main.m_constraints.clear();
m_main.m_accumulated = justification();
m_main.m_subst = substitution();
@ -189,8 +192,9 @@ class elaborator {
/* \brief Move all constraints generated by the type checker to the buffer m_constraints. */
void consume_tc_cnstrs() {
while (auto c = m_tc->next_cnstr())
m_constraints.push_back(*c);
for (unsigned i = 0; i < 2; i++)
while (auto c = m_tc[i]->next_cnstr())
m_constraints.push_back(*c);
}
struct choice_elaborator {
@ -212,8 +216,9 @@ class elaborator {
context m_ctx;
substitution m_subst;
unsigned m_idx;
choice_expr_elaborator(elaborator & elab, expr const & mvar, expr const & c, context const & ctx, substitution const & s):
m_elab(elab), m_mvar(mvar), m_choice(c), m_ctx(ctx), m_subst(s), m_idx(0) {
bool m_relax_main_opaque;
choice_expr_elaborator(elaborator & elab, expr const & mvar, expr const & c, context const & ctx, substitution const & s, bool relax):
m_elab(elab), m_mvar(mvar), m_choice(c), m_ctx(ctx), m_subst(s), m_idx(0), m_relax_main_opaque(relax) {
}
virtual optional<constraints> next() {
@ -226,7 +231,7 @@ class elaborator {
justification j = m_elab.m_accumulated;
m_elab.consume_tc_cnstrs();
list<constraint> cs = to_list(m_elab.m_constraints.begin(), m_elab.m_constraints.end());
cs = cons(mk_eq_cnstr(m_mvar, r, j), cs);
cs = cons(mk_eq_cnstr(m_mvar, r, j, m_relax_main_opaque), cs);
return optional<constraints>(cs);
} catch (exception &) {}
}
@ -263,13 +268,14 @@ class elaborator {
context m_ctx; // local context for m_meta
substitution m_subst;
justification m_jst;
bool m_relax_main_opaque;
placeholder_elaborator(elaborator & elab, expr const & meta, expr const & meta_type,
list<expr> const & local_insts, list<name> const & instances, list<tactic_hint_entry> const & tacs,
context const & ctx, substitution const & s, justification const & j, bool ignore_failure):
context const & ctx, substitution const & s, justification const & j, bool ignore_failure, bool relax):
choice_elaborator(ignore_failure),
m_elab(elab), m_meta(meta), m_meta_type(meta_type), m_local_instances(local_insts), m_instances(instances),
m_tactics(tacs), m_ctx(ctx), m_subst(s), m_jst(j) {
m_tactics(tacs), m_ctx(ctx), m_subst(s), m_jst(j), m_relax_main_opaque(relax) {
collect_metavars(meta_type, m_mvars_in_meta_type);
}
@ -292,7 +298,7 @@ class elaborator {
for (auto & c : m_elab.m_constraints)
c = update_justification(c, mk_composite1(m_jst, c.get_justification()));
list<constraint> cs = to_list(m_elab.m_constraints.begin(), m_elab.m_constraints.end());
cs = cons(mk_eq_cnstr(m_meta, r, mk_composite1(m_jst, j)), cs);
cs = cons(mk_eq_cnstr(m_meta, r, mk_composite1(m_jst, j), m_relax_main_opaque), cs);
return optional<constraints>(cs);
} catch (exception &) {
return optional<constraints>();
@ -307,9 +313,9 @@ class elaborator {
substitution subst = next->first.get_subst();
buffer<constraint> cs;
expr const & mvar = get_app_fn(m_meta);
cs.push_back(mk_eq_cnstr(mvar, subst.instantiate(mvar), m_jst));
cs.push_back(mk_eq_cnstr(mvar, subst.instantiate(mvar), m_jst, m_relax_main_opaque));
for (auto const & mvar : m_mvars_in_meta_type)
cs.push_back(mk_eq_cnstr(mvar, subst.instantiate(mvar), m_jst));
cs.push_back(mk_eq_cnstr(mvar, subst.instantiate(mvar), m_jst, m_relax_main_opaque));
return optional<constraints>(to_list(cs.begin(), cs.end()));
}
return optional<constraints>();
@ -319,7 +325,7 @@ class elaborator {
while (!empty(m_local_instances)) {
expr inst = head(m_local_instances);
m_local_instances = tail(m_local_instances);
constraints cs(mk_eq_cnstr(m_meta, inst, m_jst));
constraints cs(mk_eq_cnstr(m_meta, inst, m_jst, m_relax_main_opaque));
return optional<constraints>(cs);
}
while (!empty(m_instances)) {
@ -362,8 +368,11 @@ public:
elaborator(environment const & env, local_decls<level> const & lls, list<expr> const & ctx, io_state const & ios, name_generator const & ngen,
pos_info_provider * pp, bool check_unassigned):
m_env(env), m_lls(lls), m_ios(ios),
m_ngen(ngen), m_tc(mk_type_checker_with_hints(env, m_ngen.mk_child())),
m_ngen(ngen),
m_pos_provider(pp) {
m_relax_main_opaque = false;
m_tc[0] = mk_type_checker_with_hints(env, m_ngen.mk_child(), false);
m_tc[1] = mk_type_checker_with_hints(env, m_ngen.mk_child(), true);
m_check_unassigned = check_unassigned;
m_use_local_instances = get_elaborator_local_instances(ios.get_options());
set_ctx(ctx);
@ -375,10 +384,11 @@ public:
expr infer_type(expr const & e) {
lean_assert(closed(e));
return m_tc->infer(e); }
return m_tc[m_relax_main_opaque]->infer(e);
}
expr whnf(expr const & e) {
return m_tc->whnf(e);
return m_tc[m_relax_main_opaque]->whnf(e);
}
/** \brief Clear constraint buffer \c m_constraints, and associated datastructures
@ -593,7 +603,7 @@ public:
return lazy_list<constraints>(); // nothing to be done
bool ignore_failure = false; // we are always strict with placeholders associated with classes
return choose(std::make_shared<placeholder_elaborator>(*this, meta, meta_type, local_insts, insts, tacs, ctx, s, j,
ignore_failure));
ignore_failure, m_relax_main_opaque));
} else if (s.is_assigned(mvar)) {
// if the metavariable is assigned and it is not a class, then we just ignore it, and return
// the an empty set of constraints.
@ -602,10 +612,10 @@ public:
list<tactic_hint_entry> tacs = get_tactic_hints(m_env);
bool ignore_failure = !is_strict;
return choose(std::make_shared<placeholder_elaborator>(*this, meta, meta_type, list<expr>(), list<name>(), tacs, ctx, s, j,
ignore_failure));
ignore_failure, m_relax_main_opaque));
}
};
add_cnstr(mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::MaxDelayed), j));
add_cnstr(mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::MaxDelayed), j, m_relax_main_opaque));
return m;
}
@ -642,11 +652,12 @@ public:
// Possible optimization: try to lookahead and discard some of the alternatives.
expr m = mk_meta(t, e.get_tag());
context ctx = m_ctx;
bool relax = m_relax_main_opaque;
auto fn = [=](expr const & mvar, expr const & /* type */, substitution const & s, name_generator const & /* ngen */) {
return choose(std::make_shared<choice_expr_elaborator>(*this, mvar, e, ctx, s));
return choose(std::make_shared<choice_expr_elaborator>(*this, mvar, e, ctx, s, relax));
};
justification j = mk_justification("none of the overloads is applicable", some_expr(e));
add_cnstr(mk_choice_cnstr(m, fn, to_delay_factor(cnstr_group::Basic), j));
add_cnstr(mk_choice_cnstr(m, fn, to_delay_factor(cnstr_group::Basic), j, m_relax_main_opaque));
return m;
}
@ -670,7 +681,7 @@ public:
f_type = whnf(instantiate_metavars(f_type));
if (!is_pi(f_type) && is_meta(f_type)) {
// let type checker add constraint
f_type = m_tc->ensure_pi(f_type, f);
f_type = m_tc[m_relax_main_opaque]->ensure_pi(f_type, f);
}
}
if (!is_pi(f_type)) {
@ -710,6 +721,7 @@ public:
}
constraint mk_delayed_coercion_cnstr(expr const & m, expr const & a, expr const & a_type, justification const & j, unsigned delay_factor) {
bool relax = m_relax_main_opaque;
auto choice_fn = [=](expr const & mvar, expr const & new_d_type, substitution const & /* s */, name_generator const & /* ngen */) {
// Remark: we want the coercions solved before we start discarding FlexFlex constraints. So, we use PreFlexFlex as a max cap
// for delaying coercions.
@ -718,10 +730,10 @@ public:
return lazy_list<constraints>(constraints(mk_delayed_coercion_cnstr(m, a, a_type, justification(), delay_factor+1)));
} else {
expr r = apply_coercion(a, a_type, new_d_type);
return lazy_list<constraints>(constraints(mk_eq_cnstr(mvar, r, justification())));
return lazy_list<constraints>(constraints(mk_eq_cnstr(mvar, r, justification(), relax)));
}
};
return mk_choice_cnstr(m, choice_fn, delay_factor, j);
return mk_choice_cnstr(m, choice_fn, delay_factor, j, m_relax_main_opaque);
}
/** \brief Given an application \c e, where the expected type is d_type, and the argument type is a_type,
@ -792,19 +804,19 @@ public:
return mk_delayed_coercion(r, d_type, a_type);
} else {
app_delayed_justification j(r, f_type, a_type);
if (!m_tc->is_def_eq(a_type, d_type, j)) {
if (!m_tc[m_relax_main_opaque]->is_def_eq(a_type, d_type, j)) {
expr new_a = apply_coercion(a, a_type, d_type);
bool coercion_worked = false;
if (!is_eqp(a, new_a)) {
expr new_a_type = instantiate_metavars(infer_type(new_a));
coercion_worked = m_tc->is_def_eq(new_a_type, d_type, j);
coercion_worked = m_tc[m_relax_main_opaque]->is_def_eq(new_a_type, d_type, j);
}
if (coercion_worked) {
r = update_app(r, f, new_a);
} else {
if (has_metavar(a_type) || has_metavar(d_type)) {
// rely on unification hints to solve this constraint
add_cnstr(mk_eq_cnstr(a_type, d_type, j.get()));
add_cnstr(mk_eq_cnstr(a_type, d_type, j.get(), m_relax_main_opaque));
} else {
throw_kernel_exception(m_env, r, [=](formatter const & fmt) { return pp_app_type_mismatch(fmt, e, d_type, a_type); });
}
@ -888,7 +900,7 @@ public:
return e;
if (is_meta(t)) {
// let type checker add constraint
m_tc->ensure_sort(t, e);
m_tc[m_relax_main_opaque]->ensure_sort(t, e);
return e;
}
}
@ -1112,7 +1124,7 @@ public:
if (!meta)
return;
meta = instantiate_meta(*meta, subst);
expr type = m_tc->infer(*meta);
expr type = m_tc[m_relax_main_opaque]->infer(*meta);
// first solve unassigned metavariables in type
type = solve_unassigned_mvars(subst, type, visited);
proof_state ps(goals(goal(*meta, type)), subst, m_ngen.mk_child());
@ -1173,7 +1185,8 @@ public:
return std::make_tuple(r, to_list(new_ps.begin(), new_ps.end()));
}
std::tuple<expr, level_param_names> operator()(expr const & e, bool _ensure_type) {
std::tuple<expr, level_param_names> operator()(expr const & e, bool _ensure_type, bool relax_main_opaque) {
flet<bool> set_relax(m_relax_main_opaque, relax_main_opaque && !get_hide_main_opaque(m_env));
expr r = visit(e);
if (_ensure_type)
r = ensure_type(r);
@ -1183,16 +1196,18 @@ public:
return apply(s, r);
}
std::tuple<expr, expr, level_param_names> operator()(expr const & t, expr const & v, name const & n) {
std::tuple<expr, expr, level_param_names> operator()(expr const & t, expr const & v, name const & n, bool is_opaque) {
lean_assert(!has_local(t)); lean_assert(!has_local(v));
expr r_t = ensure_type(visit(t));
// 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 && !get_hide_main_opaque(m_env));
expr r_v = visit(v);
expr r_v_type = infer_type(r_v);
justification j = mk_justification(v, [=](formatter const & fmt, substitution const & subst) {
substitution s(subst);
return pp_def_type_mismatch(fmt, n, s.instantiate(r_t), s.instantiate(r_v_type));
});
if (!m_tc->is_def_eq(r_v_type, r_t, j)) {
if (!m_tc[is_opaque]->is_def_eq(r_v_type, r_t, j)) {
throw_kernel_exception(m_env, v, [=](formatter const & fmt) { return pp_def_type_mismatch(fmt, n, r_t, r_v_type); });
}
auto p = solve().pull();
@ -1209,13 +1224,13 @@ public:
static name g_tmp_prefix = name::mk_internal_unique_name();
std::tuple<expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls, list<expr> const & ctx,
io_state const & ios, expr const & e, pos_info_provider * pp, bool check_unassigned,
bool ensure_type) {
return elaborator(env, lls, ctx, ios, name_generator(g_tmp_prefix), pp, check_unassigned)(e, ensure_type);
io_state const & ios, expr const & e, bool relax_main_opaque,
pos_info_provider * pp, bool check_unassigned, bool ensure_type) {
return elaborator(env, lls, ctx, ios, name_generator(g_tmp_prefix), pp, check_unassigned)(e, ensure_type, relax_main_opaque);
}
std::tuple<expr, expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls, io_state const & ios,
name const & n, expr const & t, expr const & v, pos_info_provider * pp) {
return elaborator(env, lls, list<expr>(), ios, name_generator(g_tmp_prefix), pp, true)(t, v, n);
name const & n, expr const & t, expr const & v, bool is_opaque, pos_info_provider * pp) {
return elaborator(env, lls, list<expr>(), ios, name_generator(g_tmp_prefix), pp, true)(t, v, n, is_opaque);
}
}

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

@ -14,9 +14,9 @@ Author: Leonardo de Moura
namespace lean {
std::tuple<expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls, list<expr> const & ctx,
io_state const & ios, expr const & e, pos_info_provider * pp = nullptr,
bool check_unassigned = true, bool ensure_type = false);
io_state const & ios, expr const & e, bool relax_main_opaque,
pos_info_provider * pp = nullptr, bool check_unassigned = true, bool ensure_type = false);
std::tuple<expr, expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls,
io_state const & ios, name const & n, expr const & t, expr const & v,
pos_info_provider * pp = nullptr);
bool is_opaque, pos_info_provider * pp = nullptr);
}

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

@ -90,7 +90,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_with_hints(m_env, m_p.mk_ngen());
m_tc = mk_type_checker_with_hints(m_env, m_p.mk_ngen(), false);
}
[[ noreturn ]] void throw_error(char const * error_msg) { throw parser_error(error_msg, m_pos); }
@ -402,7 +402,7 @@ struct inductive_cmd_fn {
std::tie(d_name, d_type, std::ignore) = d;
m_env = m_env.add(check(m_env, mk_var_decl(d_name, ls, d_type)));
}
m_tc = mk_type_checker_with_hints(m_env, m_p.mk_ngen());
m_tc = mk_type_checker_with_hints(m_env, m_p.mk_ngen(), false);
}
/** \brief Traverse the introduction rule type and collect the universes where non-parameters reside in \c r_lvls.

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

@ -485,28 +485,34 @@ level parser::parse_level(unsigned rbp) {
std::tuple<expr, level_param_names> parser::elaborate_relaxed(expr const & e, list<expr> const & ctx) {
parser_pos_provider pp = get_pos_provider();
return ::lean::elaborate(m_env, m_local_level_decls, ctx, m_ios, e, &pp, false);
bool relax = true;
bool check_unassigned = false;
return ::lean::elaborate(m_env, m_local_level_decls, ctx, m_ios, e, relax, &pp, check_unassigned);
}
std::tuple<expr, level_param_names> parser::elaborate_type(expr const & e, list<expr> const & ctx) {
parser_pos_provider pp = get_pos_provider();
return ::lean::elaborate(m_env, m_local_level_decls, ctx, m_ios, e, &pp, true, true);
bool relax = false;
bool ensure_type = true;
bool check_unassigned = true;
return ::lean::elaborate(m_env, m_local_level_decls, ctx, m_ios, e, relax, &pp, check_unassigned, ensure_type);
}
std::tuple<expr, level_param_names> parser::elaborate_at(environment const & env, expr const & e) {
parser_pos_provider pp = get_pos_provider();
return ::lean::elaborate(env, m_local_level_decls, list<expr>(), m_ios, e, &pp);
bool relax = false;
return ::lean::elaborate(env, m_local_level_decls, list<expr>(), m_ios, e, relax, &pp);
}
std::tuple<expr, expr, level_param_names> parser::elaborate_definition(name const & n, expr const & t, expr const & v) {
std::tuple<expr, expr, level_param_names> parser::elaborate_definition(name const & n, expr const & t, expr const & v, bool is_opaque) {
parser_pos_provider pp = get_pos_provider();
return ::lean::elaborate(m_env, m_local_level_decls, m_ios, n, t, v, &pp);
return ::lean::elaborate(m_env, m_local_level_decls, m_ios, n, t, v, is_opaque, &pp);
}
std::tuple<expr, expr, level_param_names> parser::elaborate_definition_at(environment const & env, local_level_decls const & lls,
name const & n, expr const & t, expr const & v) {
name const & n, expr const & t, expr const & v, bool is_opaque) {
parser_pos_provider pp = get_pos_provider();
return ::lean::elaborate(env, lls, m_ios, n, t, v, &pp);
return ::lean::elaborate(env, lls, m_ios, n, t, v, is_opaque, &pp);
}
[[ noreturn ]] void throw_invalid_open_binder(pos_info const & pos) {

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

@ -262,9 +262,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);
std::tuple<expr, expr, level_param_names> elaborate_definition(name const & n, expr const & t, expr const & v, bool is_opaque);
/** \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);
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);
parser_pos_provider get_pos_provider() const { return parser_pos_provider(m_pos_table, get_stream_name(), m_last_cmd_pos); }

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

@ -16,7 +16,8 @@ void theorem_queue::add(environment const & env, name const & n, level_param_nam
m_queue.add([=]() {
level_param_names new_ls;
expr type, value;
std::tie(type, value, new_ls) = m_parser.elaborate_definition_at(env, lls, n, t, v);
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);
return check(env, mk_theorem(n, append(ls, new_ls), type, value));
});
}

26
src/kernel/constraint.cpp
View file

@ -12,28 +12,29 @@ struct constraint_cell {
MK_LEAN_RC()
constraint_kind m_kind;
justification m_jst;
constraint_cell(constraint_kind k, justification const & j):m_rc(1), m_kind(k), m_jst(j) {}
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) {}
};
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):
constraint_cell(constraint_kind::Eq, j),
eq_constraint_cell(expr const & lhs, expr const & rhs, justification const & j, bool relax):
constraint_cell(constraint_kind::Eq, j, relax),
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),
constraint_cell(constraint_kind::LevelEq, j, false),
m_lhs(lhs), m_rhs(rhs) {}
};
struct choice_constraint_cell : public constraint_cell {
expr m_expr;
choice_fn m_fn;
unsigned m_delay_factor;
choice_constraint_cell(expr const & e, choice_fn const & fn, unsigned delay_factor, justification const & j):
constraint_cell(constraint_kind::Choice, j),
choice_constraint_cell(expr const & e, choice_fn const & fn, unsigned delay_factor, justification const & j, bool relax):
constraint_cell(constraint_kind::Choice, j, relax),
m_expr(e), m_fn(fn), m_delay_factor(delay_factor) {}
};
@ -57,19 +58,20 @@ 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) {
return constraint(new eq_constraint_cell(lhs, rhs, j));
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_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, unsigned delay_factor, justification const & j) {
constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j, bool relax_main_opaque) {
lean_assert(is_meta(m));
return constraint(new choice_constraint_cell(m, fn, delay_factor, j));
return constraint(new choice_constraint_cell(m, fn, delay_factor, j, relax_main_opaque));
}
expr const & cnstr_lhs_expr(constraint const & c) { lean_assert(is_eq_cnstr(c)); return static_cast<eq_constraint_cell*>(c.raw())->m_lhs; }
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;
@ -89,11 +91,11 @@ unsigned cnstr_delay_factor(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);
return mk_eq_cnstr(cnstr_lhs_expr(c), cnstr_rhs_expr(c), j, relax_main_opaque(c));
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), cnstr_delay_factor(c), j);
return mk_choice_cnstr(cnstr_expr(c), cnstr_choice_fn(c), cnstr_delay_factor(c), j, relax_main_opaque(c));
}
lean_unreachable(); // LCOV_EXCL_LINE
}

15
src/kernel/constraint.h
View file

@ -65,9 +65,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);
friend constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j, bool relax_main_opaque);
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, unsigned delay_factor, justification const & j);
friend constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j,
bool relax_main_opaque);
constraint_cell * raw() const { return m_ptr; }
};
@ -75,9 +76,13 @@ 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); }
constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j);
/**
\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);
constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification const & j);
constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j);
constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j, bool relax_main_opaque);
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; }
@ -89,6 +94,8 @@ 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. */

9
src/kernel/converter.cpp
View file

@ -74,6 +74,7 @@ bool converter::is_def_eq(expr const & t, expr const & s, type_checker & c) {
struct dummy_converter : public converter {
virtual expr whnf(expr const & e, type_checker &) { return e; }
virtual bool is_def_eq(expr const &, expr const &, type_checker &, delayed_justification &) { return true; }
virtual optional<module_idx> get_module_idx() const { return optional<module_idx>(); }
};
std::unique_ptr<converter> mk_dummy_converter() {
@ -98,6 +99,10 @@ struct default_converter : public converter {
m_env(env), m_module_idx(mod_idx), m_memoize(memoize), m_extra_opaque(extra_opaque) {
}
constraint 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));
}
optional<expr> expand_macro(expr const & m, type_checker & c) {
lean_assert(is_macro(m));
return macro_def(m).expand(m, get_extension(c));
@ -552,6 +557,10 @@ struct default_converter : public converter {
bool is_prop(expr const & e, type_checker & c) {
return whnf(infer_type(c, e), c) == Prop;
}
virtual optional<module_idx> get_module_idx() const {
return m_module_idx;
}
};
std::unique_ptr<converter> mk_default_converter(environment const & env, optional<module_idx> mod_idx,

1
src/kernel/converter.h
View file

@ -20,6 +20,7 @@ public:
virtual ~converter() {}
virtual expr whnf(expr const & e, type_checker & c) = 0;
virtual bool is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & j) = 0;
virtual optional<module_idx> get_module_idx() const = 0;
bool is_def_eq(expr const & t, expr const & s, type_checker & c);
};

4
src/kernel/type_checker.cpp
View file

@ -105,6 +105,10 @@ void type_checker::add_cnstr(constraint const & c) {
m_cs.push_back(c);
}
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()));
}
optional<constraint> type_checker::next_cnstr() {
if (m_cs_qhead < m_cs.size()) {
constraint c = m_cs[m_cs_qhead];

1
src/kernel/type_checker.h
View file

@ -105,6 +105,7 @@ class type_checker {
expr infer_type(expr const & e);
void copy_constraints(unsigned qhead, buffer<constraint> & new_cnstrs);
extension_context & get_extension() { return m_tc_ctx; }
constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j);
public:
/**
\brief Create a type checker for the given environment. The auxiliary names created by this

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,
buffer<constraint> & tc_cnstr_buffer) const {
buffer<constraint> & tc_cnstr_buffer, bool relax) const {
lean_assert(is_constant(elim));
environment const & env = tc.env();
levels elim_lvls = const_levels(elim);
@ -78,12 +78,12 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
intro_type = tc.whnf(binding_body(intro_type), tc_cnstr_buffer);
lean_assert(!tc.next_cnstr());
}
constraint c1 = mk_eq_cnstr(meta, hint, j);
constraint c1 = mk_eq_cnstr(meta, hint, j, relax);
args[major_idx] = hint;
lean_assert(!tc.next_cnstr());
expr reduce_elim = tc.whnf(mk_app(elim, args), tc_cnstr_buffer);
lean_assert(!tc.next_cnstr());
constraint c2 = mk_eq_cnstr(reduce_elim, t, j);
constraint c2 = mk_eq_cnstr(reduce_elim, t, j, relax);
list<constraint> tc_cnstrs = to_list(tc_cnstr_buffer.begin(), tc_cnstr_buffer.end());
alts.push_back(cons(c1, cons(c2, tc_cnstrs)));
}
@ -92,7 +92,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) const {
expr const & lhs, expr const & rhs, justification const & j, bool relax) const {
lean_assert(inductive::is_elim_meta_app(tc, lhs));
buffer<constraint> tc_cnstr_buffer;
lean_assert(!tc.next_cnstr());
@ -106,7 +106,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, tc_cnstr_buffer);
return add_elim_meta_cnstrs(tc, ngen, d, elim, args, rhs, j, tc_cnstr_buffer, relax);
}
lean_unreachable(); // LCOV_EXCL_LINE
}
@ -122,10 +122,11 @@ 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);
return process_elim_meta_core(tc, ngen, lhs, rhs, j, relax);
else if (inductive::is_elim_meta_app(tc, rhs))
return process_elim_meta_core(tc, ngen, rhs, lhs, j);
return process_elim_meta_core(tc, ngen, rhs, lhs, j, relax);
else
return lazy_list<constraints>();
}

16
src/library/kernel_bindings.cpp
View file

@ -1478,7 +1478,9 @@ 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()));
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)));
}
static int mk_level_eq_cnstr(lua_State * L) {
int nargs = lua_gettop(L);
@ -1508,7 +1510,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())));
r.push_back(constraints(mk_eq_cnstr(mvar, to_expr(L, -1), justification(), false)));
else
r.push_back(to_list_constraint_ext(L, -1));
lua_pop(L, 1);
@ -1526,13 +1528,15 @@ 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, justification()));
return push_constraint(L, mk_choice_cnstr(m, fn, 0, justification(), false));
else if (nargs == 3 && is_justification(L, 3))
return push_constraint(L, mk_choice_cnstr(m, fn, 0, to_justification(L, 3)));
return push_constraint(L, mk_choice_cnstr(m, fn, 0, to_justification(L, 3), false));
else if (nargs == 3)
return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), justification()));
return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), justification(), false));
else if (nargs == 4)
return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), to_justification(L, 4), false));
else
return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), to_justification(L, 4)));
return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), to_justification(L, 4), lua_toboolean(L, 5)));
}
static int constraint_expr(lua_State * L) {

10
src/library/opaque_hints.cpp
View file

@ -45,15 +45,17 @@ environment expose_definition(environment const & env, name const & n) {
ext.m_extra_opaque.erase(n);
return update(env, ext);
}
environment set_main_module_opaque_defs(environment const & env, bool f) {
environment set_hide_main_opaque(environment const & env, bool f) {
auto ext = get_extension(env);
ext.m_hide_module = f;
return update(env, ext);
}
std::unique_ptr<type_checker> mk_type_checker_with_hints(environment const & env, name_generator const & ngen) {
bool get_hide_main_opaque(environment const & env) {
return get_extension(env).m_hide_module;
}
std::unique_ptr<type_checker> mk_type_checker_with_hints(environment const & env, name_generator const & ngen, bool relax_main_opaque) {
auto const & ext = get_extension(env);
return std::unique_ptr<type_checker>(new type_checker(env, ngen, mk_default_converter(env, !ext.m_hide_module,
return std::unique_ptr<type_checker>(new type_checker(env, ngen, mk_default_converter(env, !ext.m_hide_module && relax_main_opaque,
true, ext.m_extra_opaque)));
}
}

11
src/library/opaque_hints.h
View file

@ -22,12 +22,11 @@ namespace lean {
environment hide_definition(environment const & env, name const & n);
/** \brief Undo the modification made with \c hide_definition. */
environment expose_definition(environment const & env, name const & n);
/**
\brief By default, the elaborator/unifier will treat the opaque
definitions of the current/main module as transparent. We can
change this behavior using this function.
/** \brief By default, the elaborator/unifier will treat the opaque definitions of the current/main
module as transparent (when allowed). We can change this behavior using this function.
*/
environment set_main_module_opaque_defs(environment const & env, bool f);
environment set_hide_main_opaque(environment const & env, bool f);
bool get_hide_main_opaque(environment const & env);
/** \brief Create a type checker that takes the hints into account. */
std::unique_ptr<type_checker> mk_type_checker_with_hints(environment const & env, name_generator const & ngen);
std::unique_ptr<type_checker> mk_type_checker_with_hints(environment const & env, name_generator const & ngen, bool relax_main_opaque);
}

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

@ -92,7 +92,7 @@ static void remove_redundant_metas(buffer<expr> & metas) {
}
proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & _e,
bool add_meta, bool add_subgoals) {
bool add_meta, bool add_subgoals, bool relax_main_opaque) {
goals const & gs = s.get_goals();
if (empty(gs))
return proof_state_seq();
@ -119,7 +119,7 @@ proof_state_seq apply_tactic_core(environment const & env, io_state const & ios,
}
}
list<expr> meta_lst = to_list(metas.begin(), metas.end());
lazy_list<substitution> substs = unify(env, t, e_t, ngen.mk_child(), s.get_subst(), ios.get_options());
lazy_list<substitution> substs = unify(env, t, e_t, ngen.mk_child(), relax_main_opaque, s.get_subst(), ios.get_options());
return map2<proof_state>(substs, [=](substitution const & subst) -> proof_state {
name_generator new_ngen(ngen);
type_checker tc(env, new_ngen.mk_child());
@ -182,21 +182,21 @@ expr refresh_univ_metavars(expr const & e, name_generator & ngen) {
}
}
tactic apply_tactic(expr const & e, bool refresh_univ_mvars) {
tactic apply_tactic(expr const & e, bool relax_main_opaque, bool refresh_univ_mvars) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
if (refresh_univ_mvars) {
name_generator ngen = s.get_ngen();
substitution new_subst = s.get_subst();
expr new_e = refresh_univ_metavars(new_subst.instantiate_all(e), ngen);
proof_state new_s(s.get_goals(), new_subst, ngen);
return apply_tactic_core(env, ios, new_s, new_e, true, true);
return apply_tactic_core(env, ios, new_s, new_e, true, true, relax_main_opaque);
} else {
return apply_tactic_core(env, ios, s, e, true, true);
return apply_tactic_core(env, ios, s, e, true, true, relax_main_opaque);
}
});
}
tactic eassumption_tactic() {
tactic eassumption_tactic(bool relax_main_opaque) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
goals const & gs = s.get_goals();
if (empty(gs))
@ -206,7 +206,7 @@ tactic eassumption_tactic() {
buffer<expr> hs;
get_app_args(g.get_meta(), hs);
for (expr const & h : hs) {
r = append(r, apply_tactic_core(env, ios, s, h, false, false));
r = append(r, apply_tactic_core(env, ios, s, h, false, false, relax_main_opaque));
}
return r;
});

4
src/library/tactic/apply_tactic.h
View file

@ -8,7 +8,7 @@ Author: Leonardo de Moura
#include "util/lua.h"
#include "library/tactic/tactic.h"
namespace lean {
tactic apply_tactic(expr const & e, bool refresh_univ_mvars = true);
tactic eassumption_tactic();
tactic apply_tactic(expr const & e, bool relax_main_opaque = true, bool refresh_univ_mvars = true);
tactic eassumption_tactic(bool relax_main_opaque = true);
void open_apply_tactic(lua_State * L);
}

226
src/library/unifier.cpp
View file

@ -209,7 +209,7 @@ unify_status unify_simple(substitution & s, constraint const & c) {
return unify_status::Unsupported;
}
static constraint g_dont_care_cnstr = mk_eq_cnstr(expr(), expr(), justification());
static constraint g_dont_care_cnstr = mk_eq_cnstr(expr(), expr(), justification(), false);
static unsigned g_group_size = 1u << 29;
static unsigned g_cnstr_group_first_index[6] = { 0, g_group_size, 2*g_group_size, 3*g_group_size, 4*g_group_size, 5*g_group_size};
static unsigned get_group_first_index(cnstr_group g) {
@ -241,7 +241,7 @@ struct unifier_fn {
name_generator m_ngen;
substitution m_subst;
unifier_plugin m_plugin;
type_checker_ptr m_tc;
type_checker_ptr m_tc[2];
bool m_use_exception; //!< True if we should throw an exception when there are no more solutions.
unsigned m_max_steps;
unsigned m_num_steps;
@ -292,14 +292,17 @@ struct unifier_fn {
m_assumption_idx(u.m_next_assumption_idx), m_jst(j), m_subst(u.m_subst), m_cnstrs(u.m_cnstrs),
m_mvar_occs(u.m_mvar_occs) {
u.m_next_assumption_idx++;
u.m_tc->push();
u.m_tc[0]->push();
u.m_tc[1]->push();
}
/** \brief Restore unifier's state with saved values, and update m_assumption_idx and m_failed_justifications. */
void restore_state(unifier_fn & u) {
lean_assert(u.in_conflict());
u.m_tc->pop(); // restore type checker state
u.m_tc->push();
u.m_tc[0]->pop(); // restore type checker state
u.m_tc[1]->pop(); // restore type checker state
u.m_tc[0]->push();
u.m_tc[1]->push();
u.m_subst = m_subst;
u.m_cnstrs = m_cnstrs;
u.m_mvar_occs = m_mvar_occs;
@ -333,8 +336,9 @@ struct unifier_fn {
name_generator const & ngen, substitution const & s,
bool use_exception, unsigned max_steps):
m_env(env), m_ngen(ngen), m_subst(s), m_plugin(get_unifier_plugin(env)),
m_tc(mk_type_checker_with_hints(env, m_ngen.mk_child())),
m_use_exception(use_exception), m_max_steps(max_steps), m_num_steps(0) {
m_tc[0] = mk_type_checker_with_hints(env, m_ngen.mk_child(), false);
m_tc[1] = mk_type_checker_with_hints(env, m_ngen.mk_child(), true);
m_next_assumption_idx = 0;
m_next_cidx = 0;
m_first = true;
@ -403,9 +407,12 @@ struct unifier_fn {
return cidx;
}
/** \brief Check if \c t1 and \c t2 are definitionally equal, if they are not, set a conflict with justification \c j */
bool is_def_eq(expr const & t1, expr const & t2, justification const & j) {
if (m_tc->is_def_eq(t1, t2, j)) {
/** \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) {
if (m_tc[relax]->is_def_eq(t1, t2, j)) {
return true;
} else {
set_conflict(j);
@ -417,21 +424,23 @@ struct unifier_fn {
\brief Assign \c v to metavariable \c m with justification \c j.
The type of v and m are inferred, and is_def_eq is invoked.
Any 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 & m, expr const & v, justification const & j) {
bool assign(expr const & m, expr const & v, justification const & j, bool relax) {
lean_assert(is_metavar(m));
m_subst.assign(m, v, j);
expr m_type = mlocal_type(m);
expr v_type;
try {
v_type = m_tc->infer(v);
v_type = m_tc[relax]->infer(v);
} catch (kernel_exception & e) {
set_conflict(j);
return false;
}
if (in_conflict())
return false;
if (!is_def_eq(m_type, v_type, j))
if (!is_def_eq(m_type, v_type, j, relax))
return false;
auto it = m_mvar_occs.find(mlocal_name(m));
if (it) {
@ -463,7 +472,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) {
status process_metavar_eq(expr const & lhs, expr const & rhs, justification const & j, bool relax) {
if (!is_meta(lhs))
return Continue;
buffer<expr> locals;
@ -478,7 +487,7 @@ struct unifier_fn {
return Continue;
case l_true:
lean_assert(!m_subst.is_assigned(*m));
if (assign(*m, lambda_abstract_locals(rhs, locals), j)) {
if (assign(*m, lambda_abstract_locals(rhs, locals), j, relax)) {
return Solved;
} else {
return Failed;
@ -509,7 +518,8 @@ 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)),
mk_composite1(mk_composite1(c.get_justification(), lhs_jst.second), rhs_jst.second),
relax_main_opaque(c)),
true);
}
} else if (is_level_eq_cnstr(c)) {
@ -530,19 +540,20 @@ 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) ? Solved : Failed;
return is_def_eq(lhs, rhs, jst, relax) ? Solved : Failed;
}
// Handle higher-order pattern matching.
status st = process_metavar_eq(lhs, rhs, jst);
status st = process_metavar_eq(lhs, rhs, jst, relax);
if (st != Continue) return st;
st = process_metavar_eq(rhs, lhs, jst);
st = process_metavar_eq(rhs, lhs, jst, relax);
if (st != Continue) return st;
return Continue;
@ -589,11 +600,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) ? Solved : Failed;
return is_def_eq(lhs, rhs, j, relax_main_opaque(c)) ? 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) ? Solved : Failed;
return is_def_eq(lhs, rhs, j, relax_main_opaque(c)) ? Solved : Failed;
return Continue;
}
@ -608,6 +619,7 @@ 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
@ -617,7 +629,7 @@ struct unifier_fn {
unsigned cidx = add_cnstr(c, cnstr_group::FlexFlex);
add_meta_occ(lhs, cidx);
add_meta_occ(rhs, cidx);
} else if (m_plugin->delay_constraint(*m_tc, c)) {
} else if (m_plugin->delay_constraint(*m_tc[relax], c)) {
unsigned cidx = add_cnstr(c, cnstr_group::PluginDelayed);
add_meta_occs(lhs, cidx);
add_meta_occs(rhs, cidx);
@ -749,7 +761,8 @@ struct unifier_fn {
}
void pop_case_split() {
m_tc->pop();
m_tc[0]->pop();
m_tc[1]->pop();
m_case_splits.pop_back();
}
@ -835,26 +848,28 @@ struct unifier_fn {
return lazy_list<constraints>();
justification const & j = c.get_justification();
buffer<constraint> cs;
lean_assert(!m_tc->next_cnstr());
if (!m_tc->is_def_eq(f_lhs, f_rhs, j, cs))
bool relax = relax_main_opaque(c);
lean_assert(!m_tc[relax]->next_cnstr());
if (!m_tc[relax]->is_def_eq(f_lhs, f_rhs, j, cs))
return lazy_list<constraints>();
buffer<expr> args_lhs, args_rhs;
get_app_args(lhs, args_lhs);
get_app_args(rhs, args_rhs);
if (args_lhs.size() != args_rhs.size())
return lazy_list<constraints>();
lean_assert(!m_tc->next_cnstr());
lean_assert(!m_tc[relax]->next_cnstr());
for (unsigned i = 0; i < args_lhs.size(); i++)
if (!m_tc->is_def_eq(args_lhs[i], args_rhs[i], j, cs))
if (!m_tc[relax]->is_def_eq(args_lhs[i], args_rhs[i], j, cs))
return lazy_list<constraints>();
return lazy_list<constraints>(to_list(cs.begin(), cs.end()));
}
bool process_plugin_constraint(constraint const & c) {
bool relax = relax_main_opaque(c);
lean_assert(!is_choice_cnstr(c));
lean_assert(!m_tc->next_cnstr());
lazy_list<constraints> alts = m_plugin->solve(*m_tc, c, m_ngen.mk_child());
lean_assert(!m_tc->next_cnstr());
lean_assert(!m_tc[relax]->next_cnstr());
lazy_list<constraints> alts = m_plugin->solve(*m_tc[relax], c, m_ngen.mk_child());
lean_assert(!m_tc[relax]->next_cnstr());
alts = append(alts, process_const_const_cnstr(c));
return process_lazy_constraints(alts, c.get_justification());
}
@ -864,8 +879,9 @@ struct unifier_fn {
expr const & m = cnstr_expr(c);
choice_fn const & fn = cnstr_choice_fn(c);
expr m_type;
bool relax = relax_main_opaque(c);
try {
m_type = m_tc->infer(m);
m_type = m_tc[relax]->infer(m);
} catch (kernel_exception &) {
set_conflict(c.get_justification());
return false;
@ -920,8 +936,9 @@ struct unifier_fn {
expr rhs_fn_val = instantiate_univ_params(d.get_value(), d.get_univ_params(), 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());
bool relax = relax_main_opaque(c);
buffer<constraint> cs2;
if (m_tc->is_def_eq(t, s, j, cs2)) {
if (m_tc[relax]->is_def_eq(t, s, j, cs2)) {
// create a case split
a = mk_assumption_justification(m_next_assumption_idx);
add_case_split(std::unique_ptr<case_split>(new simple_case_split(*this, j, to_list(cs2.begin(), cs2.end()))));
@ -941,7 +958,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))
if (!is_def_eq(lhs_args[i], rhs_args[i], new_j, relax))
return false;
}
return true;
@ -979,19 +996,19 @@ struct unifier_fn {
}
/** \see ensure_sufficient_args */
optional<expr> ensure_sufficient_args_core(expr mtype, unsigned i, buffer<expr> const & margs) {
optional<expr> ensure_sufficient_args_core(expr mtype, unsigned i, buffer<expr> const & margs, bool relax) {
if (i == margs.size())
return some_expr(mtype);
mtype = m_tc->ensure_pi(mtype);
mtype = m_tc[relax]->ensure_pi(mtype);
try {
if (!m_tc->is_def_eq(binding_domain(mtype), m_tc->infer(margs[i])))
if (!m_tc[relax]->is_def_eq(binding_domain(mtype), m_tc[relax]->infer(margs[i])))
return none_expr();
} catch (kernel_exception &) {
return none_expr();
}
expr local = mk_local_for(mtype);
expr body = instantiate(binding_body(mtype), local);
auto new_body = ensure_sufficient_args_core(body, i+1, margs);
auto new_body = ensure_sufficient_args_core(body, i+1, margs, relax);
if (!new_body)
return none_expr();
return some_expr(Pi(local, *new_body));
@ -1001,7 +1018,8 @@ struct unifier_fn {
\brief Make sure mtype is a Pi of size at least margs.size().
If it is not, we use ensure_pi and (potentially) add new constaints to enforce it.
*/
optional<expr> ensure_sufficient_args(expr const & mtype, buffer<expr> const & margs, buffer<constraint> & cs, justification const & j) {
optional<expr> ensure_sufficient_args(expr const & mtype, buffer<expr> const & margs, buffer<constraint> & cs, justification const & j,
bool relax) {
expr t = mtype;
unsigned num = 0;
while (is_pi(t)) {
@ -1010,13 +1028,13 @@ struct unifier_fn {
}
if (num == margs.size())
return some_expr(mtype);;
lean_assert(!m_tc->next_cnstr()); // make sure there are no pending constraints
lean_assert(!m_tc[relax]->next_cnstr()); // make sure there are no pending constraints
// We must create a scope to make sure no constraints "leak" into the current state.
type_checker::scope scope(*m_tc);
auto new_mtype = ensure_sufficient_args_core(mtype, 0, margs);
type_checker::scope scope(*m_tc[relax]);
auto new_mtype = ensure_sufficient_args_core(mtype, 0, margs, relax);
if (!new_mtype)
return none_expr();
while (auto c = m_tc->next_cnstr())
while (auto c = m_tc[relax]->next_cnstr())
cs.push_back(update_justification(*c, mk_composite1(c->get_justification(), j)));
return new_mtype;
}
@ -1073,13 +1091,13 @@ struct unifier_fn {
- variable (if g is a local constant equal to a_i)
*/
void mk_flex_rigid_app_cnstrs(expr const & m, buffer<expr> const & margs, expr const & f, expr const & rhs, justification const & j,
buffer<constraints> & alts) {
buffer<constraints> & alts, bool relax) {
lean_assert(is_metavar(m));
lean_assert(is_app(rhs));
lean_assert(is_constant(f) || is_var(f));
buffer<constraint> cs;
expr mtype = mlocal_type(m);
auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j);
auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j, relax);
if (!new_mtype) return;
mtype = *new_mtype;
buffer<expr> rargs;
@ -1090,13 +1108,13 @@ struct unifier_fn {
sargs.push_back(*v);
} else {
expr maux = mk_aux_metavar_for(m_ngen, mtype);
cs.push_back(mk_eq_cnstr(mk_app(maux, margs), rarg, j));
cs.push_back(mk_eq_cnstr(mk_app(maux, margs), rarg, j, relax));
sargs.push_back(mk_app_vars(maux, margs.size()));
}
}
expr v = mk_app(f, sargs);
v = mk_lambda_for(mtype, v);
cs.push_back(mk_eq_cnstr(m, v, j));
cs.push_back(mk_eq_cnstr(m, v, j, relax));
alts.push_back(to_list(cs.begin(), cs.end()));
}
@ -1112,25 +1130,25 @@ struct unifier_fn {
where l is a fresh local constant.
*/
void mk_bindings_imitation(expr const & m, buffer<expr> const & margs, expr const & rhs, justification const & j,
buffer<constraints> & alts) {
buffer<constraints> & alts, bool relax) {
lean_assert(is_metavar(m));
lean_assert(is_binding(rhs));
buffer<constraint> cs;
expr mtype = mlocal_type(m);
auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j);
auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j, relax);
if (!new_mtype) return;
mtype = *new_mtype;
expr maux1 = mk_aux_metavar_for(m_ngen, mtype);
cs.push_back(mk_eq_cnstr(mk_app(maux1, margs), binding_domain(rhs), j));
cs.push_back(mk_eq_cnstr(mk_app(maux1, margs), binding_domain(rhs), j, relax));
expr dontcare;
expr tmp_pi = mk_pi(binding_name(rhs), mk_app_vars(maux1, margs.size()), dontcare); // trick for "extending" the context
expr mtype2 = replace_range(mtype, tmp_pi); // trick for "extending" the context
expr maux2 = mk_aux_metavar_for(m_ngen, mtype2);
expr new_local = mk_local_for(rhs);
cs.push_back(mk_eq_cnstr(mk_app(mk_app(maux2, margs), new_local), instantiate(binding_body(rhs), new_local), j));
cs.push_back(mk_eq_cnstr(mk_app(mk_app(maux2, margs), new_local), instantiate(binding_body(rhs), new_local), j, relax));
expr v = update_binding(rhs, mk_app_vars(maux1, margs.size()), mk_app_vars(maux2, margs.size() + 1));
v = mk_lambda_for(mtype, v);
cs.push_back(mk_eq_cnstr(m, v, j));
cs.push_back(mk_eq_cnstr(m, v, j, relax));
alts.push_back(to_list(cs.begin(), cs.end()));
}
@ -1141,12 +1159,12 @@ struct unifier_fn {
Then solve (?m a_1 ... a_k) =?= rhs, by returning the constraint
?m =?= fun (x1 ... x_k), rhs
*/
void mk_simple_imitation(expr const & m, expr const & rhs, justification const & j, buffer<constraints> & alts) {
void mk_simple_imitation(expr const & m, expr const & rhs, justification const & j, buffer<constraints> & alts, bool relax) {
lean_assert(is_metavar(m));
lean_assert(is_sort(rhs) || is_constant(rhs));
expr const & mtype = mlocal_type(m);
buffer<constraint> cs;
cs.push_back(mk_eq_cnstr(m, mk_lambda_for(mtype, rhs), j));
cs.push_back(mk_eq_cnstr(m, mk_lambda_for(mtype, rhs), j, relax));
alts.push_back(to_list(cs.begin(), cs.end()));
}
@ -1162,24 +1180,24 @@ struct unifier_fn {
?m =?= fun (x_1 ... x_k), M((?m_1 x_1 ... x_k) ... (?m_n x_1 ... x_k))
*/
void mk_macro_imitation(expr const & m, buffer<expr> const & margs, expr const & rhs, justification const & j,
buffer<constraints> & alts) {
buffer<constraints> & alts, bool relax) {
lean_assert(is_metavar(m));
lean_assert(is_macro(rhs));
buffer<constraint> cs;
expr mtype = mlocal_type(m);
auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j);
auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j, relax);
if (!new_mtype) return;
mtype = *new_mtype;
// create an auxiliary metavariable for each macro argument
buffer<expr> sargs;
for (unsigned i = 0; i < macro_num_args(rhs); i++) {
expr maux = mk_aux_metavar_for(m_ngen, mtype);
cs.push_back(mk_eq_cnstr(mk_app(maux, margs), macro_arg(rhs, i), j));
cs.push_back(mk_eq_cnstr(mk_app(maux, margs), macro_arg(rhs, i), j, relax));
sargs.push_back(mk_app_vars(maux, margs.size()));
}
expr v = mk_macro(macro_def(rhs), sargs.size(), sargs.data());
v = mk_lambda_for(mtype, v);
cs.push_back(mk_eq_cnstr(m, v, j));
cs.push_back(mk_eq_cnstr(m, v, j, relax));
alts.push_back(to_list(cs.begin(), cs.end()));
}
@ -1198,17 +1216,17 @@ struct unifier_fn {
to alts as a possible solution.
*/
void mk_simple_nonlocal_projection(expr const & m, buffer<expr> const & margs, unsigned i, expr const & rhs, justification const & j,
buffer<constraints> & alts) {
buffer<constraints> & alts, bool relax) {
expr const & mtype = mlocal_type(m);
unsigned vidx = margs.size() - i - 1;
expr const & marg = margs[i];
buffer<constraint> cs;
if (auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j)) {
if (auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j, relax)) {
// Remark: we should not use mk_eq_cnstr(marg, rhs, j) since is_def_eq may be able to reduce them.
// The unifier assumes the eq constraints are reduced.
if (m_tc->is_def_eq(marg, rhs, j, cs)) {
if (m_tc[relax]->is_def_eq(marg, rhs, j, cs)) {
expr v = mk_lambda_for(*new_mtype, mk_var(vidx));
cs.push_back(mk_eq_cnstr(m, v, j));
cs.push_back(mk_eq_cnstr(m, v, j, relax));
alts.push_back(to_list(cs.begin(), cs.end()));
}
}
@ -1232,7 +1250,7 @@ struct unifier_fn {
*/
void mk_simple_projections(expr const & m, buffer<expr> const & margs, expr const & rhs, justification const & j,
buffer<constraints> & alts) {
buffer<constraints> & alts, bool relax) {
lean_assert(is_metavar(m));
lean_assert(!is_meta(rhs));
expr const & mtype = mlocal_type(m);
@ -1243,13 +1261,13 @@ struct unifier_fn {
expr const & marg = margs[i];
if ((!is_local(marg) && !is_local(rhs)) || (is_meta(marg) && is_local(rhs))) {
// if rhs is not local, then we only add projections for the nonlocal arguments of lhs
mk_simple_nonlocal_projection(m, margs, i, rhs, j, alts);
mk_simple_nonlocal_projection(m, margs, i, rhs, j, alts, relax);
} else if (is_local(marg) && is_local(rhs) && mlocal_name(marg) == mlocal_name(rhs)) {
// if the argument is local, and rhs is equal to it, then we also add a projection
buffer<constraint> cs;
if (auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j)) {
if (auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j, relax)) {
expr v = mk_lambda_for(*new_mtype, mk_var(vidx));
cs.push_back(mk_eq_cnstr(m, v, j));
cs.push_back(mk_eq_cnstr(m, v, j, relax));
alts.push_back(to_list(cs.begin(), cs.end()));
}
}
@ -1257,7 +1275,7 @@ struct unifier_fn {
}
/** \brief Process a flex rigid constraint */
bool process_flex_rigid(expr const & lhs, expr const & rhs, justification const & j) {
bool process_flex_rigid(expr const & lhs, expr const & rhs, justification const & j, bool relax) {
lean_assert(is_meta(lhs));
lean_assert(!is_meta(rhs));
buffer<expr> margs;
@ -1266,7 +1284,7 @@ struct unifier_fn {
// Make sure that if marg is reducible to a local constant, then it is replaced with it.
// We need that because of the optimization based on is_easy_flex_rigid_arg
if (!is_local(marg)) {
expr new_marg = m_tc->whnf(marg);
expr new_marg = m_tc[relax]->whnf(marg);
if (is_local(new_marg))
marg = new_marg;
}
@ -1276,19 +1294,19 @@ struct unifier_fn {
case expr_kind::Var: case expr_kind::Meta:
lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::Local:
mk_simple_projections(m, margs, rhs, j, alts);
mk_simple_projections(m, margs, rhs, j, alts, relax);
break;
case expr_kind::Sort: case expr_kind::Constant:
mk_simple_projections(m, margs, rhs, j, alts);
mk_simple_imitation(m, rhs, j, alts);
mk_simple_projections(m, margs, rhs, j, alts, relax);
mk_simple_imitation(m, rhs, j, alts, relax);
break;
case expr_kind::Pi: case expr_kind::Lambda:
mk_simple_projections(m, margs, rhs, j, alts);
mk_bindings_imitation(m, margs, rhs, j, alts);
mk_simple_projections(m, margs, rhs, j, alts, relax);
mk_bindings_imitation(m, margs, rhs, j, alts, relax);
break;
case expr_kind::Macro:
mk_simple_projections(m, margs, rhs, j, alts);
mk_macro_imitation(m, margs, rhs, j, alts);
mk_simple_projections(m, margs, rhs, j, alts, relax);
mk_macro_imitation(m, margs, rhs, j, alts, relax);
break;
case expr_kind::App: {
expr const & f = get_app_fn(rhs);
@ -1299,17 +1317,17 @@ struct unifier_fn {
--i;
expr const & marg = margs[i];
if (is_local(marg) && mlocal_name(marg) == mlocal_name(f))
mk_flex_rigid_app_cnstrs(m, margs, mk_var(vidx), rhs, j, alts);
mk_flex_rigid_app_cnstrs(m, margs, mk_var(vidx), rhs, j, alts, relax);
else
mk_simple_nonlocal_projection(m, margs, i, rhs, j, alts);
mk_simple_nonlocal_projection(m, margs, i, rhs, j, alts, relax);
}
} else if (is_constant(f)) {
mk_simple_projections(m, margs, rhs, j, alts);
mk_flex_rigid_app_cnstrs(m, margs, f, rhs, j, alts);
mk_simple_projections(m, margs, rhs, j, alts, relax);
mk_flex_rigid_app_cnstrs(m, margs, f, rhs, j, alts, relax);
} else {
expr new_rhs = m_tc->whnf(rhs);
expr new_rhs = m_tc[relax]->whnf(rhs);
lean_assert(new_rhs != rhs);
return is_def_eq(lhs, new_rhs, j);
return is_def_eq(lhs, new_rhs, j, relax);
}
break;
}}
@ -1330,12 +1348,13 @@ struct unifier_fn {
/** \brief Process a flex rigid constraint */
bool process_flex_rigid(constraint const & c) {
lean_assert(is_flex_rigid(c));
expr lhs = cnstr_lhs_expr(c);
expr rhs = cnstr_rhs_expr(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());
return process_flex_rigid(lhs, rhs, c.get_justification(), relax);
else
return process_flex_rigid(rhs, lhs, c.get_justification());
return process_flex_rigid(rhs, lhs, c.get_justification(), relax);
}
bool process_flex_flex(constraint const & c) {
@ -1358,18 +1377,20 @@ struct unifier_fn {
if (mlocal_name(lhs_args[i]) != mlocal_name(rhs_args[i]))
break;
if (i == lhs_args.size())
return assign(ml, mr, c.get_justification());
return assign(ml, mr, c.get_justification(), relax_main_opaque(c));
return true;
}
void consume_tc_cnstrs() {
while (true) {
if (in_conflict())
return;
if (auto c = m_tc->next_cnstr()) {
process_constraint(*c);
} else {
break;
for (unsigned i = 0; i < 2; i++) {
while (true) {
if (in_conflict())
return;
if (auto c = m_tc[i]->next_cnstr()) {
process_constraint(*c);
} else {
break;
}
}
}
}
@ -1417,7 +1438,8 @@ struct unifier_fn {
} else {
auto r = instantiate_metavars(c);
c = r.first;
lean_assert(!m_tc->next_cnstr());
lean_assert(!m_tc[0]->next_cnstr());
lean_assert(!m_tc[1]->next_cnstr());
bool modified = r.second;
if (is_level_eq_cnstr(c)) {
if (modified)
@ -1432,7 +1454,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());
return is_def_eq(cnstr_lhs_expr(c), cnstr_rhs_expr(c), c.get_justification(), relax_main_opaque(c));
} else if (is_flex_rigid(c)) {
return process_flex_rigid(c);
} else if (is_flex_flex(c)) {
@ -1510,21 +1532,21 @@ lazy_list<substitution> unify(environment const & env, unsigned num_cs, constra
return unify(env, num_cs, cs, ngen, use_exception, get_unifier_max_steps(o));
}
lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, substitution const & s,
unsigned max_steps) {
lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
bool relax, substitution const & s, unsigned max_steps) {
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, false, max_steps);
if (!u->m_tc->is_def_eq(_lhs, _rhs))
if (!u->m_tc[relax]->is_def_eq(_lhs, _rhs))
return lazy_list<substitution>();
else
return unify(u);
}
lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
substitution const & s, options const & o) {
return unify(env, lhs, rhs, ngen, s, get_unifier_max_steps(o));
bool relax, substitution const & s, options const & o) {
return unify(env, lhs, rhs, ngen, relax, s, get_unifier_max_steps(o));
}
static int unify_simple(lua_State * L) {
@ -1646,10 +1668,12 @@ static int unify(lua_State * L) {
lazy_list<substitution> r;
environment const & env = to_environment(L, 1);
if (is_expr(L, 2)) {
if (nargs == 6)
r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5), to_options(L, 6));
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), 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), options());
else
r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5), options());
r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), lua_toboolean(L, 5));
} else {
buffer<constraint> cs;
to_constraint_buffer(L, 2, cs);

6
src/library/unifier.h
View file

@ -40,10 +40,10 @@ lazy_list<substitution> unify(environment const & env, unsigned num_cs, constrai
bool use_exception = true, unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS);
lazy_list<substitution> unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen,
bool use_exception, options const & o);
lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, bool relax_main_opaque,
substitution const & s = substitution(), unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS);
lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, substitution const & s,
options const & o);
lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
bool relax_main_opaque, substitution const & s, options const & o);
/**
The unifier divides the constraints in 6 groups: Simple, Basic, FlexRigid, PluginDelayed, PreFlexFlex, FlexFlex, MaxDelayed

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

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

1
tests/lean/run/class4.lean
View file

@ -69,6 +69,7 @@ variable div : Π (x y : nat) {H : not_zero y}, nat
variables a b : nat
set_option pp.implicit true
opaque_hint (hiding [module])
check div a (succ b)
check (λ H : not_zero b, div a b)

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

@ -27,7 +27,7 @@ print(env:whnf(t(m)))
function test_unify(env, lhs, rhs, num_s)
print(tostring(lhs) .. " =?= " .. tostring(rhs) .. ", expected: " .. tostring(num_s))
local ss = unify(env, lhs, rhs, name_generator(), substitution(), options())
local ss = unify(env, lhs, rhs, name_generator(), true, substitution(), options())
local n = 0
for s in ss do
print("solution: ")

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

@ -30,7 +30,7 @@ print(env:whnf(t(m)))
function test_unify(env, lhs, rhs, num_s)
print(tostring(lhs) .. " =?= " .. tostring(rhs) .. ", expected: " .. tostring(num_s))
local ss = unify(env, lhs, rhs, name_generator(), substitution(), options())
local ss = unify(env, lhs, rhs, name_generator(), true, substitution(), options())
local n = 0
for s in ss do
print("solution: ")

11
tests/lean/run/univ2.lean Normal file
View file

@ -0,0 +1,11 @@
import standard
hypothesis I : Type
definition F (X : Type) : Type := (X → Prop) → Prop
hypothesis unfold : I → F I
hypothesis fold : F I → I
hypothesis iso1 : ∀x, fold (unfold x) = x
variable sorry {A : Type} : A
theorem iso2 : ∀x, fold (unfold x) = x
:= sorry

2
tests/lua/unify2.lua
View file

@ -1,6 +1,6 @@
function test_unify(env, lhs, rhs, num_s)
print(tostring(lhs) .. " =?= " .. tostring(rhs) .. ", expected: " .. tostring(num_s))
local ss = unify(env, lhs, rhs, name_generator(), substitution(), options())
local ss = unify(env, lhs, rhs, name_generator(), true, substitution(), options())
local n = 0
for s in ss do
print("solution: ")

2
tests/lua/unify4.lua
View file

@ -1,6 +1,6 @@
function test_unify(env, m, lhs, rhs, num_s)
print(tostring(lhs) .. " =?= " .. tostring(rhs) .. ", expected: " .. tostring(num_s))
local ss = unify(env, lhs, rhs, name_generator(), substitution(), options())
local ss = unify(env, lhs, rhs, name_generator(), true, substitution(), options())
local n = 0
for s in ss do
print("solution: " .. tostring(s:instantiate(m)))