feat(library/type_context): use delayed abstraction at type_context (instead of restrict_metavars_context)

src/library/delayed_abstraction.cpp

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "kernel/free_vars.h"
+#include "kernel/abstract.h"
 #include "kernel/abstract_type_context.h"
 #include "library/replace_visitor.h"
 
@@ -239,6 +240,19 @@ expr mk_delayed_abstraction(expr const & e, buffer<name> const & ns, buffer<expr
     }
 }
 
+expr delayed_abstract_locals(expr const & e, unsigned nlocals, expr const * locals) {
+    lean_assert(std::all_of(locals, locals + nlocals, is_local));
+    if (!has_expr_metavar(e))
+        return abstract_locals(e, nlocals, locals);
+    buffer<name> ns;
+    buffer<expr> vs;
+    for (unsigned i = 0; i < nlocals; i++) {
+        ns.push_back(mlocal_name(locals[i]));
+        vs.push_back(mk_var(nlocals - i - 1));
+    }
+    return push_delayed_abstraction_fn(ns, vs)(e);
+}
+
 void initialize_delayed_abstraction() {
     g_delayed_abstraction_macro = new name("delayed_abstraction");
 }

src/library/delayed_abstraction.h

@@ -27,6 +27,11 @@ expr mk_delayed_abstraction_with_locals(expr const & e, buffer<expr> const & ls)
    \pre !ns.empty() */
 expr mk_delayed_abstraction(expr const & e, buffer<name> const & ns, buffer<expr> const & vs);
 
+/* Similar to abstract_locals, but create a delayed_abstraction macro around metavariables
+   occurring in \c e. */
+expr delayed_abstract_locals(expr const & e, unsigned nlocals, expr const * locals);
+inline expr delayed_abstract_local(expr const & e, expr const & s) { return delayed_abstract_locals(e, 1, &s); }
+
 void initialize_delayed_abstraction();
 void finalize_delayed_abstraction();
 }

src/library/type_context.cpp

@@ -281,57 +281,19 @@ expr type_context::revert(buffer<expr> & to_revert, expr const & mvar) {
     return r;
 }
 
-/* Make sure that for any (unassigned) metavariable ?M@C occurring in \c e,
-   \c C does not contain any local in \c locals. This can be achieved by creating new metavariables
-   ?M'@C' where C' is C without any locals (and its dependencies) */
-void type_context::restrict_metavars_context(expr const & e, unsigned num_locals, expr const * locals) {
-    if (!has_expr_metavar(e))
-        return;
-    for_each(e, [&](expr const & e, unsigned) {
-            if (!has_expr_metavar(e)) return false;
-            if (is_metavar_decl_ref(e)) {
-                metavar_decl const & decl  = *m_mctx.get_metavar_decl(e);
-                restrict_metavars_context(decl.get_type(), num_locals, locals);
-                if (optional<expr> v = m_mctx.get_assignment(e)) {
-                    restrict_metavars_context(*v, num_locals, locals);
-                } else {
-                    local_context const &  ctx = decl.get_context();
-                    buffer<expr> to_revert;
-                    for (unsigned i = 0; i < num_locals; i++) {
-                        if (ctx.get_local_decl(locals[i]))
-                            to_revert.push_back(locals[i]);
-                    }
-                    if (!to_revert.empty()) {
-                        revert(to_revert, e);
-                        lean_assert(m_mctx.is_assigned(e));
-                    }
-                }
-            }
-            return true;
-        });
-}
-
-void type_context::restrict_metavars_context(local_decl const & d, unsigned num_locals, expr const * locals) {
-    restrict_metavars_context(d.get_type(), num_locals, locals);
-    if (auto v = d.get_value())
-        restrict_metavars_context(*v, num_locals, locals);
-}
-
+/* We use delayed_abstract_locals to make sure the variables being abstracted
+   will be abstracted correctly when any unassigned metavar ?M occurring in \c e gets instantiated. */
 expr type_context::abstract_locals(expr const & e, unsigned num_locals, expr const * locals) {
     lean_assert(std::all_of(locals, locals+num_locals, is_local_decl_ref));
     if (num_locals == 0)
         return e;
-    if (!in_tmp_mode()) {
-        /* In regular mode, we have to make sure the context of the metavariables occurring \c e
-           does not include the locals being abstracted.
-
-           Claim: this check is not necessary in tmp_mode because
-           1- Regular metavariables should not depend on temporary local constants that have been created in tmp mode.
-           2- The tmp metavariables all share the same fixed local context.
-        */
-        restrict_metavars_context(e, num_locals, locals);
+    if (in_tmp_mode()) {
+        /* 1- Regular metavariables should not depend on temporary local constants that have been created in tmp mode.
+           2- The tmp metavariables all share the same fixed local context. */
+        return ::lean::abstract_locals(e, num_locals, locals);
     }
-    return ::lean::abstract_locals(e, num_locals, locals);
+    expr new_e = instantiate_mvars(e);
+    return delayed_abstract_locals(new_e, num_locals, locals);
 }
 
 expr type_context::mk_binding(bool is_pi, unsigned num_locals, expr const * locals, expr const & e) {

src/library/type_context.h

@@ -357,8 +357,6 @@ private:
     pair<local_context, expr> revert_core(buffer<expr> & to_revert, local_context const & ctx,
                                           expr const & type);
     expr revert_core(buffer<expr> & to_revert, expr const & mvar);
-    void restrict_metavars_context(expr const & e, unsigned num_locals, expr const * locals);
-    void restrict_metavars_context(local_decl const & d, unsigned num_locals, expr const * locals);
     expr mk_binding(bool is_pi, unsigned num_locals, expr const * locals, expr const & e);
 
     /* ------------