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

fix(library/coercion): error message

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-17 06:59:52 -07:00
parent 1436212a34
commit 5bc62f0ba9
1 changed files with 11 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/library/coercion.cpp
View file

@ -109,6 +109,16 @@ static void check_pi(name const & f, expr const & t) {
throw exception(sstream() << "invalid coercion, '" << f << "' is not function");
}
// similar to check_pi, but produces a more informative message
static void check_valid_coercion(name const & f, expr const & t) {
if (!is_pi(t)) {
throw exception(sstream() << "invalid coercion, type of '" << f << "' does not match any of the allowed expected types for coercions\n"
<< " Pi (x_1 : A_1) ... (x_n : A_n) (y: C x_1 ... x_n), D t_1 ... t_m\n"
<< " Pi (x_1 : A_1) ... (x_n : A_n) (y: C x_1 ... x_n), Type\n"
<< " Pi (x_1 : A_1) ... (x_n : A_n) (y: C x_1 ... x_n), A -> B\n");
}
}
/** \brief Return true iff args contains Var(0), Var(1), ..., Var(args.size() - 1) */
static bool check_var_args(buffer<expr> const & args) {
for (unsigned i = 0; i < args.size(); i++) {
@ -294,7 +304,7 @@ coercion_state add_coercion(environment const & env, io_state const & ios, coerc
}
t = binding_body(t);
num++;
check_pi(f, t);
check_valid_coercion(f, t);
}
}