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

fix(frontends/lean/builtin_exprs): do not hide elaborated field info when local inference fails

Browse source
This commit is contained in:
Sebastian Ullrich 2017-03-27 14:45:39 +02:00 • committed by Leonardo de Moura
parent e63c1d3347
commit 00cb784bd8
1 changed files with 5 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/frontends/lean/builtin_exprs.cpp
View file

@ -1039,7 +1039,6 @@ unsigned get_field_notation_field_idx(expr const & e) {
static expr parse_proj(parser_state & p, unsigned, expr const * args, pos_info const & pos) {
try {
p.check_break_at_pos(break_at_pos_exception::token_context::expr);
if (p.curr_is_numeral()) {
pos_info num_pos = p.pos();
unsigned fidx = p.parse_small_nat();
@ -1051,6 +1050,10 @@ static expr parse_proj(parser_state & p, unsigned, expr const * args, pos_info c
return p.save_pos(mk_proj_notation(args[0], field), pos);
}
} catch (break_at_pos_exception & ex) {
if (!p.get_complete()) {
// info is stored at position of notation token
ex.m_token_info.m_pos = pos;
}
expr lhs = args[0];
expr lhs_type;
try {
@ -1061,16 +1064,12 @@ static expr parse_proj(parser_state & p, unsigned, expr const * args, pos_info c
lhs_type = tc.infer(lhs);
} catch (exception &) {
/* failed to elaborate or infer type */
throw;
throw ex;
}
expr fn = get_app_fn(lhs_type);
if (is_constant(fn)) {
ex.m_token_info.m_struct = const_name(fn);
ex.m_token_info.m_context = break_at_pos_exception::token_context::field;
if (!p.get_complete()) {
// info is stored at position of notation token
ex.m_token_info.m_pos = pos;
}
}
throw;
}