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

feat(kernel/error_msgs): add error message for unsatisfied level constraints, remove messages for dependent pairs

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-04-25 10:46:17 -07:00
parent 508bccb0c5
commit 3e122ed355
2 changed files with 8 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/kernel/error_msgs.cpp
View file

@ -19,10 +19,6 @@ format pp_function_expected(formatter const & fmt, options const & opts, expr co
return compose(format("function expected at"), pp_indent_expr(fmt, opts, e)); return compose(format("function expected at"), pp_indent_expr(fmt, opts, e));
} }
format pp_pair_expected(formatter const & fmt, options const & opts, expr const & e) {
return compose(format("pair expected at"), pp_indent_expr(fmt, opts, e));
}
format pp_app_type_mismatch(formatter const & fmt, options const & opts, expr const & app, format pp_app_type_mismatch(formatter const & fmt, options const & opts, expr const & app,
expr const & expected_type, expr const & given_type) { expr const & expected_type, expr const & given_type) {
format r; format r;
@ -35,16 +31,6 @@ format pp_app_type_mismatch(formatter const & fmt, options const & opts, expr co
return r; return r;
} }
format pp_proj_type_mismatch(formatter const & fmt, options const & opts, expr const & proj,
expr const & arg_type) {
format r;
r += format("type mismatch at projection");
r += pp_indent_expr(fmt, opts, proj);
r += format("pair expected, given type:");
r += pp_indent_expr(fmt, opts, arg_type);
return r;
}
format pp_def_type_mismatch(formatter const & fmt, options const & opts, name const & n, format pp_def_type_mismatch(formatter const & fmt, options const & opts, name const & n,
expr const & expected_type, expr const & given_type) { expr const & expected_type, expr const & given_type) {
format r("type mismatch at definition '"); format r("type mismatch at definition '");
@ -55,4 +41,11 @@ format pp_def_type_mismatch(formatter const & fmt, options const & opts, name co
r += pp_indent_expr(fmt, opts, given_type); r += pp_indent_expr(fmt, opts, given_type);
return r; return r;
} }
format pp_def_lvl_cnstrs_satisfied(formatter const & fmt, options const & opts, expr const & e, level const & lhs, level const & rhs) {
format r("constand definition level constraints are not satisfied");
r += pp_indent_expr(fmt, opts, e);
r += format("level constraint:");
r += pp(lhs, rhs, opts);
return r;
}
} }

4
src/kernel/error_msgs.h
View file

@ -10,11 +10,9 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
format pp_type_expected(formatter const & fmt, options const & opts, expr const & e); format pp_type_expected(formatter const & fmt, options const & opts, expr const & e);
format pp_function_expected(formatter const & fmt, options const & opts, expr const & e); format pp_function_expected(formatter const & fmt, options const & opts, expr const & e);
format pp_pair_expected(formatter const & fmt, options const & opts, expr const & e);
format pp_app_type_mismatch(formatter const & fmt, options const & opts, expr const & app, format pp_app_type_mismatch(formatter const & fmt, options const & opts, expr const & app,
expr const & expected_type, expr const & given_type); expr const & expected_type, expr const & given_type);
format pp_proj_type_mismatch(formatter const & fmt, options const & opts, expr const & proj,
expr const & arg_type);
format pp_def_type_mismatch(formatter const & fmt, options const & opts, name const & n, format pp_def_type_mismatch(formatter const & fmt, options const & opts, name const & n,
expr const & expected_type, expr const & given_type); expr const & expected_type, expr const & given_type);
format pp_def_lvl_cnstrs_satisfied(formatter const & fmt, options const & opts, expr const & e, level const & lhs, level const & rhs);
} }