From c626e2e3c6f3771e07c32e82ee5b9e030de5b050 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 4 Oct 2015 21:59:37 -0700 Subject: [PATCH] refactor(library/blast): divide hypotheses in: assumption, active and todo The sets active and todo are disjoint. A metavariable declaration can only depend on assumptions. --- src/library/blast/branch.cpp | 3 +++ src/library/blast/branch.h | 21 ++++++++++++++++++++- src/library/blast/state.cpp | 33 +++++++++++++++------------------ src/library/blast/state.h | 20 +++++++++++--------- 4 files changed, 49 insertions(+), 28 deletions(-) diff --git a/src/library/blast/branch.cpp b/src/library/blast/branch.cpp index 722174624..5dd640635 100644 --- a/src/library/blast/branch.cpp +++ b/src/library/blast/branch.cpp @@ -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); } diff --git a/src/library/blast/branch.h b/src/library/blast/branch.h index f7948e727..dbe944930 100644 --- a/src/library/blast/branch.h +++ b/src/library/blast/branch.h @@ -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(); diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index 1d3bcb369..89da3cb6e 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -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 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 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()); diff --git a/src/library/blast/state.h b/src/library/blast/state.h index db51e131e..13feda3c6 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -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