chore(library/blast): remove "leftover" file used in the old blast architecture

src/library/blast/CMakeLists.txt

@@ -1,4 +1,4 @@
-add_library(blast OBJECT expr.cpp state.cpp blast.cpp blast_tactic.cpp
+add_library(blast OBJECT hypothesis.cpp state.cpp blast.cpp blast_tactic.cpp
   init_module.cpp proof_expr.cpp options.cpp choice_point.cpp util.cpp
   gexpr.cpp revert.cpp strategy.cpp congruence_closure.cpp trace.cpp
   imp_extension.cpp)

src/library/blast/blast.cpp

@@ -22,7 +22,6 @@ Author: Leonardo de Moura
 #include "library/projection.h"
 #include "library/scoped_ext.h"
 #include "library/tactic/goal.h"
-#include "library/blast/expr.h"
 #include "library/blast/state.h"
 #include "library/blast/blast.h"
 #include "library/blast/proof_expr.h"
@@ -36,7 +35,9 @@ Author: Leonardo de Moura
 namespace lean {
 namespace blast {
 static name * g_prefix     = nullptr;
+static name * g_ref_prefix = nullptr;
 static name * g_tmp_prefix = nullptr;
+static expr * g_dummy_type = nullptr; // dummy type for href/mref
 
 class imp_extension_manager {
     std::vector<pair<ext_state_maker &, unsigned> > m_entries;
@@ -74,6 +75,9 @@ class blastenv {
     environment                m_env;
     io_state                   m_ios;
     name_generator             m_ngen;
+    unsigned                   m_next_uref_idx{0};
+    unsigned                   m_next_mref_idx{0};
+    unsigned                   m_next_href_idx{0};
     tmp_local_generator        m_tmp_local_generator;
     list<expr>                 m_initial_context; // for setting type_context local instances
     name_set                   m_lemma_hints;
@@ -484,7 +488,6 @@ public:
         m_unfold_macro_pred([](expr const &) { return true; }),
         m_tctx(*this),
         m_normalizer(m_tctx) {
-        init_uref_mref_href_idxs();
         clear_choice_points();
     }
 
@@ -707,6 +710,24 @@ public:
     optional<relation_info> get_relation_info(name const & rop) const {
         return m_rel_getter(rop);
     }
+
+    unsigned mk_uref_idx() {
+        unsigned r = m_next_uref_idx;
+        m_next_uref_idx++;
+        return r;
+    }
+
+    unsigned mk_mref_idx() {
+        unsigned r = m_next_mref_idx;
+        m_next_mref_idx++;
+        return r;
+    }
+
+    unsigned mk_href_idx() {
+        unsigned r = m_next_href_idx;
+        m_next_href_idx++;
+        return r;
+    }
 };
 
 LEAN_THREAD_PTR(blastenv, g_blastenv);
@@ -717,6 +738,68 @@ public:
     ~scope_blastenv() { g_blastenv = m_prev_blastenv; }
 };
 
+level mk_uref(unsigned idx) {
+    return lean::mk_meta_univ(name(*g_ref_prefix, idx));
+}
+
+bool is_uref(level const & l) {
+    return is_meta(l) && meta_id(l).is_numeral();
+}
+
+unsigned uref_index(level const & l) {
+    lean_assert(is_uref(l));
+    return meta_id(l).get_numeral();
+}
+
+expr mk_href(unsigned idx) {
+    return lean::mk_local(name(*g_ref_prefix, idx), *g_dummy_type);
+}
+
+bool is_href(expr const & e) {
+    return lean::is_local(e) && mlocal_type(e) == *g_dummy_type;
+}
+
+expr mk_mref(unsigned idx) {
+    return mk_metavar(name(*g_ref_prefix, idx), *g_dummy_type);
+}
+
+bool is_mref(expr const & e) {
+    return is_metavar(e) && mlocal_type(e) == *g_dummy_type;
+}
+
+unsigned mref_index(expr const & e) {
+    lean_assert(is_mref(e));
+    return mlocal_name(e).get_numeral();
+}
+
+unsigned href_index(expr const & e) {
+    lean_assert(is_href(e));
+    return mlocal_name(e).get_numeral();
+}
+
+bool has_href(expr const & e) {
+    return lean::has_local(e);
+}
+
+bool has_mref(expr const & e) {
+    return lean::has_expr_metavar(e);
+}
+
+unsigned mk_uref_idx() {
+    lean_assert(g_blastenv);
+    return g_blastenv->mk_uref_idx();
+}
+
+unsigned mk_mref_idx() {
+    lean_assert(g_blastenv);
+    return g_blastenv->mk_mref_idx();
+}
+
+unsigned mk_href_idx() {
+    lean_assert(g_blastenv);
+    return g_blastenv->mk_href_idx();
+}
+
 environment const & env() {
     lean_assert(g_blastenv);
     return g_blastenv->get_env();
@@ -1056,11 +1139,15 @@ optional<expr> blast_goal(environment const & env, io_state const & ios, list<na
 void initialize_blast() {
     blast::g_prefix                  = new name(name::mk_internal_unique_name());
     blast::g_tmp_prefix              = new name(name::mk_internal_unique_name());
+    blast::g_ref_prefix              = new name(name::mk_internal_unique_name());
     blast::g_imp_extension_manager   = new blast::imp_extension_manager();
+    blast::g_dummy_type              = new expr(mk_constant(*blast::g_ref_prefix));
 }
 void finalize_blast() {
     delete blast::g_imp_extension_manager;
     delete blast::g_prefix;
     delete blast::g_tmp_prefix;
+    delete blast::g_ref_prefix;
+    delete blast::g_dummy_type;
 }
 }

src/library/blast/blast.h

@@ -20,6 +20,43 @@ struct projection_info;
 class goal;
 typedef std::unique_ptr<tmp_type_context> tmp_type_context_ptr;
 namespace blast {
+/** \brief Create a blast-state universe meta-variable */
+level mk_uref(unsigned idx);
+/** \brief Return true iff \c l is a blast-state universe meta-variable */
+bool is_uref(level const & l);
+/** \brief Return the index of the given blast-state universe meta-variable */
+unsigned uref_index(level const & l);
+
+/** \brief Create a blast-state hypothesis (reference).
+    \remark these references are local constants, but they do **not** store their types */
+expr mk_href(unsigned idx);
+/** \brief Create a blast-state meta-variable (reference).
+    \remark these references are local constants, but they do **not** store their types */
+expr mk_mref(unsigned idx);
+
+/** \brief Return true iff \c e is a hypothesis reference */
+bool is_href(expr const & e);
+/** \brief Return the index of the given hypothesis reference */
+unsigned href_index(expr const & e);
+/** \brief Return true iff \c e is a blast-state meta-variable (reference) */
+bool is_mref(expr const & e);
+/** \brief Return the index of the given blast-state meta-variable (reference) */
+unsigned mref_index(expr const & e);
+/** \brief Return true iff \c e contain href's */
+bool has_href(expr const & e);
+/** \brief Return true iff \c e contain mref's */
+bool has_mref(expr const & e);
+/** \brief Return true if \c is a local constant, but it is not a hypothesis reference */
+inline bool is_local_non_href(expr const & e) { return is_local(e) && !is_href(e); }
+
+/** \brief Return the a fresh index for uref/mref/href.
+    \remark It is implemented using thread local storage. */
+unsigned mk_uref_idx();
+unsigned mk_mref_idx();
+unsigned mk_href_idx();
+
+inline level mk_fresh_uref() { return mk_uref(mk_uref_idx()); }
+
 /** \brief Return the thread local environment being used by the blast tactic. */
 environment const & env();
 /** \brief Return the thread local io_state being used by the blast tactic. */

src/library/blast/expr.cpp

@@ -1,105 +0,0 @@
-/*
-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 <vector>
-#include <unordered_set>
-#include "util/interrupt.h"
-#include "kernel/expr_eq_fn.h"
-#include "kernel/replace_cache.h"
-#include "kernel/cache_stack.h"
-#include "kernel/instantiate_univ_cache.h"
-#include "library/blast/expr.h"
-
-namespace lean {
-namespace blast {
-static name * g_prefix = nullptr;
-static expr * g_dummy_type = nullptr; // dummy type for href/mref
-
-level mk_uref(unsigned idx) {
-    return lean::mk_meta_univ(name(*g_prefix, idx));
-}
-
-bool is_uref(level const & l) {
-    return is_meta(l) && meta_id(l).is_numeral();
-}
-
-unsigned uref_index(level const & l) {
-    lean_assert(is_uref(l));
-    return meta_id(l).get_numeral();
-}
-
-expr mk_href(unsigned idx) {
-    return lean::mk_local(name(*g_prefix, idx), *g_dummy_type);
-}
-
-bool is_href(expr const & e) {
-    return lean::is_local(e) && mlocal_type(e) == *g_dummy_type;
-}
-
-expr mk_mref(unsigned idx) {
-    return mk_metavar(name(*g_prefix, idx), *g_dummy_type);
-}
-
-bool is_mref(expr const & e) {
-    return is_metavar(e) && mlocal_type(e) == *g_dummy_type;
-}
-
-unsigned mref_index(expr const & e) {
-    lean_assert(is_mref(e));
-    return mlocal_name(e).get_numeral();
-}
-
-unsigned href_index(expr const & e) {
-    lean_assert(is_href(e));
-    return mlocal_name(e).get_numeral();
-}
-
-bool has_href(expr const & e) {
-    return lean::has_local(e);
-}
-
-bool has_mref(expr const & e) {
-    return lean::has_expr_metavar(e);
-}
-
-LEAN_THREAD_VALUE(unsigned, m_next_uref_idx, 0);
-LEAN_THREAD_VALUE(unsigned, m_next_mref_idx, 0);
-LEAN_THREAD_VALUE(unsigned, m_next_href_idx, 0);
-
-unsigned mk_uref_idx() {
-    unsigned r = m_next_uref_idx;
-    m_next_uref_idx++;
-    return r;
-}
-
-unsigned mk_mref_idx() {
-    unsigned r = m_next_mref_idx;
-    m_next_mref_idx++;
-    return r;
-}
-
-unsigned mk_href_idx() {
-    unsigned r = m_next_href_idx;
-    m_next_href_idx++;
-    return r;
-}
-
-void init_uref_mref_href_idxs() {
-    m_next_uref_idx = 0;
-    m_next_mref_idx = 0;
-    m_next_href_idx = 0;
-}
-
-void initialize_expr() {
-    g_prefix     = new name(name::mk_internal_unique_name());
-    g_dummy_type = new expr(mk_constant(*g_prefix));
-}
-
-void finalize_expr() {
-    delete g_prefix;
-    delete g_dummy_type;
-}
-}}

src/library/blast/expr.h

@@ -1,47 +0,0 @@
-/*
-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
-#include "kernel/expr.h"
-#include "kernel/declaration.h"
-
-namespace lean {
-namespace blast {
-level mk_uref(unsigned idx);
-
-bool is_uref(level const & l);
-unsigned uref_index(level const & l);
-
-// mk_href and mk_mref are helper functions for creating hypotheses and meta-variables used in the blast tactic.
-// Remark: the local constants and metavariables manipulated by the blast tactic do **not** store their types.
-expr mk_href(unsigned idx);
-expr mk_mref(unsigned idx);
-
-bool is_href(expr const & e);
-unsigned href_index(expr const & e);
-bool is_mref(expr const & e);
-unsigned mref_index(expr const & e);
-/** \brief Return true iff \c e contain href's */
-bool has_href(expr const & e);
-/** \brief Return true iff \c e contain mref's */
-bool has_mref(expr const & e);
-
-inline bool is_local_non_href(expr const & e) { return is_local(e) && !is_href(e); }
-
-/** \brief Return the a fresh index for uref/mref/href.
-    \remark It is implemented using thread local storage. */
-unsigned mk_uref_idx();
-unsigned mk_mref_idx();
-unsigned mk_href_idx();
-/** \brief Reset thread local counters */
-void init_uref_mref_href_idxs();
-
-inline level mk_fresh_uref() { return mk_uref(mk_uref_idx()); }
-
-void initialize_expr();
-void finalize_expr();
-}
-}

src/library/blast/hypothesis.cpp

@@ -0,0 +1,14 @@
+/*
+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/hypothesis.h"
+#include "library/blast/blast.h"
+
+namespace lean {
+namespace blast {
+bool hypothesis::depends_on(expr const & h) const { return m_deps.contains(href_index(h)); }
+bool hypothesis::is_assumption() const { return !m_value || is_local_non_href(*m_value); }
+}}

src/library/blast/hypothesis.h

@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "util/rc.h"
 #include "util/rb_map.h"
-#include "library/blast/expr.h"
+#include "kernel/expr.h"
 
 namespace lean {
 namespace blast {
@@ -51,8 +51,8 @@ public:
     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. */
-    bool depends_on(expr const & h) const { return m_deps.contains(href_index(h)); }
+    bool depends_on(expr const & h) const;
-    bool is_assumption() const { return !m_value || is_local_non_href(*m_value); }
+    bool is_assumption() const;
 };
 
 class hypothesis_idx_buffer_set {

src/library/blast/init_module.cpp

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "library/blast/expr.h"
 #include "library/blast/state.h"
 #include "library/blast/blast.h"
 #include "library/blast/blast_tactic.h"
@@ -19,7 +18,6 @@ Author: Leonardo de Moura
 namespace lean {
 void initialize_blast_module() {
     blast::initialize_options();
-    blast::initialize_expr();
     blast::initialize_state();
     initialize_blast();
     blast::initialize_simplifier_module();
@@ -40,7 +38,6 @@ void finalize_blast_module() {
     blast::finalize_simplifier_module();
     finalize_blast();
     blast::finalize_state();
-    blast::finalize_expr();
     blast::finalize_options();
 }
 }

src/library/blast/simplifier/simplifier.cpp

@@ -10,7 +10,6 @@
 #include "library/expr_lt.h"
 #include "library/class_instance_resolution.h"
 #include "library/relation_manager.h"
-#include "library/blast/expr.h"
 #include "library/blast/blast_exception.h"
 #include "library/blast/blast.h"
 #include "library/blast/simplifier/simplifier.h"

src/library/blast/state.cpp

@@ -20,6 +20,10 @@ namespace blast {
 static name * g_prefix = nullptr;
 static name * g_H      = nullptr;
 
+bool metavar_decl::contains_href(expr const & h) const {
+    return contains_href(href_index(h));
+}
+
 bool metavar_decl::restrict_context_using(metavar_decl const & other) {
     buffer<unsigned> to_erase;
     m_assumptions.for_each([&](unsigned hidx) {
@@ -140,6 +144,10 @@ branch & branch::operator=(branch s) {
 
 state::state() {}
 
+metavar_decl const * state::get_metavar_decl(expr const & e) const {
+    return get_metavar_decl(mref_index(e));
+}
+
 expr state::mk_metavar(hypothesis_idx_set const & c, expr const & type) {
     unsigned midx = mk_mref_idx();
     m_metavar_decls.insert(midx, metavar_decl(c, type));
@@ -157,6 +165,32 @@ expr state::mk_metavar(expr const & type) {
     return state::mk_metavar(get_assumptions(), type);
 }
 
+bool state::is_uref_assigned(level const & l) const {
+    return m_uassignment.contains(uref_index(l));
+}
+
+/* u := l */
+void state::assign_uref(level const & u, level const & l) {
+    m_uassignment.insert(uref_index(u), l);
+}
+
+level const * state::get_uref_assignment(level const & l) const {
+    return m_uassignment.find(uref_index(l));
+}
+
+bool state::is_mref_assigned(expr const & e) const {
+    lean_assert(is_mref(e));
+    return m_eassignment.contains(mref_index(e));
+}
+
+expr const * state::get_mref_assignment(expr const & e) const {
+    return m_eassignment.find(mref_index(e));
+}
+
+void state::assign_mref(expr const & m, expr const & e) {
+    m_eassignment.insert(mref_index(m), e);
+}
+
 void state::restrict_mref_context_using(expr const & mref1, expr const & mref2) {
     metavar_decl const * d1 = m_metavar_decls.find(mref_index(mref1));
     metavar_decl const * d2 = m_metavar_decls.find(mref_index(mref2));
@@ -167,6 +201,10 @@ void state::restrict_mref_context_using(expr const & mref1, expr const & mref2)
         m_metavar_decls.insert(mref_index(mref1), new_d1);
 }
 
+hypothesis const & state::get_hypothesis_decl(expr const & h) const {
+    return get_hypothesis_decl(href_index(h));
+}
+
 expr state::to_kernel_expr(expr const & e, hypothesis_idx_map<expr> & hidx2local, metavar_idx_map<expr> & midx2meta) const {
     return lean::replace(e, [&](expr const & e) {
             if (is_href(e)) {
@@ -812,6 +850,10 @@ void state::set_target(expr const & t) {
     }
 }
 
+bool state::target_depends_on(expr const & h) const {
+    return target_depends_on(href_index(h));
+}
+
 struct expand_hrefs_fn : public replace_visitor {
     state const &      m_state;
     list<expr> const & m_hrefs;

src/library/blast/state.h

@@ -31,7 +31,7 @@ public:
         m_assumptions(a), m_type(t) {}
     /** \brief Return true iff \c h is in the context of the this metavar declaration */
     bool contains_href(unsigned hidx) const { return m_assumptions.contains(hidx); }
-    bool contains_href(expr const & h) const { return contains_href(href_index(h)); }
+    bool contains_href(expr const & h) const;
     expr const & get_type() const { return m_type; }
     /** \brief Make sure the declaration context of this declaration is a subset of \c other.
         \remark Return true iff the context has been modified. */
@@ -231,7 +231,7 @@ public:
         in the current branch. */
     expr mk_metavar(expr const & type);
     metavar_decl const * get_metavar_decl(hypothesis_idx idx) const { return m_metavar_decls.find(idx); }
-    metavar_decl const * get_metavar_decl(expr const & e) const { return get_metavar_decl(mref_index(e)); }
+    metavar_decl const * get_metavar_decl(expr const & e) const;
 
     /************************
        Save/Restore branch
@@ -284,7 +284,7 @@ public:
     bool hidx_depends_on(hypothesis_idx hidx_user, hypothesis_idx hidx_provider) const;
 
     hypothesis const & get_hypothesis_decl(hypothesis_idx hidx) const { auto h = m_branch.m_hyp_decls.find(hidx); lean_assert(h); return *h; }
-    hypothesis const & get_hypothesis_decl(expr const & h) const { return get_hypothesis_decl(href_index(h)); }
+    hypothesis const & get_hypothesis_decl(expr const & h) const;
 
     void for_each_hypothesis(std::function<void(hypothesis_idx, hypothesis const &)> const & fn) const { m_branch.m_hyp_decls.for_each(fn); }
     optional<hypothesis_idx> find_active_hypothesis(std::function<bool(hypothesis_idx, hypothesis const &)> const & fn) const { // NOLINT
@@ -349,7 +349,7 @@ public:
     expr const & get_target() const { return m_branch.m_target; }
     /** \brief Return true iff the target depends on the given hypothesis */
     bool target_depends_on(hypothesis_idx hidx) const { return m_branch.m_target_deps.contains(hidx); }
-    bool target_depends_on(expr const & h) const { return target_depends_on(href_index(h)); }
+    bool target_depends_on(expr const & h) const;
 
     /************************
        Proof steps
@@ -395,40 +395,26 @@ public:
        Assignment management
     *************************/
 
-    bool is_uref_assigned(level const & l) const {
+    bool is_uref_assigned(level const & l) const;
-        return m_uassignment.contains(uref_index(l));
-    }
-
     /* u := l */
-    void assign_uref(level const & u, level const & l) {
+    void assign_uref(level const & u, level const & l);
-        m_uassignment.insert(uref_index(u), l);
-    }
 
-    level const * get_uref_assignment(level const & l) const {
+    level const * get_uref_assignment(level const & l) const;
-        return m_uassignment.find(uref_index(l));
-    }
 
     /** \brief Make sure the metavariable declaration context of mref1 is a
         subset of the metavariable declaration context of mref2. */
     void restrict_mref_context_using(expr const & mref1, expr const & mref2);
 
-    bool is_mref_assigned(expr const & e) const {
+    bool is_mref_assigned(expr const & e) const;
-        lean_assert(is_mref(e));
-        return m_eassignment.contains(mref_index(e));
-    }
 
     /** \brief Return true iff \c l contains an assigned uref */
     bool has_assigned_uref(level const & l) const;
     bool has_assigned_uref(levels const & ls) const;
 
-    expr const * get_mref_assignment(expr const & e) const {
+    expr const * get_mref_assignment(expr const & e) const;
-        return m_eassignment.find(mref_index(e));
-    }
 
     /* m := e */
-    void assign_mref(expr const & m, expr const & e) {
+    void assign_mref(expr const & m, expr const & e);
-        m_eassignment.insert(mref_index(m), e);
-    }
 
     /** \brief Return true if \c e contains an assigned mref or uref */
     bool has_assigned_uref_mref(expr const & e) const;