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

fix(frontends/lean): error localization bugs

Browse source
This commit is contained in:
Leonardo de Moura 2016-10-15 13:40:57 -07:00
parent c3861c7ab3
commit 9b84db083d
12 changed files with 90 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/frontends/lean/brackets.cpp
View file

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

33
src/frontends/lean/builtin_exprs.cpp
View file

@ -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<expr> 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<expr> locals;
to_buffer(lhss_locals[i], locals);
buffer<expr> 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<expr> 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) {

30
src/frontends/lean/decl_util.cpp
View file

@ -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<name> & 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<expr> const & from, buffer<expr> 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<name> & lp_names, buffer<expr> & params, buffer<expr> const & all_exprs) {
collected_locals locals;
buffer<expr> include_vars;
@ -250,7 +276,7 @@ void collect_implicit_locals(parser & p, buffer<name> & lp_names, buffer<expr> &
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<name> & lp_names, buffer<expr> &
void elaborate_params(elaborator & elab, buffer<expr> const & params, buffer<expr> & 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);

4
src/frontends/lean/decl_util.h
View file

@ -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<name> const & fn_names);
equations_header mk_equations_header(name const & fn_name);
expr replace_locals_preserving_pos_info(expr const & e, buffer<expr> const & from, buffer<expr> const & to);
expr replace_local_preserving_pos_info(expr const & e, expr const & from, expr const & to);
}

12
src/frontends/lean/definition_cmds.cpp
View file

@ -132,7 +132,7 @@ expr parse_mutual_definition(parser & p, buffer<name> & lp_names, buffer<expr> &
throw parser_error("unexpected 'with' clause", p.pos());
optional<expr_pair> 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<expr> 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<name> & lp_names, buffer<ex
}
static void replace_params(buffer<expr> const & params, buffer<expr> 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));
}

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

@ -2088,7 +2088,8 @@ expr elaborator::visit_let(expr const & e, optional<expr> 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);

2
src/frontends/lean/match_expr.cpp
View file

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

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

@ -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,

10
src/frontends/lean/util.cpp
View file

@ -201,11 +201,21 @@ expr Fun(buffer<expr> 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<expr> 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<bool is_lambda>
static expr mk_binding_as_is(unsigned num, expr const * locals, expr const & b) {
expr r = abstract_locals(b, num, locals);

2
src/frontends/lean/util.h
View file

@ -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<expr> 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<expr> 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<expr> 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. */

3
tests/lean/error_pos.lean
View file

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

8
tests/lean/error_pos.lean.expected.out
View file

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