refactor(library/blast): revise how goal meta-vars are compiled into blast mrefs

src/library/blast/CMakeLists.txt

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

src/library/blast/blast.cpp

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "kernel/for_each_fn.h"
 #include "kernel/type_checker.h"
 #include "library/replace_visitor.h"
 #include "library/blast/expr.h"
@@ -31,16 +32,16 @@ level to_blast_level(level const & l) {
 }
 
 class context {
-    environment m_env;
+    environment    m_env;
-    io_state    m_ios;
+    io_state       m_ios;
-    name_set    m_lemma_hints;
+    name_set       m_lemma_hints;
-    name_set    m_unfold_hints;
+    name_set       m_unfold_hints;
+    name_map<expr> m_mvar2mref; // map goal metavariables to blast mref's
 
     class to_blast_expr_fn : public replace_visitor {
         type_checker                 m_tc;
         state &                      m_state;
-        // We map each metavariable to a metavariable application that contains only pairwise
+        // We map each metavariable to a metavariable application and the mref associated with it.
-        // distinct local constants (that have been converted into lrefs).
         name_map<pair<expr, expr>> & m_mvar2meta_mref;
         name_map<expr> &             m_local2lref;
 
@@ -90,38 +91,49 @@ class context {
                 get_app_args(meta_mref->first, decl_args);
                 if (decl_args.size() > args.size())
                     throw_unsupported_metavar_occ(e);
+                // Make sure the the current metavariable application prefix matches the one
+                // found before.
                 for (unsigned i = 0; i < decl_args.size(); i++) {
-                    lean_assert(is_local(decl_args[i]));
+                    if (is_local(decl_args[i])) {
-                    if (!is_local(args[i]) || mlocal_name(args[i]) != mlocal_name(decl_args[i]))
+                        if (!is_local(args[i]) || mlocal_name(args[i]) != mlocal_name(decl_args[i]))
+                            throw_unsupported_metavar_occ(e);
+                    } else if (decl_args[i] != args[i]) {
                         throw_unsupported_metavar_occ(e);
+                    }
                 }
                 return mk_mref_app(meta_mref->second, args.size() - decl_args.size(), args.data() + decl_args.size());
             } else {
                 unsigned i = 0;
-                hypothesis_set ctx;
+                hypothesis_idx_buffer ctx;
-                // find prefix of pair-wise distinct local constants that have already been processed.
+                // Find prefix that contains only closed terms.
                 for (; i < args.size(); i++) {
-                    if (!is_local(args[i]))
+                    if (!closed(args[i]))
                         break;
+                    if (!is_local(args[i])) {
+                        // Ignore arguments that are not local constants.
+                        // In the blast tactic we only support higher-order patterns.
+                        continue;
+                    }
                     expr const & l = args[i];
                     if (!std::all_of(args.begin(), args.begin() + i,
-                                     [&](expr const & prev) { return mlocal_name(prev) != mlocal_name(l); }))
+                                     [&](expr const & prev) { return mlocal_name(prev) != mlocal_name(l); })) {
-                        break;
+                        // Local has already been processed
-                    if (auto lref = m_local2lref.find(mlocal_name(l))) {
+                        continue;
-                        ctx.insert(lref_index(*lref));
-                    } else {
-                        break;
                     }
+                    auto lref = m_local2lref.find(mlocal_name(l));
+                    if (!lref) {
+                        // One of the arguments is a local constant that is not in m_local2lref
+                        throw_unsupported_metavar_occ(e);
+                    }
+                    ctx.push_back(lref_index(*lref));
                 }
                 unsigned  prefix_sz = i;
                 expr aux  = e;
                 for (; i < args.size(); i++)
                     aux = app_fn(aux);
                 lean_assert(is_meta(aux));
-                expr type           = visit(m_tc.infer(aux).first);
+                expr type = visit(m_tc.infer(aux).first);
-                unsigned mref_index = m_state.add_metavar_decl(metavar_decl(ctx, type));
+                expr mref = m_state.mk_metavar(ctx, type);
-                expr mref           = blast::mk_mref(mref_index);
-                m_mvar2meta_mref.insert(mlocal_name(mvar), mk_pair(aux, mref));
                 return mk_mref_app(mref, args.size() - prefix_sz, args.data() + prefix_sz);
             }
         }
