feat(library/tactic/simplifier): add simplify_core_fn
TODO: remove dead code from old simplifier
This commit is contained in:
Leonardo de Moura
parent
ce28e1aedb
commit
fa01e062ef
2 changed files with 663 additions and 4 deletions
|
|
@ -1,7 +1,7 @@
|
|||
/*
|
||||
Copyright (c) 2015 Daniel Selsam. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Daniel Selsam
|
||||
Author: Daniel Selsam, Leonardo de Moura
|
||||
*/
|
||||
#include <functional>
|
||||
#include <iostream>
|
||||
|
|
@ -58,6 +58,583 @@ Author: Daniel Selsam
|
|||
#endif
|
||||
|
||||
namespace lean {
|
||||
#define lean_simp_trace(CTX, N, CODE) lean_trace(N, scope_trace_env _scope1(CTX.env(), CTX); CODE)
|
||||
|
||||
simp_result simplify_core_fn::join(simp_result const & r1, simp_result const & r2) {
|
||||
return ::lean::join(m_ctx, m_rel, r1, r2);
|
||||
}
|
||||
|
||||
void simplify_core_fn::inc_num_steps() {
|
||||
m_num_steps++;
|
||||
if (m_num_steps > m_max_steps)
|
||||
throw exception("simplify failed, maximum number of steps exceeded");
|
||||
}
|
||||
|
||||
bool simplify_core_fn::is_dependent_fn(expr const & f) {
|
||||
expr f_type = m_ctx.whnf(m_ctx.infer(f));
|
||||
lean_assert(is_pi(f_type));
|
||||
return !is_arrow(f_type);
|
||||
}
|
||||
|
||||
bool simplify_core_fn::instantiate_emetas(tmp_type_context & tmp_ctx, unsigned num_emeta,
|
||||
list<expr> const & emetas, list<bool> const & instances) {
|
||||
bool failed = false;
|
||||
unsigned i = num_emeta;
|
||||
for_each2(emetas, instances, [&](expr const & mvar, bool const & is_instance) {
|
||||
i--;
|
||||
if (failed) return;
|
||||
expr mvar_type = tmp_ctx.instantiate_mvars(tmp_ctx.infer(mvar));
|
||||
if (has_metavar(mvar_type)) {
|
||||
failed = true;
|
||||
return;
|
||||
}
|
||||
|
||||
if (tmp_ctx.is_eassigned(i)) return;
|
||||
|
||||
if (is_instance) {
|
||||
if (auto v = m_ctx.mk_class_instance(mvar_type)) {
|
||||
if (!tmp_ctx.is_def_eq(mvar, *v)) {
|
||||
lean_simp_trace(tmp_ctx, name({"simplify", "failure"}),
|
||||
tout() << "unable to assign instance for: " << mvar_type << "\n";);
|
||||
failed = true;
|
||||
return;
|
||||
}
|
||||
} else {
|
||||
lean_simp_trace(tmp_ctx, name({"simplify", "failure"}),
|
||||
tout() << "unable to synthesize instance for: " << mvar_type << "\n";);
|
||||
failed = true;
|
||||
return;
|
||||
}
|
||||
}
|
||||
|
||||
if (tmp_ctx.is_eassigned(i)) return;
|
||||
|
||||
if (m_ctx.is_prop(mvar_type)) {
|
||||
if (auto pf = prove(mvar_type)) {
|
||||
lean_verify(tmp_ctx.is_def_eq(mvar, *pf));
|
||||
return;
|
||||
}
|
||||
}
|
||||
|
||||
lean_simp_trace(tmp_ctx, name({"simplify", "failure"}),
|
||||
tout() << "failed to assign: " << mvar << " : " << mvar_type << "\n";);
|
||||
|
||||
failed = true;
|
||||
return;
|
||||
});
|
||||
return !failed;
|
||||
}
|
||||
|
||||
simp_result simplify_core_fn::lift_from_eq(simp_result const & r_eq) {
|
||||
if (!r_eq.has_proof()) return r_eq;
|
||||
expr new_pr = ::lean::lift_from_eq(m_ctx, m_rel, r_eq.get_proof());
|
||||
return simp_result(r_eq.get_new(), new_pr);
|
||||
}
|
||||
|
||||
simp_lemmas simplify_core_fn::add_to_slss(simp_lemmas const & _slss, buffer<expr> const & ls) {
|
||||
simp_lemmas slss = _slss;
|
||||
for (unsigned i = 0; i < ls.size(); i++) {
|
||||
expr const & l = ls[i];
|
||||
try {
|
||||
slss = add(m_ctx, slss, mlocal_name(l), m_ctx.infer(l), l, LEAN_DEFAULT_PRIORITY);
|
||||
lean_simp_trace(m_ctx, name({"simplify", "context"}),
|
||||
tout() << mlocal_name(l) << " : " << m_ctx.infer(l) << "\n";);
|
||||
} catch (exception & e) {}
|
||||
}
|
||||
return slss;
|
||||
}
|
||||
|
||||
/* Given the application 'e', remove unnecessary casts of the form (eq.nrec a rfl) and (eq.drec a rfl) */
|
||||
expr simplify_core_fn::remove_unnecessary_casts(expr const & e) {
|
||||
buffer<expr> args;
|
||||
expr f = get_app_args(e, args);
|
||||
ss_param_infos ss_infos = get_specialized_subsingleton_info(m_ctx, e);
|
||||
int i = -1;
|
||||
bool modified = false;
|
||||
for (ss_param_info const & ss_info : ss_infos) {
|
||||
i++;
|
||||
if (ss_info.is_subsingleton()) {
|
||||
while (is_constant(get_app_fn(args[i]))) {
|
||||
buffer<expr> cast_args;
|
||||
expr f_cast = get_app_args(args[i], cast_args);
|
||||
name n_f = const_name(f_cast);
|
||||
if (n_f == get_eq_rec_name() || n_f == get_eq_drec_name() || n_f == get_eq_nrec_name()) {
|
||||
lean_assert(cast_args.size() == 6);
|
||||
expr major_premise = cast_args[5];
|
||||
expr f_major_premise = get_app_fn(major_premise);
|
||||
if (is_constant(f_major_premise) && const_name(f_major_premise) == get_eq_refl_name()) {
|
||||
args[i] = cast_args[3];
|
||||
modified = true;
|
||||
} else {
|
||||
break;
|
||||
}
|
||||
} else {
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
return modified ? mk_app(f, args) : e;
|
||||
}
|
||||
|
||||
expr simplify_core_fn::defeq_canonize_args_step(expr const & e) {
|
||||
buffer<expr> args;
|
||||
bool modified = false;
|
||||
expr f = get_app_args(e, args);
|
||||
fun_info info = get_fun_info(m_ctx, f, args.size());
|
||||
unsigned i = 0;
|
||||
for (param_info const & pinfo : info.get_params_info()) {
|
||||
lean_assert(i < args.size());
|
||||
expr new_a;
|
||||
if ((m_canonize_instances && pinfo.is_inst_implicit()) || (m_canonize_proofs && pinfo.is_prop())) {
|
||||
new_a = ::lean::defeq_canonize(m_ctx, args[i], m_need_restart);
|
||||
lean_simp_trace(m_ctx, name({"simplify", "canonize"}),
|
||||
tout() << "\n" << args[i] << "\n==>\n" << new_a << "\n";);
|
||||
if (new_a != args[i]) {
|
||||
modified = true;
|
||||
args[i] = new_a;
|
||||
}
|
||||
}
|
||||
i++;
|
||||
}
|
||||
|
||||
return modified ? mk_app(f, args) : e;
|
||||
}
|
||||
|
||||
/* Try user defined congruence lemmas */
|
||||
simp_result simplify_core_fn::try_user_congrs(expr const & e) {
|
||||
simp_lemmas_for const * sls = m_slss.find(m_rel);
|
||||
if (!sls) return simp_result(e);
|
||||
|
||||
list<simp_lemma> const * cls = sls->find_congr(e);
|
||||
if (!cls) return simp_result(e);
|
||||
|
||||
for (simp_lemma const & cl : *cls) {
|
||||
simp_result r = try_user_congr(e, cl);
|
||||
if (r.get_new() != e)
|
||||
return r;
|
||||
}
|
||||
return simp_result(e);
|
||||
}
|
||||
|
||||
simp_result simplify_core_fn::try_user_congr(expr const & e, simp_lemma const & cl) {
|
||||
tmp_type_context tmp_ctx(m_ctx, cl.get_num_umeta(), cl.get_num_emeta());
|
||||
if (!tmp_ctx.is_def_eq(e, cl.get_lhs()))
|
||||
return simp_result(e);
|
||||
|
||||
lean_simp_trace(tmp_ctx, name({"debug", "simplify", "try_congruence"}),
|
||||
tout() << "(" << cl.get_id() << ") " << e << "\n";);
|
||||
|
||||
bool simplified = false;
|
||||
|
||||
buffer<expr> congr_hyps;
|
||||
to_buffer(cl.get_congr_hyps(), congr_hyps);
|
||||
|
||||
buffer<simp_result> congr_hyp_results;
|
||||
buffer<type_context::tmp_locals> factories;
|
||||
buffer<name> relations;
|
||||
for (expr const & m : congr_hyps) {
|
||||
factories.emplace_back(m_ctx);
|
||||
type_context::tmp_locals & local_factory = factories.back();
|
||||
expr m_type = tmp_ctx.instantiate_mvars(tmp_ctx.infer(m));
|
||||
|
||||
while (is_pi(m_type)) {
|
||||
expr d = instantiate_rev(binding_domain(m_type), local_factory.as_buffer().size(), local_factory.as_buffer().data());
|
||||
expr l = local_factory.push_local(binding_name(m_type), d, binding_info(m_type));
|
||||
lean_assert(!has_metavar(l));
|
||||
m_type = binding_body(m_type);
|
||||
}
|
||||
m_type = instantiate_rev(m_type, local_factory.as_buffer().size(), local_factory.as_buffer().data());
|
||||
|
||||
expr h_rel, h_lhs, h_rhs;
|
||||
lean_verify(is_simp_relation(tmp_ctx.env(), m_type, h_rel, h_lhs, h_rhs) && is_constant(h_rel));
|
||||
{
|
||||
relations.push_back(const_name(h_rel));
|
||||
flet<simp_lemmas> set_slss(m_slss, m_contextual ? add_to_slss(m_slss, local_factory.as_buffer()) : m_slss);
|
||||
|
||||
h_lhs = tmp_ctx.instantiate_mvars(h_lhs);
|
||||
|
||||
if (m_contextual || m_rel != const_name(h_rel)) {
|
||||
flet<name> set_name(m_rel, const_name(h_rel));
|
||||
freset<simplify_cache> reset_cache(m_cache);
|
||||
congr_hyp_results.emplace_back(visit(h_lhs, some_expr(e)));
|
||||
} else {
|
||||
congr_hyp_results.emplace_back(visit(h_lhs, some_expr(e)));
|
||||
}
|
||||
simp_result const & r_congr_hyp = congr_hyp_results.back();
|
||||
|
||||
if (r_congr_hyp.has_proof())
|
||||
simplified = true;
|
||||
|
||||
lean_assert(is_meta(h_rhs));
|
||||
buffer<expr> new_val_meta_args;
|
||||
expr new_val_meta = get_app_args(h_rhs, new_val_meta_args);
|
||||
lean_assert(is_metavar(new_val_meta));
|
||||
expr new_val = tmp_ctx.mk_lambda(new_val_meta_args, r_congr_hyp.get_new());
|
||||
tmp_ctx.assign(new_val_meta, new_val);
|
||||
}
|
||||
}
|
||||
|
||||
if (!simplified)
|
||||
return simp_result(e);
|
||||
|
||||
lean_assert(congr_hyps.size() == congr_hyp_results.size());
|
||||
for (unsigned i = 0; i < congr_hyps.size(); ++i) {
|
||||
expr const & pf_meta = congr_hyps[i];
|
||||
simp_result const & r_congr_hyp = congr_hyp_results[i];
|
||||
name const & rel = relations[i];
|
||||
type_context::tmp_locals & local_factory = factories[i];
|
||||
expr hyp = finalize(m_ctx, rel, r_congr_hyp).get_proof();
|
||||
// This is the current bottleneck
|
||||
// Can address somewhat by keeping the proofs as small as possible using macros
|
||||
expr pf = local_factory.mk_lambda(hyp);
|
||||
tmp_ctx.assign(pf_meta, pf);
|
||||
}
|
||||
|
||||
if (!instantiate_emetas(tmp_ctx, cl.get_num_emeta(), cl.get_emetas(), cl.get_instances()))
|
||||
return simp_result(e);
|
||||
|
||||
for (unsigned i = 0; i < cl.get_num_umeta(); i++) {
|
||||
if (!tmp_ctx.is_uassigned(i))
|
||||
return simp_result(e);
|
||||
}
|
||||
|
||||
expr e_s = tmp_ctx.instantiate_mvars(cl.get_rhs());
|
||||
expr pf = tmp_ctx.instantiate_mvars(cl.get_proof());
|
||||
|
||||
simp_result r(e_s, pf);
|
||||
|
||||
lean_simp_trace(tmp_ctx, name({"simplify", "congruence"}),
|
||||
tout() << "(" << cl.get_id() << ") "
|
||||
<< "[" << e << " ==> " << e_s << "]\n";);
|
||||
|
||||
return r;
|
||||
}
|
||||
|
||||
/* Try to use congruence lemmas generated by the congr_lemma module.
|
||||
\remark these lemmas are for the equality relation. */
|
||||
optional<simp_result> simplify_core_fn::try_auto_eq_congr(expr const & e) {
|
||||
lean_assert(m_rel == get_eq_name());
|
||||
lean_assert(is_app(e));
|
||||
buffer<expr> args;
|
||||
expr f = get_app_args(e, args);
|
||||
auto congr_lemma = mk_specialized_congr_simp(m_ctx, e);
|
||||
if (!congr_lemma) return optional<simp_result>();
|
||||
|
||||
buffer<simp_result> r_args;
|
||||
buffer<expr> new_args;
|
||||
bool has_proof = false;
|
||||
bool has_cast = false;
|
||||
bool has_simplified = false;
|
||||
|
||||
unsigned i = 0;
|
||||
|
||||
// First pass, try to simplify all the Eq arguments
|
||||
for (congr_arg_kind const & ckind : congr_lemma->get_arg_kinds()) {
|
||||
switch (ckind) {
|
||||
case congr_arg_kind::HEq:
|
||||
lean_unreachable();
|
||||
case congr_arg_kind::Fixed:
|
||||
case congr_arg_kind::FixedNoParam:
|
||||
new_args.emplace_back(args[i]);
|
||||
break;
|
||||
case congr_arg_kind::Eq:
|
||||
{
|
||||
r_args.emplace_back(visit(args[i], some_expr(e)));
|
||||
simp_result & r_arg = r_args.back();
|
||||
new_args.emplace_back(r_arg.get_new());
|
||||
if (r_arg.has_proof())
|
||||
has_proof = true;
|
||||
if (r_arg.get_new() != args[i])
|
||||
has_simplified = true;
|
||||
}
|
||||
break;
|
||||
case congr_arg_kind::Cast:
|
||||
has_cast = true;
|
||||
new_args.emplace_back(args[i]);
|
||||
break;
|
||||
}
|
||||
i++;
|
||||
}
|
||||
|
||||
if (!has_simplified) {
|
||||
simp_result r = simp_result(e);
|
||||
return optional<simp_result>(r);
|
||||
}
|
||||
|
||||
if (!has_proof) {
|
||||
simp_result r = simp_result(mk_app(f, new_args));
|
||||
return optional<simp_result>(r);
|
||||
}
|
||||
|
||||
// We have a proof, so we need to build the congruence lemma
|
||||
expr proof = congr_lemma->get_proof();
|
||||
expr type = congr_lemma->get_type();
|
||||
buffer<expr> subst;
|
||||
|
||||
i = 0;
|
||||
unsigned i_eq = 0;
|
||||
for (congr_arg_kind const & ckind : congr_lemma->get_arg_kinds()) {
|
||||
switch (ckind) {
|
||||
case congr_arg_kind::HEq:
|
||||
lean_unreachable();
|
||||
case congr_arg_kind::Fixed:
|
||||
proof = mk_app(proof, args[i]);
|
||||
subst.push_back(args[i]);
|
||||
type = binding_body(type);
|
||||
break;
|
||||
case congr_arg_kind::FixedNoParam:
|
||||
break;
|
||||
case congr_arg_kind::Eq:
|
||||
proof = mk_app(proof, args[i]);
|
||||
subst.push_back(args[i]);
|
||||
type = binding_body(type);
|
||||
{
|
||||
simp_result r_arg = finalize(m_ctx, m_rel, r_args[i_eq]);
|
||||
proof = mk_app(proof, r_arg.get_new(), r_arg.get_proof());
|
||||
subst.push_back(r_arg.get_new());
|
||||
subst.push_back(r_arg.get_proof());
|
||||
}
|
||||
type = binding_body(binding_body(type));
|
||||
i_eq++;
|
||||
break;
|
||||
case congr_arg_kind::Cast:
|
||||
lean_assert(has_cast);
|
||||
proof = mk_app(proof, args[i]);
|
||||
subst.push_back(args[i]);
|
||||
type = binding_body(type);
|
||||
break;
|
||||
}
|
||||
i++;
|
||||
}
|
||||
lean_assert(is_eq(type));
|
||||
expr rhs = instantiate_rev(app_arg(type), subst.size(), subst.data());
|
||||
simp_result r(rhs, proof);
|
||||
|
||||
if (has_cast) {
|
||||
r.update(remove_unnecessary_casts(r.get_new()));
|
||||
}
|
||||
|
||||
return optional<simp_result>(r);
|
||||
}
|
||||
|
||||
simp_result simplify_core_fn::congr_fun_arg(simp_result const & r_f, simp_result const & r_arg) {
|
||||
if (!r_f.has_proof() && !r_arg.has_proof()) return simp_result(mk_app(r_f.get_new(), r_arg.get_new()));
|
||||
else if (!r_f.has_proof()) return congr_arg(r_f.get_new(), r_arg);
|
||||
else if (!r_arg.has_proof()) return congr_fun(r_f, r_arg.get_new());
|
||||
else return congr(r_f, r_arg);
|
||||
}
|
||||
|
||||
simp_result simplify_core_fn::congr(simp_result const & r_f, simp_result const & r_arg) {
|
||||
lean_assert(r_f.has_proof() && r_arg.has_proof());
|
||||
// theorem congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂
|
||||
expr e = mk_app(r_f.get_new(), r_arg.get_new());
|
||||
expr pf = mk_congr(m_ctx, r_f.get_proof(), r_arg.get_proof());
|
||||
return simp_result(e, pf);
|
||||
}
|
||||
|
||||
simp_result simplify_core_fn::congr_fun(simp_result const & r_f, expr const & arg) {
|
||||
lean_assert(r_f.has_proof());
|
||||
// theorem congr_fun {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a
|
||||
expr e = mk_app(r_f.get_new(), arg);
|
||||
expr pf = mk_congr_fun(m_ctx, r_f.get_proof(), arg);
|
||||
return simp_result(e, pf);
|
||||
}
|
||||
|
||||
simp_result simplify_core_fn::congr_arg(expr const & f, simp_result const & r_arg) {
|
||||
lean_assert(r_arg.has_proof());
|
||||
// theorem congr_arg {A B : Type} {a₁ a₂ : A} (f : A → B) : a₁ = a₂ → f a₁ = f a₂
|
||||
expr e = mk_app(f, r_arg.get_new());
|
||||
expr pf = mk_congr_arg(m_ctx, f, r_arg.get_proof());
|
||||
return simp_result(e, pf);
|
||||
}
|
||||
|
||||
simp_result simplify_core_fn::congr_funs(simp_result const & r_f, buffer<expr> const & args) {
|
||||
expr e = r_f.get_new();
|
||||
for (unsigned i = 0; i < args.size(); ++i) {
|
||||
e = mk_app(e, args[i]);
|
||||
}
|
||||
if (!r_f.has_proof())
|
||||
return simp_result(e);
|
||||
expr pf = r_f.get_proof();
|
||||
for (unsigned i = 0; i < args.size(); ++i) {
|
||||
pf = mk_congr_fun(m_ctx, pf, args[i]);
|
||||
}
|
||||
return simp_result(e, pf);
|
||||
}
|
||||
|
||||
simp_result simplify_core_fn::visit(expr const & e, optional<expr> const & parent) {
|
||||
check_system("simplify");
|
||||
inc_num_steps();
|
||||
lean_trace_inc_depth("simplify");
|
||||
lean_simp_trace(m_ctx, "simplify", tout() << m_rel << ": " << e << "\n";);
|
||||
|
||||
auto it = m_cache.find(e);
|
||||
if (it != m_cache.end())
|
||||
return it->second;
|
||||
|
||||
simp_result curr_result(e);
|
||||
if (auto r1 = pre(e, parent)) {
|
||||
if (!r1->second) {
|
||||
m_cache.insert(mk_pair(e, r1->first));
|
||||
return r1->first;
|
||||
}
|
||||
curr_result = r1->first;
|
||||
}
|
||||
|
||||
while (true) {
|
||||
simp_result new_result;
|
||||
switch (curr_result.get_new().kind()) {
|
||||
case expr_kind::Local:
|
||||
case expr_kind::Meta:
|
||||
case expr_kind::Sort:
|
||||
case expr_kind::Constant:
|
||||
case expr_kind::Macro:
|
||||
new_result = curr_result;
|
||||
break;
|
||||
case expr_kind::Var:
|
||||
lean_unreachable();
|
||||
case expr_kind::Lambda:
|
||||
new_result = join(curr_result, visit_lambda(curr_result.get_new()));
|
||||
break;
|
||||
case expr_kind::Pi:
|
||||
new_result = join(curr_result, visit_pi(curr_result.get_new()));
|
||||
break;
|
||||
case expr_kind::App:
|
||||
new_result = join(curr_result, visit_app(curr_result.get_new()));
|
||||
break;
|
||||
case expr_kind::Let:
|
||||
new_result = join(curr_result, visit_let(curr_result.get_new()));
|
||||
break;
|
||||
}
|
||||
|
||||
if (auto r2 = post(new_result.get_new(), parent)) {
|
||||
if (!r2->second) {
|
||||
curr_result = join(new_result, r2->first);
|
||||
break;
|
||||
} else if (r2->first.get_new() == curr_result.get_new()) {
|
||||
break;
|
||||
} else {
|
||||
/* continue simplifying */
|
||||
curr_result = join(new_result, r2->first);
|
||||
}
|
||||
} else {
|
||||
curr_result = new_result;
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
if (m_lift_eq && m_rel != get_eq_name()) {
|
||||
simp_result eq_result;
|
||||
{
|
||||
flet<name> use_eq(m_rel, get_eq_name());
|
||||
freset<simplify_cache> reset_cache(m_cache);
|
||||
eq_result = visit(curr_result.get_new(), parent);
|
||||
}
|
||||
if (eq_result.get_new() != curr_result.get_new()) {
|
||||
curr_result = join(curr_result, lift_from_eq(eq_result));
|
||||
curr_result = join(curr_result, visit(curr_result.get_new(), parent));
|
||||
}
|
||||
}
|
||||
|
||||
m_cache.insert(mk_pair(e, curr_result));
|
||||
return curr_result;
|
||||
}
|
||||
|
||||
simp_result simplify_core_fn::visit_fn(expr const & e) {
|
||||
lean_assert(m_rel == get_eq_name());
|
||||
lean_assert(is_app(e));
|
||||
buffer<expr> args;
|
||||
expr const & f = get_app_args(e, args);
|
||||
simp_result r_f = visit(f, some_expr(e));
|
||||
return congr_funs(r_f, args);
|
||||
}
|
||||
|
||||
simp_result simplify_core_fn::visit_app(expr const & _e) {
|
||||
lean_assert(is_app(_e));
|
||||
expr e = should_defeq_canonize() ? defeq_canonize_args_step(_e) : _e;
|
||||
|
||||
// (1) Try user-defined congruences
|
||||
simp_result r_user = try_user_congrs(e);
|
||||
if (r_user.has_proof()) {
|
||||
if (m_rel == get_eq_name()) {
|
||||
return join(r_user, visit_fn(r_user.get_new()));
|
||||
} else {
|
||||
return r_user;
|
||||
}
|
||||
}
|
||||
|
||||
if (m_rel == get_eq_name()) {
|
||||
// (2) Synthesize congruence lemma
|
||||
optional<simp_result> r_args = try_auto_eq_congr(e);
|
||||
if (r_args) return join(*r_args, visit_fn(r_args->get_new()));
|
||||
|
||||
// (3) Fall back on generic binary congruence
|
||||
expr const & f = app_fn(e);
|
||||
expr const & arg = app_arg(e);
|
||||
|
||||
simp_result r_f = visit(f, some_expr(e));
|
||||
|
||||
if (is_dependent_fn(f)) {
|
||||
if (r_f.has_proof()) return congr_fun(r_f, arg);
|
||||
else return mk_app(r_f.get_new(), arg);
|
||||
} else {
|
||||
simp_result r_arg = visit(arg, some_expr(e));
|
||||
return congr_fun_arg(r_f, r_arg);
|
||||
}
|
||||
}
|
||||
|
||||
return simp_result(e);
|
||||
}
|
||||
|
||||
optional<expr> simplify_core_fn::prove(expr const &) {
|
||||
return none_expr();
|
||||
}
|
||||
|
||||
simp_result simplify_core_fn::visit_lambda(expr const & e) {
|
||||
return simp_result(e);
|
||||
}
|
||||
|
||||
simp_result simplify_core_fn::visit_pi(expr const & e) {
|
||||
return try_user_congrs(e);
|
||||
}
|
||||
|
||||
simp_result simplify_core_fn::visit_let(expr const & e) {
|
||||
return simp_result(e);
|
||||
}
|
||||
|
||||
simp_result simplify_core_fn::visit_macro(expr const & e) {
|
||||
return simp_result(e);
|
||||
}
|
||||
|
||||
optional<pair<simp_result, bool>> simplify_core_fn::pre(expr const &, optional<expr> const &) {
|
||||
return optional<pair<simp_result, bool>>();
|
||||
}
|
||||
|
||||
optional<pair<simp_result, bool>> simplify_core_fn::post(expr const &, optional<expr> const &) {
|
||||
return optional<pair<simp_result, bool>>();
|
||||
}
|
||||
|
||||
simplify_core_fn::simplify_core_fn(type_context & ctx, simp_lemmas const & slss,
|
||||
unsigned max_steps, bool contextual, bool lift_eq,
|
||||
bool canonize_instances, bool canonize_proofs):
|
||||
m_ctx(ctx), m_slss(slss), m_max_steps(max_steps), m_contextual(contextual),
|
||||
m_lift_eq(lift_eq), m_canonize_instances(canonize_instances), m_canonize_proofs(canonize_proofs) {
|
||||
}
|
||||
|
||||
simp_result simplify_core_fn::operator()(name const & rel, expr const & e) {
|
||||
m_rel = rel;
|
||||
m_cache.clear();
|
||||
simp_result r(e);
|
||||
while (true) {
|
||||
m_need_restart = false;
|
||||
r = join(r, visit(r.get_new(), none_expr()));
|
||||
if (!m_need_restart || !should_defeq_canonize())
|
||||
return r;
|
||||
m_cache.clear();
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
static name * g_simplify_prefix = nullptr;
|
||||
name get_simplify_prefix_name() { return *g_simplify_prefix; }
|
||||
|
|
@ -102,8 +679,6 @@ static bool get_simplify_canonize_proofs_fixed_point(options const & o) {
|
|||
return o.get_bool(*g_simplify_canonize_proofs_fixed_point, LEAN_DEFAULT_SIMPLIFY_DEFEQ_CANONIZE_PROOFS_FIXED_POINT);
|
||||
}
|
||||
|
||||
#define lean_simp_trace(tctx, n, code) lean_trace(n, scope_trace_env _scope1(tctx.env(), tctx); code)
|
||||
|
||||
/* Main simplifier class */
|
||||
|
||||
class simplifier {
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
/*
|
||||
Copyright (c) 2015 Daniel Selsam. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Daniel Selsam
|
||||
Author: Daniel Selsam, Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include "kernel/expr_pair.h"
|
||||
|
|
@ -11,6 +11,90 @@ Author: Daniel Selsam
|
|||
#include "library/tactic/simp_result.h"
|
||||
|
||||
namespace lean {
|
||||
/* Core simplification procedure. It performs the following tasks:
|
||||
1- Manages the cache;
|
||||
2- Applies congruence lemmas;
|
||||
3- Canonizes instances & proofs;
|
||||
4- Manages contextual rewriting
|
||||
|
||||
This is a base class for many simplification strategies.
|
||||
Its behavior can be configured by overriding its virtual methods.
|
||||
This class does *not* apply any simp lemma, nor it tries to
|
||||
put subterms in weak-head-normal-form.
|
||||
|
||||
This class also does *not* use axioms. For example, it will
|
||||
not use funext to go inside lambda terms. This feature is provided
|
||||
by subclasses.
|
||||
|
||||
Remark: it is debatable whether the options m_lift_eq, m_canonize_instances and
|
||||
m_canonize_proofs really need to be here. They may be moved to subclasses in the
|
||||
future.
|
||||
*/
|
||||
class simplify_core_fn {
|
||||
protected:
|
||||
typedef expr_struct_map<simp_result> simplify_cache;
|
||||
|
||||
type_context m_ctx;
|
||||
name m_rel;
|
||||
simp_lemmas m_slss;
|
||||
simplify_cache m_cache;
|
||||
|
||||
/* Logging */
|
||||
unsigned m_num_steps{0};
|
||||
bool m_need_restart{false};
|
||||
|
||||
/* Options */
|
||||
unsigned m_max_steps;
|
||||
bool m_contextual;
|
||||
bool m_lift_eq;
|
||||
bool m_canonize_instances;
|
||||
bool m_canonize_proofs;
|
||||
|
||||
simp_result join(simp_result const & r1, simp_result const & r2);
|
||||
void inc_num_steps();
|
||||
bool is_dependent_fn(expr const & f);
|
||||
bool should_defeq_canonize() const { return m_canonize_instances || m_canonize_proofs; }
|
||||
bool instantiate_emetas(tmp_type_context & tmp_tctx, unsigned num_emeta, list<expr> const & emetas, list<bool> const & instances);
|
||||
simp_result lift_from_eq(simp_result const & r_eq);
|
||||
simp_lemmas add_to_slss(simp_lemmas const & slss, buffer<expr> const & ls);
|
||||
expr remove_unnecessary_casts(expr const & e);
|
||||
expr defeq_canonize_args_step(expr const & e);
|
||||
|
||||
/* Congruence */
|
||||
simp_result try_user_congrs(expr const & e);
|
||||
simp_result try_user_congr(expr const & e, simp_lemma const & cr);
|
||||
|
||||
optional<simp_result> try_auto_eq_congr(expr const & e);
|
||||
|
||||
simp_result congr_fun_arg(simp_result const & r_f, simp_result const & r_arg);
|
||||
simp_result congr(simp_result const & r_f, simp_result const & r_arg);
|
||||
simp_result congr_fun(simp_result const & r_f, expr const & arg);
|
||||
simp_result congr_arg(expr const & f, simp_result const & r_arg);
|
||||
simp_result congr_funs(simp_result const & r_f, buffer<expr> const & args);
|
||||
|
||||
/* Visitors */
|
||||
virtual optional<pair<simp_result, bool>> pre(expr const & e, optional<expr> const & parent);
|
||||
virtual optional<pair<simp_result, bool>> post(expr const & e, optional<expr> const & parent);
|
||||
|
||||
virtual optional<expr> prove(expr const & goal);
|
||||
|
||||
simp_result visit_fn(expr const & e);
|
||||
virtual simp_result visit_lambda(expr const & e);
|
||||
virtual simp_result visit_pi(expr const & e);
|
||||
virtual simp_result visit_let(expr const & e);
|
||||
virtual simp_result visit_app(expr const & e);
|
||||
virtual simp_result visit_macro(expr const & e);
|
||||
|
||||
virtual simp_result visit(expr const & e, optional<expr> const & parent);
|
||||
|
||||
public:
|
||||
simplify_core_fn(type_context & ctx, simp_lemmas const & slss,
|
||||
unsigned max_steps, bool contextual, bool lift_eq,
|
||||
bool canonize_instances, bool canonize_proofs);
|
||||
|
||||
environment const & env() const;
|
||||
simp_result operator()(name const & rel, expr const & e);
|
||||
};
|
||||
|
||||
simp_result simplify(type_context & tctx, name const & rel, simp_lemmas const & simp_lemmas, vm_obj const & prove_fn, expr const & e);
|
||||
simp_result simplify(type_context & tctx, name const & rel, simp_lemmas const & simp_lemmas, expr const & e);
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue