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

feat(library/blast): add blast.ematch option, and ematching search procedure

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-30 07:19:23 -07:00
parent 4c624206f4
commit 2296168bda
4 changed files with 78 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

69
src/library/blast/forward/ematch.cpp
View file

@ -5,8 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "library/constants.h"
#include "library/idx_metavar.h"
#include "library/blast/blast.h"
#include "library/blast/trace.h"
#include "library/blast/options.h"
#include "library/blast/congruence_closure.h"
#include "library/blast/forward/pattern.h"
@ -137,7 +139,7 @@ struct ematch_fn {
}
bool is_done() const {
return !m_state;
return is_nil(m_state);
}
bool is_eqv(name const & R, expr const & p, expr const & t) {
@ -211,6 +213,7 @@ struct ematch_fn {
name R; frame_kind kind; expr p, t;
std::tie(R, kind, p, t) = head(m_state);
m_state = tail(m_state);
diagnostic(env(), ios()) << ">> " << R << ", " << ppb(p) << " =?= " << ppb(t) << "\n";
switch (kind) {
case DefEqOnly:
return m_ctx->is_def_eq(p, t);
@ -222,19 +225,50 @@ struct ematch_fn {
lean_unreachable();
}
bool match() {
// TODO(Leo)
bool backtrack() {
if (m_choice_stack.empty())
return false;
m_ctx->pop();
lean_assert(m_choice_stack.back());
m_state = head(m_choice_stack.back());
m_ctx->push();
m_choice_stack.back() = tail(m_choice_stack.back());
if (!m_choice_stack.back())
m_choice_stack.pop_back();
return true;
}
void instantiate(hi_lemma const & lemma) {
std::cout << "FOUND\n";
for (expr const & mvar : lemma.m_mvars) {
diagnostic(env(), ios()) << "[" << mvar << "] := " << ppb(m_ctx->instantiate_uvars_mvars(mvar)) << "\n";
}
}
void search(hi_lemma const & lemma) {
while (true) {
if (is_done()) {
instantiate(lemma);
if (!backtrack())
return;
}
if (!process_next()) {
if (!backtrack())
return;
}
}
}
void instantiate_lemma_using(hi_lemma const & lemma, buffer<expr> const & ps, bool filter) {
expr const & p0 = ps[0];
expr const & f = get_app_fn(p0);
buffer<expr> p0_args;
expr const & f = get_app_args(p0, p0_args);
name const & R = is_prop(p0) ? get_iff_name() : get_eq_name();
unsigned gmt = m_cc.get_gmt();
if (auto s = m_ext.m_apps.find(f)) {
s->for_each([&](expr const & t) {
if (m_cc.is_congr_root(R, t) && (!filter || m_cc.get_mt(R, t) == gmt)) {
m_ctx->clear();
m_ctx->set_next_uvar_idx(lemma.m_num_uvars);
m_ctx->set_next_mvar_idx(lemma.m_num_mvars);
state s;
@ -243,11 +277,27 @@ struct ematch_fn {
--i;
s = cons(entry(name(), Continue, ps[i], expr()), s);
}
s = cons(entry(R, Match, p0, t), s);
diagnostic(env(), ios()) << "ematch " << ppb(p0) << " =?= " << ppb(t) << "\n";
if (match()) {
// TODO(Leo): add instance
m_choice_stack.clear();
m_state = s;
optional<ext_congr_lemma> cg_lemma = mk_ext_congr_lemma(R, f, p0_args.size());
if (!cg_lemma)
return;
buffer<expr> t_args;
get_app_args(t, t_args);
if (p0_args.size() != t_args.size())
return;
auto const * r_names = &cg_lemma->m_rel_names;
for (unsigned i = 0; i < p0_args.size(); i++) {
lean_assert(*r_names);
if (auto Rc = head(*r_names)) {
m_state = cons(entry(*Rc, Match, p0_args[i], t_args[i]), m_state);
} else {
m_state = cons(entry(get_eq_name(), DefEqOnly, p0_args[i], t_args[i]), m_state);
}
r_names = &tail(*r_names);
}
search(lemma);
}
});
}
@ -295,6 +345,9 @@ struct ematch_fn {
};
action_result ematch_action() {
if (get_config().m_ematch)
return ematch_fn()();
else
return action_result::failed();
}
}}

12
src/library/blast/options.cpp
View file

@ -38,6 +38,9 @@ Author: Leonardo de Moura
#ifndef LEAN_DEFAULT_BLAST_RECURSOR
#define LEAN_DEFAULT_BLAST_RECURSOR true
#endif
#ifndef LEAN_DEFAULT_BLAST_EMATCH
#define LEAN_DEFAULT_BLAST_EMATCH false
#endif
namespace lean {
@ -52,6 +55,7 @@ static name * g_blast_simp = nullptr;
static name * g_blast_cc = nullptr;
static name * g_blast_trace_cc = nullptr;
static name * g_blast_recursor = nullptr;
static name * g_blast_ematch = nullptr;
static name * g_blast_show_failure = nullptr;
unsigned get_blast_max_depth(options const & o) {
@ -81,6 +85,9 @@ bool get_blast_trace_cc(options const & o) {
bool get_blast_recursor(options const & o) {
return o.get_bool(*g_blast_recursor, LEAN_DEFAULT_BLAST_RECURSOR);
}
bool get_blast_ematch(options const & o) {
return o.get_bool(*g_blast_ematch, LEAN_DEFAULT_BLAST_EMATCH);
}
bool get_blast_show_failure(options const & o) {
return o.get_bool(*g_blast_show_failure, LEAN_DEFAULT_BLAST_SHOW_FAILURE);
}
@ -95,6 +102,7 @@ config::config(options const & o) {
m_cc = get_blast_cc(o);
m_trace_cc = get_blast_trace_cc(o);
m_recursor = get_blast_recursor(o);
m_ematch = get_blast_ematch(o);
m_show_failure = get_blast_show_failure(o);
m_pattern_max_steps = get_pattern_max_steps(o);
}
@ -126,6 +134,7 @@ void initialize_options() {
g_blast_cc = new name{"blast", "cc"};
g_blast_trace_cc = new name{"blast", "trace_cc"};
g_blast_recursor = new name{"blast", "recursor"};
g_blast_ematch = new name{"blast", "ematch"};
g_blast_show_failure = new name{"blast", "show_failure"};
register_unsigned_option(*blast::g_blast_max_depth, LEAN_DEFAULT_BLAST_MAX_DEPTH,
@ -146,6 +155,8 @@ void initialize_options() {
"(blast) (for debugging purposes) trace congruence closure");
register_bool_option(*blast::g_blast_recursor, LEAN_DEFAULT_BLAST_RECURSOR,
"(blast) enable recursor action");
register_bool_option(*blast::g_blast_ematch, LEAN_DEFAULT_BLAST_EMATCH,
"(blast) enable heuristic instantiation based on e-matching");
register_bool_option(*blast::g_blast_show_failure, LEAN_DEFAULT_BLAST_SHOW_FAILURE,
"(blast) show failure state");
}
@ -159,6 +170,7 @@ void finalize_options() {
delete g_blast_cc;
delete g_blast_trace_cc;
delete g_blast_recursor;
delete g_blast_ematch;
delete g_blast_show_failure;
}
}}

1
src/library/blast/options.h
View file

@ -18,6 +18,7 @@ struct config {
bool m_subst;
bool m_simp;
bool m_recursor;
bool m_ematch;
bool m_cc;
bool m_trace_cc;
bool m_show_failure;

3
src/library/blast/simple_strategy.cpp
View file

@ -14,6 +14,7 @@ Author: Leonardo de Moura
#include "library/blast/backward/backward_action.h"
#include "library/blast/backward/backward_strategy.h"
#include "library/blast/forward/forward_actions.h"
#include "library/blast/forward/ematch.h"
#include "library/blast/unit/unit_action.h"
#include "library/blast/no_confusion_action.h"
#include "library/blast/simplifier/simplifier_actions.h"
@ -67,7 +68,7 @@ class simple_strategy : public strategy {
Try(assumption_action());
Try(recursor_action());
Try(constructor_action());
Try(ematch_action());
TryStrategy(apply_backward_strategy());
Try(qfc_action(list<gexpr>()));