feat(library/blast): add proof_expr thin layer for creating proof terms at blast

src/library/blast/CMakeLists.txt

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

src/library/blast/assumption.cpp

@@ -18,12 +18,7 @@ optional<expr> assumption_action() {
         });
     if (!hidx)
         return none_expr();
-    // TODO(Leo): cleanup
     hypothesis const * h = s.get_hypothesis_decl(*hidx);
-    if (h->get_value()) {
+    return some_expr(h->get_self());
-        return some_expr(*h->get_value());
-    } else {
-        return some_expr(mk_href(*hidx));
-    }
 }
 }}

src/library/blast/blast.cpp

@@ -23,6 +23,7 @@ Author: Leonardo de Moura
 #include "library/blast/blast.h"
 #include "library/blast/assumption.h"
 #include "library/blast/intros.h"
+#include "library/blast/proof_expr.h"
 #include "library/blast/blast_exception.h"
 
 #ifndef LEAN_DEFAULT_BLAST_MAX_DEPTH
@@ -494,43 +495,18 @@ class blastenv {
         return none_expr();
     }
 
-    struct to_tactic_proof_fn : public replace_visitor {
-        state &  m_state;
-
-        virtual expr visit_local(expr const & e) {
-            // TODO(Leo): cleanup
-            if (is_href(e)) {
-                hypothesis const * h = m_state.get_hypothesis_decl(e);
-                if (auto r = h->get_value()) {
-                    return visit(*r);
-                }
-            }
-            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) {}
-    };
-
     expr to_tactic_proof(expr const & pr) {
-        // TODO(Leo): when a proof is found we must
+        // When a proof is found we must
-        // 1- (done) remove all occurrences of href's from pr
+        // 1- Remove all occurrences of href's from pr
-        // 2- (done) replace mrefs with their assignments,
+        expr pr1 = unfold_hypotheses_ge(m_curr_state, pr, 0);
+        // 2- Replace mrefs with their assignments,
         //    and convert unassigned meta-variables back into
         //    tactic meta-variables.
+        expr pr2 = m_curr_state.instantiate_urefs_mrefs(pr1);
+        // TODO(Leo):
         // 3- The external tactic meta-variables that have been instantiated
         //    by blast must also be communicated back to the tactic framework.
-        return to_tactic_proof_fn(m_curr_state)(pr);
+        return pr2;
     }
 
 public:

src/library/blast/hypothesis.h

