From 7842036aba6c20e0ed91f64a60addebd10c84754 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 29 May 2018 16:37:33 -0700 Subject: [PATCH] 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 | 15 +++++++++- src/frontends/lean/parser.cpp | 8 ++++- src/library/type_context.cpp | 49 +++++++++++++++++++++++++++---- src/library/type_context.h | 1 + 4 files changed, 66 insertions(+), 7 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index e415ead8a6..7b47567966 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/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 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 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 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"); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index e6a893940e..a9ac262f7e 100644 --- a/src/frontends/lean/parser.cpp +++ b/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))); diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 1a87fe521f..f9408bdca8 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -289,7 +289,7 @@ static bool process_to_revert(metavar_context const & mctx, buffer & to_re } pair type_context_old::revert_core(buffer & 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,6 +387,44 @@ 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 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 to_revert; + for (unsigned i = 0; i < num; i++) { + if (optional 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 decls; buffer types; @@ -394,13 +432,13 @@ expr type_context_old::mk_binding(bool is_pi, local_context const & lctx, unsign 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"})); diff --git a/src/library/type_context.h b/src/library/type_context.h index 655223f632..1a3611a646 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -876,6 +876,7 @@ private: pair revert_core(buffer & to_revert, local_context const & ctx, expr const & type, bool preserve_to_revert_order); expr revert_core(buffer & 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); /* ------------