From 9b84db083dfd46a89855e4e6b1938169a3caf9f2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 15 Oct 2016 13:40:57 -0700 Subject: [PATCH] fix(frontends/lean): error localization bugs --- src/frontends/lean/brackets.cpp | 9 ++++--- src/frontends/lean/builtin_exprs.cpp | 33 +++++++++++++------------- src/frontends/lean/decl_util.cpp | 30 +++++++++++++++++++++-- src/frontends/lean/decl_util.h | 4 ++++ src/frontends/lean/definition_cmds.cpp | 12 +++++----- src/frontends/lean/elaborator.cpp | 3 ++- src/frontends/lean/match_expr.cpp | 2 +- src/frontends/lean/structure_cmd.cpp | 8 +++---- src/frontends/lean/util.cpp | 10 ++++++++ src/frontends/lean/util.h | 2 ++ tests/lean/error_pos.lean | 3 +++ tests/lean/error_pos.lean.expected.out | 8 ++++++- 12 files changed, 90 insertions(+), 34 deletions(-) diff --git a/src/frontends/lean/brackets.cpp b/src/frontends/lean/brackets.cpp index a857e635c5..7af13b4762 100644 --- a/src/frontends/lean/brackets.cpp +++ b/src/frontends/lean/brackets.cpp @@ -19,7 +19,8 @@ static expr parse_subtype(parser & p, pos_info const & pos, expr const & local) p.add_local(local); expr pred = p.parse_expr(); p.check_token_next(get_rcurly_tk(), "invalid subtype, '}' expected"); - pred = p.save_pos(Fun(local, pred), pos); + bool use_cache = false; + pred = p.save_pos(Fun(local, pred, use_cache), pos); expr subtype = p.save_pos(mk_constant(get_subtype_name()), pos); return p.mk_app(subtype, pred, pos); } @@ -30,7 +31,8 @@ static expr parse_set_of(parser & p, pos_info const & pos, expr const & local) { p.add_local(local); expr pred = p.parse_expr(); p.check_token_next(get_rcurly_tk(), "invalid set_of, '}' expected"); - pred = p.save_pos(Fun(local, pred), pos); + bool use_cache = false; + pred = p.save_pos(Fun(local, pred, use_cache), pos); expr set_of = p.save_pos(mk_constant(get_set_of_name()), pos); return p.mk_app(set_of, pred, pos); } @@ -69,7 +71,8 @@ static expr parse_sep(parser & p, pos_info const & pos, name const & id) { p.add_local(local); expr pred = p.parse_expr(); p.check_token_next(get_rcurly_tk(), "invalid sep expression, '}' expected"); - pred = Fun(local, pred); + bool use_cache = false; + pred = p.rec_save_pos(Fun(local, pred, use_cache), pos); return p.rec_save_pos(mk_app(mk_constant(get_sep_name()), pred, s), pos); } diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index c0a01d7ecc..06734f7021 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -140,7 +140,7 @@ static expr parse_let(parser & p, pos_info const & pos) { expr body = parse_let_body(p, pos); match_definition_scope match_scope; expr fn = p.save_pos(mk_local(mk_fresh_name(), *g_let_match_name, mk_expr_placeholder(), binder_info()), pos); - expr eqn = p.rec_save_pos(Fun(fn, Fun(new_locals, p.save_pos(mk_equation(p.rec_save_pos(mk_app(fn, lhs), pos), body), pos), p)), pos); + expr eqn = Fun(fn, Fun(new_locals, p.save_pos(mk_equation(p.rec_save_pos(mk_app(fn, lhs), pos), body), pos), p), p); equations_header h = mk_equations_header(match_scope.get_name()); expr eqns = p.save_pos(mk_equations(h, 1, &eqn), pos); return p.save_pos(mk_app(eqns, value), pos); @@ -203,7 +203,7 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional con p.add_local(*prev_local); auto proof_pos = p.pos(); proof = parse_proof(p); - proof = p.save_pos(Fun(*prev_local, proof), proof_pos); + proof = Fun(*prev_local, proof, p); proof = p.save_pos(mk_app(proof, *prev_local), proof_pos); } else { proof = parse_proof(p); @@ -260,7 +260,7 @@ static expr parse_suppose(parser & p, unsigned, expr const *, pos_info const & p expr l = p.save_pos(mk_local(id, prop), id_pos); p.add_local(l); expr body = p.parse_expr(); - return p.save_pos(Fun(l, body), pos); + return p.save_pos(Fun(l, body, p), pos); } static expr parse_show(parser & p, unsigned, expr const *, pos_info const & pos) { @@ -303,7 +303,7 @@ static expr parse_suffices(parser & p, unsigned, expr const *, pos_info const & p.add_local(local); body = parse_proof(p); } - expr proof = p.save_pos(Fun(local, body), pos); + expr proof = p.save_pos(Fun(local, body, p), pos); p.check_token_next(get_comma_tk(), "invalid 'suffices' declaration, ',' expected"); expr rest = p.parse_expr(); expr r = p.mk_app(proof, rest, pos); @@ -331,7 +331,7 @@ static expr parse_dite(parser & p, name const & H_name, expr const & c, pos_info expr H = mk_local(H_name, c); p.add_local(H); auto pos = p.pos(); - t = p.save_pos(Fun(H, p.parse_expr(g_then_else_prec)), pos); + t = p.save_pos(Fun(H, p.parse_expr(g_then_else_prec), p), pos); } p.check_token_next(get_else_tk(), "invalid 'if-then-else' expression, 'else' expected"); { @@ -339,7 +339,7 @@ static expr parse_dite(parser & p, name const & H_name, expr const & c, pos_info expr H = mk_local(H_name, mk_app(*g_not, c)); p.add_local(H); auto pos = p.pos(); - e = p.save_pos(Fun(H, p.parse_expr(g_then_else_prec)), pos); + e = p.save_pos(Fun(H, p.parse_expr(g_then_else_prec), p), pos); } return p.save_pos(mk_app(p.save_pos(mk_constant(get_dite_name()), pos), c, t, e), pos); } @@ -522,7 +522,7 @@ static expr parse_do(parser & p, unsigned, expr const *, pos_info const &) { --i; if (auto lhs = lhss[i]) { if (is_local(*lhs)) { - r = p.rec_save_pos(mk_app(p.save_pos(mk_constant(get_monad_bind_name()), ps[i]), es[i], Fun(*lhs, r)), ps[i]); + r = p.rec_save_pos(mk_app(p.save_pos(mk_constant(get_monad_bind_name()), ps[i]), es[i], Fun(*lhs, r, p)), ps[i]); } else { // must introduce a "fake" match auto pos = ps[i]; @@ -531,15 +531,14 @@ static expr parse_do(parser & p, unsigned, expr const *, pos_info const &) { buffer locals; to_buffer(lhss_locals[i], locals); buffer eqs; - eqs.push_back(p.rec_save_pos(Fun(fn, Fun(locals, p.save_pos(mk_equation(p.rec_save_pos(mk_app(fn, *lhs), pos), r), pos), p)), pos)); + eqs.push_back(Fun(fn, Fun(locals, p.save_pos(mk_equation(p.rec_save_pos(mk_app(fn, *lhs), pos), r), pos), p), p)); if (optional else_case = else_cases[i]) { // add case // _ := else_case expr x = mk_local(mk_fresh_name(), "_x", mk_expr_placeholder(), binder_info()); - eqs.push_back(p.rec_save_pos(Fun(fn, Fun(x, p.save_pos(mk_equation(p.rec_save_pos(mk_app(fn, x), pos), - *else_case), - pos))), - pos)); + eqs.push_back(Fun(fn, Fun(x, p.save_pos(mk_equation(p.rec_save_pos(mk_app(fn, x), pos), + *else_case), + pos), p), p)); } equations_header h = mk_equations_header(match_scope.get_name()); expr eqns = p.save_pos(mk_equations(h, eqs.size(), eqs.data()), pos); @@ -547,7 +546,7 @@ static expr parse_do(parser & p, unsigned, expr const *, pos_info const &) { expr match = p.mk_app(eqns, local, pos); r = p.rec_save_pos(mk_app(p.save_pos(mk_constant(get_monad_bind_name()), ps[i]), es[i], - p.save_pos(Fun(local, match), pos)), + p.save_pos(Fun(local, match, p), pos)), pos); } } else { @@ -669,7 +668,8 @@ static expr parse_lambda_binder(parser & p, pos_info const & pos) { } else { throw parser_error("invalid lambda expression, ',' or '⟨' expected", p.pos()); } - return p.rec_save_pos(Fun(locals, body), pos); + bool use_cache = false; + return p.rec_save_pos(Fun(locals, body, use_cache), pos); } static name * g_lambda_match_name = nullptr; @@ -692,10 +692,11 @@ static expr parse_lambda_constructor(parser & p, pos_info const & ini_pos) { } match_definition_scope match_scope; expr fn = p.save_pos(mk_local(mk_fresh_name(), *g_lambda_match_name, mk_expr_placeholder(), binder_info()), pos); - expr eqn = p.rec_save_pos(Fun(fn, Fun(locals, p.save_pos(mk_equation(p.rec_save_pos(mk_app(fn, pattern), pos), body), pos), p)), pos); + expr eqn = Fun(fn, Fun(locals, p.save_pos(mk_equation(p.rec_save_pos(mk_app(fn, pattern), pos), body), pos), p), p); equations_header h = mk_equations_header(match_scope.get_name()); expr x = p.rec_save_pos(mk_local(mk_fresh_name(), "_x", mk_expr_placeholder(), binder_info()), pos); - return p.rec_save_pos(Fun(x, mk_app(mk_equations(h, 1, &eqn), x)), pos); + bool use_cache = false; + return p.rec_save_pos(Fun(x, mk_app(mk_equations(h, 1, &eqn), x), use_cache), pos); } static expr parse_lambda_core(parser & p, pos_info const & pos) { diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp index 4b48a32680..15f5de731d 100644 --- a/src/frontends/lean/decl_util.cpp +++ b/src/frontends/lean/decl_util.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/abstract.h" #include "kernel/for_each_fn.h" +#include "kernel/replace_fn.h" #include "library/locals.h" #include "library/trace.h" #include "library/placeholder.h" @@ -213,6 +214,31 @@ void update_univ_parameters(parser & p, buffer & lp_names, name_set const }); } +expr replace_locals_preserving_pos_info(expr const & e, unsigned sz, expr const * from, expr const * to) { + bool use_cache = false; + return replace(e, [&](expr const & e, unsigned) { + if (is_local(e)) { + unsigned i = sz; + while (i > 0) { + --i; + if (mlocal_name(from[i]) == mlocal_name(e)) { + return some_expr(copy_tag(e, copy(to[i]))); + } + } + } + return none_expr(); + }, use_cache); +} + +expr replace_locals_preserving_pos_info(expr const & e, buffer const & from, buffer const & to) { + lean_assert(from.size() == to.size()); + return replace_locals_preserving_pos_info(e, from.size(), from.data(), to.data()); +} + +expr replace_local_preserving_pos_info(expr const & e, expr const & from, expr const & to) { + return replace_locals_preserving_pos_info(e, 1, &from, &to); +} + void collect_implicit_locals(parser & p, buffer & lp_names, buffer & params, buffer const & all_exprs) { collected_locals locals; buffer include_vars; @@ -250,7 +276,7 @@ void collect_implicit_locals(parser & p, buffer & lp_names, buffer & expr & param = params[i]; old_params.push_back(param); expr type = mlocal_type(param); - expr new_type = copy_tag(type, replace_locals(type, i, old_params.data(), params.data())); + expr new_type = replace_locals_preserving_pos_info(type, i, old_params.data(), params.data()); if (!given_params.contains(mlocal_name(param))) { new_type = copy_tag(type, mk_as_is(new_type)); } @@ -271,7 +297,7 @@ void collect_implicit_locals(parser & p, buffer & lp_names, buffer & void elaborate_params(elaborator & elab, buffer const & params, buffer & new_params) { for (unsigned i = 0; i < params.size(); i++) { expr const & param = params[i]; - expr type = copy_tag(mlocal_type(param), replace_locals(mlocal_type(param), i, params.data(), new_params.data())); + expr type = replace_locals_preserving_pos_info(mlocal_type(param), i, params.data(), new_params.data()); expr new_type = elab.elaborate_type(type); expr new_param = elab.push_local(local_pp_name(param), new_type, local_info(param)); new_params.push_back(new_param); diff --git a/src/frontends/lean/decl_util.h b/src/frontends/lean/decl_util.h index dce80f7281..8a41dca885 100644 --- a/src/frontends/lean/decl_util.h +++ b/src/frontends/lean/decl_util.h @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include "kernel/expr.h" +#include "library/deep_copy.h" #include "library/equations_compiler/equations.h" #include "frontends/lean/decl_attributes.h" namespace lean { @@ -122,4 +123,7 @@ public: It uses the information set using declaration_info_scope */ equations_header mk_equations_header(list const & fn_names); equations_header mk_equations_header(name const & fn_name); + +expr replace_locals_preserving_pos_info(expr const & e, buffer const & from, buffer const & to); +expr replace_local_preserving_pos_info(expr const & e, expr const & from, expr const & to); } diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index a678ebf6dd..2c09453328 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -132,7 +132,7 @@ expr parse_mutual_definition(parser & p, buffer & lp_names, buffer & throw parser_error("unexpected 'with' clause", p.pos()); optional R_Rwf = parse_using_well_founded(p); for (expr & eq : eqns) { - eq = replace_locals(eq, pre_fns, fns); + eq = replace_locals_preserving_pos_info(eq, pre_fns, fns); } expr r = mk_equations(p, fns, full_names, eqns, R_Rwf, header_pos); collect_implicit_locals(p, lp_names, params, r); @@ -147,7 +147,7 @@ environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif elaborator elab(p.env(), p.get_options(), metavar_context(), local_context()); buffer new_params; elaborate_params(elab, params, new_params); - val = replace_locals(val, params, new_params); + val = replace_locals_preserving_pos_info(val, params, new_params); // TODO(Leo) for (auto p : new_params) { tout() << ">> " << p << " : " << mlocal_type(p) << "\n"; } @@ -193,10 +193,10 @@ static expr_pair parse_definition(parser & p, buffer & lp_names, buffer const & params, buffer const & new_params, expr & fn, expr & val) { - expr fn_type = replace_locals(mlocal_type(fn), params, new_params); + expr fn_type = replace_locals_preserving_pos_info(mlocal_type(fn), params, new_params); expr new_fn = update_mlocal(fn, fn_type); - val = replace_locals(val, params, new_params); - val = replace_local(val, fn, new_fn); + val = replace_locals_preserving_pos_info(val, params, new_params); + val = replace_local_preserving_pos_info(val, fn, new_fn); fn = new_fn; } @@ -204,7 +204,7 @@ static expr_pair elaborate_theorem(elaborator & elab, expr const & fn, expr val) expr fn_type = elab.elaborate_type(mlocal_type(fn)); elab.ensure_no_unassigned_metavars(fn_type); expr new_fn = update_mlocal(fn, fn_type); - val = replace_local(val, fn, new_fn); + val = replace_local_preserving_pos_info(val, fn, new_fn); return elab.elaborate_with_type(val, mk_as_is(fn_type)); } diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 389281e675..61ae1cc172 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -2088,7 +2088,8 @@ expr elaborator::visit_let(expr const & e, optional const & expected_type) expr new_type = visit(let_type(e), none_expr()); synthesize_no_tactics(); expr new_value = visit(let_value(e), some_expr(new_type)); - new_value = enforce_type(new_value, new_type, "invalid let-expression", let_value(e)); + expr ref_value = get_ref_for_child(let_value(e), ref); + new_value = enforce_type(new_value, new_type, "invalid let-expression", ref_value); synthesize(); new_type = instantiate_mvars(new_type); new_value = instantiate_mvars(new_value); diff --git a/src/frontends/lean/match_expr.cpp b/src/frontends/lean/match_expr.cpp index e234596c3f..ba68d34726 100644 --- a/src/frontends/lean/match_expr.cpp +++ b/src/frontends/lean/match_expr.cpp @@ -71,7 +71,7 @@ expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) { for (expr const & local : locals) p.add_local(local); expr rhs = p.parse_expr(); - eqns.push_back(Fun(fn, Fun(locals, p.save_pos(mk_equation(lhs, rhs), assign_pos), p))); + eqns.push_back(Fun(fn, Fun(locals, p.save_pos(mk_equation(lhs, rhs), assign_pos), p), p)); } if (!is_eqn_prefix(p)) break; diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 6f854a0d57..1005d55942 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -663,13 +663,13 @@ struct structure_cmd_fn { } expr mk_structure_type() { - return Pi(m_params, m_type); + return Pi(m_params, m_type, m_p); } expr mk_intro_type() { levels ls = param_names_to_levels(to_list(m_level_names.begin(), m_level_names.end())); expr r = mk_app(mk_constant(m_name, ls), m_params); - r = Pi(m_params, Pi(m_fields, r)); + r = Pi(m_params, Pi(m_fields, r, m_p), m_p); return infer_implicit_params(r, m_params.size(), m_mk_infer); } @@ -802,7 +802,7 @@ struct structure_cmd_fn { if (m_attrs.has_class()) bi = mk_inst_implicit_binder_info(); expr st = mk_local(mk_fresh_name(), "s", st_type, bi); - expr coercion_type = infer_implicit(Pi(m_params, Pi(st, parent)), m_params.size(), true);; + expr coercion_type = infer_implicit(Pi(m_params, Pi(st, parent, m_p), m_p), m_params.size(), true);; expr coercion_value = parent_intro; for (unsigned idx : fmap) { expr const & field = m_fields[idx]; @@ -810,7 +810,7 @@ struct structure_cmd_fn { expr proj = mk_app(mk_app(mk_constant(proj_name, st_ls), m_params), st); coercion_value = mk_app(coercion_value, proj); } - coercion_value = Fun(m_params, Fun(st, coercion_value)); + coercion_value = Fun(m_params, Fun(st, coercion_value, m_p), m_p); name coercion_name = coercion_names[i]; bool use_conv_opt = false; declaration coercion_decl = mk_definition_inferring_trusted(m_env, coercion_name, lnames, diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index 646e6eba60..f54ca6b1ac 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -201,11 +201,21 @@ expr Fun(buffer const & locals, expr const & e, parser & p) { return p.rec_save_pos(Fun(locals, e, use_cache), p.pos_of(e)); } +expr Fun(expr const & local, expr const & e, parser & p) { + bool use_cache = false; + return p.rec_save_pos(Fun(local, e, use_cache), p.pos_of(e)); +} + expr Pi(buffer const & locals, expr const & e, parser & p) { bool use_cache = false; return p.rec_save_pos(Pi(locals, e, use_cache), p.pos_of(e)); } +expr Pi(expr const & local, expr const & e, parser & p) { + bool use_cache = false; + return p.rec_save_pos(Pi(local, e, use_cache), p.pos_of(e)); +} + template static expr mk_binding_as_is(unsigned num, expr const * locals, expr const & b) { expr r = abstract_locals(b, num, locals); diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h index 68c039840d..3ae11cf66d 100644 --- a/src/frontends/lean/util.h +++ b/src/frontends/lean/util.h @@ -71,8 +71,10 @@ expr update_local_ref(expr const & e, name_set const & lvls_to_remove, name_set /** \brief Fun(locals, e), but also propagate \c e position to result */ expr Fun(buffer const & locals, expr const & e, parser & p); +expr Fun(expr const & local, expr const & e, parser & p); /** \brief Pi(locals, e), but also propagate \c e position to result */ expr Pi(buffer const & locals, expr const & e, parser & p); +expr Pi(expr const & local, expr const & e, parser & p); /** \brief Similar to Fun(locals, e, p), but the types are marked as 'as-is' (i.e., they are not processed by the elaborator. */ expr Fun_as_is(buffer const & locals, expr const & e, parser & p); /** \brief Similar to Pi(locals, e, p), but the types are marked as 'as-is' (i.e., they are not processed by the elaborator. */ diff --git a/tests/lean/error_pos.lean b/tests/lean/error_pos.lean index 7045f06bb4..9b01dda21a 100644 --- a/tests/lean/error_pos.lean +++ b/tests/lean/error_pos.lean @@ -11,3 +11,6 @@ check λ (A : Type) (B : A → Type) (b : B), true check λ (A : Type) (B : A → Type), B → true check λ (A : Type) (B : A → Type) b, (b : B) + +example {A : Type} {B : Type} {a₁ a₂ : B} {b₁ b₂ : A → B} : a₁ = a₂ → (∀ x, b₁ x = b₂ x) → (let x : A := a₁ in b₁ x) = (let x : A := a₂ in b₂ x) := +sorry diff --git a/tests/lean/error_pos.lean.expected.out b/tests/lean/error_pos.lean.expected.out index a363dd55f2..8f6155c7d9 100644 --- a/tests/lean/error_pos.lean.expected.out +++ b/tests/lean/error_pos.lean.expected.out @@ -2,9 +2,15 @@ error_pos.lean:1:39: error: type expected at B error_pos.lean:4:43: error: type expected at B -error_pos.lean:4:43: error: type expected at +error_pos.lean:9:39: error: type expected at B error_pos.lean:11:37: error: type expected at B error_pos.lean:13:37: error: type expected at B +error_pos.lean:15:105: error: invalid let-expression, expression + a₁ +has type + B +but is expected to have type + A