feat(library/blast): add intros action

src/library/blast/CMakeLists.txt

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

src/library/blast/blast.cpp

@@ -22,6 +22,7 @@ Author: Leonardo de Moura
 #include "library/blast/state.h"
 #include "library/blast/blast.h"
 #include "library/blast/assumption.h"
+#include "library/blast/intros.h"
 #include "library/blast/blast_exception.h"
 
 #ifndef LEAN_DEFAULT_BLAST_MAX_DEPTH
@@ -432,7 +433,9 @@ class blastenv {
     }
 
     pair<status, expr> next_action() {
-        if (activate_hypothesis()) {
+        if (intros_action()) {
+            return mk_pair(Continue, expr());
+        } else if (activate_hypothesis()) {
             // TODO(Leo): we should probably eagerly simplify the activated hypothesis.
             return mk_pair(Continue, expr());
         } else if (auto pr = assumption_action()) {
@@ -493,15 +496,44 @@ class blastenv {
         return none_expr();
     }
 
+    struct to_tactic_proof_fn : public replace_visitor {
+        state &  m_state;
+        branch & m_branch;
+
+        virtual expr visit_local(expr const & e) {
+            if (is_href(e)) {
+                hypothesis const * h = m_branch.get(e);
+                lean_assert(h);
+                expr v = h->get_value();
+                return visit(v);
+            } else {
+                return replace_visitor::visit_local(e);
+            }
+        }
+
+        virtual expr visit_meta(expr const & e) {
+            lean_assert(is_mref(e));
+            expr v = m_state.instantiate_urefs_mrefs(e);
+            if (v == e) {
+                return v;
+            } else {
+                return replace_visitor::visit_meta(v);
+            }
+        }
+
+        to_tactic_proof_fn(state & s):
+            m_state(s), m_branch(s.get_main_branch()) {}
+    };
+
     expr to_tactic_proof(expr const & pr) {
         // TODO(Leo): when a proof is found we must
-        // 1- remove all occurrences of href's from pr
-        // 2- replace mrefs with their assignments,
+        // 1- (done) remove all occurrences of href's from pr
+        // 2- (done) replace mrefs with their assignments,
         //    and convert unassigned meta-variables back into
         //    tactic meta-variables.
         // 3- The external tactic meta-variables that have been instantiated
         //    by blast must also be communicated back to the tactic framework.
-        return pr;
+        return to_tactic_proof_fn(m_curr_state)(pr);
     }
 
 public:

src/library/blast/branch.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <algorithm>
 #include "kernel/for_each_fn.h"
+#include "library/replace_visitor.h"
 #include "library/blast/branch.h"
 
 namespace lean {
@@ -145,6 +146,26 @@ void branch::set_target(expr const & t) {
     }
 }
 
+struct expand_hrefs_fn : public replace_visitor {
+    branch const &     m_branch;
+    list<expr> const & m_hrefs;
+
+    expand_hrefs_fn(branch const & b, list<expr> const & hrefs):
+        m_branch(b), m_hrefs(hrefs) {}
+
+    virtual expr visit_local(expr const & e) {
+        if (is_href(e) && std::find(m_hrefs.begin(), m_hrefs.end(), e) != m_hrefs.end()) {
+            return visit(m_branch.get(e)->get_value());
+        } else {
+            return replace_visitor::visit_local(e);
+        }
+    }
+};
+
+expr branch::expand_hrefs(expr const & e, list<expr> const & hrefs) const {
+    return expand_hrefs_fn(*this, hrefs)(e);
+}
+
 void initialize_branch() {
     g_prefix     = new name(name::mk_internal_unique_name());
 }

src/library/blast/branch.h

@@ -94,6 +94,8 @@ public:
 
     bool has_mvar(expr const & e) const { return m_mvar_idxs.contains(mref_index(e)); }
 
+    expr expand_hrefs(expr const & e, list<expr> const & hrefs) const;
+
     hypothesis_idx_set get_assumptions() const { return m_assumption; }
 };
 

src/library/blast/intros.cpp

@@ -0,0 +1,48 @@
+/*
+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 "kernel/abstract.h"
+#include "kernel/instantiate.h"
+#include "library/blast/blast.h"
+
+namespace lean {
+namespace blast {
+class intros_proof_step_cell : public proof_step_cell {
+    list<expr> m_new_hs;
+    list<expr> m_new_locals;
+public:
+    intros_proof_step_cell(list<expr> const & new_hs, list<expr> const & new_locals):
+        m_new_hs(new_hs), m_new_locals(new_locals) {}
+    virtual ~intros_proof_step_cell() {}
+
+    virtual optional<expr> resolve(state & s, expr const & pr) {
+        buffer<expr> locals;
+        to_buffer(m_new_locals, locals);
+        expr new_pr = Fun(locals, s.get_main_branch().expand_hrefs(pr, m_new_hs));
+        return some_expr(new_pr);
+    }
+};
+
+bool intros_action() {
+    state &  s  = curr_state();
+    branch & b  = s.get_main_branch();
+    expr target = whnf(b.get_target());
+    if (!is_pi(target))
+        return false;
+    buffer<expr> new_hs;
+    buffer<expr> new_locals;
+    while (is_pi(target)) {
+        expr local = mk_fresh_local(binding_domain(target));
+        expr href  = b.add_hypothesis(binding_name(target), binding_domain(target), local);
+        new_hs.push_back(href);
+        new_locals.push_back(local);
+        target     = whnf(instantiate(binding_body(target), href));
+    }
+    s.push_proof_step(proof_step(new intros_proof_step_cell(to_list(new_hs), to_list(new_locals))));
+    b.set_target(target);
+    return true;
+}
+}}

src/library/blast/intros.h

@@ -0,0 +1,11 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+namespace lean {
+namespace blast {
+bool intros_action();
+}}

src/library/blast/state.h

@@ -49,6 +49,7 @@ class proof_step {
     proof_step_cell * m_ptr;
 public:
     proof_step():m_ptr(nullptr) {}
+    proof_step(proof_step_cell * c):m_ptr(c) { m_ptr->inc_ref(); }
     proof_step(proof_step const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
     proof_step(proof_step && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
     ~proof_step() { if (m_ptr) m_ptr->dec_ref(); }