feat(library/blast/hypothesis): track proof depth in hypotheses

src/library/blast/blast.cpp

@@ -459,7 +459,7 @@ class blastenv {
 
     optional<expr> search_upto(unsigned depth) {
         while (true) {
-            if (m_curr_state.get_depth() > depth) {
+            if (m_curr_state.get_proof_depth() > depth) {
                 // maximum depth reached
                 if (!next_choice_point()) {
                     return none_expr();

src/library/blast/hypothesis.h

@@ -23,18 +23,20 @@ using hypothesis_idx_map = typename lean::rb_map<unsigned, T, unsigned_cmp>;
 
 class hypothesis {
     friend class state;
-    name               m_name;      // for pretty printing
+    name               m_name;         // for pretty printing
     unsigned           m_active:1;
-    unsigned           m_dep_depth; // dependency depth
-    hypothesis_idx_set m_deps;      // hypotheses used by the type and/or value of this 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_type;
-    optional<expr>     m_value;     // justification for this object.
+    optional<expr>     m_value;        // justification for this object.
     // Remark: if blast::is_local(m_value) is true, then the hypothesis is an assumption
 public:
     hypothesis():m_active(false), m_dep_depth(0) {}
     name const & get_name() const { return m_name; }
     bool is_active() const { return m_active; }
     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_type() const { return m_type; }
     optional<expr> const & get_value() const { return m_value; }

src/library/blast/intros.cpp

@@ -10,13 +10,9 @@ Author: Leonardo de Moura
 
 namespace lean {
 namespace blast {
-class intros_proof_step_cell : public proof_step_cell {
+struct intros_proof_step_cell : public proof_step_cell {
     list<expr> m_new_hs;
-public:
-    intros_proof_step_cell(list<expr> const & new_hs):
-        m_new_hs(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);
         return some_expr(new_pr);
@@ -28,13 +24,15 @@ bool intros_action() {
     expr target = whnf(s.get_target());
     if (!is_pi(target))
         return false;
+    auto pcell = new intros_proof_step_cell();
+    s.push_proof_step(proof_step(pcell));
     buffer<expr> new_hs;
     while (is_pi(target)) {
         expr href  = s.mk_hypothesis(binding_name(target), binding_domain(target));
         new_hs.push_back(href);
         target     = whnf(instantiate(binding_body(target), href));
     }
-    s.push_proof_step(proof_step(new intros_proof_step_cell(to_list(new_hs))));
+    pcell->m_new_hs = to_list(new_hs);
     s.set_target(target);
     return true;
 }

src/library/blast/state.cpp

@@ -432,6 +432,7 @@ expr state::mk_hypothesis(unsigned new_hidx, name const & n, expr const & type,
     new_h.m_name          = n;
     new_h.m_type          = type;
     new_h.m_value         = value;
+    new_h.m_proof_depth   = m_proof_depth;
     add_deps(new_h, new_hidx);
     m_hyp_decls.insert(new_hidx, new_h);
     if (new_h.is_assumption())

src/library/blast/state.h

@@ -94,7 +94,7 @@ class state {
     // If this check fails, then we should replace any assigned `m_i` with its value, if the intersection is still
     // non-empty, then we cannot clear `h`.
     fixed_by           m_fixed_by;
-    unsigned           m_depth{0};
+    unsigned           m_proof_depth{0};
     proof_steps        m_proof_steps;
     // Hypothesis/facts in the current state
     hypothesis_decls   m_hyp_decls;
@@ -192,7 +192,7 @@ public:
     /** \brief Activate the next hypothesis in the TODO queue, return none if the TODO queue is empty. */
     optional<unsigned> activate_hypothesis();
 
-    /** \brief Store in \c r the hypotheses in this branch sorted by depth */
+    /** \brief Store in \c r the hypotheses in this branch sorted by dependency depth */
     void get_sorted_hypotheses(hypothesis_idx_buffer & r) const;
 
     expr expand_hrefs(expr const & e, list<expr> const & hrefs) const;
@@ -235,7 +235,7 @@ public:
     *************************/
 
     void push_proof_step(proof_step const & ps) {
-        m_depth++;
+        m_proof_depth++;
         m_proof_steps = cons(ps, m_proof_steps);
     }
 
@@ -249,12 +249,12 @@ public:
 
     void pop_proof_step() {
         lean_assert(m_proof_steps);
-        m_depth--;
+        m_proof_depth--;
         m_proof_steps = tail(m_proof_steps);
     }
 
-    unsigned get_depth() const {
-        return m_depth;
+    unsigned get_proof_depth() const {
+        return m_proof_depth;
     }