refactor(library/blast): use simpler encoding for lref and mref

src/library/blast/expr.cpp

@@ -23,66 +23,6 @@ Author: Leonardo de Moura
 
 namespace lean {
 namespace blast {
-/** \brief Auxiliary macro used to encode mref and lref expressions used by the blast tactic
-    \remark This macro should never occur in fully elaborated terms. */
-class ref_definition_cell : public macro_definition_cell {
-    bool     m_local;
-    unsigned m_idx;
-public:
-    ref_definition_cell(bool local, unsigned idx):m_local(local), m_idx(idx) {}
-
-    bool     is_local() const { return m_local; }
-    unsigned get_index() const { return m_idx; }
-
-    virtual name get_name() const { return name("ref"); }
-
-    virtual pair<expr, constraint_seq> check_type(expr const &, extension_context &, bool) const {
-        lean_unreachable();
-    }
-
-    virtual optional<expr> expand(expr const &, extension_context &) const {
-        lean_unreachable();
-    }
-
-    virtual void write(serializer &) const {
-        lean_unreachable();
-    }
-
-    virtual bool operator==(macro_definition_cell const & other) const {
-        return
-            dynamic_cast<ref_definition_cell const *>(&other) != nullptr &&
-            m_idx   == static_cast<ref_definition_cell const&>(other).m_idx &&
-            m_local == static_cast<ref_definition_cell const&>(other).m_local;
-    }
-
-    virtual unsigned hash() const { return lean::hash(m_local, m_idx); }
-};
-
-static expr mk_lref_core(unsigned idx) {
-    return lean::mk_macro(macro_definition(new ref_definition_cell(true, idx)), 0, nullptr);
-}
-
-static expr mk_mref_core(unsigned idx) {
-    return lean::mk_macro(macro_definition(new ref_definition_cell(false, idx)), 0, nullptr);
-}
-
-bool is_lmref(expr const & e) {
-    return is_macro(e) && dynamic_cast<ref_definition_cell const *>(macro_def(e).raw());
-}
-
-bool is_lref(expr const & e) {
-    return is_lmref(e) && static_cast<ref_definition_cell const *>(macro_def(e).raw())->is_local();
-}
-
-bool is_mref(expr const & e) {
-    return is_lmref(e) && !is_lref(e);
-}
-
-unsigned lmref_index(expr const & e) {
-    lean_assert(is_lmref(e));
-    return static_cast<ref_definition_cell const *>(macro_def(e).raw())->get_index();
-}
-
 typedef typename std::unordered_set<expr, expr_hash, is_bi_equal_proc> expr_table;
 typedef typename std::unordered_set<level, level_hash>                 level_table;
 typedef typename std::vector<expr>                                     expr_array;
@@ -209,17 +149,11 @@ level update_max(level const & l, level const & new_lhs, level const & new_rhs)
     }
 }
 