@@ -157,16 +169,21 @@ class context {
         }
 
     public:
-        to_blast_expr_fn(environment const & env, state & s, name_map<pair<expr, expr>> & mvar2meta_mref,
+        to_blast_expr_fn(environment const & env, state & s,
-                         name_map<expr> & local2lref):
+                         name_map<pair<expr, expr>> & mvar2meta_mref, name_map<expr> & local2lref):
             m_tc(env), m_state(s), m_mvar2meta_mref(mvar2meta_mref), m_local2lref(local2lref) {}
     };
 
+    void init_mvar2mref(name_map<pair<expr, expr>> & m) {
+        m.for_each([&](name const & n, pair<expr, expr> const & p) {
+                m_mvar2mref.insert(n, p.second);
+            });
+    }
+
     state to_state(goal const & g) {
         state s;
-        branch b;
         name_map<pair<expr, expr>> mvar2meta_mref;
-        name_map<expr> local2lref;
+        name_map<expr>             local2lref;
         to_blast_expr_fn to_blast_expr(m_env, s, mvar2meta_mref, local2lref);
         buffer<expr> hs;
         g.get_hyps(hs);
@@ -175,7 +192,7 @@ class context {
             // TODO(Leo): create hypothesis using new_type
         }
         expr new_target = to_blast_expr(g.get_type());
-        // TODO(Leo): create branch and store in the state.
+        init_mvar2mref(mvar2meta_mref);
         return s;
     }
 

src/library/blast/branch.cpp

@@ -0,0 +1,35 @@
+/*
+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 "library/blast/branch.h"
+
+namespace lean {
+namespace blast {
+void branch::fix_hypothesis(unsigned idx) {
+    auto h = m_context.find(idx);
+    lean_assert(h);
+    hypothesis new_h(*h);
+    new_h.mark_fixed();
+    m_context.insert(idx, new_h);
+}
+
+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) {
+    m_context.for_each([&](unsigned hidx, hypothesis const &) {
+            r.push_back(hidx);
+        });
+    std::sort(r.begin(), r.end(), hypothesis_depth_lt(*this));
+}
+}}

src/library/blast/branch.h

@@ -14,14 +14,26 @@ namespace blast {
 typedef rb_tree<unsigned, unsigned_cmp> metavar_set;
 
 class branch {
-    typedef rb_map<unsigned, hypothesis, unsigned_cmp> context;
+    typedef rb_map<unsigned, hypothesis, unsigned_cmp>         context;
+    typedef rb_map<unsigned, hypothesis_idx_set, unsigned_cmp> dependencies;
     friend class state;
     unsigned      m_next;
     context       m_context;
+    dependencies  m_forward_deps;
     expr          m_target;
     metavar_set   m_mvars;
+
+    /** \brief Mark a hypothesis as fixed. The type/value of a fixed hypothesis cannot be
+        modified. A hypothesis is fixed when it occurs in the type of some metavariable. */
+    void fix_hypothesis(unsigned idx);
+    void fix_hypothesis(expr const & e) {
+        lean_assert(is_lref(e));
+        fix_hypothesis(lref_index(e));
+    }
 public:
     branch():m_next(0) {}
