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

fix(frontends/lean/builtin_exprs): better error position

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-06 13:43:09 -07:00
parent fb8ae7f411
commit 5eddff44ab
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -548,18 +548,18 @@ static expr parse_do(parser & p, unsigned, expr const *, pos_info const & pos) {
r = p.rec_save_pos(mk_app(p.save_pos(mk_constant(get_monad_bind_name()), ps[i]), es[i], Fun(*lhs, r)), ps[i]);
} else {
// must introduce a "fake" match
expr fn = mk_local(mk_fresh_name(), *g_do_match_name, mk_expr_placeholder(), binder_info());
auto pos = ps[i];
expr fn = p.save_pos(mk_local(mk_fresh_name(), *g_do_match_name, mk_expr_placeholder(), binder_info()), pos);
buffer<expr> locals;
to_buffer(lhss_locals[i], locals);
auto pos = ps[i];
buffer<expr> eqs;
eqs.push_back(p.save_pos(Fun(fn, Fun(locals, p.save_pos(mk_equation(mk_app(fn, *lhs), r), pos), p)), pos));
eqs.push_back(p.rec_save_pos(Fun(fn, Fun(locals, p.save_pos(mk_equation(p.rec_save_pos(mk_app(fn, *lhs), pos), r), pos), p)), pos));
if (optional<expr> else_case = else_cases[i]) {
// add case
// _ := else_case
eqs.push_back(p.save_pos(Fun(fn, p.save_pos(mk_equation(mk_app(fn, mk_expr_placeholder()),
*else_case),
pos)),
eqs.push_back(p.rec_save_pos(Fun(fn, p.save_pos(mk_equation(p.rec_save_pos(mk_app(fn, mk_expr_placeholder()), pos),
*else_case),
pos)),
pos));
}
expr eqns = p.save_pos(mk_equations(1, eqs.size(), eqs.data()), pos);