feat(library/simplify): use custom matcher in the simplifier, and remove hack from type_context
@joehendrix This commit is implementing the matcher that postpones implicit arguments. The lemma get_data_mk_byte can be proved without using any hacks in the type_context unifier. I also added the trace class: simplify.implicit_failure If we use the command set_option trace.simplify.implicit_failure true Then, the simplifier will generate a diagnostic message every time it succeeds in the explicit part, but fails in the implicit one. Please feel free to suggest a better name to his option. BTW, we can now easily extend the matcher with additional features. I'm wondering if we will eventually want to write some of these extensions in Lean.
This commit is contained in:
Leonardo de Moura
parent
f5e0fc4876
commit
e4b3dee526
6 changed files with 136 additions and 96 deletions
|
|
@ -1269,6 +1269,7 @@ class add_nested_inductive_decl_fn {
|
|||
defeq_can_state dcs;
|
||||
simplify_fn simplifier(tctx, dcs, all_lemmas, max_steps, contextual, lift_eq,
|
||||
canonize_instances, canonize_proofs, use_axioms);
|
||||
simplifier.set_use_matcher(false); // hack
|
||||
auto thm_pr = simplifier.prove_by_simp(get_eq_name(), thm);
|
||||
if (!thm_pr) {
|
||||
formatter_factory const & fmtf = get_global_ios().get_formatter_factory();
|
||||
|
|
|
|||
|
|
@ -497,14 +497,79 @@ simp_result simplify_core_fn::rewrite(expr const & e) {
|
|||
return simp_result(e);
|
||||
}
|
||||
|
||||
struct match_fn {
|
||||
tmp_type_context & m_ctx;
|
||||
name const & m_id;
|
||||
buffer<std::tuple<expr, expr, bool>> m_postponed;
|
||||
|
||||
match_fn(tmp_type_context & ctx, name const & id):m_ctx(ctx), m_id(id) {}
|
||||
|
||||
bool match(expr const & p, expr const & t) {
|
||||
if (m_ctx.ctx().is_mvar(p))
|
||||
if (auto v = m_ctx.ctx().get_assignment(p))
|
||||
return match(*v, t);
|
||||
if (is_app(p) && is_app(t)) {
|
||||
expr const & fn = get_app_fn(p);
|
||||
if (m_ctx.is_def_eq(fn, get_app_fn(t))) {
|
||||
buffer<expr> p_args;
|
||||
buffer<expr> t_args;
|
||||
get_app_args(p, p_args);
|
||||
get_app_args(t, t_args);
|
||||
fun_info finfo = get_fun_info(m_ctx.ctx(), fn);
|
||||
if (p_args.size() != t_args.size())
|
||||
return false;
|
||||
auto it = finfo.get_params_info();
|
||||
for (unsigned i = 0; i < p_args.size(); i++) {
|
||||
if (it && head(it).is_inst_implicit()) {
|
||||
m_postponed.emplace_back(p_args[i], t_args[i], true);
|
||||
} else if (it && head(it).is_implicit()) {
|
||||
m_postponed.emplace_back(p_args[i], t_args[i], false);
|
||||
} else if (!match(p_args[i], t_args[i])) {
|
||||
return false;
|
||||
}
|
||||
if (it) it = tail(it);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return m_ctx.is_def_eq(p, t);
|
||||
}
|
||||
|
||||
bool operator()(expr const & p, expr const & t) {
|
||||
if (!match(p, t)) return false;
|
||||
|
||||
for (auto const & e : m_postponed) {
|
||||
expr p1, t1; bool implicit;
|
||||
std::tie(p1, t1, implicit) = e;
|
||||
p1 = m_ctx.instantiate_mvars(p1);
|
||||
if (implicit)
|
||||
p1 = m_ctx.ctx().complete_instance(p1);
|
||||
if (!match(p1, t1)) {
|
||||
lean_trace(name({"simplify", "implicit_failure"}), scope_trace_env scope(m_ctx.env(), m_ctx.ctx());
|
||||
tout() << "fail to match '" << m_id << "':\n";
|
||||
tout() << p << "\n=?=\n" << t << "\nbecause the following implicit match\n";
|
||||
tout() << p1 << "\n=?=\n" << t1 << "\n";);
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
};
|
||||
|
||||
bool simplify_core_fn::match(tmp_type_context & ctx, simp_lemma const & sl, expr const & t) {
|
||||
if (m_use_matcher)
|
||||
return match_fn(ctx, sl.get_id())(sl.get_lhs(), t);
|
||||
else
|
||||
return ctx.is_def_eq(t, sl.get_lhs());
|
||||
}
|
||||
|
||||
simp_result simplify_core_fn::rewrite_core(expr const & e, simp_lemma const & sl) {
|
||||
tmp_type_context tmp_ctx(m_ctx, sl.get_num_umeta(), sl.get_num_emeta());
|
||||
if (!tmp_ctx.is_def_eq(e, sl.get_lhs())) {
|
||||
|
||||
if (!match(tmp_ctx, sl, e)) {
|
||||
lean_trace_d(name({"debug", "simplify", "try_rewrite"}),
|
||||
tout() << "fail to unify '" << sl.get_id()
|
||||
<< "':\n------------------------------------------------\n"
|
||||
<< e << "\n=?=\n" << sl.get_lhs()
|
||||
<< "\n------------------------------------------------\n";);
|
||||
tout() << "fail to unify '" << sl.get_id() << "':\n"
|
||||
<< e << "\n=?=\n" << sl.get_lhs() << "\n--------------\n";);
|
||||
return simp_result(e);
|
||||
}
|
||||
|
||||
|
|
@ -1158,6 +1223,7 @@ vm_obj tactic_ext_simplify_core(unsigned DEBUG_CODE(num), vm_obj const * args) {
|
|||
void initialize_simplify() {
|
||||
register_trace_class("simplify");
|
||||
register_trace_class(name({"simplify", "failure"}));
|
||||
register_trace_class(name({"simplify", "implicit_failure"}));
|
||||
register_trace_class(name({"simplify", "context"}));
|
||||
register_trace_class(name({"simplify", "canonize"}));
|
||||
register_trace_class(name({"simplify", "congruence"}));
|
||||
|
|
|
|||
|
|
@ -51,6 +51,9 @@ protected:
|
|||
bool m_lift_eq;
|
||||
bool m_canonize_instances;
|
||||
bool m_canonize_proofs;
|
||||
/* The following option should be removed as soon as we
|
||||
refactor the inductive compiler. */
|
||||
bool m_use_matcher{true};
|
||||
|
||||
simp_result join(simp_result const & r1, simp_result const & r2);
|
||||
void inc_num_steps();
|
||||
|
|
@ -100,6 +103,8 @@ protected:
|
|||
|
||||
simp_result simplify(expr const & e);
|
||||
|
||||
bool match(tmp_type_context & ctx, simp_lemma const & sl, expr const & t);
|
||||
|
||||
public:
|
||||
simplify_core_fn(type_context & ctx, defeq_canonizer::state & dcs, simp_lemmas const & slss,
|
||||
unsigned max_steps, bool contextual, bool lift_eq,
|
||||
|
|
@ -108,6 +113,8 @@ public:
|
|||
environment const & env() const;
|
||||
simp_result operator()(name const & rel, expr const & e);
|
||||
|
||||
void set_use_matcher(bool flag) { m_use_matcher = flag; }
|
||||
|
||||
optional<expr> prove_by_simp(name const & rel, expr const & e);
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -2220,73 +2220,18 @@ bool type_context::is_def_eq_args(expr const & e1, expr const & e2) {
|
|||
return false;
|
||||
fun_info finfo = get_fun_info(*this, fn, args1.size());
|
||||
unsigned i = 0;
|
||||
/*
|
||||
Try to solve unification constraint
|
||||
(f a_1 ... a_n) =?= (f b_1 ... b_n)
|
||||
by solving
|
||||
a_i =?= b_i
|
||||
|
||||
We add i to postponed, if a_i or b_i is a numeral and
|
||||
the i-th argument of f has forward dependencies.
|
||||
|
||||
The goal is to be able to handle unification constraints
|
||||
coming from fixed size vector problems.
|
||||
|
||||
In this kind of problem, we have constraints such as
|
||||
|
||||
@to_list ?α (?m - ?n) (@dropn ?α ?m ?n ?v) =?= @to_list bool 6 (@dropn bool 8 2 v)
|
||||
|
||||
In the first pass, we have the constraint
|
||||
|
||||
?m - ?n =?= 6
|
||||
|
||||
which cannot be solved. However, after we unify the next argument, we have
|
||||
|
||||
?m := 8 and ?n := 2
|
||||
|
||||
and the constraint above becomes
|
||||
|
||||
8 - 2 =?= 6
|
||||
|
||||
which can be solved.
|
||||
*/
|
||||
buffer<unsigned> postponed;
|
||||
bool progress = false;
|
||||
for (param_info const & pinfo : finfo.get_params_info()) {
|
||||
if (pinfo.is_inst_implicit()) {
|
||||
args1[i] = complete_instance(args1[i]);
|
||||
args2[i] = complete_instance(args2[i]);
|
||||
}
|
||||
if (is_def_eq_core(args1[i], args2[i])) {
|
||||
progress = true;
|
||||
} else if (pinfo.has_fwd_deps() && (to_small_num(args1[i]) || to_small_num(args2[i]))) {
|
||||
postponed.push_back(i);
|
||||
} else {
|
||||
if (!is_def_eq_core(args1[i], args2[i]))
|
||||
return false;
|
||||
}
|
||||
i++;
|
||||
}
|
||||
for (; i < args1.size(); i++) {
|
||||
if (is_def_eq_core(args1[i], args2[i])) {
|
||||
progress = true;
|
||||
} else {
|
||||
if (!is_def_eq_core(args1[i], args2[i]))
|
||||
return false;
|
||||
}
|
||||
}
|
||||
while (true) {
|
||||
if (postponed.empty()) return true;
|
||||
if (!progress) return false;
|
||||
progress = false;
|
||||
unsigned j = 0;
|
||||
for (unsigned i = 0; i < postponed.size(); i++) {
|
||||
if (is_def_eq_core(instantiate_mvars(args1[postponed[i]]), instantiate_mvars(args2[postponed[i]]))) {
|
||||
progress = true;
|
||||
} else {
|
||||
postponed[j] = postponed[i];
|
||||
j++;
|
||||
}
|
||||
}
|
||||
postponed.shrink(j);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
|
@ -3675,34 +3620,34 @@ expr type_context::eta_expand(expr const & e) {
|
|||
return locals.mk_lambda(r);
|
||||
}
|
||||
|
||||
tmp_type_context::tmp_type_context(type_context & tctx, unsigned num_umeta, unsigned num_emeta): m_tctx(tctx) {
|
||||
tmp_type_context::tmp_type_context(type_context & ctx, unsigned num_umeta, unsigned num_emeta): m_ctx(ctx) {
|
||||
m_tmp_uassignment.resize(num_umeta, none_level());
|
||||
m_tmp_eassignment.resize(num_emeta, none_expr());
|
||||
}
|
||||
|
||||
bool tmp_type_context::is_def_eq(expr const & e1, expr const & e2) {
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_tctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
return m_tctx.is_def_eq(e1, e2);
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_ctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
return m_ctx.is_def_eq(e1, e2);
|
||||
}
|
||||
|
||||
expr tmp_type_context::infer(expr const & e) {
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_tctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
return m_tctx.infer(e);
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_ctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
return m_ctx.infer(e);
|
||||
}
|
||||
|
||||
expr tmp_type_context::whnf(expr const & e) {
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_tctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
return m_tctx.whnf(e);
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_ctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
return m_ctx.whnf(e);
|
||||
}
|
||||
|
||||
level tmp_type_context::mk_tmp_univ_mvar() {
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_tctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
return m_tctx.mk_tmp_univ_mvar();
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_ctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
return m_ctx.mk_tmp_univ_mvar();
|
||||
}
|
||||
|
||||
expr tmp_type_context::mk_tmp_mvar(expr const & type) {
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_tctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
return m_tctx.mk_tmp_mvar(type);
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_ctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
return m_ctx.mk_tmp_mvar(type);
|
||||
}
|
||||
|
||||
bool tmp_type_context::is_uassigned(unsigned i) const {
|
||||
|
|
@ -3720,48 +3665,48 @@ void tmp_type_context::clear_eassignment() {
|
|||
}
|
||||
|
||||
expr tmp_type_context::instantiate_mvars(expr const & e) {
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_tctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
return m_tctx.instantiate_mvars(e);
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_ctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
return m_ctx.instantiate_mvars(e);
|
||||
}
|
||||
|
||||
void tmp_type_context::assign(expr const & m, expr const & v) {
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_tctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
m_tctx.assign(m, v);
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_ctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
m_ctx.assign(m, v);
|
||||
}
|
||||
|
||||
expr tmp_type_context::mk_lambda(buffer<expr> const & locals, expr const & e) {
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_tctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
return m_tctx.mk_lambda(locals, e);
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_ctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
return m_ctx.mk_lambda(locals, e);
|
||||
}
|
||||
|
||||
expr tmp_type_context::mk_pi(buffer<expr> const & locals, expr const & e) {
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_tctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
return m_tctx.mk_pi(locals, e);
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_ctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
return m_ctx.mk_pi(locals, e);
|
||||
}
|
||||
|
||||
expr tmp_type_context::mk_lambda(expr const & local, expr const & e) {
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_tctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
return m_tctx.mk_lambda(local, e);
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_ctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
return m_ctx.mk_lambda(local, e);
|
||||
}
|
||||
|
||||
expr tmp_type_context::mk_pi(expr const & local, expr const & e) {
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_tctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
return m_tctx.mk_pi(local, e);
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_ctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
return m_ctx.mk_pi(local, e);
|
||||
}
|
||||
|
||||
expr tmp_type_context::mk_lambda(std::initializer_list<expr> const & locals, expr const & e) {
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_tctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
return m_tctx.mk_lambda(locals, e);
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_ctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
return m_ctx.mk_lambda(locals, e);
|
||||
}
|
||||
|
||||
expr tmp_type_context::mk_pi(std::initializer_list<expr> const & locals, expr const & e) {
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_tctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
return m_tctx.mk_pi(locals, e);
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_ctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
return m_ctx.mk_pi(locals, e);
|
||||
}
|
||||
|
||||
bool tmp_type_context::is_prop(expr const & e) {
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_tctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
return m_tctx.is_prop(e);
|
||||
type_context::tmp_mode_scope_with_buffers tmp_scope(m_ctx, m_tmp_uassignment, m_tmp_eassignment);
|
||||
return m_ctx.is_prop(e);
|
||||
}
|
||||
|
||||
/** \brief Helper class for pretty printing terms that contain local_decl_ref's and metavar_decl_ref's */
|
||||
|
|
|
|||
|
|
@ -418,6 +418,9 @@ public:
|
|||
|
||||
expr eta_expand(expr const & e);
|
||||
|
||||
/* Try to assign metavariables occuring in e using type class resolution */
|
||||
expr complete_instance(expr const & e);
|
||||
|
||||
struct transparency_scope : public flet<transparency_mode> {
|
||||
transparency_scope(type_context & ctx, transparency_mode m):
|
||||
flet<transparency_mode>(ctx.m_transparency_mode, m) {
|
||||
|
|
@ -618,7 +621,6 @@ private:
|
|||
bool is_def_eq_core_core(expr const & t, expr const & s);
|
||||
bool is_def_eq_core(expr const & t, expr const & s);
|
||||
bool is_def_eq_binding(expr e1, expr e2);
|
||||
expr complete_instance(expr const & e);
|
||||
expr try_to_unstuck_using_complete_instance(expr const & e);
|
||||
bool is_def_eq_args(expr const & e1, expr const & e2);
|
||||
bool is_def_eq_eta(expr const & e1, expr const & e2);
|
||||
|
|
@ -703,15 +705,15 @@ public:
|
|||
};
|
||||
|
||||
class tmp_type_context : public abstract_type_context {
|
||||
type_context & m_tctx;
|
||||
type_context & m_ctx;
|
||||
buffer<optional<level>> m_tmp_uassignment;
|
||||
buffer<optional<expr>> m_tmp_eassignment;
|
||||
|
||||
public:
|
||||
tmp_type_context(type_context & tctx, unsigned num_umeta = 0, unsigned num_emeta = 0);
|
||||
type_context & tctx() const { return m_tctx; }
|
||||
tmp_type_context(type_context & ctx, unsigned num_umeta = 0, unsigned num_emeta = 0);
|
||||
type_context & ctx() const { return m_ctx; }
|
||||
|
||||
virtual environment const & env() const override { return m_tctx.env(); }
|
||||
virtual environment const & env() const override { return m_ctx.env(); }
|
||||
virtual expr infer(expr const & e) override;
|
||||
virtual expr whnf(expr const & e) override;
|
||||
virtual bool is_def_eq(expr const & e1, expr const & e2) override;
|
||||
|
|
|
|||
19
tests/lean/run/mk_byte.lean
Normal file
19
tests/lean/run/mk_byte.lean
Normal file
|
|
@ -0,0 +1,19 @@
|
|||
import data.bitvec
|
||||
|
||||
open vector
|
||||
|
||||
def byte_type := bitvec 8
|
||||
|
||||
-- A byte is formed from concatenating two bits and a 6-bit field.
|
||||
def mk_byte (a b : bool) (l : bitvec 6) : byte_type := a :: b :: l
|
||||
|
||||
-- Get the third component
|
||||
def get_data (byte : byte_type) : bitvec 6 := vector.dropn 2 byte
|
||||
|
||||
lemma get_data_mk_byte {a b : bool} {l : bitvec 6} : get_data (mk_byte a b l) = l :=
|
||||
begin
|
||||
apply vector.eq,
|
||||
unfold mk_byte,
|
||||
unfold get_data,
|
||||
simp [to_list_dropn, to_list_cons, list.dropn]
|
||||
end
|
||||
Loading…
Add table
Reference in a new issue