michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(kernel,library,frontends/lean): improve error messages

Browse source 
see #669
This commit is contained in:
Leonardo de Moura 2015-06-14 19:44:00 -07:00
parent ff5022c2f4
commit d8620ef4c9
15 changed files with 92 additions and 64 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -61,7 +61,7 @@ static optional<pair<expr, expr>> mk_op(environment const & env, local_context &
return optional<pair<expr, expr>>();
r = mk_app(r, explicit_arg);
expr type = tc->infer(explicit_arg, cs);
justification j = mk_app_justification(r, explicit_arg, binding_domain(op_type), type);
justification j = mk_app_justification(r, op_type, explicit_arg, type);
if (!tc->is_def_eq(binding_domain(op_type), type, j, cs))
return optional<pair<expr, expr>>();
op_type = instantiate(binding_body(op_type), explicit_arg);

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

@ -318,7 +318,7 @@ expr elaborator::visit_choice(expr const & e, optional<expr> const & t, constrai
name_generator && /* ngen */) {
return choose(std::make_shared<choice_expr_elaborator>(*this, ctx, full_ctx, meta, type, e));
};
auto pp_fn = [=](formatter const & fmt, pos_info_provider const * pos_prov, substitution const &, bool is_main) {
auto pp_fn = [=](formatter const & fmt, pos_info_provider const * pos_prov, substitution const &, bool is_main, bool) {
format r = pp_previous_error_header(fmt, pos_prov, some_expr(e), is_main);
r += format("none of the overloads is applicable:");
for (unsigned i = 0; i < get_num_choices(e); i++) {
@ -449,7 +449,7 @@ pair<expr, expr> elaborator::ensure_fun(expr f, constraint_seq & cs) {
} else {
local_context ctx = m_context;
local_context full_ctx = m_full_context;
justification j = mk_justification(f, [=](formatter const & fmt, substitution const & subst) {
justification j = mk_justification(f, [=](formatter const & fmt, substitution const & subst, bool) {
return pp_function_expected(fmt, substitution(subst).instantiate(f));
});
auto choice_fn = [=](expr const & meta, expr const &, substitution const &, name_generator &&) {
@ -667,7 +667,7 @@ expr elaborator::visit_app(expr const & e, constraint_seq & cs) {
expr a = visit_expecting_type_of(app_arg(e), d_type, a_cs);
expr a_type = infer_type(a, a_cs);
expr r = mk_app(f, a, e.get_tag());
justification j = mk_app_justification(r, a, d_type, a_type);
justification j = mk_app_justification(r, f_type, a, a_type);
auto new_a_cs = ensure_has_type(a, a_type, d_type, j);
expr new_a = new_a_cs.first;
cs += f_cs + new_a_cs.second + a_cs;
@ -1175,7 +1175,7 @@ expr elaborator::visit_equations(expr const & eqns, constraint_seq & cs) {
new_cs.linearize(tmp_cs);
for (constraint const & c : tmp_cs) {
justification j = c.get_justification();
auto pp_fn = [=](formatter const & fmt, pos_info_provider const * pp, substitution const & s, bool is_main) {
auto pp_fn = [=](formatter const & fmt, pos_info_provider const * pp, substitution const & s, bool is_main, bool) {
if (!is_main)
return format();
format r = j.pp(fmt, pp, s);
@ -1230,12 +1230,12 @@ expr elaborator::visit_equation(expr const & eq, constraint_seq & cs) {
expr lhs_type = infer_type(new_lhs, cs);
expr rhs_type = infer_type(new_rhs, cs);
justification j = mk_justification(eq, [=](formatter const & fmt, substitution const & subst) {
justification j = mk_justification(eq, [=](formatter const & fmt, substitution const & subst, bool as_error) {
substitution s(subst);
name n = local_pp_name(lhs_fn);
if (is_match_binder_name(n))
n = "match";
return pp_def_type_mismatch(fmt, n, s.instantiate(lhs_type), s.instantiate(rhs_type));
return pp_def_type_mismatch(fmt, n, s.instantiate(lhs_type), s.instantiate(rhs_type), as_error);
});
pair<expr, constraint_seq> new_rhs_cs = ensure_has_type(new_rhs, rhs_type, lhs_type, j);
new_rhs = new_rhs_cs.first;
@ -1379,7 +1379,7 @@ expr elaborator::visit_structure_instance(expr const & e, constraint_seq & cs) {
}
S_mk = mk_app(S_mk, v, result_tag);
expr v_type = infer_type(v, cs);
justification j = mk_app_justification(S_mk, v, d_type, v_type);
justification j = mk_app_justification(S_mk, S_mk_type, v, v_type);
auto new_v_cs = ensure_has_type(v, v_type, d_type, j);
expr new_v = new_v_cs.first;
cs += new_v_cs.second;
@ -2062,9 +2062,9 @@ std::tuple<expr, expr, level_param_names> elaborator::operator()(expr const & t,
constraint_seq v_cs;
expr r_v = visit(v, v_cs);
expr r_v_type = infer_type(r_v, v_cs);
justification j = mk_justification(r_v, [=](formatter const & fmt, substitution const & subst) {
justification j = mk_justification(r_v, [=](formatter const & fmt, substitution const & subst, bool as_error) {
substitution s(subst);
return pp_def_type_mismatch(fmt, n, s.instantiate(r_t), s.instantiate(r_v_type));
return pp_def_type_mismatch(fmt, n, s.instantiate(r_t), s.instantiate(r_v_type), as_error);
});
pair<expr, constraint_seq> r_v_cs = ensure_has_type(r_v, r_v_type, r_t, j);
r_v = r_v_cs.first;

2
src/kernel/default_converter.cpp
View file

@ -336,7 +336,7 @@ bool default_converter::try_eta_expansion_core(expr const & t, expr const & s, c
} else if (auto m = m_tc->is_stuck(s_type)) {
name_generator ngen = m_tc->mk_ngen();
expr r = mk_pi_for(ngen, *m);
justification j = mk_justification(s, [=](formatter const & fmt, substitution const & subst) {
justification j = mk_justification(s, [=](formatter const & fmt, substitution const & subst, bool) {
return pp_function_expected(fmt, substitution(subst).instantiate(s));
});
aux_cs += mk_eq_cnstr(s_type, r, j);

37
src/kernel/error_msgs.cpp
View file

@ -63,30 +63,51 @@ std::tuple<format, format> pp_until_different(formatter const & fmt, expr const
return pp_until_different(fmt, e1, e2, get_distinguishing_pp_options());
}
format pp_app_type_mismatch(formatter const & fmt, expr const & app, expr const & arg, expr const & expected_type, expr const & given_type) {
format pp_app_type_mismatch(formatter const & _fmt, expr const & app, expr const & fn_type, expr const & arg, expr const & given_type, bool as_error) {
formatter fmt(_fmt);
format r;
format expected_fmt, given_fmt;
lean_assert(is_pi(fn_type));
if (!is_explicit(binding_info(fn_type))) {
// For implicit arguments to be shown if argument is implicit
options opts = fmt.get_options();
// TODO(Leo): this is hackish, the option is defined in the folder library
opts = opts.update_if_undef(name{"pp", "implicit"}, true);
fmt = fmt.update_options(opts);
}
expr expected_type = binding_domain(fn_type);
std::tie(expected_fmt, given_fmt) = pp_until_different(fmt, expected_type, given_type);
r += format("type mismatch at application");
if (as_error)
r += format("type mismatch at application");
else
r += format("application type constraint");
r += pp_indent_expr(fmt, app);
r += compose(line(), format("term"));
r += pp_indent_expr(fmt, arg);
r += compose(line(), format("has type"));
r += given_fmt;
r += compose(line(), format("but is expected to have type"));
r += expected_fmt;
if (as_error) {
r += compose(line(), format("but is expected to have type"));
r += expected_fmt;
}
return r;
}
format pp_def_type_mismatch(formatter const & fmt, name const & n, expr const & expected_type, expr const & given_type) {
format pp_def_type_mismatch(formatter const & fmt, name const & n, expr const & expected_type, expr const & given_type, bool as_error) {
format expected_fmt, given_fmt;
std::tie(expected_fmt, given_fmt) = pp_until_different(fmt, expected_type, given_type);
format r("type mismatch at definition '");
format r;
if (as_error)
r += format("type mismatch at definition '");
else
r += format("definition type constraint '");
r += format(n);
r += format("', has type");
r += given_fmt;
r += compose(line(), format("but is expected to have type"));
r += expected_fmt;
if (as_error) {
r += compose(line(), format("but is expected to have type"));
r += expected_fmt;
}
return r;
}

4
src/kernel/error_msgs.h
View file

@ -11,8 +11,8 @@ namespace lean {
format pp_indent_expr(formatter const & fmt, expr const & e);
format pp_type_expected(formatter const & fmt, expr const & e);
format pp_function_expected(formatter const & fmt, expr const & e);
format pp_app_type_mismatch(formatter const & fmt, expr const & app, expr const & arg, expr const & expected_type, expr const & given_type);
format pp_def_type_mismatch(formatter const & fmt, name const & n, expr const & expected_type, expr const & given_type);
format pp_app_type_mismatch(formatter const & fmt, expr const & app, expr const & fn_type, expr const & arg, expr const & given_type, bool as_error);
format pp_def_type_mismatch(formatter const & fmt, name const & n, expr const & expected_type, expr const & given_type, bool as_error);
format pp_decl_has_metavars(formatter const & fmt, name const & n, expr const & e, bool is_type);
/** \brief Set a list extra configuration options that are used to try to distinguish error such as given/expected type mismatch

20
src/kernel/justification.cpp
View file

@ -293,7 +293,7 @@ public:
};
format justification::pp_core(formatter const & fmt, pos_info_provider const * p, substitution const & s,
justification_set & set, bool is_main) const {
justification_set & set, bool is_main, bool as_error) const {
if (set.contains(*this))
return format();
set.insert(*this);
@ -302,25 +302,25 @@ format justification::pp_core(formatter const & fmt, pos_info_provider const * p
return format();
switch (it->m_kind) {
case justification_kind::Asserted:
return to_asserted(it)->m_fn(fmt, p, s, is_main);
return to_asserted(it)->m_fn(fmt, p, s, is_main, as_error);
case justification_kind::Wrapper:
return to_wrapper(it)->m_fn(fmt, p, s, is_main);
return to_wrapper(it)->m_fn(fmt, p, s, is_main, as_error);
case justification_kind::Assumption:
if (is_main)
return format(format("Assumption "), format(to_assumption(it)->m_idx));
else
return format();
case justification_kind::Composite: {
format r1 = to_composite(it)->m_child[0].pp_core(fmt, p, s, set, is_main);
format r2 = to_composite(it)->m_child[1].pp_core(fmt, p, s, set, false);
format r1 = to_composite(it)->m_child[0].pp_core(fmt, p, s, set, is_main, as_error);
format r2 = to_composite(it)->m_child[1].pp_core(fmt, p, s, set, false, as_error);
return r1 + r2;
}}
lean_unreachable();
}
format justification::pp(formatter const & fmt, pos_info_provider const * p, substitution const & s) const {
format justification::pp(formatter const & fmt, pos_info_provider const * p, substitution const & s, bool as_error) const {
justification_set set;
return pp_core(fmt, p, s, set, true);
return pp_core(fmt, p, s, set, true, as_error);
}
justification mk_wrapper(justification const & j, optional<expr> const & s, pp_jst_fn const & fn) {
@ -346,18 +346,18 @@ justification mk_justification(optional<expr> const & s, pp_jst_fn const & fn) {
return justification(new (get_asserted_allocator().allocate()) asserted_cell(fn, s));
}
justification mk_justification(optional<expr> const & s, pp_jst_sfn const & fn) {
return mk_justification(s, [=](formatter const & fmt, pos_info_provider const *, substitution const & subst, bool is_main) {
return mk_justification(s, [=](formatter const & fmt, pos_info_provider const *, substitution const & subst, bool is_main, bool as_error) {
// Remark: we are not using to_pos(s, p) anymore because we don't try to display complicated error messages anymore.
// return compose(to_pos(s, p), fn(fmt, subst));
if (is_main)
return fn(fmt, subst);
return fn(fmt, subst, as_error);
else
return format();
});
}
justification mk_justification(char const * msg, optional<expr> const & s) {
std::string _msg(msg);
return mk_justification(s, [=](formatter const &, pos_info_provider const *, substitution const &, bool is_main) {
return mk_justification(s, [=](formatter const &, pos_info_provider const *, substitution const &, bool is_main, bool) {
if (is_main)
return format(_msg);
else

8
src/kernel/justification.h
View file

@ -23,7 +23,7 @@ struct justification_cell;
The pp_jst_fn is a generic funciton that produces these messages. We can associate these functions
to justification objects.
*/
typedef std::function<format(formatter const &, pos_info_provider const *, substitution const &, bool)> pp_jst_fn;
typedef std::function<format(formatter const &, pos_info_provider const *, substitution const &, bool, bool)> pp_jst_fn;
class justification_set;
@ -43,7 +43,7 @@ class justification {
justification_cell * m_ptr;
justification(justification_cell * ptr);
format pp_core(formatter const & fmt, pos_info_provider const * p, substitution const & s,
justification_set & visited, bool is_main) const;
justification_set & visited, bool is_main, bool as_error) const;
public:
justification();
justification(justification const & s);
@ -66,7 +66,7 @@ public:
\brief Convert this justification into a format object. This method is usually used to report
"error" messages to users.
*/
format pp(formatter const & fmt, pos_info_provider const * p, substitution const & s) const;
format pp(formatter const & fmt, pos_info_provider const * p, substitution const & s, bool as_error = true) const;
/**
\brief Return an expression associated with the justification object.
*/
@ -85,7 +85,7 @@ public:
/**
\brief Simpler version of pp_jst_fn
*/
typedef std::function<format(formatter const &, substitution const &)> pp_jst_sfn;
typedef std::function<format(formatter const &, substitution const &, bool)> pp_jst_sfn;
/** \brief Return a format object containing position information for the given expression (if available) */
format to_pos(optional<expr> const & e, pos_info_provider const * p);

22
src/kernel/type_checker.cpp
View file

@ -106,7 +106,7 @@ pair<expr, constraint_seq> type_checker::ensure_sort_core(expr e, expr const & s
} else if (is_meta(ecs.first)) {
expr r = mk_sort(mk_meta_univ(m_gen.next()));
justification j = mk_justification(s,
[=](formatter const & fmt, substitution const & subst) {
[=](formatter const & fmt, substitution const & subst, bool) {
return pp_type_expected(fmt, substitution(subst).instantiate(s));
});
return to_ecs(r, mk_eq_cnstr(ecs.first, r, j), ecs.second);
@ -124,7 +124,7 @@ pair<expr, constraint_seq> type_checker::ensure_pi_core(expr e, expr const & s)
return ecs;
} else if (auto m = is_stuck(ecs.first)) {
expr r = mk_pi_for(m_gen, *m);
justification j = mk_justification(s, [=](formatter const & fmt, substitution const & subst) {
justification j = mk_justification(s, [=](formatter const & fmt, substitution const & subst, bool) {
return pp_function_expected(fmt, substitution(subst).instantiate(s));
});
return to_ecs(r, mk_eq_cnstr(ecs.first, r, j), ecs.second);
@ -136,7 +136,7 @@ pair<expr, constraint_seq> type_checker::ensure_pi_core(expr e, expr const & s)
static constexpr char const * g_macro_error_msg = "failed to type check macro expansion";
justification type_checker::mk_macro_jst(expr const & e) {
return mk_justification(e, [=](formatter const &, substitution const &) {
return mk_justification(e, [=](formatter const &, substitution const &, bool) {
return format(g_macro_error_msg);
});
}
@ -155,10 +155,10 @@ app_delayed_justification::app_delayed_justification(expr const & e, expr const
expr const & a_type):
m_e(e), m_arg(arg), m_fn_type(f_type), m_arg_type(a_type) {}
justification mk_app_justification(expr const & e, expr const & arg, expr const & d_type, expr const & a_type) {
auto pp_fn = [=](formatter const & fmt, substitution const & subst) {
justification mk_app_justification(expr const & e, expr const & fn_type, expr const & arg, expr const & a_type) {
auto pp_fn = [=](formatter const & fmt, substitution const & subst, bool as_error) {
substitution s(subst);
return pp_app_type_mismatch(fmt, s.instantiate(e), s.instantiate(arg), s.instantiate(d_type), s.instantiate(a_type));
return pp_app_type_mismatch(fmt, s.instantiate(e), s.instantiate(fn_type), s.instantiate(arg), s.instantiate(a_type), as_error);
};
return mk_justification(e, pp_fn);
}
@ -167,7 +167,7 @@ justification app_delayed_justification::get() {
if (!m_jst) {
// We should not have a reference to this object inside the closure.
// So, we create the following locals that will be captured by the closure instead of 'this'.
m_jst = mk_app_justification(m_e, m_arg, binding_domain(m_fn_type), m_arg_type);
m_jst = mk_app_justification(m_e, m_fn_type, m_arg, m_arg_type);
}
return *m_jst;
}
@ -264,15 +264,15 @@ pair<expr, constraint_seq> type_checker::infer_app(expr const & e, bool infer_on
pair<expr, constraint_seq> acs = infer_type_core(app_arg(e), infer_only);
expr a_type = acs.first;
app_delayed_justification jst(e, app_arg(e), f_type, a_type);
expr d_type = binding_domain(pics.first);
expr d_type = binding_domain(f_type);
pair<bool, constraint_seq> dcs = is_def_eq(a_type, d_type, jst);
if (!dcs.first) {
throw_kernel_exception(m_env, e,
[=](formatter const & fmt) {
return pp_app_type_mismatch(fmt, e, app_arg(e), d_type, a_type);
return pp_app_type_mismatch(fmt, e, f_type, app_arg(e), a_type, true);
});
}
return mk_pair(instantiate(binding_body(pics.first), app_arg(e)),
return mk_pair(instantiate(binding_body(f_type), app_arg(e)),
pics.second + ftcs.second + dcs.second + acs.second);
} else {
buffer<expr> args;
@ -491,7 +491,7 @@ certified_declaration check(environment const & env, declaration const & d, name
expr val_type = checker2.check(d.get_value(), d.get_univ_params()).first;
if (!checker2.is_def_eq(val_type, d.get_type()).first) {
throw_kernel_exception(env, d.get_value(), [=](formatter const & fmt) {
return pp_def_type_mismatch(fmt, d.get_name(), d.get_type(), val_type);
return pp_def_type_mismatch(fmt, d.get_name(), d.get_type(), val_type, true);
});
}
}

4
src/library/kernel_bindings.cpp
View file

@ -1402,14 +1402,14 @@ static int mk_justification(lua_State * L) {
return push_justification(L, justification());
} else if (nargs == 1) {
std::string s = lua_tostring(L, 1);
return push_justification(L, mk_justification(none_expr(), [=](formatter const &, substitution const &) {
return push_justification(L, mk_justification(none_expr(), [=](formatter const &, substitution const &, bool) {
return format(s.c_str());
}));
} else {
std::string s = lua_tostring(L, 1);
environment env = to_environment(L, 2);
expr e = to_expr(L, 3);
justification j = mk_justification(some_expr(e), [=](formatter const & fmt, substitution const & subst) {
justification j = mk_justification(some_expr(e), [=](formatter const & fmt, substitution const & subst, bool) {
expr new_e = substitution(subst).instantiate(e);
format r;
r += format(s.c_str());

12
src/library/unifier.cpp
View file

@ -641,7 +641,7 @@ struct unifier_fn {
justification mk_assign_justification(expr const & m, expr const & m_type, expr const & v_type, justification const & j) {
auto r = j.get_main_expr();
if (!r) r = m;
justification new_j = mk_justification(r, [=](formatter const & fmt, substitution const & subst) {
justification new_j = mk_justification(r, [=](formatter const & fmt, substitution const & subst, bool) {
substitution s(subst);
format r;
expr _m = s.instantiate(m);
@ -657,8 +657,8 @@ struct unifier_fn {
r += given_fmt;
r += compose(line(), format("but is expected to have type"));
r += expected_fmt;
r += compose(line(), format("the assignment was attempted when trying to solve"));
r += nest(2*get_pp_indent(fmt.get_options()), compose(line(), j.pp(fmt, nullptr, subst)));
r += compose(line(), format("the assignment was attempted when processing"));
r += nest(2*get_pp_indent(fmt.get_options()), compose(line(), j.pp(fmt, nullptr, subst, false)));
return r;
});
return mk_composite1(new_j, j);
@ -712,7 +712,7 @@ struct unifier_fn {
justification mk_invalid_local_ctx_justification(expr const & lhs, expr const & rhs, justification const & j,
expr const & bad_local) {
justification new_j = mk_justification(get_app_fn(lhs), [=](formatter const & fmt, substitution const & subst) {
justification new_j = mk_justification(get_app_fn(lhs), [=](formatter const & fmt, substitution const & subst, bool) {
format r = format("invalid local context when tried to assign");
r += pp_indent_expr(fmt, rhs);
buffer<expr> locals;
@ -730,8 +730,8 @@ struct unifier_fn {
}
r += nest(get_pp_indent(fmt.get_options()), compose(line(), aux));
}
r += compose(line(), format("the assignment was attempted when trying to solve"));
r += nest(2*get_pp_indent(fmt.get_options()), compose(line(), j.pp(fmt, nullptr, subst)));
r += compose(line(), format("the assignment was attempted when processing"));
r += nest(2*get_pp_indent(fmt.get_options()), compose(line(), j.pp(fmt, nullptr, subst, false)));
return r;
});
return mk_composite1(new_j, j);

4
src/library/util.cpp
View file

@ -792,7 +792,7 @@ format pp_type_mismatch(formatter const & fmt, expr const & v, expr const & v_ty
}
justification mk_type_mismatch_jst(expr const & v, expr const & v_type, expr const & t, expr const & src) {
return mk_justification(src, [=](formatter const & fmt, substitution const & subst) {
return mk_justification(src, [=](formatter const & fmt, substitution const & subst, bool) {
substitution s(subst);
return pp_type_mismatch(fmt, s.instantiate(v), s.instantiate(v_type), s.instantiate(t));
});
@ -870,7 +870,7 @@ expr instantiate_meta(expr const & meta, substitution & subst) {
}
justification mk_failed_to_synthesize_jst(environment const & env, expr const & m) {
return mk_justification(m, [=](formatter const & fmt, substitution const & subst) {
return mk_justification(m, [=](formatter const & fmt, substitution const & subst, bool) {
substitution tmp(subst);
expr new_m = instantiate_meta(m, tmp);
expr new_type = type_checker(env).infer(new_m).first;

6
tests/lean/669.lean.expected.out
View file

@ -4,12 +4,10 @@ placeholder has type
Type₁
but is expected to have type
Prop
the assignment was attempted when trying to solve
type mismatch at application
the assignment was attempted when processing
application type constraint
(λ {T : Prop} (t : T), t) bool.tt
term
bool.tt
has type
bool
but is expected to have type
bool

6
tests/lean/error_pos_bug.lean.expected.out
View file

@ -5,12 +5,10 @@ placeholder has type
Category
but is expected to have type
Type
the assignment was attempted when trying to solve
type mismatch at application
the assignment was attempted when processing
application type constraint
Category.mk a (category.mk b c)
term
category.mk b c
has type
category a
but is expected to have type
category a

3
tests/lean/mismatch.lean Normal file
View file

@ -0,0 +1,3 @@
definition id {A : Type} {a : A} := a
check @id nat 1

8
tests/lean/mismatch.lean.expected.out Normal file
View file

@ -0,0 +1,8 @@
mismatch.lean:3:7: error: type mismatch at application
@id nat 1
term
1
has type
num
but is expected to have type
nat