-expr mk_var(unsigned idx) {
+static name * g_prefix = nullptr;
-    lean_assert(g_var_array);
+static expr * g_dummy_type = nullptr; // dummy type for lref/mref
-    lean_assert(g_expr_table);
+
-    while (g_var_array->size() <= idx) {
+static expr mk_lref_core(unsigned idx) {
-        unsigned j   = g_var_array->size();
+    return mk_local(name(*g_prefix, idx), *g_dummy_type);
-        expr new_var = lean::mk_var(j);
-        g_var_array->push_back(new_var);
-        g_expr_table->insert(new_var);
-    }
-    lean_assert(idx < g_var_array->size());
-    return (*g_var_array)[idx];
 }
 
 expr mk_lref(unsigned idx) {
@@ -235,6 +169,14 @@ expr mk_lref(unsigned idx) {
     return (*g_lref_array)[idx];
 }
 
+bool is_lref(expr const & e) {
+    return is_local(e) && mlocal_type(e) == *g_dummy_type;
+}
+
+static expr mk_mref_core(unsigned idx) {
+    return mk_metavar(name(*g_prefix, idx), *g_dummy_type);
+}
+
 expr mk_mref(unsigned idx) {
     lean_assert(g_mref_array);
     lean_assert(g_expr_table);
@@ -248,6 +190,33 @@ expr mk_mref(unsigned idx) {
     return (*g_mref_array)[idx];
 }
 
+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 lref_index(expr const & e) {
+    lean_assert(is_lref(e));
+    return mlocal_name(e).get_numeral();
+}
+
+expr mk_var(unsigned idx) {
+    lean_assert(g_var_array);
+    lean_assert(g_expr_table);
+    while (g_var_array->size() <= idx) {
+        unsigned j   = g_var_array->size();
+        expr new_var = lean::mk_var(j);
+        g_var_array->push_back(new_var);
+        g_expr_table->insert(new_var);
+    }
+    lean_assert(idx < g_var_array->size());
+    return (*g_var_array)[idx];
+}
+
 expr mk_app(expr const & f, expr const & a) {
     lean_assert(is_cached(f));
     lean_assert(is_cached(a));
@@ -351,8 +320,12 @@ class replace_rec_fn {
             switch (e.kind()) {
             case expr_kind::Constant: case expr_kind::Sort: case expr_kind::Var:
                 return save_result(e, offset, e);
-            case expr_kind::Meta:     case expr_kind::Local:
+            case expr_kind::Meta:
-                lean_unreachable();
+                lean_assert(is_mref(e));
+                return save_result(e, offset, e);
+            case expr_kind::Local:
+                lean_assert(is_lref(e));
+                return save_result(e, offset, e);
             case expr_kind::App: {
                 expr new_f = apply(app_fn(e), offset);
                 expr new_a = apply(app_arg(e), offset);
@@ -592,5 +565,14 @@ expr abstract_lrefs(expr const & e, unsigned n, expr const * subst) {
             return none_expr();
         });
 }
+
+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

@@ -40,8 +40,8 @@ level mk_global_univ(name const & n);
 level mk_meta_univ(name const & n);
 
 expr mk_var(unsigned idx);
-// Remark: lref and mref expressions are implemented using kernel macros.
+// mk_lref and mk_mref are helper functions for creating local constants and meta-variables used in the blast tactic.
-// We use them to encode local constants and meta-variables in the blast tactic.
+// Remark: the local constants and metavariables manipulated by the blast tactic do **not** store their types.
 expr mk_lref(unsigned idx);
 expr mk_mref(unsigned idx);
 expr mk_sort(level const & l);
@@ -67,15 +67,10 @@ inline expr mk_lambda(name const & n, expr const & t, expr const & e) {
 }
 expr mk_macro(macro_definition const & m, unsigned num, expr const * args);
 
-// Return true iff \c e is a lref of mref.
-bool is_lmref(expr const & e);
-bool is_mref(expr const & e);
 bool is_lref(expr const & e);
-/** \brief Return the index of the give lref/mref.
+unsigned lref_index(expr const & e);
-    \pre is_mref(e) || is_lref(e) */
+bool is_mref(expr const & e);
-unsigned lmref_index(expr const & e);
+unsigned mref_index(expr const & e);
-inline unsigned mref_index(expr const & e) { return lmref_index(e); }
-inline unsigned lref_index(expr const & e) { return lmref_index(e); }
 
 level update_succ(level const & l, level const & new_arg);
 level update_max(level const & l, level const & new_lhs, level const & new_rhs);
@@ -83,6 +78,7 @@ level update_max(level const & l, level const & new_lhs, level const & new_rhs);
 level replace(level const & l, std::function<optional<level>(level const & l)> const & f);
 
 expr update_app(expr const & e, expr const & new_fn, expr const & new_arg);
+expr update_metavar(expr const & e, expr const & new_type);
 expr update_binding(expr const & e, expr const & new_domain, expr const & new_body);
 expr update_sort(expr const & e, level const & new_level);
 expr update_constant(expr const & e, levels const & new_levels);
@@ -105,5 +101,8 @@ expr  instantiate_type_univ_params(declaration const & d, levels const & ls);
 expr  instantiate_value_univ_params(declaration const & d, levels const & ls);
 
 expr abstract_lrefs(expr const & e, unsigned n, expr const * s);
+
+void initialize_expr();
+void finalize_expr();
 }
 }

src/library/blast/init_module.cpp

@@ -4,15 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "library/blast/expr.h"
 #include "library/blast/blast.h"
 #include "library/blast/blast_tactic.h"
 
 namespace lean {
 void initialize_blast_module() {
+    blast::initialize_expr();
     initialize_blast();
     initialize_blast_tactic();
 }
 void finalize_blast_module() {
+    blast::finalize_expr();
     finalize_blast();
     finalize_blast_tactic();
 }