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

feat(library/coercion): closes #794

Browse source 
Include level information in primary coercion error message if
pp_options are set to display levels.
This commit is contained in:
Daniel Selsam 2015-08-13 19:30:29 -07:00 • committed by Leonardo de Moura
parent 6c934229f7
commit f4e1e9d671
1 changed files with 19 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/library/coercion.cpp
View file

@ -16,6 +16,8 @@ Author: Leonardo de Moura
#include "library/module.h" #include "library/module.h"
#include "library/kernel_serializer.h" #include "library/kernel_serializer.h"
#include "library/scoped_ext.h" #include "library/scoped_ext.h"
#include "library/pp_options.h"
#include "library/generic_exception.h"
namespace lean { namespace lean {
static name * g_fun = nullptr; static name * g_fun = nullptr;
@ -230,11 +232,23 @@ static void check_pi(name const & f, expr const & t) {
// similar to check_pi, but produces a more informative message // similar to check_pi, but produces a more informative message
static void check_valid_coercion(name const & f, expr const & t) { static void check_valid_coercion(name const & f, expr const & t) {
if (!is_pi(t)) { if (!is_pi(t)) {
throw exception(sstream() << "invalid coercion, type of '" << f throw_generic_exception(optional<expr>(),[=](formatter const & fmt) {
<< "' does not match any of the allowed expected types for coercions\n" options o = fmt.get_options();
<< " Pi (x_1 : A_1) ... (x_n : A_n) (y: C x_1 ... x_n), D t_1 ... t_m\n" bool show_universes = get_pp_universes(o) || get_pp_all(o);
<< " Pi (x_1 : A_1) ... (x_n : A_n) (y: C x_1 ... x_n), Type\n" std::string ls = show_universes ? ".{ls}" : "";
<< " Pi (x_1 : A_1) ... (x_n : A_n) (y: C x_1 ... x_n), A -> B"); std::string us = show_universes ? ".{us}" : "";
std::string u = show_universes ? ".{u}" : "";
return format((sstream()
<< "invalid coercion, type of '" << f
<< "' does not match any of the acceptable forms "
<< "for coercions\n"
<< "coe" << ls << " : Pi (x_1 : A_1) ... (x_n : A_n) (y: C"
<< ls << " x_1 ... x_n), D" << us << " t_1 ... t_m\n"
<< "coe" << ls << " : Pi (x_1 : A_1) ... (x_n : A_n) (y: C"
<< ls << " x_1 ... x_n), Type" << u << "\n"
<< "coe" << ls << " : Pi (x_1 : A_1) ... (x_n : A_n) (y: C"
<< ls << " x_1 ... x_n), (Pi x : A, B x)").str());
});
} }
} }