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

feat(library/tactic/elaborate): better error message for tactics using elaborate_with_respect_to

Browse source
This commit is contained in:
Leonardo de Moura 2015-03-01 13:42:53 -08:00
parent a1066ebdf4
commit e07c6675b3
1 changed files with 12 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/library/tactic/elaborate.cpp
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura Author: Leonardo de Moura
*/ */
#include "kernel/error_msgs.h"
#include "library/reducible.h" #include "library/reducible.h"
#include "library/unifier.h" #include "library/unifier.h"
#include "library/tactic/elaborate.h" #include "library/tactic/elaborate.h"
@ -53,8 +54,18 @@ optional<expr> elaborate_with_respect_to(environment const & env, io_state const
expr t = subst.instantiate(*expected_type); expr t = subst.instantiate(*expected_type);
e_t_cs.second.linearize(cs); e_t_cs.second.linearize(cs);
auto d_cs = tc->is_def_eq(e_t_cs.first, t); auto d_cs = tc->is_def_eq(e_t_cs.first, t);
if (!d_cs.first) if (!d_cs.first) {
throw_tactic_exception_if_enabled(s, [=](formatter const & fmt) {
format r = format("invalid tactic, term");
r += pp_indent_expr(fmt, new_e);
r += compose(line(), format("has type"));
r += pp_indent_expr(fmt, e_t_cs.first);
r += compose(line(), format("but is expected to have type"));
r += pp_indent_expr(fmt, t);
return r;
});
return none_expr(); return none_expr();
}
d_cs.second.linearize(cs); d_cs.second.linearize(cs);
} }
unifier_config cfg(ios.get_options()); unifier_config cfg(ios.get_options());