diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index 9ea7991a7..9ad5fe134 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -22,7 +22,7 @@ namespace lean { namespace blast { static name * g_prefix = nullptr; -class context { +class blastenv { environment m_env; io_state m_ios; name_set m_lemma_hints; @@ -227,7 +227,7 @@ class context { } public: - context(environment const & env, io_state const & ios, list const & ls, list const & ds): + blastenv(environment const & env, io_state const & ios, list const & ls, list const & ds): m_env(env), m_ios(ios), m_lemma_hints(to_name_set(ls)), m_unfold_hints(to_name_set(ds)), m_not_reducible_pred(mk_not_reducible_pred(env)) { } @@ -236,7 +236,7 @@ public: m_curr_state = to_state(g); // TODO(Leo): blast main loop - display("Blast tactic initial state"); + display("Blast tactic initial state\n"); display_curr_state(); return none_expr(); @@ -259,37 +259,37 @@ public: } }; -LEAN_THREAD_PTR(context, g_context); -struct scope_context { - context * m_prev_context; +LEAN_THREAD_PTR(blastenv, g_blastenv); +struct scope_blastenv { + blastenv * m_prev_blastenv; public: - scope_context(context & c):m_prev_context(g_context) { g_context = &c; } - ~scope_context() { g_context = m_prev_context; } + scope_blastenv(blastenv & c):m_prev_blastenv(g_blastenv) { g_blastenv = &c; } + ~scope_blastenv() { g_blastenv = m_prev_blastenv; } }; environment const & env() { - lean_assert(g_context); - return g_context->get_env(); + lean_assert(g_blastenv); + return g_blastenv->get_env(); } io_state const & ios() { - lean_assert(g_context); - return g_context->get_ios(); + lean_assert(g_blastenv); + return g_blastenv->get_ios(); } state & curr_state() { - lean_assert(g_context); - return g_context->get_curr_state(); + lean_assert(g_blastenv); + return g_blastenv->get_curr_state(); } bool is_reducible(name const & n) { - lean_assert(g_context); - return g_context->is_reducible(n); + lean_assert(g_blastenv); + return g_blastenv->is_reducible(n); } projection_info const * get_projection_info(name const & n) { - lean_assert(g_context); - return g_context->get_projection_info(n); + lean_assert(g_blastenv); + return g_blastenv->get_projection_info(n); } void display_curr_state() { @@ -353,11 +353,11 @@ name mk_fresh_local_name() { optional blast_goal(environment const & env, io_state const & ios, list const & ls, list const & ds, goal const & g) { blast::scope_hash_consing scope1; - blast::context c(env, ios, ls, ds); + blast::blastenv b(env, ios, ls, ds); blast::ext_context x; - blast::scope_context scope2(c); + blast::scope_blastenv scope2(b); blast::scope_ext_context scope3(x); - return c(g); + return b(g); } void initialize_blast() { blast::g_prefix = new name(name::mk_internal_unique_name()); diff --git a/src/library/blast/branch.h b/src/library/blast/branch.h index 8c6bc8f60..d7be58594 100644 --- a/src/library/blast/branch.h +++ b/src/library/blast/branch.h @@ -12,11 +12,12 @@ Author: Leonardo de Moura namespace lean { namespace blast { typedef rb_tree metavar_idx_set; +typedef hypothesis_idx_map context; + template using metavar_idx_map = typename lean::rb_map; class branch { - typedef hypothesis_idx_map context; typedef hypothesis_idx_map forward_deps; friend class state; unsigned m_next; diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index 879d4583f..0ddcb7a63 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -14,18 +14,13 @@ Author: Leonardo de Moura namespace lean { namespace blast { bool metavar_decl::restrict_context_using(metavar_decl const & other) { - buffer new_ctx; bool modified = false; - for (unsigned href : m_context) { - if (other.m_context_as_set.contains(href)) { - new_ctx.push_back(href); - } else { - modified = true; - m_context_as_set.erase(href); - } - } - if (modified) - m_context = to_list(new_ctx); + m_context.for_each([&](unsigned hidx, hypothesis const &) { + if (!other.contains_href(hidx)) { + modified = true; + m_context.erase(hidx); + } + }); return modified; } @@ -53,30 +48,35 @@ level state::mk_uref() { return blast::mk_uref(idx); } -expr state::mk_metavar(hypothesis_idx_buffer const & ctx, expr const & type) { - hypothesis_idx_set ctx_as_set; - for (unsigned const & hidx : ctx) - ctx_as_set.insert(hidx); +expr state::mk_metavar(context const & ctx, 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_as_set.contains(href_index(e))); + lean_assert(ctx.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(to_list(ctx), ctx_as_set, type)); + m_metavar_decls.insert(midx, metavar_decl(ctx, 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); + } + return mk_metavar(ctx, type); +} + expr state::mk_metavar(expr const & type) { - hypothesis_idx_buffer ctx; - m_main.get_sorted_hypotheses(ctx); - return state::mk_metavar(ctx, type); + return state::mk_metavar(m_main.m_context, type); } void state::restrict_mref_context_using(expr const & mref1, expr const & mref2) { @@ -107,9 +107,9 @@ goal state::to_goal(branch const & b) const { metavar_decl const * decl = m_metavar_decls.find(mref_index(e)); lean_assert(decl); buffer ctx; - for (unsigned hidx : decl->get_context()) { - ctx.push_back(*hidx2local.find(hidx)); - } + decl->get_context().for_each([&](unsigned hidx, hypothesis const &) { + ctx.push_back(*hidx2local.find(hidx)); + }); expr type = convert(decl->get_type()); expr new_type = Pi(ctx, type); expr new_mvar = lean::mk_metavar(name(M, mref_index(e)), new_type); diff --git a/src/library/blast/state.h b/src/library/blast/state.h index afa731aab..09e3908fc 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -14,18 +14,16 @@ Author: Leonardo de Moura namespace lean { namespace blast { class metavar_decl { - hypothesis_idx_list m_context; - hypothesis_idx_set m_context_as_set; - expr m_type; + context m_context; + expr m_type; public: metavar_decl() {} - metavar_decl(hypothesis_idx_list const & c, hypothesis_idx_set const & s, expr const & t): - m_context(c), m_context_as_set(s), m_type(t) {} - hypothesis_idx_list get_context() const { return m_context; } + metavar_decl(context const & c, expr const & t): + m_context(c), m_type(t) {} + context get_context() const { return m_context; } /** \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_as_set.contains(href_index(h)); - } + 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); } 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. */ @@ -33,7 +31,6 @@ public: }; class state { - friend class context; typedef metavar_idx_map metavar_decls; typedef metavar_idx_map eassignment; typedef metavar_idx_map uassignment; @@ -92,7 +89,8 @@ 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); - /** \brief Create a new metavariable using the given type. + expr mk_metavar(context 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. */ expr mk_metavar(expr const & type);