feat(library/type_context): avoid delayed_abstractions when creating …

…binders lambda/pi/let

This is the first step to eliminate the delayed_abstraction macro.

src/frontends/lean/elaborator.cpp

@@ -125,6 +125,9 @@ elaborator_strategy get_elaborator_strategy(environment const & env, name const
 #define trace_elab(CODE) lean_trace("elaborator", scope_trace_env _scope(m_env, m_ctx); CODE)
 #define trace_elab_detail(CODE) lean_trace("elaborator_detail", scope_trace_env _scope(m_env, m_ctx); CODE)
 #define trace_elab_debug(CODE) lean_trace("elaborator_debug", scope_trace_env _scope(m_env, m_ctx); CODE)
+#define trace_elab_numeral(CODE) lean_trace(name({"elaborator", "numeral"}), scope_trace_env _scope(m_env, m_ctx); CODE)
+#define trace_elab_instances(CODE) lean_trace(name({"elaborator", "instances"}), scope_trace_env _scope(m_env, m_ctx); CODE)
+#define trace_elab_equation(CODE) lean_trace(name({"elaborator", "equation"}), scope_trace_env _scope(m_env, m_ctx); CODE)
 
 elaborator::elaborator(environment const & env, options const & opts, name const & decl_name,
                        metavar_context const & mctx, local_context const & lctx, bool recover_from_errors,
@@ -2594,6 +2597,7 @@ expr elaborator::visit_equation(expr const & e, unsigned num_fns) {
     if (is_no_equation(it)) {
         return fns.mk_lambda(it);
     } else {
+        trace_elab_equation(tout() << "visit_equation\n";);
         metavar_context mctx0 = m_ctx.mctx();
         it = instantiate_rev_locals(it, fns);
         buffer<expr> local_mvars;
@@ -2622,7 +2626,9 @@ expr elaborator::visit_equation(expr const & e, unsigned num_fns) {
             new_lhs = visit(lhs, none_expr());
             synthesize_no_tactics();
         }
+        trace_elab_equation(tout() << "new_lhs:\n" << new_lhs << "\n";);
         new_lhs = instantiate_pattern_mvars(m_ctx, new_lhs);
+        trace_elab_equation(tout() << "new_lhs (after instantiate_pattern_mvars):\n" << new_lhs << "\n";);
         // collect unassigned metavariables not in mctx0
         buffer<expr> unassigned_mvars;
         validate_and_collect_lhs_mvars(*this, ref, mctx0, unassigned_mvars)(new_lhs);
@@ -2673,6 +2679,7 @@ expr elaborator::visit_equation(expr const & e, unsigned num_fns) {
         // new_rhs       = instantiate_mvars(new_rhs);
         new_rhs       = enforce_type(new_rhs, new_lhs_type, "equation type mismatch", it);
         expr new_eq = copy_tag(it, mk_equation(new_lhs, new_rhs, ignore_equation_if_unused(it)));
+        trace_elab_equation(tout() << new_eq << "\n";);
         expr r = copy_tag(ref, fns.mk_lambda(new_locals.mk_lambda(new_eq)));
         return r;
     }
@@ -3516,6 +3523,7 @@ expr elaborator::visit_let(expr const & e, optional<expr> const & expected_type)
     save_identifier_info(l);
     expr body      = instantiate_rev_locals(let_body(e), locals);
     expr new_body  = visit(body, expected_type);
+    /* TODO(Leo): add synthesize here? */
     expr new_e     = locals.mk_lambda(new_body);
     return new_e;
 }
@@ -3660,7 +3668,8 @@ expr elaborator::get_default_numeral_type() {
 
 void elaborator::synthesize_numeral_types() {
     for (expr const & A : m_numeral_types) {
-        if (is_metavar(instantiate_mvars(A))) {
+        trace_elab_numeral(tout() << "synthesize num type: " << A << ", " << instantiate_mvars(A) << "\n";);
+        if (is_meta(instantiate_mvars(A))) {
             if (!is_def_eq(A, get_default_numeral_type()))
                 report_or_throw(elaborator_exception(A, "invalid numeral, failed to force numeral to be a nat"));
         }
@@ -3674,6 +3683,7 @@ bool elaborator::synthesize_type_class_instance_core(expr const & mvar, expr con
     metavar_decl mdecl = m_ctx.mctx().get_metavar_decl(mvar);
     expr ref = mvar;
     expr synthesized_inst = mk_instance_core(mdecl.get_context(), inst_type, ref);
+    trace_elab_instances(tout() << inferred_inst << " =?= " << synthesized_inst << "\n";);
     if (!m_ctx.is_def_eq_at(mdecl.get_context(), inferred_inst, synthesized_inst)) {
         auto pp_fn = mk_pp_ctx();
         throw elaborator_exception(mvar,
@@ -4341,6 +4351,9 @@ static vm_obj tactic_save_type_info(vm_obj const &, vm_obj const & _e, vm_obj co
 void initialize_elaborator() {
     g_elab_strategy = new name("elab_strategy");
     register_trace_class("elaborator");
+    register_trace_class(name({"elaborator", "numeral"}));
+    register_trace_class(name({"elaborator", "instances"}));
+    register_trace_class(name({"elaborator", "equation"}));
     register_trace_class("elaborator_detail");
     register_trace_class("elaborator_debug");
 

src/frontends/lean/parser.cpp

@@ -1756,7 +1756,13 @@ static expr quote(expr const & e) {
             throw elaborator_exception(e, sstream() << "invalid quotation, unexpected local constant '"
                                                     << mlocal_pp_name(e) << "'");
         case expr_kind::App:
-            return mk_app(mk_constant({"expr", "app"}), quote(app_fn(e)), quote(app_arg(e)));
+            if (is_meta(e)) {
+                /* Remark: metavariable applications of the form `?m x1 ... xn` may be introduced
+                   by type_context::elim_mvar_deps when we create lambda/pi-expressions. */
+                return mk_expr_placeholder();
+            } else {
+                return mk_app(mk_constant({"expr", "app"}), quote(app_fn(e)), quote(app_arg(e)));
+            }
         case expr_kind::Lambda:
             return mk_app(mk_constant({"expr", "lam"}), mk_expr_placeholder(), mk_expr_placeholder(),
                           quote(binding_domain(e)), quote(binding_body(e)));

src/library/type_context.cpp

@@ -289,7 +289,7 @@ static bool process_to_revert(metavar_context const & mctx, buffer<expr> & to_re
 }
 
 pair<local_context, expr> type_context_old::revert_core(buffer<expr> & to_revert, local_context const & ctx,
-                                                    expr const & type, bool preserve_to_revert_order) {
+                                                        expr const & type, bool preserve_to_revert_order) {
     unsigned num   = to_revert.size();
     if (num == 0)
         return mk_pair(ctx, type);
@@ -387,20 +387,58 @@ expr type_context_old::abstract_locals(expr const & e, unsigned num_locals, expr
     return delayed_abstract_locals(m_mctx, new_e, num_locals, locals);
 }
 
+/* For every metavariable `?m` occurring at `e`, revert all locals in `?m` that are in `locals` (or depend on them) and obtain `?m1`.
+   `?m` is replaced with `?m1 x_1 ... x_n` where `x_1 ... x_n` are the reverted locals. */
+expr type_context_old::elim_mvar_deps(expr const & e, unsigned num, expr const * locals) {
+    if (num == 0)
+        return e;
+    expr new_e = instantiate_mvars(e);
+    if (!has_expr_metavar(new_e))
+        return new_e;
+    lean_trace(name({"type_context", "mvar_deps"}), tout() << "elim_mvar_deps:\n" << new_e << "\n";);
+    return replace(new_e, [&](expr const & m, unsigned) {
+            if (!has_expr_metavar(m)) {
+                return some_expr(m);
+            } else if (is_metavar_decl_ref(m)) {
+                if (optional<expr> const & v = m_mctx.get_assignment(m)) {
+                    /* We don't need to visit v, since this assignment
+                       was created by this procedure. */
+                    return v;
+                } else {
+                    metavar_decl const & d     = m_mctx.get_metavar_decl(m);
+                    local_context const & lctx = d.get_context();
+                    buffer<expr> to_revert;
+                    for (unsigned i = 0; i < num; i++) {
+                        if (optional<local_decl> decl = lctx.find_local_decl(locals[i])) {
+                            to_revert.push_back(locals[i]);
+                        }
+                    }
+                    if (to_revert.empty())
+                        return some_expr(m);
+                    bool preserve_to_revert_order = false;
+                    expr new_m = revert(to_revert, m, preserve_to_revert_order);
+                    lean_trace(name({"type_context", "mvar_deps"}), tout() << m << " ==> " << new_m << "\n";);
+                    return some_expr(new_m);
+                }
+            }
+            return none_expr();
+        });
+}
+
 expr type_context_old::mk_binding(bool is_pi, local_context const & lctx, unsigned num_locals, expr const * locals, expr const & e) {
     buffer<local_decl>     decls;
     buffer<expr>           types;
     buffer<optional<expr>> values;
     for (unsigned i = 0; i < num_locals; i++) {
         local_decl decl = lctx.get_local_decl(locals[i]);
         decls.push_back(decl);
-        types.push_back(abstract_locals(instantiate_mvars(decl.get_type()), i, locals));
+        types.push_back(::lean::abstract_locals(elim_mvar_deps(decl.get_type(), i, locals), i, locals));
         if (auto v = decl.get_value())
-            values.push_back(some_expr(abstract_locals(instantiate_mvars(*v), i, locals)));
+            values.push_back(some_expr(::lean::abstract_locals(elim_mvar_deps(*v, i, locals), i, locals)));
         else
             values.push_back(none_expr());
     }
-    expr new_e = abstract_locals(instantiate_mvars(e), num_locals, locals);
+    expr new_e = ::lean::abstract_locals(elim_mvar_deps(e, num_locals, locals), num_locals, locals);
     lean_assert(types.size() == values.size());
     unsigned i = types.size();
     while (i > 0) {
@@ -1083,7 +1121,7 @@ expr type_context_old::infer_lambda(expr e) {
     }
     check_system("infer_type");
     expr t = infer_core(instantiate_rev(e, ls.size(), ls.data()));
-    expr r = abstract_locals(t, ls.size(), ls.data());
+    expr r = ::lean::abstract_locals(t, ls.size(), ls.data());
     unsigned i = es.size();
     while (i > 0) {
         --i;
@@ -4256,6 +4294,7 @@ mk_pp_ctx(type_context_old const & ctx) {
 void initialize_type_context() {
     register_trace_class("class_instances");
     register_trace_class(name({"type_context", "is_def_eq"}));
+    register_trace_class(name({"type_context", "mvar_deps"}));
     register_trace_class(name({"type_context", "is_def_eq_detail"}));
     register_trace_class(name({"type_context", "univ_is_def_eq"}));
     register_trace_class(name({"type_context", "univ_is_def_eq_detail"}));

src/library/type_context.h

@@ -876,6 +876,7 @@ class type_context_old : public abstract_type_context {
     pair<local_context, expr> revert_core(buffer<expr> & to_revert, local_context const & ctx,
                                           expr const & type, bool preserve_to_revert_order);
     expr revert_core(buffer<expr> & to_revert, expr const & mvar, bool preserve_to_revert_order);
+    expr elim_mvar_deps(expr const & e, unsigned num, expr const * locals);
     expr mk_binding(bool is_pi, local_context const & lctx, unsigned num_locals, expr const * locals, expr const & e);
 
     /* ------------