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

refactor(library/blast): divide hypotheses in: assumption, active and todo

Browse source 
The sets active and todo are disjoint.

A metavariable declaration can only depend on assumptions.
This commit is contained in:
Leonardo de Moura 2015-10-04 21:59:37 -07:00
parent 44881552b4
commit c626e2e3c6
4 changed files with 49 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -83,6 +83,9 @@ expr branch::add_hypothesis(name const & n, expr const & type, expr const & valu
m_next++;
add_deps(new_h, new_hidx);
m_context.insert(new_hidx, new_h);
if (new_h.is_assumption())
m_assumption.insert(new_hidx);
m_todo.insert(new_hidx);
return blast::mk_href(new_hidx);
}

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

@ -22,6 +22,24 @@ class branch {
friend class state;
unsigned m_next;
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;
hypothesis_idx_set m_todo;
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;
@ -30,7 +48,6 @@ class branch {
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);
public:
branch():m_next(0) {}
@ -56,6 +73,8 @@ public:
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)); }
hypothesis_idx_set get_assumptions() const { return m_assumption; }
};
void initialize_branch();

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

@ -14,14 +14,14 @@ Author: Leonardo de Moura
namespace lean {
namespace blast {
bool metavar_decl::restrict_context_using(metavar_decl const & other) {
bool modified = false;
m_context.for_each([&](unsigned hidx, hypothesis const &) {
if (!other.contains_href(hidx)) {
modified = true;
m_context.erase(hidx);
}
buffer<unsigned> to_erase;
m_assumptions.for_each([&](unsigned hidx) {
if (!other.contains_href(hidx))
to_erase.push_back(hidx);
});
return modified;
for (unsigned hidx : to_erase)
m_assumptions.erase(hidx);
return !to_erase.empty();
}
state::state():m_next_uref_index(0), m_next_mref_index(0) {}
@ -48,35 +48,32 @@ level state::mk_uref() {
return blast::mk_uref(idx);
}
expr state::mk_metavar(context const & ctx, expr const & type) {
expr state::mk_metavar(hypothesis_idx_set const & c, expr const & type) {
unsigned midx = m_next_mref_index;
for_each(type, [&](expr const & e, unsigned) {
if (!has_href(e))
return false;
if (is_href(e)) {
lean_assert(ctx.contains(href_index(e)));
lean_assert(c.contains(href_index(e)));
add_fixed_by(href_index(e), midx);
return false;
}
return true; // continue search
});
m_next_mref_index++;
m_metavar_decls.insert(midx, metavar_decl(ctx, type));
m_metavar_decls.insert(midx, metavar_decl(c, type));
return blast::mk_mref(midx);
}
expr state::mk_metavar(hypothesis_idx_buffer const & b, expr const & type) {
context ctx;
for (unsigned const & hidx : b) {
hypothesis const * h = m_main.get(hidx);
lean_assert(h);
ctx.insert(hidx, *h);
}
hypothesis_idx_set ctx;
for (unsigned const & hidx : b)
ctx.insert(hidx);
return mk_metavar(ctx, type);
}
expr state::mk_metavar(expr const & type) {
return state::mk_metavar(m_main.m_context, type);
return state::mk_metavar(m_main.get_assumptions(), type);
}
void state::restrict_mref_context_using(expr const & mref1, expr const & mref2) {
@ -107,7 +104,7 @@ goal state::to_goal(branch const & b) const {
metavar_decl const * decl = m_metavar_decls.find(mref_index(e));
lean_assert(decl);
buffer<expr> ctx;
decl->get_context().for_each([&](unsigned hidx, hypothesis const &) {
decl->get_assumptions().for_each([&](unsigned hidx) {
ctx.push_back(*hidx2local.find(hidx));
});
expr type = convert(decl->get_type());

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

@ -14,20 +14,22 @@ Author: Leonardo de Moura
namespace lean {
namespace blast {
class metavar_decl {
context m_context;
expr m_type;
// A metavariable can be assigned to a value that contains references only to the assumptions
// that were available when the metavariable was defined.
hypothesis_idx_set m_assumptions;
expr m_type;
public:
metavar_decl() {}
metavar_decl(context const & c, expr const & t):
m_context(c), m_type(t) {}
context get_context() const { return m_context; }
metavar_decl(hypothesis_idx_set const & a, expr const & t):
m_assumptions(a), m_type(t) {}
/** \brief Return true iff \c h is in the context of the this metavar declaration */
bool contains_href(expr const & h) const { return m_context.contains(href_index(h)); }
bool contains_href(unsigned hidx) const { return m_context.contains(hidx); }
bool contains_href(unsigned hidx) const { return m_assumptions.contains(hidx); }
bool contains_href(expr const & h) const { return contains_href(href_index(h)); }
expr const & get_type() const { return m_type; }
/** \brief Make sure the declaration context of this declaration is a subset of \c other.
\remark Return true iff the context has been modified. */
bool restrict_context_using(metavar_decl const & other);
hypothesis_idx_set get_assumptions() const { return m_assumptions; }
};
class state {
@ -89,9 +91,9 @@ public:
/** \brief Create a new metavariable using the given type and context.
\pre ctx must be a subset of the hypotheses in the main branch. */
expr mk_metavar(hypothesis_idx_buffer const & ctx, expr const & type);
expr mk_metavar(context const & ctx, expr const & type);
expr mk_metavar(hypothesis_idx_set const & ctx, expr const & type);
/** \brief Create a new metavariable using the given type.
The context of this metavariable will be all hypotheses occurring in the main branch. */
The context of this metavariable will be all assumption hypotheses occurring in the main branch. */
expr mk_metavar(expr const & type);
/** \brief Make sure the metavariable declaration context of mref1 is a