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

Improve elaborator error messages

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-04 13:21:57 -07:00
parent 613d83cdf4
commit 87d3961158
12 changed files with 310 additions and 40 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

113
src/frontends/lean/lean_elaborator.cpp
View file

@ -46,20 +46,65 @@ expr const & get_choice(expr const & e, unsigned i) {
}
class elaborator::imp {
// Information for producing error messages regarding application type mismatch during elaboration
struct app_mismatch_info {
expr m_app; // original application
context m_ctx; // context where application occurs
std::vector<expr> m_args; // arguments after processing
std::vector<expr> m_types; // inferred types of the arguments
app_mismatch_info(expr const & app, context const & ctx, unsigned sz, expr const * args, expr const * types):
m_app(app), m_ctx(ctx), m_args(args, args+sz), m_types(types, types+sz) {}
};
// Information for producing error messages regarding expected type mismatch during elaboration
struct expected_type_info {
expr m_expr; // original expression
expr m_processed_expr; // expression after processing
expr m_expected; // expected type
expr m_given; // inferred type of the processed expr.
context m_ctx;
expected_type_info(expr const & e, expr const & p, expr const & exp, expr const & given, context const & ctx):
m_expr(e), m_processed_expr(p), m_expected(exp), m_given(given), m_ctx(ctx) {}
};
enum class info_kind { AppMismatchInfo, ExpectedTypeInfo };
typedef std::pair<info_kind, unsigned> info_ref;
std::vector<app_mismatch_info> m_app_mismatch_info;
std::vector<expected_type_info> m_expected_type_info;
info_ref mk_app_mismatch_info(expr const & app, context const & ctx, unsigned sz, expr const * args, expr const * types) {
unsigned idx = m_app_mismatch_info.size();
m_app_mismatch_info.push_back(app_mismatch_info(app, ctx, sz, args, types));
return mk_pair(info_kind::AppMismatchInfo, idx);
}
info_ref mk_expected_type_info(expr const & e, expr const & p, expr const & exp, expr const & g, context const & ctx) {
unsigned idx = m_expected_type_info.size();
m_expected_type_info.push_back(expected_type_info(e, p, exp, g, ctx));
return mk_pair(info_kind::ExpectedTypeInfo, idx);
}
context get_context(info_ref const & r) const {
if (r.first == info_kind::AppMismatchInfo)
return m_app_mismatch_info[r.second].m_ctx;
else
return m_expected_type_info[r.second].m_ctx;
}
// unification constraint lhs == second
struct constraint {
expr m_lhs;
expr m_rhs;
context m_ctx;
expr m_source; // auxiliary field used for producing error msgs
context m_source_ctx; // auxiliary field used for producing error msgs
unsigned m_arg_pos; // auxiliary field used for producing error msgs
constraint(expr const & lhs, expr const & rhs, context const & ctx, expr const & src, context const & src_ctx, unsigned arg_pos):
m_lhs(lhs), m_rhs(rhs), m_ctx(ctx), m_source(src), m_source_ctx(src_ctx), m_arg_pos(arg_pos) {}
info_ref m_info;
constraint(expr const & lhs, expr const & rhs, context const & ctx, info_ref const & r):
m_lhs(lhs), m_rhs(rhs), m_ctx(ctx), m_info(r) {}
constraint(expr const & lhs, expr const & rhs, constraint const & c):
m_lhs(lhs), m_rhs(rhs), m_ctx(c.m_ctx), m_source(c.m_source), m_source_ctx(c.m_source_ctx), m_arg_pos(c.m_arg_pos) {}
m_lhs(lhs), m_rhs(rhs), m_ctx(c.m_ctx), m_info(c.m_info) {}
constraint(expr const & lhs, expr const & rhs, context const & ctx, constraint const & c):
m_lhs(lhs), m_rhs(rhs), m_ctx(ctx), m_source(c.m_source), m_source_ctx(c.m_source_ctx), m_arg_pos(c.m_arg_pos) {}
m_lhs(lhs), m_rhs(rhs), m_ctx(ctx), m_info(c.m_info) {}
};
// information associated with the metavariable
@ -331,7 +376,8 @@ class elaborator::imp {
expr expected = abst_domain(f_t);
expr given = types[i];
if (has_metavar(expected) || has_metavar(given)) {
m_constraints.push_back(constraint(expected, given, ctx, e, ctx, i));
info_ref r = mk_app_mismatch_info(e, ctx, args.size(), args.data(), types.data());
m_constraints.push_back(constraint(expected, given, ctx, r));
} else {
if (!is_convertible(expected, given, ctx)) {
expr coercion = m_frontend.get_coercion(given, expected);
@ -439,10 +485,21 @@ class elaborator::imp {
[[noreturn]] void throw_unification_exception(constraint const & c) {
// display(std::cout);
m_constraints.push_back(c);
if (c.m_arg_pos != static_cast<unsigned>(-1)) {
throw unification_app_mismatch_exception(*m_owner, c.m_source_ctx, c.m_source, c.m_arg_pos);
info_ref const & r = c.m_info;
if (r.first == info_kind::AppMismatchInfo) {
app_mismatch_info & info = m_app_mismatch_info[r.second];
for (expr & arg : info.m_args)
arg = instantiate(arg);
for (expr & type : info.m_types)
type = instantiate(type);
throw unification_app_mismatch_exception(*m_owner, info.m_ctx, info.m_app, info.m_args, info.m_types);
} else {
throw unification_type_mismatch_exception(*m_owner, c.m_source_ctx, c.m_source);
expected_type_info & info = m_expected_type_info[r.second];
info.m_processed_expr = instantiate(info.m_processed_expr);
info.m_given = instantiate(info.m_given);
info.m_expected = instantiate(info.m_expected);
throw unification_type_mismatch_exception(*m_owner, info.m_ctx, info.m_expr, info.m_processed_expr,
info.m_expected, info.m_given);
}
}
@ -651,25 +708,31 @@ class elaborator::imp {
cont = true; // must continue
} else {
if (m_metavars[midx].m_type && !m_metavars[midx].m_type_cnstr) {
context ctx = m_metavars[midx].m_ctx;
try {
expr t = infer(m_metavars[midx].m_assignment, m_metavars[midx].m_ctx);
expr t = infer(m_metavars[midx].m_assignment, ctx);
m_metavars[midx].m_type_cnstr = true;
m_constraints.push_back(constraint(m_metavars[midx].m_type, t, m_metavars[midx].m_ctx,
m_metavars[midx].m_mvar, m_metavars[midx].m_ctx, static_cast<unsigned>(-1)));
info_ref r = mk_expected_type_info(m_metavars[midx].m_mvar, m_metavars[midx].m_mvar,
m_metavars[midx].m_type, t, ctx);
m_constraints.push_back(constraint(m_metavars[midx].m_type, t, ctx, r));
progress = true;
} catch (exception&) {
// std::cout << "Failed to infer type of: ?M" << midx << "\n"
// << m_metavars[midx].m_assignment << "\nAT\n" << m_metavars[midx].m_ctx << "\n";
throw unification_type_mismatch_exception(*m_owner, m_metavars[midx].m_ctx, m_metavars[midx].m_mvar);
expr null_given_type; // failed to infer given type.
throw unification_type_mismatch_exception(*m_owner, ctx, m_metavars[midx].m_mvar, m_metavars[midx].m_mvar,
m_metavars[midx].m_type, null_given_type);
}
}
}
} else {
cont = true;
}
}
if (!cont)
return;
if (!progress)
throw unsolved_placeholder_exception(*m_owner, context(), m_root);
return;
}
}
@ -716,20 +779,27 @@ public:
}
expr operator()(expr const & e, expr const & expected_type, elaborator const & elb) {
m_owner = &elb;
m_constraints.clear();
m_metavars.clear();
m_owner = &elb;
m_app_mismatch_info.clear();
m_expected_type_info.clear();
m_processing_root = true;
auto p = process(e, context());
m_root = p.first;
expr given_type = p.second;
if (expected_type) {
if (has_metavar(given_type))
m_constraints.push_back(constraint(expected_type, given_type, context(), e, context(), static_cast<unsigned>(-1)));
if (has_metavar(given_type)) {
info_ref r = mk_expected_type_info(e, m_root, expected_type, given_type, context());
m_constraints.push_back(constraint(expected_type, given_type, context(), r));
}
}
if (has_metavar(m_root)) {
solve();
return instantiate(m_root);
expr r = instantiate(m_root);
if (has_metavar(r))
throw unsolved_placeholder_exception(elb, context(), m_root);
return r;
} else {
return m_root;
}
@ -756,6 +826,8 @@ public:
}
return r;
}
bool has_constraints() const { return !m_constraints.empty(); }
};
elaborator::elaborator(frontend const & fe):m_ptr(new imp(fe, nullptr)) {}
elaborator::~elaborator() {}
@ -768,4 +840,5 @@ environment const & elaborator::get_environment() const { return m_ptr->get_envi
void elaborator::display(std::ostream & out) const { m_ptr->display(out); }
format elaborator::pp(formatter & f, options const & o) const { return m_ptr->pp(f,o); }
void elaborator::print(imp * ptr) { ptr->display(std::cout); }
bool elaborator::has_constraints() const { return m_ptr->has_constraints(); }
}

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

