refactor(library/blast): change how we mark fixed/frozen hypothesis

src/library/blast/branch.cpp

@@ -10,14 +10,6 @@ Author: Leonardo de Moura
 
 namespace lean {
 namespace blast {
-void branch::fix_hypothesis(unsigned idx) {
-    auto h = m_context.find(idx);
-    lean_assert(h);
-    hypothesis new_h(*h);
-    new_h.mark_fixed();
-    m_context.insert(idx, new_h);
-}
-
 struct hypothesis_depth_lt {
     branch const & m_branch;
     hypothesis_depth_lt(branch const & b): m_branch(b) {}

src/library/blast/branch.h

@@ -26,14 +26,6 @@ class branch {
     hypothesis_idx_set m_target_deps;
     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. */
-    void fix_hypothesis(unsigned idx);
-    void fix_hypothesis(expr const & e) {
-        lean_assert(is_href(e));
-        fix_hypothesis(href_index(e));
-    }
-
     void add_forward_dep(unsigned hidx_user, unsigned hidx_provider);
     void add_deps(expr const & e, hypothesis & h_user, unsigned hidx_user);
     void add_deps(hypothesis & h_user, unsigned hidx_user);

src/library/blast/hypothesis.h

@@ -25,14 +25,13 @@ class hypothesis {
     friend class branch;
     name               m_name;     // for pretty printing
     unsigned           m_active:1;
-    unsigned           m_fixed:1;  // occurs in the type of a metavariable, so we should not update its type.
     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;
     optional<expr>     m_justification;
 public:
-    hypothesis():m_active(true), m_fixed(false), m_depth(0) {}
+    hypothesis():m_active(true), 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; }
@@ -40,7 +39,6 @@ public:
     expr const & get_type() const { return m_type; }
     optional<expr> const & get_value() const { return m_value; }
     optional<expr> const & get_justification() const { return m_justification; }
-    void mark_fixed() { m_fixed = true; }
     /** \brief Return true iff this hypothesis depends on \c h. */
     bool depends_on(expr const & h) const { return m_deps.contains(href_index(h)); }
 };

src/library/blast/state.cpp

@@ -13,24 +13,40 @@ namespace lean {
 namespace blast {
 state::state():m_next_mref_index(0) {}
 
+/** \brief Mark that hypothesis h with index hidx is fixed by the meta-variable midx.
+    That is, `h` occurs in the type of `midx`. */
+void state::add_fixed_by(unsigned hidx, unsigned midx) {
+    if (auto s = m_fixed_by.find(hidx)) {
+        if (!s->contains(midx)) {
+            metavar_idx_set new_s(*s);
+            new_s.insert(midx);
+            m_fixed_by.insert(hidx, new_s);
+        }
+    } else {
+        metavar_idx_set new_s;
+        new_s.insert(midx);
+        m_fixed_by.insert(hidx, new_s);
+    }
+}
+
 expr state::mk_metavar(hypothesis_idx_buffer const & ctx, expr const & type) {
     hypothesis_idx_set  ctx_as_set;
     for (unsigned const & hidx : ctx)
         ctx_as_set.insert(hidx);
+    unsigned midx = m_next_mref_index;
     for_each(type, [&](expr const & e, unsigned) {
             if (!has_href(e))
                 return false;
             if (is_href(e)) {
                 lean_assert(ctx_as_set.contains(href_index(e)));
-                m_main.fix_hypothesis(e);
+                add_fixed_by(href_index(e), midx);
                 return false;
             }
             return true; // continue search
         });
-    unsigned idx = m_next_mref_index;
     m_next_mref_index++;
-    m_metavar_decls.insert(idx, metavar_decl(to_list(ctx), ctx_as_set, type));
-    return blast::mk_mref(idx);
+    m_metavar_decls.insert(midx, metavar_decl(to_list(ctx), ctx_as_set, type));
+    return blast::mk_mref(midx);
 }
 
 expr state::mk_metavar(expr const & type) {

src/library/blast/state.h

@@ -27,13 +27,24 @@ public:
 
 class state {
     friend class context;
-    typedef metavar_idx_map<metavar_decl> metavar_decls;
-    typedef metavar_idx_map<expr>         assignment;
+    typedef metavar_idx_map<metavar_decl>       metavar_decls;
+    typedef metavar_idx_map<expr>               assignment;
+    typedef hypothesis_idx_map<metavar_idx_set> fixed_by;
     unsigned      m_next_mref_index;
     metavar_decls m_metavar_decls;
     assignment    m_assignment;
     branch        m_main;
+    // In the following mapping, each entry (h -> {m_1 ... m_n}) means that hypothesis `h` cannot be cleared
+    // in any branch where the metavariables m_1 ... m_n have not been replaced with the values assigned to them.
+    // That is, to be able to clear `h` in a branch `B`, we first need to check whether it
+    // is contained in this mapping or not. If it is, we should check whether any of the
+    // metavariables `m_1` ... `m_n` occur in `B` (this is a relatively quick check since
+    // `B` contains an over-approximation of all meta-variables occuring in it (i.e., m_mvar_idxs).
+    // 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;
 
+    void add_fixed_by(unsigned hidx, unsigned midx);
     unsigned add_metavar_decl(metavar_decl const & decl);
     goal to_goal(branch const &) const;