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

refactor(library/blast): merge state and branch classes

Browse source 
We will keep only one active branch in blast.
All other branches are implicit.
This commit is contained in:
Leonardo de Moura 2015-11-09 13:19:59 -08:00
parent 9bdf3a0d33
commit 9a557958f4
14 changed files with 313 additions and 381 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1324,8 +1324,7 @@ static environment simplify_cmd(parser & p) {
std::tie(e, ls) = parse_local_expr(p);
blast::scope_debug scope(p.env(), p.ios());
blast::branch b;
blast::simp::result r = blast::simplify(b, rel, e);
blast::simp::result r = blast::simplify(rel, e);
flycheck_information info(p.regular_stream());
if (info.enabled()) {

2
src/library/blast/CMakeLists.txt
View file

@ -1,2 +1,2 @@
add_library(blast OBJECT expr.cpp branch.cpp state.cpp blast.cpp
add_library(blast OBJECT expr.cpp state.cpp blast.cpp
blast_tactic.cpp init_module.cpp simplifier.cpp assumption.cpp intros.cpp)

8
src/library/blast/assumption.cpp
View file

@ -11,13 +11,13 @@ namespace blast {
optional<expr> assumption_action() {
// TODO(Leo): this is a very naive implementation that just traverses the set of
// active hypothesis
branch const & b = main_branch();
expr const & target = b.get_target();
auto hidx = b.find_active_hypothesis([&](unsigned, hypothesis const & h) {
state const & s = curr_state();
expr const & target = s.get_target();
auto hidx = s.find_active_hypothesis([&](unsigned, hypothesis const & h) {
return is_def_eq(h.get_type(), target);
});
if (!hidx)
return none_expr();
return some_expr(b.get(*hidx)->get_value());
return some_expr(s.get(*hidx)->get_value());
}
}}

17
src/library/blast/blast.cpp
View file

@ -172,8 +172,8 @@ class blastenv {
in a different place. */
virtual expr infer_local(expr const & e) const {
if (is_href(e)) {
branch const & b = m_benv.m_curr_state.get_main_branch();
hypothesis const * h = b.get(e);
state const & s = m_benv.m_curr_state;
hypothesis const * h = s.get(e);
lean_assert(h);
return h->get_type();
} else {
@ -402,9 +402,8 @@ class blastenv {
tctx m_tctx;
void save_initial_context() {
branch const & b = m_curr_state.get_main_branch();
hypothesis_idx_buffer hidxs;
b.get_sorted_hypotheses(hidxs);
m_curr_state.get_sorted_hypotheses(hidxs);
buffer<expr> ctx;
for (unsigned hidx : hidxs) {
ctx.push_back(mk_href(hidx));
@ -429,7 +428,7 @@ class blastenv {
enum status { NoAction, ClosedBranch, Continue };
optional<unsigned> activate_hypothesis() {
return m_curr_state.get_main_branch().activate_hypothesis();
return m_curr_state.activate_hypothesis();
}
pair<status, expr> next_action() {
@ -498,11 +497,10 @@ class blastenv {
struct to_tactic_proof_fn : public replace_visitor {
state & m_state;
branch & m_branch;
virtual expr visit_local(expr const & e) {
if (is_href(e)) {
hypothesis const * h = m_branch.get(e);
hypothesis const * h = m_state.get(e);
lean_assert(h);
expr v = h->get_value();
return visit(v);
@ -522,7 +520,7 @@ class blastenv {
}
to_tactic_proof_fn(state & s):
m_state(s), m_branch(s.get_main_branch()) {}
m_state(s) {}
};
expr to_tactic_proof(expr const & pr) {
@ -789,8 +787,7 @@ public:
virtual expr infer_local(expr const & e) const {
state const & s = curr_state();
if (is_href(e)) {
branch const & b = s.get_main_branch();
hypothesis const * h = b.get(e);
hypothesis const * h = s.get(e);
lean_assert(h);
return h->get_type();
} else {

2
src/library/blast/blast.h
View file

@ -26,8 +26,6 @@ io_state const & ios();
app_builder & get_app_builder();
/** \brief Return the thread local current state being processed by the blast tactic. */
state & curr_state();
/** brief Return the main branch of the current state being processed by the blast tactic. */
inline branch & main_branch() { return curr_state().get_main_branch(); }
/** \brief Return a thread local fresh local constant. */
expr mk_fresh_local(expr const & type, binder_info const & bi = binder_info());
/** \brief Return true iff the given constant name is marked as reducible in env() */

179
src/library/blast/branch.cpp
View file

@ -1,179 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <algorithm>
#include "kernel/for_each_fn.h"
#include "library/replace_visitor.h"
#include "library/blast/branch.h"
namespace lean {
namespace blast {
struct hypothesis_depth_lt {
branch const & m_branch;
hypothesis_depth_lt(branch const & b): m_branch(b) {}
bool operator()(unsigned hidx1, unsigned hidx2) const {
hypothesis const * h1 = m_branch.get(hidx1);
hypothesis const * h2 = m_branch.get(hidx2);
return h1 && h2 && h1->get_depth() < h2->get_depth() && (h1->get_depth() == h2->get_depth() && hidx1 < hidx2);
}
};
void branch::get_sorted_hypotheses(hypothesis_idx_buffer & r) const {
m_context.for_each([&](unsigned hidx, hypothesis const &) {
r.push_back(hidx);
});
std::sort(r.begin(), r.end(), hypothesis_depth_lt(*this));
}
void branch::add_forward_dep(unsigned hidx_user, unsigned hidx_provider) {
if (auto s = m_forward_deps.find(hidx_provider)) {
if (!s->contains(hidx_user)) {
hypothesis_idx_set new_s(*s);
new_s.insert(hidx_user);
m_forward_deps.insert(hidx_provider, new_s);
}
} else {
hypothesis_idx_set new_s;
new_s.insert(hidx_user);
m_forward_deps.insert(hidx_provider, new_s);
}
}
void branch::add_deps(expr const & e, hypothesis & h_user, unsigned hidx_user) {
if (!has_href(e) && !has_mref(e))
return; // nothing to be done
for_each(e, [&](expr const & l, unsigned) {
if (!has_href(l) && !has_mref(l)) {
return false;
} else if (is_href(l)) {
unsigned hidx_provider = href_index(l);
hypothesis const * h_provider = get(hidx_provider);
lean_assert(h_provider);
if (h_user.m_depth <= h_provider->m_depth)
h_user.m_depth = h_provider->m_depth + 1;
if (!h_user.m_deps.contains(hidx_provider)) {
h_user.m_deps.insert(hidx_provider);
add_forward_dep(hidx_user, hidx_provider);
}
return false;
} else if (is_mref(l)) {
m_mvar_idxs.insert(mref_index(l));
return false;
} else {
return true;
}
});
}
void branch::add_deps(hypothesis & h_user, unsigned hidx_user) {
add_deps(h_user.m_type, h_user, hidx_user);
if (!is_local_non_href(h_user.m_value)) {
add_deps(h_user.m_value, h_user, hidx_user);
}
}
double branch::compute_weight(unsigned hidx, expr const & /* type */) {
// TODO(Leo): use heuristics and machine learning for computing the weight of a new hypothesis
return 1.0 / (static_cast<double>(hidx) + 1.0);
}
expr branch::add_hypothesis(unsigned new_hidx, name const & n, expr const & type, expr const & value) {
hypothesis new_h;
new_h.m_name = n;
new_h.m_type = type;
new_h.m_value = value;
add_deps(new_h, new_hidx);
m_context.insert(new_hidx, new_h);
if (new_h.is_assumption())
m_assumption.insert(new_hidx);
double w = compute_weight(new_hidx, type);
m_todo_queue.insert(w, new_hidx);
return blast::mk_href(new_hidx);
}
static name * g_prefix = nullptr;
expr branch::add_hypothesis(name const & n, expr const & type, expr const & value) {
return add_hypothesis(mk_href_idx(), n, type, value);
}
expr branch::add_hypothesis(expr const & type, expr const & value) {
unsigned hidx = mk_href_idx();
return add_hypothesis(hidx, name(*g_prefix, hidx), type, value);
}
void branch::update_indices(unsigned /* hidx */) {
// TODO(Leo): we need to update the indexing data-structures and send
// the hypothesis if to the congruence closure module after it is implemented.
}
optional<unsigned> branch::activate_hypothesis() {
if (m_todo_queue.empty()) {
return optional<unsigned>();
} else {
unsigned hidx = m_todo_queue.erase_min();
m_active.insert(hidx);
update_indices(hidx);
return optional<unsigned>(hidx);
}
}
bool branch::hidx_depends_on(unsigned hidx_user, unsigned hidx_provider) const {
if (auto s = m_forward_deps.find(hidx_provider)) {
return s->contains(hidx_user);
} else {
return false;
}
}
void branch::set_target(expr const & t) {
m_target = t;
m_target_deps.clear();
if (has_href(t) || has_mref(t)) {
for_each(t, [&](expr const & e, unsigned) {
if (!has_href(e) && !has_mref(e)) {
return false;
} else if (is_href(e)) {
m_target_deps.insert(href_index(e));
return false;
} else if (is_mref(e)) {
m_mvar_idxs.insert(mref_index(e));
return false;
} else {
return true;
}
});
}
}
struct expand_hrefs_fn : public replace_visitor {
branch const & m_branch;
list<expr> const & m_hrefs;
expand_hrefs_fn(branch const & b, list<expr> const & hrefs):
m_branch(b), m_hrefs(hrefs) {}
virtual expr visit_local(expr const & e) {
if (is_href(e) && std::find(m_hrefs.begin(), m_hrefs.end(), e) != m_hrefs.end()) {
return visit(m_branch.get(e)->get_value());
} else {
return replace_visitor::visit_local(e);
}
}
};
expr branch::expand_hrefs(expr const & e, list<expr> const & hrefs) const {
return expand_hrefs_fn(*this, hrefs)(e);
}
void initialize_branch() {
g_prefix = new name(name::mk_internal_unique_name());
}
void finalize_branch() {
delete g_prefix;
}
}}

105
src/library/blast/branch.h
View file

@ -1,105 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "util/rb_map.h"
#include "library/blast/expr.h"
#include "library/blast/hypothesis.h"
namespace lean {
namespace blast {
typedef rb_tree<unsigned, unsigned_cmp> metavar_idx_set;
typedef hypothesis_idx_map<hypothesis> context;
template<typename T>
using metavar_idx_map = typename lean::rb_map<unsigned, T, unsigned_cmp>;
class branch {
typedef hypothesis_idx_map<hypothesis_idx_set> forward_deps;
typedef rb_map<double, unsigned, double_cmp> todo_queue;
friend class state;
context m_context;
// We break the set of hypotheses in m_context in 3 sets that are not necessarily disjoint:
// - assumption
// - active
// - todo
//
// The sets active and todo are disjoint.
//
// A hypothesis is an "assumption" if it comes from the input goal,
// "intros" proof step, or an assumption obtained when applying an elimination step.
//
// A hypothesis is derived when it is obtained by forward chaining.
// A derived hypothesis can be in the to-do or active sets.
//
// We say a hypothesis is in the to-do set when the blast haven't process it yet.
hypothesis_idx_set m_assumption;
hypothesis_idx_set m_active;
todo_queue m_todo_queue;
forward_deps m_forward_deps; // given an entry (h -> {h_1, ..., h_n}), we have that each h_i uses h.
expr m_target;
hypothesis_idx_set m_target_deps;
metavar_idx_set m_mvar_idxs;
void add_forward_dep(unsigned hidx_user, unsigned hidx_provider);
void add_deps(expr const & e, hypothesis & h_user, unsigned hidx_user);
void add_deps(hypothesis & h_user, unsigned hidx_user);
/** \brief Compute the weight of a hypothesis with the given type
We use this weight to update the todo_queue. */
double compute_weight(unsigned hidx, expr const & type);
/** \brief This method is invoked when a hypothesis move from todo to active.
We will update indices and data-structures (e.g., congruence closure). */
void update_indices(unsigned hidx);
expr add_hypothesis(unsigned new_hidx, name const & n, expr const & type, expr const & value);
public:
branch() {}
expr add_hypothesis(name const & n, expr const & type, expr const & value);
expr add_hypothesis(expr const & type, expr const & value);
/** \brief Return true iff the hypothesis with index \c hidx_user depends on the hypothesis with index
\c hidx_provider. */
bool hidx_depends_on(unsigned hidx_user, unsigned hidx_provider) const;
hypothesis const * get(unsigned hidx) const { return m_context.find(hidx); }
hypothesis const * get(expr const & h) const {
lean_assert(is_href(h));
return get(href_index(h));
}
void for_each_hypothesis(std::function<void(unsigned, hypothesis const &)> const & fn) const { m_context.for_each(fn); }
optional<unsigned> find_active_hypothesis(std::function<bool(unsigned, hypothesis const &)> const & fn) const { // NOLINT
return m_active.find_if([&](unsigned hidx) {
return fn(hidx, *get(hidx));
});
}
/** \brief Activate the next hypothesis in the TODO queue, return none if the TODO queue is empty. */
optional<unsigned> activate_hypothesis();
/** \brief Store in \c r the hypotheses in this branch sorted by depth */
void get_sorted_hypotheses(hypothesis_idx_buffer & r) const;
void set_target(expr const & t);
expr const & get_target() const { return m_target; }
/** \brief Return true iff the target depends on the given hypothesis */
bool target_depends_on(expr const & h) const { return m_target_deps.contains(href_index(h)); }
bool has_mvar(expr const & e) const { return m_mvar_idxs.contains(mref_index(e)); }
expr expand_hrefs(expr const & e, list<expr> const & hrefs) const;
hypothesis_idx_set get_assumptions() const { return m_assumption; }
};
void initialize_branch();
void finalize_branch();
}}

2
src/library/blast/hypothesis.h
View file

@ -22,7 +22,7 @@ template<typename T>
using hypothesis_idx_map = typename lean::rb_map<unsigned, T, unsigned_cmp>;
class hypothesis {
friend class branch;
friend class state;
name m_name; // for pretty printing
unsigned m_active:1;
unsigned m_depth;

6
src/library/blast/init_module.cpp
View file

@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "library/blast/expr.h"
#include "library/blast/branch.h"
#include "library/blast/state.h"
#include "library/blast/blast.h"
#include "library/blast/blast_tactic.h"
#include "library/blast/simplifier.h"
@ -13,7 +13,7 @@ Author: Leonardo de Moura
namespace lean {
void initialize_blast_module() {
blast::initialize_expr();
blast::initialize_branch();
blast::initialize_state();
initialize_blast();
blast::initialize_simplifier();
initialize_blast_tactic();
@ -22,7 +22,7 @@ void finalize_blast_module() {
finalize_blast_tactic();
blast::finalize_simplifier();
finalize_blast();
blast::finalize_branch();
blast::finalize_state();
blast::finalize_expr();
}
}

9
src/library/blast/intros.cpp
View file

@ -21,28 +21,27 @@ public:
virtual optional<expr> resolve(state & s, expr const & pr) {
buffer<expr> locals;
to_buffer(m_new_locals, locals);
expr new_pr = Fun(locals, s.get_main_branch().expand_hrefs(pr, m_new_hs));
expr new_pr = Fun(locals, s.expand_hrefs(pr, m_new_hs));
return some_expr(new_pr);
}
};
bool intros_action() {
state & s = curr_state();
branch & b = s.get_main_branch();
expr target = whnf(b.get_target());
expr target = whnf(s.get_target());
if (!is_pi(target))
return false;
buffer<expr> new_hs;
buffer<expr> new_locals;
while (is_pi(target)) {
expr local = mk_fresh_local(binding_domain(target));
expr href = b.add_hypothesis(binding_name(target), binding_domain(target), local);
expr href = s.add_hypothesis(binding_name(target), binding_domain(target), local);
new_hs.push_back(href);
new_locals.push_back(local);
target = whnf(instantiate(binding_body(target), href));
}
s.push_proof_step(proof_step(new intros_proof_step_cell(to_list(new_hs), to_list(new_locals))));
b.set_target(target);
s.set_target(target);
return true;
}
}}

11
src/library/blast/simplifier.cpp
View file

@ -93,7 +93,6 @@ bool get_simplify_trace() {
class simplifier {
blast_tmp_type_context m_tmp_tctx;
app_builder m_app_builder;
branch m_branch;
name m_rel;
simp_rule_sets m_ctx_srss;
@ -166,14 +165,14 @@ class simplifier {
result try_congr(expr const & e, congr_rule const & cr);
public:
simplifier(branch const & b, name const & rel);
simplifier(name const & rel);
result operator()(expr const & e) { return simplify(e); }
};
/* Constructor */
simplifier::simplifier(branch const & b, name const & rel):
m_app_builder(*m_tmp_tctx), m_branch(b), m_rel(rel) { }
simplifier::simplifier(name const & rel):
m_app_builder(*m_tmp_tctx), m_rel(rel) { }
/* Cache */
@ -684,8 +683,8 @@ void finalize_simplifier() {
/* Entry point */
result simplify(branch const & b, name const & rel, expr const & e) {
return simplifier(b, rel)(e);
result simplify(name const & rel, expr const & e) {
return simplifier(rel)(e);
}
}}

4
src/library/blast/simplifier.h
View file

@ -5,7 +5,7 @@ Author: Daniel Selsam
*/
#pragma once
#include "kernel/expr_pair.h"
#include "library/blast/branch.h"
#include "library/blast/state.h"
namespace lean {
namespace blast {
@ -33,7 +33,7 @@ public:
}
simp::result simplify(branch const & b, name const & rel, expr const & e);
simp::result simplify(name const & rel, expr const & e);
void initialize_simplifier();
void finalize_simplifier();

217
src/library/blast/state.cpp
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <algorithm>
#include "kernel/instantiate.h"
#include "kernel/abstract.h"
#include "kernel/for_each_fn.h"
@ -13,6 +14,8 @@ Author: Leonardo de Moura
namespace lean {
namespace blast {
static name * g_prefix = nullptr;
bool metavar_decl::restrict_context_using(metavar_decl const & other) {
buffer<unsigned> to_erase;
m_assumptions.for_each([&](unsigned hidx) {
@ -66,7 +69,7 @@ expr state::mk_metavar(hypothesis_idx_buffer const & b, expr const & type) {
}
expr state::mk_metavar(expr const & type) {
return state::mk_metavar(m_main.get_assumptions(), type);
return state::mk_metavar(get_assumptions(), type);
}
void state::restrict_mref_context_using(expr const & mref1, expr const & mref2) {
@ -79,7 +82,7 @@ void state::restrict_mref_context_using(expr const & mref1, expr const & mref2)
m_metavar_decls.insert(mref_index(mref1), new_d1);
}
goal state::to_goal(branch const & b) const {
goal state::to_goal() const {
hypothesis_idx_map<expr> hidx2local;
metavar_idx_map<expr> midx2meta;
name M("M");
@ -114,27 +117,23 @@ goal state::to_goal(branch const & b) const {
};
name H("H");
hypothesis_idx_buffer hidxs;
b.get_sorted_hypotheses(hidxs);
get_sorted_hypotheses(hidxs);
buffer<expr> hyps;
for (unsigned hidx : hidxs) {
hypothesis const * h = b.get(hidx);
hypothesis const * h = get(hidx);
lean_assert(h);
// after we add support for let-decls in goals, we must convert back h->get_value() if it is available
expr new_h = lean::mk_local(name(H, hidx), h->get_name(), convert(h->get_type()), binder_info());
hidx2local.insert(hidx, new_h);
hyps.push_back(new_h);
}
expr new_target = convert(b.get_target());
expr new_target = convert(get_target());
expr new_mvar_type = Pi(hyps, new_target);
expr new_mvar = lean::mk_metavar(M, new_mvar_type);
expr new_meta = mk_app(new_mvar, hyps);
return goal(new_meta, new_target);
}
goal state::to_goal() const {
return to_goal(m_main);
}
void state::display(environment const & env, io_state const & ios) const {
formatter fmt = ios.get_formatter_factory()(env, ios.get_options());
ios.get_diagnostic_channel() << mk_pair(to_goal().pp(fmt), ios.get_options());
@ -312,51 +311,211 @@ expr state::instantiate_urefs_mrefs(expr const & e) {
}
#ifdef LEAN_DEBUG
bool state::check_hypothesis(expr const & e, branch const & b, unsigned hidx, hypothesis const & h) const {
bool state::check_hypothesis(expr const & e, unsigned hidx, hypothesis const & h) const {
lean_assert(closed(e));
for_each(e, [&](expr const & n, unsigned) {
if (is_href(n)) {
lean_assert(h.depends_on(n));
lean_assert(b.hidx_depends_on(hidx, href_index(n)));
lean_assert(hidx_depends_on(hidx, href_index(n)));
} else if (is_mref(n)) {
// metavariable is in the set of used metavariables
lean_assert(b.has_mvar(n));
lean_assert(has_mvar(n));
}
return true;
});
return true;
}
bool state::check_hypothesis(branch const & b, unsigned hidx, hypothesis const & h) const {
lean_assert(check_hypothesis(h.get_type(), b, hidx, h));
lean_assert(h.is_assumption() || check_hypothesis(h.get_value(), b, hidx, h));
bool state::check_hypothesis(unsigned hidx, hypothesis const & h) const {
lean_assert(check_hypothesis(h.get_type(), hidx, h));
lean_assert(h.is_assumption() || check_hypothesis(h.get_value(), hidx, h));
return true;
}
bool state::check_target(branch const & b) const {
lean_assert(closed(b.get_target()));
for_each(b.get_target(), [&](expr const & n, unsigned) {
bool state::check_target() const {
lean_assert(closed(get_target()));
for_each(get_target(), [&](expr const & n, unsigned) {
if (is_href(n)) {
lean_assert(b.target_depends_on(n));
lean_assert(target_depends_on(n));
} else if (is_mref(n)) {
// metavariable is in the set of used metavariables
lean_assert(b.has_mvar(n));
lean_assert(has_mvar(n));
}
return true;
});
return true;
}
bool state::check_invariant(branch const & b) const {
b.for_each_hypothesis([&](unsigned hidx, hypothesis const & h) {
lean_assert(check_hypothesis(b, hidx, h));
});
lean_assert(check_target(b));
return true;
}
bool state::check_invariant() const {
return check_invariant(m_main);
for_each_hypothesis([&](unsigned hidx, hypothesis const & h) {
lean_assert(check_hypothesis(b, hidx, h));
});
lean_assert(check_target());
return true;
}
#endif
struct hypothesis_depth_lt {
state const & m_state;
hypothesis_depth_lt(state const & s): m_state(s) {}
bool operator()(unsigned hidx1, unsigned hidx2) const {
hypothesis const * h1 = m_state.get(hidx1);
hypothesis const * h2 = m_state.get(hidx2);
return h1 && h2 && h1->get_depth() < h2->get_depth() && (h1->get_depth() == h2->get_depth() && hidx1 < hidx2);
}
};
void state::get_sorted_hypotheses(hypothesis_idx_buffer & r) const {
m_context.for_each([&](unsigned hidx, hypothesis const &) {
r.push_back(hidx);
});
std::sort(r.begin(), r.end(), hypothesis_depth_lt(*this));
}
void state::add_forward_dep(unsigned hidx_user, unsigned hidx_provider) {
if (auto s = m_forward_deps.find(hidx_provider)) {
if (!s->contains(hidx_user)) {
hypothesis_idx_set new_s(*s);
new_s.insert(hidx_user);
m_forward_deps.insert(hidx_provider, new_s);
}
} else {
hypothesis_idx_set new_s;
new_s.insert(hidx_user);
m_forward_deps.insert(hidx_provider, new_s);
}
}
void state::add_deps(expr const & e, hypothesis & h_user, unsigned hidx_user) {
if (!has_href(e) && !has_mref(e))
return; // nothing to be done
for_each(e, [&](expr const & l, unsigned) {
if (!has_href(l) && !has_mref(l)) {
return false;
} else if (is_href(l)) {
unsigned hidx_provider = href_index(l);
hypothesis const * h_provider = get(hidx_provider);
lean_assert(h_provider);
if (h_user.m_depth <= h_provider->m_depth)
h_user.m_depth = h_provider->m_depth + 1;
if (!h_user.m_deps.contains(hidx_provider)) {
h_user.m_deps.insert(hidx_provider);
add_forward_dep(hidx_user, hidx_provider);
}
return false;
} else if (is_mref(l)) {
m_mvar_idxs.insert(mref_index(l));
return false;
} else {
return true;
}
});
}
void state::add_deps(hypothesis & h_user, unsigned hidx_user) {
add_deps(h_user.m_type, h_user, hidx_user);
if (!is_local_non_href(h_user.m_value)) {
add_deps(h_user.m_value, h_user, hidx_user);
}
}
double state::compute_weight(unsigned hidx, expr const & /* type */) {
// TODO(Leo): use heuristics and machine learning for computing the weight of a new hypothesis
return 1.0 / (static_cast<double>(hidx) + 1.0);
}
expr state::add_hypothesis(unsigned new_hidx, name const & n, expr const & type, expr const & value) {
hypothesis new_h;
new_h.m_name = n;
new_h.m_type = type;
new_h.m_value = value;
add_deps(new_h, new_hidx);
m_context.insert(new_hidx, new_h);
if (new_h.is_assumption())
m_assumption.insert(new_hidx);
double w = compute_weight(new_hidx, type);
m_todo_queue.insert(w, new_hidx);
return blast::mk_href(new_hidx);
}
expr state::add_hypothesis(name const & n, expr const & type, expr const & value) {
return add_hypothesis(mk_href_idx(), n, type, value);
}
expr state::add_hypothesis(expr const & type, expr const & value) {
unsigned hidx = mk_href_idx();
return add_hypothesis(hidx, name(*g_prefix, hidx), type, value);
}
void state::update_indices(unsigned /* hidx */) {
// TODO(Leo): we need to update the indexing data-structures and send
// the hypothesis if to the congruence closure module after it is implemented.
}
optional<unsigned> state::activate_hypothesis() {
if (m_todo_queue.empty()) {
return optional<unsigned>();
} else {
unsigned hidx = m_todo_queue.erase_min();
m_active.insert(hidx);
update_indices(hidx);
return optional<unsigned>(hidx);
}
}
bool state::hidx_depends_on(unsigned hidx_user, unsigned hidx_provider) const {
if (auto s = m_forward_deps.find(hidx_provider)) {
return s->contains(hidx_user);
} else {
return false;
}
}
void state::set_target(expr const & t) {
m_target = t;
m_target_deps.clear();
if (has_href(t) || has_mref(t)) {
for_each(t, [&](expr const & e, unsigned) {
if (!has_href(e) && !has_mref(e)) {
return false;
} else if (is_href(e)) {
m_target_deps.insert(href_index(e));
return false;
} else if (is_mref(e)) {
m_mvar_idxs.insert(mref_index(e));
return false;
} else {
return true;
}
});
}
}
struct expand_hrefs_fn : public replace_visitor {
state const & m_state;
list<expr> const & m_hrefs;
expand_hrefs_fn(state const & s, list<expr> const & hrefs):
m_state(s), m_hrefs(hrefs) {}
virtual expr visit_local(expr const & e) {
if (is_href(e) && std::find(m_hrefs.begin(), m_hrefs.end(), e) != m_hrefs.end()) {
return visit(m_state.get(e)->get_value());
} else {
return replace_visitor::visit_local(e);
}
}
};
expr state::expand_hrefs(expr const & e, list<expr> const & hrefs) const {
return expand_hrefs_fn(*this, hrefs)(e);
}
void initialize_state() {
g_prefix = new name(name::mk_internal_unique_name());
}
void finalize_state() {
delete g_prefix;
}
}}

107
src/library/blast/state.h
View file

@ -9,10 +9,15 @@ Author: Leonardo de Moura
#include "kernel/expr.h"
#include "library/tactic/goal.h"
#include "library/blast/hypothesis.h"
#include "library/blast/branch.h"
namespace lean {
namespace blast {
typedef rb_tree<unsigned, unsigned_cmp> metavar_idx_set;
typedef hypothesis_idx_map<hypothesis> context;
template<typename T>
using metavar_idx_map = typename lean::rb_map<unsigned, T, unsigned_cmp>;
class metavar_decl {
// A metavariable can be assigned to a value that contains references only to the assumptions
// that were available when the metavariable was defined.
@ -63,6 +68,8 @@ public:
};
class state {
typedef hypothesis_idx_map<hypothesis_idx_set> forward_deps;
typedef rb_map<double, unsigned, double_cmp> todo_queue;
typedef metavar_idx_map<metavar_decl> metavar_decls;
typedef metavar_idx_map<expr> eassignment;
typedef metavar_idx_map<level> uassignment;
@ -71,7 +78,6 @@ class state {
uassignment m_uassignment;
metavar_decls m_metavar_decls;
eassignment m_eassignment;
branch m_main;
// In the following mapping, each entry (h -> {m_1 ... m_n}) means that hypothesis `h` cannot be cleared
// in any branch where the metavariables m_1 ... m_n have not been replaced with the values assigned to them.
// That is, to be able to clear `h` in a branch `B`, we first need to check whether it
@ -83,16 +89,54 @@ class state {
fixed_by m_fixed_by;
unsigned m_depth{0};
proof_steps m_proof_steps;
// Hypothesis/facts in the current state
context m_context;
// We break the set of hypotheses in m_context in 3 sets that are not necessarily disjoint:
// - assumption
// - active
// - todo
//
// The sets active and todo are disjoint.
//
// A hypothesis is an "assumption" if it comes from the input goal,
// "intros" proof step, or an assumption obtained when applying an elimination step.
//
// A hypothesis is derived when it is obtained by forward chaining.
// A derived hypothesis can be in the to-do or active sets.
//
// We say a hypothesis is in the to-do set when the blast haven't process it yet.
hypothesis_idx_set m_assumption;
hypothesis_idx_set m_active;
todo_queue m_todo_queue;
forward_deps m_forward_deps; // given an entry (h -> {h_1, ..., h_n}), we have that each h_i uses h.
expr m_target;
hypothesis_idx_set m_target_deps;
metavar_idx_set m_mvar_idxs;
void add_forward_dep(unsigned hidx_user, unsigned hidx_provider);
void add_deps(expr const & e, hypothesis & h_user, unsigned hidx_user);
void add_deps(hypothesis & h_user, unsigned hidx_user);
/** \brief Compute the weight of a hypothesis with the given type
We use this weight to update the todo_queue. */
double compute_weight(unsigned hidx, expr const & type);
/** \brief This method is invoked when a hypothesis move from todo to active.
We will update indices and data-structures (e.g., congruence closure). */
void update_indices(unsigned hidx);
expr add_hypothesis(unsigned new_hidx, name const & n, expr const & type, expr const & value);
void add_fixed_by(unsigned hidx, unsigned midx);
unsigned add_metavar_decl(metavar_decl const & decl);
goal to_goal(branch const &) const;
#ifdef LEAN_DEBUG
bool check_hypothesis(expr const & e, branch const & b, unsigned hidx, hypothesis const & h) const;
bool check_hypothesis(branch const & b, unsigned hidx, hypothesis const & h) const;
bool check_target(branch const & b) const;
bool check_invariant(branch const &) const;
bool check_hypothesis(expr const & e, unsigned hidx, hypothesis const & h) const;
bool check_hypothesis(unsigned hidx, hypothesis const & h) const;
bool check_target() const;
#endif
public:
state();
@ -154,29 +198,48 @@ public:
\remark This is not a const method because it may normalize the assignment. */
expr instantiate_urefs_mrefs(expr const & e);
/** \brief Add a new hypothesis to the main branch */
expr add_hypothesis(name const & n, expr const & type, expr const & value) {
return m_main.add_hypothesis(n, type, value);
expr add_hypothesis(name const & n, expr const & type, expr const & value);
expr add_hypothesis(expr const & type, expr const & value);
/** \brief Return true iff the hypothesis with index \c hidx_user depends on the hypothesis with index
\c hidx_provider. */
bool hidx_depends_on(unsigned hidx_user, unsigned hidx_provider) const;
hypothesis const * get(unsigned hidx) const { return m_context.find(hidx); }
hypothesis const * get(expr const & h) const {
lean_assert(is_href(h));
return get(href_index(h));
}
void for_each_hypothesis(std::function<void(unsigned, hypothesis const &)> const & fn) const { m_context.for_each(fn); }
optional<unsigned> find_active_hypothesis(std::function<bool(unsigned, hypothesis const &)> const & fn) const { // NOLINT
return m_active.find_if([&](unsigned hidx) {
return fn(hidx, *get(hidx));
});
}
branch & get_main_branch() { return m_main; }
branch const & get_main_branch() const { return m_main; }
/** \brief Activate the next hypothesis in the TODO queue, return none if the TODO queue is empty. */
optional<unsigned> activate_hypothesis();
/** \brief Add a new hypothesis to the main branch */
expr add_hypothesis(expr const & type, expr const & value) {
return m_main.add_hypothesis(type, value);
}
/** \brief Store in \c r the hypotheses in this branch sorted by depth */
void get_sorted_hypotheses(hypothesis_idx_buffer & r) const;
/** \brief Set target (aka conclusion, aka type of the goal, aka type of the term that must be synthesize in this branch)
of the main branch */
void set_target(expr const & type) {
return m_main.set_target(type);
}
/** \brief Set target (aka conclusion, aka type of the goal, aka type of the term that
must be synthesize in the current branch) */
void set_target(expr const & t);
expr const & get_target() const { return m_target; }
/** \brief Return true iff the target depends on the given hypothesis */
bool target_depends_on(expr const & h) const { return m_target_deps.contains(href_index(h)); }
bool has_mvar(expr const & e) const { return m_mvar_idxs.contains(mref_index(e)); }
expr expand_hrefs(expr const & e, list<expr> const & hrefs) const;
hypothesis_idx_set get_assumptions() const { return m_assumption; }
metavar_decl const * get_metavar_decl(unsigned idx) const { return m_metavar_decls.find(idx); }
metavar_decl const * get_metavar_decl(expr const & e) const { return get_metavar_decl(mref_index(e)); }
/** \brief Convert main branch to a goal.
/** \brief Convert current branch into a goal.
This is mainly used for pretty printing. However, in the future, we may use this capability
to invoke the tactic framework from the blast tactic. */
goal to_goal() const;
@ -225,4 +288,6 @@ public:
bool check_invariant() const;
#endif
};
void initialize_state();
void finalize_state();
}}