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

Fix type mismatch error message

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-13 19:24:11 -07:00
parent 392b347f53
commit 2dad1e0e33
2 changed files with 17 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/kernel/type_check.cpp
View file

@ -134,12 +134,12 @@ struct infer_type_fn {
expr const & c = arg(e, i);
expr c_t = infer_type(c, ctx);
if (!is_convertible(abst_domain(f_t), c_t, m_env, ctx)) {
format msg = format{format("type mismatch at argument "), format(i), format("of"),
format msg = format{format("type mismatch at argument "), format(i), space(), format("of"),
nl_indent(fmt()(e, ctx)), line(),
format("expected type:"),
nl_indent(fmt()(abst_domain(f_t), ctx)), line(),
format("given type:"),
nl_indent(fmt()(c_t, ctx))};
nl_indent(fmt()(c_t, ctx)), line()};
push_context(msg, ctx);
throw_exception(arg(e,i), msg);
}

15
src/tests/kernel/type_check.cpp
View file

@ -115,6 +115,20 @@ static void tst6() {
}
}
static void tst7() {
environment env = mk_toplevel();
expr A = Const(name{"foo", "bla", "bla", "foo"});
expr f = Const("f");
expr x = Const("x");
expr t = Fun({A, Type()}, Fun({f, arrow(Int, arrow(A, arrow(A, arrow(A, arrow(A, arrow(A, A))))))}, Fun({x, Int}, f(x, x))));
try {
infer_type(t, env);
lean_unreachable();
} catch (exception & ex) {
std::cout << "Error: " << ex.what() << "\n";
}
}
int main() {
continue_on_violation(true);
tst1();
@ -123,5 +137,6 @@ int main() {
tst4();
tst5();
tst6();
tst7();
return has_violations() ? 1 : 0;
}