feat(library/bast): convert a blast branch back into a goal

src/library/blast/branch.cpp

@@ -27,7 +27,7 @@ struct hypothesis_depth_lt {
     }
 };
 
-void branch::get_sorted_hypotheses(hypothesis_idx_buffer & r) {
+void branch::get_sorted_hypotheses(hypothesis_idx_buffer & r) const {
     m_context.for_each([&](unsigned hidx, hypothesis const &) {
             r.push_back(hidx);
         });
@@ -66,7 +66,7 @@ void branch::add_deps(expr const & e, hypothesis & h_user, unsigned hidx_user) {
                 }
                 return false;
             } else if (is_mref(l)) {
-                m_mvars.insert(mref_index(l));
+                m_mvar_idxs.insert(mref_index(l));
                 return false;
             } else {
                 return true;
@@ -110,7 +110,7 @@ void branch::set_target(expr const & t) {
                     m_target_deps.insert(lref_index(e));
                     return false;
                 } else if (is_mref(e)) {
-                    m_mvars.insert(mref_index(e));
+                    m_mvar_idxs.insert(mref_index(e));
                     return false;
                 } else {
                     return true;

src/library/blast/branch.h

@@ -11,18 +11,20 @@ Author: Leonardo de Moura
 
 namespace lean {
 namespace blast {
-typedef rb_tree<unsigned, unsigned_cmp> metavar_set;
+typedef rb_tree<unsigned, unsigned_cmp> metavar_idx_set;
+template<typename T>
+using metavar_idx_map = typename lean::rb_map<unsigned, T, unsigned_cmp>;
 
 class branch {
-    typedef rb_map<unsigned, hypothesis, unsigned_cmp>         context;
+    typedef hypothesis_idx_map<hypothesis>         context;
-    typedef rb_map<unsigned, hypothesis_idx_set, unsigned_cmp> forward_deps;
+    typedef hypothesis_idx_map<hypothesis_idx_set> forward_deps;
     friend class state;
     unsigned           m_next;
     context            m_context;
     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;
-    metavar_set        m_mvars;
+    metavar_idx_set    m_mvar_idxs;
 
     /** \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. */
@@ -39,7 +41,7 @@ class branch {
 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);
+    void get_sorted_hypotheses(hypothesis_idx_buffer & r) const;
 
     expr add_hypothesis(name const & n, expr const & type, optional<expr> const & value, optional<expr> const & jst);
     expr add_hypothesis(expr const & type, optional<expr> const & value, optional<expr> const & jst);
@@ -51,6 +53,8 @@ public:
         lean_assert(is_lref(e));
         return get(lref_index(e));
     }
+
+    expr const & get_target() const { return m_target; }
 };
 
 void initialize_branch();

src/library/blast/hypothesis.h

@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "util/rc.h"
-#include "util/rb_tree.h"
+#include "util/rb_map.h"
 #include "kernel/expr.h"
 
 namespace lean {
@@ -18,6 +18,8 @@ class state;
 typedef rb_tree<unsigned, unsigned_cmp> hypothesis_idx_set;
 typedef list<unsigned>                  hypothesis_idx_list;
 typedef buffer<unsigned>                hypothesis_idx_buffer;
+template<typename T>
+using hypothesis_idx_map = typename lean::rb_map<unsigned, T, unsigned_cmp>;
 
 class hypothesis {
     friend class branch;
@@ -31,6 +33,7 @@ class hypothesis {
     optional<expr>     m_justification;
 public:
     hypothesis():m_active(true), m_fixed(false), m_depth(0) {}
+    name const & get_name() const { return m_name; }
     bool is_active() const { return m_active; }
     unsigned get_depth() const { return m_depth; }
     hypothesis_idx_set const & get_backward_deps() const { return m_deps; }

src/library/blast/state.cpp

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "kernel/abstract.h"
 #include "kernel/for_each_fn.h"
 #include "library/blast/state.h"
 
@@ -34,6 +35,62 @@ expr state::mk_metavar(hypothesis_idx_buffer const & ctx, expr const & type) {
 expr state::mk_metavar(expr const & type) {
     hypothesis_idx_buffer ctx;
     m_main.get_sorted_hypotheses(ctx);
-    return mk_metavar(ctx, type);
+    return state::mk_metavar(ctx, type);
+}
+
+goal state::to_goal(branch const & b) const {
+    hypothesis_idx_map<expr> hidx2local;
+    metavar_idx_map<expr>    midx2meta;
+    name M("M");
+    std::function<expr(expr const &)> convert = [&](expr const & e) {
+        return replace(e, [&](expr const & e) {
+                if (is_lref(e)) {
+                    auto r = hidx2local.find(lref_index(e));
+                    lean_assert(r);
+                    return some_expr(*r);
+                } else if (is_mref(e)) {
+                    auto r = midx2meta.find(mref_index(e));
+                    if (r) {
+                        return some_expr(*r);
+                    } else {
+                        metavar_decl const * decl = m_metavar_decls.find(mref_index(e));
+                        lean_assert(decl);
+                        buffer<expr> ctx;
+                        for (unsigned hidx : decl->get_context()) {
+                            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);
+                        expr new_meta = mk_app(new_mvar, ctx);
+                        midx2meta.insert(mref_index(e), new_meta);
+                        return some_expr(new_meta);
+                    }
+                } else {
+                    return none_expr();
+                }
+            });
+    };
+    name H("H");
+    hypothesis_idx_buffer hidxs;
+    b.get_sorted_hypotheses(hidxs);
+    buffer<expr> hyps;
+    for (unsigned hidx : hidxs) {
+        hypothesis const * h = b.get(hidx);
+        lean_assert(h);
+        // after we add support for let-decls in goals, we must convert back h->get_value() if it is available
+        expr new_h = lean::mk_local(h->get_name(), name(H, hidx), convert(h->get_type()), binder_info());
+        hidx2local.insert(hidx, new_h);
+        hyps.push_back(new_h);
+    }
+    expr new_target    = convert(b.get_target());
+    expr new_mvar_type = Pi(hyps, new_target);
+    expr new_mvar      = lean::mk_metavar(M, new_mvar_type);
+    expr new_meta      = mk_app(new_mvar, hyps);
+    return goal(new_meta, new_target);
+}
+
+goal state::to_goal() const {
+    return to_goal(m_main);
 }
 }}

src/library/blast/state.h

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "util/rb_map.h"
 #include "kernel/expr.h"
+#include "library/tactic/goal.h"
 #include "library/blast/hypothesis.h"
 #include "library/blast/branch.h"
 
@@ -20,18 +21,21 @@ 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; }
+    expr const & get_type() const { return m_type; }
 };
 
 class state {
     friend class context;
-    unsigned m_next_mref_index;
+    typedef metavar_idx_map<metavar_decl> metavar_decls;
-    typedef rb_map<unsigned, metavar_decl, unsigned_cmp> metavar_decls;
+    typedef metavar_idx_map<expr>         assignment;
-    typedef rb_map<unsigned, expr, unsigned_cmp>         assignment;
+    unsigned      m_next_mref_index;
     metavar_decls m_metavar_decls;
     assignment    m_assignment;
     branch        m_main;
 
     unsigned add_metavar_decl(metavar_decl const & decl);
+    goal to_goal(branch const &) const;
 
 public:
     state();
@@ -61,5 +65,10 @@ public:
     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)); }
+
+    /** \brief Convert main branch to a goal.
+        This is mainly used for pretty printing. However, in the future, we may use this capability
+        to invoke the tactic framework from the blast tactic. */
+    goal to_goal() const;
 };
 }}