From c652eeeac6f14bb392103c130c0f6d20aa90f8df Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 29 Sep 2015 12:27:18 -0700
Subject: [PATCH] feat(library/data/expr): add support for regular local
 constants in blast tactic

We need them when inferring types and checking whether two expressions
are definitionally equal or not.

Remark: they are temporary objects, and should never be included in the
blast state object.
---
 src/library/blast/expr.cpp | 49 +++++++++++++++++++++++++++++++++++---
 src/library/blast/expr.h   |  7 ++++++
 2 files changed, 53 insertions(+), 3 deletions(-)

diff --git a/src/library/blast/expr.cpp b/src/library/blast/expr.cpp
index 881af06ca..c72dbda77 100644
--- a/src/library/blast/expr.cpp
+++ b/src/library/blast/expr.cpp
@@ -153,7 +153,7 @@ static name * g_prefix = nullptr;
 static expr * g_dummy_type = nullptr; // dummy type for href/mref
 
 static expr mk_href_core(unsigned idx) {
-    return mk_local(name(*g_prefix, idx), *g_dummy_type);
+    return lean::mk_local(name(*g_prefix, idx), *g_dummy_type);
 }
 
 expr mk_href(unsigned idx) {
@@ -205,11 +205,34 @@ unsigned href_index(expr const & e) {
 }
 
 bool has_href(expr const & e) {
-    return has_local(e);
+    return lean::has_local(e);
 }
 
 bool has_mref(expr const & e) {
-    return has_expr_metavar(e);
+    return lean::has_expr_metavar(e);
+}
+
+expr mk_local(unsigned idx, expr const & t) {
+    lean_assert(is_cached(t));
+    return cache(lean::mk_local(name(*g_prefix, idx), t));
+}
+
+bool is_local(expr const & e) {
+    return is_local(e) && mlocal_type(e) != *g_dummy_type;
+}
+
+bool has_local(expr const & e) {
+    return lean::has_local(e);
+}
+
+unsigned local_index(expr const & e) {
+    lean_assert(blast::is_local(e));
+    return mlocal_name(e).get_numeral();
+}
+
+expr const & local_type(expr const & e) {
+    lean_assert(blast::is_local(e));
+    return mlocal_type(e);
 }
 
 expr mk_var(unsigned idx) {
@@ -578,6 +601,26 @@ expr abstract_hrefs(expr const & e, unsigned n, expr const * subst) {
         });
 }
 
+expr abstract_locals(expr const & e, unsigned n, expr const * subst) {
+    if (!blast::has_local(e))
+        return e;
+    lean_assert(std::all_of(subst, subst+n, [](expr const & e) { return closed(e) && blast::is_local(e); }));
+    return blast::replace(e, [=](expr const & m, unsigned offset) -> optional<expr> {
+            if (!blast::has_local(m))
+                return some_expr(m); // skip: m does not contain locals
+            if (is_local(m)) {
+                unsigned i = n;
+                while (i > 0) {
+                    --i;
+                    if (local_index(subst[i]) == local_index(m)) //
+                        return some_expr(blast::mk_var(offset + n - i - 1));
+                }
+                return none_expr();
+            }
+            return none_expr();
+        });
+}
+
 void initialize_expr() {
     g_prefix     = new name(name::mk_internal_unique_name());
     g_dummy_type = new expr(mk_constant(*g_prefix));
diff --git a/src/library/blast/expr.h b/src/library/blast/expr.h
index fa8340928..e9c3dc219 100644
--- a/src/library/blast/expr.h
+++ b/src/library/blast/expr.h
@@ -46,6 +46,7 @@ expr mk_href(unsigned idx);
 expr mk_mref(unsigned idx);
 expr mk_sort(level const & l);
 expr mk_constant(name const & n, levels const & ls);
+expr mk_local(unsigned idx, expr const & t);
 expr mk_app(expr const & f, expr const & a);
 expr mk_app(expr const & f, unsigned num_args, expr const * args);
 expr mk_app(unsigned num_args, expr const * args);
@@ -76,6 +77,11 @@ bool has_href(expr const & e);
 /** \brief Return true iff \c e contain mref's */
 bool has_mref(expr const & e);
 
+bool is_local(expr const & e);
+unsigned local_index(expr const & e);
+expr const & local_type(expr const & e);
+bool has_local(expr const & 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);
 
@@ -105,6 +111,7 @@ expr  instantiate_type_univ_params(declaration const & d, levels const & ls);
 expr  instantiate_value_univ_params(declaration const & d, levels const & ls);
 
 expr abstract_hrefs(expr const & e, unsigned n, expr const * s);
+expr abstract_locals(expr const & e, unsigned n, expr const * s);
 
 void initialize_expr();
 void finalize_expr();