refactor(library/blast): refactor hypothesis object: merge m_value and m_justification fields

src/library/blast/blast.cpp

@@ -215,7 +215,7 @@ class blastenv {
             lean_assert(is_local(h));
             expr type     = normalize(*norm_tc, mlocal_type(h));
             expr new_type = to_blast_expr(type);
-            expr href     = s.add_hypothesis(local_pp_name(h), new_type, none_expr(), some_expr(h));
+            expr href     = s.add_hypothesis(local_pp_name(h), new_type, h);
             local2href.insert(mlocal_name(h), href);
         }
         expr target     = normalize(*norm_tc, g.get_type());

src/library/blast/branch.cpp

@@ -69,16 +69,16 @@ void branch::add_deps(expr const & e, hypothesis & h_user, unsigned hidx_user) {
 
 void branch::add_deps(hypothesis & h_user, unsigned hidx_user) {
     add_deps(h_user.m_type, h_user, hidx_user);
-    if (h_user.m_value)
+    if (!blast::is_local(h_user.m_value)) {
-        add_deps(*h_user.m_value, h_user, hidx_user);
+        add_deps(h_user.m_value, h_user, hidx_user);
+    }
 }
 
-expr branch::add_hypothesis(name const & n, expr const & type, optional<expr> const & value, optional<expr> const & jst) {
+expr branch::add_hypothesis(name const & n, expr const & type, expr const & value) {
     hypothesis new_h;
     new_h.m_name          = n;
     new_h.m_type          = type;
     new_h.m_value         = value;
-    new_h.m_justification = jst;
     unsigned new_hidx = m_next;
     m_next++;
     add_deps(new_h, new_hidx);
@@ -88,8 +88,8 @@ expr branch::add_hypothesis(name const & n, expr const & type, optional<expr> co
 
 static name * g_prefix = nullptr;
 
-expr branch::add_hypothesis(expr const & type, optional<expr> const & value, optional<expr> const & jst) {
+expr branch::add_hypothesis(expr const & type, expr const & value) {
-    return add_hypothesis(name(*g_prefix, m_next), type, value, jst);
+    return add_hypothesis(name(*g_prefix, m_next), type, value);
 }
 
 bool branch::hidx_depends_on(unsigned hidx_user, unsigned hidx_provider) const {

src/library/blast/branch.h

@@ -34,8 +34,8 @@ class branch {
 public:
     branch():m_next(0) {}
 
-    expr add_hypothesis(name const & n, expr const & type, optional<expr> const & value, optional<expr> const & jst);
+    expr add_hypothesis(name const & n, expr const & type, expr const & value);
-    expr add_hypothesis(expr const & type, optional<expr> const & value, optional<expr> const & jst);
+    expr add_hypothesis(expr const & type, expr const & value);
 
     /** \brief Return true iff the hypothesis with index \c hidx_user depends on the hypothesis with index
         \c hidx_provider. */

src/library/blast/hypothesis.h

@@ -28,8 +28,8 @@ class hypothesis {
     unsigned           m_depth;
     hypothesis_idx_set m_deps;     // hypotheses used by the type and/or value of this hypothesis.
     expr               m_type;
-    optional<expr>     m_value;
+    expr               m_value;    // justification for this object.
-    optional<expr>     m_justification;
+    // Remark: if blast::is_local(m_value) is true, then the hypothesis is an assumption
 public:
     hypothesis():m_active(true), m_depth(0) {}
     name const & get_name() const { return m_name; }
@@ -37,9 +37,9 @@ public:
     unsigned get_depth() const { return m_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; }
+    expr const & get_value() const { return m_value; }
-    optional<expr> const & get_justification() const { return m_justification; }
     /** \brief Return true iff this hypothesis depends on \c h. */
     bool depends_on(expr const & h) const { return m_deps.contains(href_index(h)); }
+    bool is_assumption() const { return blast::is_local(m_value); }
 };
 }}

src/library/blast/state.cpp

@@ -341,7 +341,7 @@ bool state::check_hypothesis(expr const & e, branch const & b, unsigned hidx, hy
 
 bool state::check_hypothesis(branch const & b, unsigned hidx, hypothesis const & h) const {
     lean_assert(check_hypothesis(h.get_type(), b, hidx, h));
-    lean_assert(!h.get_value() || check_hypothesis(*h.get_value(), b, hidx, h));
+    lean_assert(h.is_assumption() || check_hypothesis(h.get_value(), b, hidx, h));
     return true;
 }
 

src/library/blast/state.h

@@ -126,16 +126,16 @@ public:
     expr instantiate_urefs_mrefs(expr const & e);
 
     /** \brief Add a new hypothesis to the main branch */
-    expr add_hypothesis(name const & n, expr const & type, optional<expr> const & value, optional<expr> const & jst) {
+    expr add_hypothesis(name const & n, expr const & type, expr const & value) {
-        return m_main.add_hypothesis(n, type, value, jst);
+        return m_main.add_hypothesis(n, type, value);
     }
 
     branch & get_main_branch() { return m_main; }
     branch const & get_main_branch() const { return m_main; }
 
     /** \brief Add a new hypothesis to the main branch */
-    expr add_hypothesis(expr const & type, optional<expr> const & value, optional<expr> const & jst) {
+    expr add_hypothesis(expr const & type, expr const & value) {
-        return m_main.add_hypothesis(type, value, jst);
+        return m_main.add_hypothesis(type, value);
     }
 
     /** \brief Set target (aka conclusion, aka type of the goal, aka type of the term that must be synthesize in this branch)