feat(library/blast): simplify metavar_decl

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<name> const & ls, list<name> const & ds):
+    blastenv(environment const & env, io_state const & ios, list<name> const & ls, list<name> 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);
+LEAN_THREAD_PTR(blastenv, g_blastenv);
-struct scope_context {
+struct scope_blastenv {
-    context * m_prev_context;
+    blastenv * m_prev_blastenv;
 public:
-    scope_context(context & c):m_prev_context(g_context) { g_context = &c; }
+    scope_blastenv(blastenv & c):m_prev_blastenv(g_blastenv) { g_blastenv = &c; }
-    ~scope_context() { g_context = m_prev_context; }
+    ~scope_blastenv() { g_blastenv = m_prev_blastenv; }
 };
 
 environment const & env() {
-    lean_assert(g_context);
+    lean_assert(g_blastenv);
-    return g_context->get_env();
+    return g_blastenv->get_env();
 }
 
 io_state const & ios() {
-    lean_assert(g_context);
+    lean_assert(g_blastenv);
-    return g_context->get_ios();
+    return g_blastenv->get_ios();
 }
 
 state & curr_state() {
-    lean_assert(g_context);
+    lean_assert(g_blastenv);
-    return g_context->get_curr_state();
+    return g_blastenv->get_curr_state();
 }
 
 bool is_reducible(name const & n) {
-    lean_assert(g_context);
+    lean_assert(g_blastenv);
-    return g_context->is_reducible(n);
+    return g_blastenv->is_reducible(n);
 }
 
 projection_info const * get_projection_info(name const & n) {
-    lean_assert(g_context);
+    lean_assert(g_blastenv);
-    return g_context->get_projection_info(n);
+    return g_blastenv->get_projection_info(n);
 }
 
 void display_curr_state() {
@@ -353,11 +353,11 @@ name mk_fresh_local_name() {
 optional<expr> blast_goal(environment const & env, io_state const & ios, list<name> const & ls, list<name> 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());

src/library/blast/branch.h

@@ -12,11 +12,12 @@ Author: Leonardo de Moura
 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>         context;
     typedef hypothesis_idx_map<hypothesis_idx_set> forward_deps;
     friend class state;
     unsigned           m_next;

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<unsigned> new_ctx;
     bool modified = false;
-    for (unsigned href : m_context) {
+    m_context.for_each([&](unsigned hidx, hypothesis const &) {
-        if (other.m_context_as_set.contains(href)) {
+            if (!other.contains_href(hidx)) {
-            new_ctx.push_back(href);
+                modified = true;
-        } else {
+                m_context.erase(hidx);
-            modified = true;
+            }
-            m_context_as_set.erase(href);
+        });
-        }
-    }
-    if (modified)
-        m_context = to_list(new_ctx);
     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) {
+expr state::mk_metavar(context const & ctx, expr const & type) {
-    hypothesis_idx_set  ctx_as_set;
-    for (unsigned const & hidx : ctx)
-        ctx_as_set.insert(hidx);
     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;
+    return state::mk_metavar(m_main.m_context, type);
-    m_main.get_sorted_hypotheses(ctx);
-    return state::mk_metavar(ctx, 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<expr> ctx;
-                        for (unsigned hidx : decl->get_context()) {
+                        decl->get_context().for_each([&](unsigned hidx, hypothesis const &) {
-                            ctx.push_back(*hidx2local.find(hidx));
+                                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);

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;
+    context m_context;
-    hypothesis_idx_set  m_context_as_set;
+    expr    m_type;
-    expr                m_type;
 public:
     metavar_decl() {}
-    metavar_decl(hypothesis_idx_list const & c, hypothesis_idx_set const & s, expr const & t):
+    metavar_decl(context const & c, expr const & t):
-        m_context(c), m_context_as_set(s), m_type(t) {}
+        m_context(c), m_type(t) {}
-    hypothesis_idx_list get_context() const { return m_context; }
+    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 {
+    bool contains_href(expr const & h) const { return m_context.contains(href_index(h)); }
-        return m_context_as_set.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_decl>       metavar_decls;
     typedef metavar_idx_map<expr>               eassignment;
     typedef metavar_idx_map<level>              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);