@ -44,6 +44,8 @@ public:
void display(std::ostream & out) const;
format pp(formatter & f, options const & o) const;
bool has_constraints() const;
};
/**
\brief Create a choice expression for the given functions.

70
src/frontends/lean/lean_elaborator_exception.cpp
View file

@ -21,6 +21,17 @@ format pp(formatter fmt, context const & ctx, std::vector<expr> const & exprs, s
return r;
}
format pp_elaborator_state(formatter fmt, elaborator const & elb, options const & opts) {
unsigned indent = get_pp_indent(opts);
format r;
if (elb.has_constraints()) {
format elb_fmt = elb.pp(fmt, opts);
r += compose(line(), format("Elaborator state"));
r += nest(indent, compose(line(), elb_fmt));
}
return r;
}
format pp(formatter fmt, elaborator_exception const & ex, options const & opts) {
unsigned indent = get_pp_indent(opts);
context const & ctx = ex.get_context();
@ -31,13 +42,60 @@ format pp(formatter fmt, elaborator_exception const & ex, options const & opts)
r += format{line(), format("Arguments:")};
r += pp(fmt, ctx, _ex->get_args(), _ex->get_arg_types(), opts);
return r;
} else if (unification_app_mismatch_exception const * _ex = dynamic_cast<unification_app_mismatch_exception const *>(&ex)) {
unsigned indent = get_pp_indent(opts);
auto const & elb = _ex->get_elaborator();
auto const & ctx = _ex->get_context();
expr const & app = _ex->get_expr();
auto const & args = _ex->get_args();
auto const & types = _ex->get_types();
auto args_it = args.begin();
auto types_it = types.begin();
format app_fmt = fmt(ctx, app, false, opts);
format r = format{format(_ex->what()), nest(indent, compose(line(), app_fmt))};
format fun_type_fmt = fmt(ctx, *types_it, false, opts);
r += compose(line(), format("Function type:"));
r += nest(indent, compose(line(), fun_type_fmt));
++args_it;
++types_it;
if (args.size() > 2)
r += compose(line(), format("Arguments types:"));
else
r += compose(line(), format("Argument type:"));
for (; args_it != args.end(); ++args_it, ++types_it) {
format arg_fmt = fmt(ctx, *args_it, false, opts);
format type_fmt = fmt(ctx, *types_it, false, opts);
r += nest(indent, compose(line(), group(format{arg_fmt, space(), colon(), nest(indent, format{line(), type_fmt})})));
}
r += pp_elaborator_state(fmt, elb, opts);
return r;
} else if (unification_type_mismatch_exception const * _ex = dynamic_cast<unification_type_mismatch_exception const *>(&ex)) {
unsigned indent = get_pp_indent(opts);
auto const & elb = _ex->get_elaborator();
auto const & ctx = _ex->get_context();
expr const & e = _ex->get_expr();
expr const & p = _ex->get_processed_expr();
expr const & exp = _ex->get_expected_type();
expr const & given = _ex->get_given_type();
format r = format{format(_ex->what()), nest(indent, compose(line(), fmt(ctx, e, false, opts)))};
if (p != e) {
r += compose(line(), format("Term after elaboration:"));
r += nest(indent, compose(line(), fmt(ctx, p, false, opts)));
}
r += compose(line(), format("Expected type:"));
r += nest(indent, compose(line(), fmt(ctx, exp, false, opts)));
if (given) {
r += compose(line(), format("Got:"));
r += nest(indent, compose(line(), fmt(ctx, given, false, opts)));
}
r += pp_elaborator_state(fmt, elb, opts);
return r;
} else {
format expr_f = fmt(ctx, ex.get_expr(), false, opts);
format elb_f = ex.get_elaborator().pp(fmt, opts);
return format({format(ex.what()), space(), format("at term"),
nest(indent, compose(line(), expr_f)),
line(), format("Elaborator state"),
nest(indent, compose(line(), elb_f))});
auto const & elb = ex.get_elaborator();
format expr_fmt = fmt(ctx, ex.get_expr(), false, opts);
format r = format{format(ex.what()), space(), format("at term"), nest(indent, compose(line(), expr_fmt))};
r += pp_elaborator_state(fmt, elb, opts);
return r;
}
}

24
src/frontends/lean/lean_elaborator_exception.h
View file

@ -42,16 +42,32 @@ public:
};
class unification_app_mismatch_exception : public elaborator_exception {
unsigned m_arg_pos;
std::vector<expr> m_args;
std::vector<expr> m_types;
public:
unification_app_mismatch_exception(elaborator const & elb, context const & ctx, expr const & s, unsigned pos):elaborator_exception(elb, ctx, s), m_arg_pos(pos) {}
unsigned get_arg_pos() const { return m_arg_pos; }
unification_app_mismatch_exception(elaborator const & elb, context const & ctx, expr const & s,
std::vector<expr> const & args, std::vector<expr> const & types):
elaborator_exception(elb, ctx, s),
m_args(args),
m_types(types) {}
virtual ~unification_app_mismatch_exception() {}
std::vector<expr> const & get_args() const { return m_args; }
std::vector<expr> const & get_types() const { return m_types; }
virtual char const * what() const noexcept { return "application type mismatch during term elaboration"; }
};
class unification_type_mismatch_exception : public elaborator_exception {
expr m_processed_expr;
expr m_expected_type;
expr m_given_type;
public:
unification_type_mismatch_exception(elaborator const & elb, context const & ctx, expr const & s):elaborator_exception(elb, ctx, s) {}
unification_type_mismatch_exception(elaborator const & elb, context const & ctx, expr const & s,
expr const & processed, expr const & expected, expr const & given):
elaborator_exception(elb, ctx, s), m_processed_expr(processed), m_expected_type(expected), m_given_type(given) {}
virtual ~unification_type_mismatch_exception() {}
expr const & get_processed_expr() const { return m_processed_expr; }
expr const & get_expected_type() const { return m_expected_type; }
expr const & get_given_type() const { return m_given_type; }
virtual char const * what() const noexcept { return "type mismatch during term elaboration"; }
};

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

@ -247,7 +247,7 @@ class pp_fn {
// expression, but an alias is created for it.
return r;
} else {
return mk_result(format{lp(), nest(1, format{r.first, rp()})}, r.second);
return mk_result(paren(r.first), r.second);
}
}

2
src/kernel/level.cpp
View file

@ -219,7 +219,7 @@ format pp(level const & l, bool unicode) {
format r = format("max");
for (unsigned i = 0; i < max_size(l); i++)
r += format{line(), pp(max_level(l, i), unicode)};
return group(nest(1, format{lp(), r, rp()}));
return paren(r);
}
}}
lean_unreachable();

5
src/library/formatter.cpp
View file

@ -53,7 +53,10 @@ format formatter::operator()(kernel_exception const & ex, options const & opts)
format arg_types_fmt;
++it;
for (unsigned i = 1; it != arg_types.end(); ++it, ++i) {
format arg_fmt = operator()(ctx, arg(app, i), false, opts);
expr const & a = arg(app, i);
format arg_fmt = operator()(ctx, a, false, opts);
if (is_pi(a) || is_lambda(a) || is_let(a))
arg_fmt = paren(arg_fmt);
format arg_type_fmt = operator()(ctx, *it, false, opts);
arg_types_fmt += nest(indent, compose(line(), group(format{arg_fmt, space(), colon(), nest(indent, format{line(), arg_type_fmt})})));
}

7
src/tests/frontends/lean/implicit_args.cpp
View file

@ -30,7 +30,7 @@ static void success(expr const & e, expr const & expected, frontend const & env)
try {
std::cout << elaborate(e, env) << "\n";
} catch (unification_app_mismatch_exception & ex) {
std::cout << "Error at argumet " << ex.get_arg_pos() << " of " << mk_pair(ex.get_expr(), ex.get_context()) << "\n";
std::cout << "Error at " << mk_pair(ex.get_expr(), ex.get_context()) << "\n";
} catch (unification_type_mismatch_exception & ex) {
std::cout << "Error at " << mk_pair(ex.get_expr(), ex.get_context()) << " " << ex.what() << "\n";
std::cout << "Elaborator:\n"; ex.get_elaborator().display(std::cout); std::cout << "-----------------\n";
@ -58,8 +58,11 @@ static void fails(expr const & e, frontend const & env) {
// Check elaborator partial success (i.e., result still contain some metavariables */
static void unsolved(expr const & e, frontend const & env) {
try {
std::cout << "\n" << e << "\n------>\n" << elaborate(e, env) << "\n";
lean_assert(has_metavar(elaborate(e, env)));
lean_unreachable();
} catch (unsolved_placeholder_exception) {
}
}
#define _ mk_placholder()