+    /** \brief Store in \c r the hypotheses in this branch sorted by depth */
+    void get_sorted_hypotheses(hypothesis_idx_buffer & r);
     hypothesis const * get(unsigned idx) const { return m_context.find(idx); }
     hypothesis const * get(expr const & e) const {
         lean_assert(is_lref(e));

src/library/blast/expr.cpp

@@ -204,6 +204,14 @@ unsigned lref_index(expr const & e) {
     return mlocal_name(e).get_numeral();
 }
 
+bool has_lref(expr const & e) {
+    return has_local(e);
+}
+
+bool has_mref(expr const & e) {
+    return has_expr_metavar(e);
+}
+
 expr mk_var(unsigned idx) {
     lean_assert(g_var_array);
     lean_assert(g_expr_table);

src/library/blast/expr.h

@@ -71,6 +71,10 @@ bool is_lref(expr const & e);
 unsigned lref_index(expr const & e);
 bool is_mref(expr const & e);
 unsigned mref_index(expr const & e);
+/** \brief Return true iff \c e contain lref's */
+bool has_lref(expr const & e);
+/** \brief Return true iff \c e contain mref's */
+bool has_mref(expr const & e);
 
 level update_succ(level const & l, level const & new_arg);
 level update_max(level const & l, level const & new_lhs, level const & new_rhs);

src/library/blast/hypothesis.h

@@ -15,26 +15,28 @@ class hypothesis;
 class branch;
 class state;
 
-typedef rb_tree<unsigned, unsigned_cmp> hypothesis_set;
+typedef rb_tree<unsigned, unsigned_cmp> hypothesis_idx_set;
+typedef list<unsigned>                  hypothesis_idx_list;
+typedef buffer<unsigned>                hypothesis_idx_buffer;
 
 class hypothesis {
     friend class branch;
-    name           m_name; // for pretty printing
+    name               m_name;     // for pretty printing
-    bool           m_active;
+    unsigned           m_active:1;
-    unsigned       m_depth;
+    unsigned           m_fixed:1;  // occurs in the type of a metavariable, so we should not update its type.
-    hypothesis_set m_backward_deps;
+    unsigned           m_depth;
-    hypothesis_set m_forward_deps;
+    hypothesis_idx_set m_deps;     // hypotheses used by the type and/or value of this hypothesis.
-    expr           m_type;
+    expr               m_type;
-    optional<expr> m_value;
+    optional<expr>     m_value;
-    optional<expr> m_justification;
+    optional<expr>     m_justification;
 public:
-    hypothesis():m_active(0), m_depth(0) {}
+    hypothesis():m_active(true), m_fixed(false), m_depth(0) {}
     bool is_active() const { return m_active; }
     unsigned get_depth() const { return m_depth; }
-    hypothesis_set const & get_backward_deps() const { return m_backward_deps; }
+    hypothesis_idx_set const & get_backward_deps() const { return m_deps; }
-    hypothesis_set const & get_forward_deps() const { return m_forward_deps; }
     expr const & get_type() const { return m_type; }
     optional<expr> const & get_value() const { return m_value; }
     optional<expr> const & get_justification() const { return m_justification; }
+    void mark_fixed() { m_fixed = true; }
 };
 }}

src/library/blast/state.cpp

@@ -4,15 +4,36 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "kernel/for_each_fn.h"
 #include "library/blast/state.h"
 
 namespace lean {
 namespace blast {
 state::state():m_next_mref_index(0) {}
-unsigned state::add_metavar_decl(metavar_decl const & decl) {
+
-    unsigned r = m_next_mref_index;
+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);
+    for_each(type, [&](expr const & e, unsigned) {
+            if (!has_lref(e))
+                return false;
+            if (is_lref(e)) {
+                lean_assert(ctx_as_set.contains(lref_index(e)));
+                m_main.fix_hypothesis(e);
+                return false;
+            }
+            return true; // continue search
+        });
+    unsigned idx = m_next_mref_index;
     m_next_mref_index++;
-    m_metavar_decls.insert(r, decl);
+    m_metavar_decls.insert(idx, metavar_decl(to_list(ctx), ctx_as_set, type));
-    return r;
+    return blast::mk_mref(idx);
+}
+
+expr state::mk_metavar(expr const & type) {
+    hypothesis_idx_buffer ctx;
+    m_main.get_sorted_hypotheses(ctx);
+    return mk_metavar(ctx, type);
 }
 }}

src/library/blast/state.h

@@ -13,11 +13,13 @@ Author: Leonardo de Moura
 namespace lean {
 namespace blast {
 class metavar_decl {
-    hypothesis_set m_context;
+    hypothesis_idx_list m_context;
-    expr           m_type;
+    hypothesis_idx_set  m_context_as_set;
+    expr                m_type;
 public:
     metavar_decl() {}
-    metavar_decl(hypothesis_set const & c, expr const & t):m_context(c), m_type(t) {}
+    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) {}
 };
 
 class state {
@@ -27,9 +29,19 @@ class state {
     typedef rb_map<unsigned, expr, unsigned_cmp>         assignment;
     metavar_decls m_metavar_decls;
     assignment    m_assignment;
+    branch        m_main;
+
+    unsigned add_metavar_decl(metavar_decl const & decl);
+
 public:
     state();
-    unsigned add_metavar_decl(metavar_decl const & decl);
+    /** \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.
+        The context of this metavariable will be all hypotheses occurring in the main branch. */
+    expr mk_metavar(expr const & type);
+
     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)); }
 };