@@ -28,6 +28,7 @@ class hypothesis {
     unsigned           m_dep_depth;    // dependency depth
     unsigned           m_proof_depth;  // proof depth when the hypothesis was created
     hypothesis_idx_set m_deps;         // hypotheses used by the type and/or value of this hypothesis.
+    expr               m_self;
     expr               m_type;
     optional<expr>     m_value;        // justification for this object.
     // Remark: if blast::is_local(m_value) is true, then the hypothesis is an assumption
@@ -38,6 +39,7 @@ public:
     unsigned get_dep_depth() const { return m_dep_depth; }
     unsigned get_proof_depth() const { return m_proof_depth; }
     hypothesis_idx_set const & get_backward_deps() const { return m_deps; }
+    expr const & get_self() const { return m_self; }
     expr const & get_type() const { return m_type; }
     optional<expr> const & get_value() const { return m_value; }
     /** \brief Return true iff this hypothesis depends on \c h. */

src/library/blast/intros.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
 #include "library/blast/blast.h"
+#include "library/blast/proof_expr.h"
 
 namespace lean {
 namespace blast {
@@ -14,7 +15,7 @@ struct intros_proof_step_cell : public proof_step_cell {
     list<expr> m_new_hs;
     virtual ~intros_proof_step_cell() {}
     virtual optional<expr> resolve(state & s, expr const & pr) const {
-        expr new_pr = s.mk_lambda(m_new_hs, pr);
+        expr new_pr = mk_proof_lambda(s, m_new_hs, unfold_hypotheses_ge(s, pr));
         return some_expr(new_pr);
     }
 };

src/library/blast/proof_expr.cpp

@@ -0,0 +1,50 @@
+/*
+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/replace_visitor.h"
+#include "library/blast/blast.h"
+#include "library/blast/proof_expr.h"
+
+namespace lean {
+namespace blast {
+expr to_proof_expr(expr const & e) {
+    return e;
+}
+
+struct unfold_hypotheses_ge_fn : public replace_visitor {
+    state const &      m_state;
+    unsigned           m_depth;
+
+    unfold_hypotheses_ge_fn(state const & s, unsigned d):
+        m_state(s), m_depth(d) {}
+
+    virtual expr visit_local(expr const & e) {
+        if (is_href(e)) {
+            hypothesis const * h = m_state.get_hypothesis_decl(e);
+            if (h->get_proof_depth() >= m_depth && h->get_value()) {
+                return visit(*h->get_value());
+            }
+        }
+        return replace_visitor::visit_local(e);
+    }
+};
+
+expr unfold_hypotheses_ge(state const & s, expr const & pr, unsigned d) {
+    return unfold_hypotheses_ge_fn(s, d)(pr);
+}
+
+expr mk_proof_lambda(state const & s, list<expr> const & hs, expr const & pr) {
+    return s.mk_lambda(hs, pr);
+}
+
+expr mk_proof_app(name const & fname, unsigned nargs, expr const * args) {
+    return get_app_builder().mk_app(fname, nargs, args);
+}
+
+expr mk_proof_app(expr const & f, unsigned nargs, expr const * args) {
+    return mk_app(f, nargs, args);
+}
+}}

src/library/blast/proof_expr.h

@@ -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/state.h"
+
+namespace lean {
+namespace blast {
+/*
+   This module provides a thin layer for creating proof terms at proof-step resolve.
+   The idea is to allow us to refactor the code in the future, and implement
+   more efficient ways of representing proof terms.
+
+   One current performance bottleneck is unfold_hypotheses_ge.
+*/
+
+/** \brief This is currently a noop. */
+expr to_proof_expr(expr const & e);
+
+/** \brief Unfold hrefs occurring in \c pr that have a value and were created
+    at proof depth >= d */
+expr unfold_hypotheses_ge(state const & s, expr const & pr, unsigned d);
+inline expr unfold_hypotheses_ge(state const & s, expr const & pr) {
+    return unfold_hypotheses_ge(s, pr, s.get_proof_depth());
+}
+
+/** \brief Create an lambda abstraction. */
+expr mk_proof_lambda(state const & s, list<expr> const & hs, expr const & pr);
+
+/** \brief Create an application using the app_builder */
+expr mk_proof_app(name const & fname, unsigned nargs, expr const * args);
+expr mk_proof_app(expr const & f, unsigned nargs, expr const * args);
+}}

src/library/blast/state.cpp

@@ -429,9 +429,11 @@ double state::compute_weight(unsigned hidx, expr const & /* type */) {
 
 expr state::mk_hypothesis(unsigned new_hidx, name const & n, expr const & type, optional<expr> const & value) {
     hypothesis new_h;
+    expr r                = mk_href(new_hidx);
     new_h.m_name          = n;
     new_h.m_type          = type;
     new_h.m_value         = value;
+    new_h.m_self          = r;
     new_h.m_proof_depth   = m_proof_depth;
     add_deps(new_h, new_hidx);
     m_hyp_decls.insert(new_hidx, new_h);
@@ -439,7 +441,7 @@ expr state::mk_hypothesis(unsigned new_hidx, name const & n, expr const & type,
         m_assumption.insert(new_hidx);
     double w = compute_weight(new_hidx, type);
     m_todo_queue.insert(w, new_hidx);
-    return blast::mk_href(new_hidx);
+    return r;
 }
 
 expr state::mk_hypothesis(name const & n, expr const & type, expr const & value) {