max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/type_context): avoid delayed_abstractions when creating binders lambda/pi/let

Browse source 
This is the first step to eliminate the delayed_abstraction macro.
This commit is contained in:
Leonardo de Moura 2018-05-29 16:37:33 -07:00
parent 73f83216c1
commit 7842036aba
4 changed files with 66 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/frontends/lean/elaborator.cpp
View file

@ -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");

8
src/frontends/lean/parser.cpp
View file

@ -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)));

49
src/library/type_context.cpp
View file

@ -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,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<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;
@ -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"}));

1
src/library/type_context.h
View file

@ -876,6 +876,7 @@ private:
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);
/* ------------