From 3e122ed3556b7287e42427fb2b0371579cc8a1f5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Apr 2014 10:46:17 -0700 Subject: [PATCH] feat(kernel/error_msgs): add error message for unsatisfied level constraints, remove messages for dependent pairs Signed-off-by: Leonardo de Moura --- src/kernel/error_msgs.cpp | 21 +++++++-------------- src/kernel/error_msgs.h | 4 +--- 2 files changed, 8 insertions(+), 17 deletions(-) diff --git a/src/kernel/error_msgs.cpp b/src/kernel/error_msgs.cpp index 2e70d4606..4e3739438 100644 --- a/src/kernel/error_msgs.cpp +++ b/src/kernel/error_msgs.cpp @@ -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)); } -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, expr const & expected_type, expr const & given_type) { format r; @@ -35,16 +31,6 @@ format pp_app_type_mismatch(formatter const & fmt, options const & opts, expr co 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, expr const & expected_type, expr const & given_type) { 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); 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; +} } diff --git a/src/kernel/error_msgs.h b/src/kernel/error_msgs.h index a8bd4c473..b24b1f63e 100644 --- a/src/kernel/error_msgs.h +++ b/src/kernel/error_msgs.h @@ -10,11 +10,9 @@ Author: Leonardo de Moura namespace lean { 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_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, 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, 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); }