max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(frontends/lean/builtin_cmds): display warning message if has_repr instance could not be synthesized

Browse source 
See issue #1861
This commit is contained in:
Leonardo de Moura 2017-11-06 19:23:29 -08:00
parent 8ffdef0b3a
commit 426a9064bf
2 changed files with 9 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/frontends/lean/builtin_cmds.cpp
View file

@ -456,6 +456,7 @@ static environment eval_cmd(parser & p) {
type_context tc(p.env(), transparency_mode::All);
auto type = tc.infer(e);
bool has_repr_inst = false;
/* Check if resultant type has an instance of has_repr */
try {
@ -463,8 +464,9 @@ static environment eval_cmd(parser & p) {
optional<expr> repr_instance = tc.mk_class_instance(has_repr_type);
if (repr_instance) {
/* Modify the 'program' to (repr e) */
e = mk_app(tc, get_repr_name(), type, *repr_instance, e);
type = tc.infer(e);
e = mk_app(tc, get_repr_name(), type, *repr_instance, e);
type = tc.infer(e);
has_repr_inst = true;
}
} catch (exception &) {}
@ -490,6 +492,9 @@ static environment eval_cmd(parser & p) {
if (!fn.try_exec()) {
auto r = fn.invoke_fn();
should_report = true;
if (!has_repr_inst) {
(p.mk_message(p.cmd_pos(), WARNING) << "result type does not have an instance of type class 'has_repr', dumping internal representation").report();
}
if (is_constant(fn.get_type(), get_string_name())) {
out << to_string(r);
} else {

2
tests/lean/1861.lean.expected.out
View file

@ -1,4 +1,6 @@
1861.lean:3:0: warning: result type does not have an instance of type class 'has_repr', dumping internal representation
#2147483647
-1
-1
1861.lean:22:0: warning: result type does not have an instance of type class 'has_repr', dumping internal representation
(#0 #1)