4
src/util/sexpr/format.cpp
View file

@ -216,7 +216,7 @@ format bracket(std::string const l, format const & x, std::string const r) {
format(r)});
}
format paren(format const & x) {
return bracket("(", x, ")");
return group(nest(1, format{lp(), x, rp()}));
}
// wrap = <+/>
@ -415,7 +415,7 @@ struct sexpr_pp_fn {
r += apply(head(*curr));
curr = &tail(*curr);
if (is_nil(*curr)) {
return group(nest(1, format{lp(), r, rp()}));
return paren(r);
} else if (!is_cons(*curr)) {
return group(nest(1, format{lp(), r, space(), dot(), line(), apply(*curr), rp()}));
} else {

29
tests/lean/elab1.lean Normal file
View file

@ -0,0 +1,29 @@
Variable f {A : Type} (a b : A) : A.
Check f 10 true
Variable g {A B : Type} (a : A) : A.
Check g 10
Variable h : Pi (A : Type), A -> A.
Check fun x, fun A : Type, h A x
Variable eq : Pi A : Type, A -> A -> Bool.
Check fun (A B : Type) (a : _) (b : _) (C : Type), eq C a b.
Variable a : Bool
Variable b : Bool
Variable H : a /\ b
Theorem t1 : b := Discharge (fun H1, Conj H1 (Conjunct1 H)).
Theorem t2 : a = b := Trans (Refl a) (Refl b).
Check f Bool Bool.
Theorem pierce (a b : Bool) : ((a ⇒ b) ⇒ a) ⇒ a :=
Discharge (λ H, DisjCases (EM a)
(λ H_a, H)
(λ H_na, NotImp1 (MT H H_na)))

81
tests/lean/elab1.lean.expected.out Normal file
View file

@ -0,0 +1,81 @@
Set: pp::colors
Set: pp::unicode
Assumed: f
Error (line: 4, pos: 6) type mismatch at application
f 10 ⊤
Function type:
Π (A : Type) (a b : A), A
Arguments types:
ℕ : Type
10 : ℕ
⊤ : Bool
Assumed: g
Error (line: 7, pos: 6) unsolved placeholder at term
g 10
Assumed: h
Error (line: 11, pos: 27) application type mismatch during term elaboration
h A x
Function type:
Π (A : Type) (_ : A), A
Arguments types:
A : Type
x : lift:0:2 ?M0
Elaborator state
#0 ≈ lift:0:2 ?M0
Assumed: eq
Error (line: 15, pos: 51) application type mismatch during term elaboration
eq C a b
Function type:
Π (A : Type) (_ _ : A), Bool
Arguments types:
C : Type
a : lift:0:3 ?M0
b : lift:0:2 ?M2
Elaborator state
#0 ≈ lift:0:2 ?M2
#0 ≈ lift:0:3 ?M0
Assumed: a
Assumed: b
Assumed: H
Error (line: 20, pos: 18) type mismatch during term elaboration
Discharge (λ H1 : _, Conj H1 (Conjunct1 H))
Term after elaboration:
Discharge (λ H1 : ?M4, Conj H1 (Conjunct1 H))
Expected type:
b
Got:
?M4 ⇒ ?M2
Elaborator state
lift:0:1 ?M2 ≈ lift:0:1 ?M4 ∧ a
b ≈ if Bool ?M4 ?M2 ⊤
b ≈ if Bool ?M4 ?M2 ⊤
Error (line: 22, pos: 22) type mismatch at application
Trans (Refl a) (Refl b)
Function type:
Π (A : Type U) (a b c : A) (H1 : a = b) (H2 : b = c), a = c
Arguments types:
Bool : Type
a : Bool
a : Bool
b : Bool
Refl a : a = a
Refl b : b = b
Error (line: 24, pos: 6) type mismatch at application
f Bool Bool
Function type:
Π (A : Type) (a b : A), A
Arguments types:
Type : Type 1
Bool : Type
Bool : Type
Error (line: 27, pos: 21) type mismatch at application
DisjCases (EM a) (λ H_a : a, H) (λ H_na : ¬ a, NotImp1 (MT H H_na))
Function type:
Π (a b c : Bool) (H1 : a ∨ b) (H2 : a → c) (H3 : b → c), c
Arguments types:
a : Bool
¬ a : Bool
a : Bool
EM a : a ∨ ¬ a
(λ H_a : a, H) : a → ((a ⇒ b) ⇒ a)
(λ H_na : ¬ a, NotImp1 (MT H H_na)) : (¬ a) → a

7
tests/lean/tst7.lean.expected.out
View file

@ -2,8 +2,13 @@
Set: pp::unicode
Assumed: f
λ (A B : Type) (a : B), f B a
Error (line: 4, pos: 40) application type mismatch during term elaboration at term
Error (line: 4, pos: 40) application type mismatch during term elaboration
f B a
Function type:
Π (A : Type) (_ : A), Bool
Arguments types:
B : Type
a : lift:0:2 ?M0
Elaborator state
#0 ≈ lift:0:2 ?M0
Assumed: myeq