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

fix(frontends/lean): save equations position

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-06 15:55:04 -08:00
parent 760dc2162a
commit a9b6e20a22
2 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/decl_cmds.cpp
View file

@ -400,10 +400,11 @@ expr parse_equations(parser & p, name const & n, expr const & type, buffer<name>
if (p.curr_is_token(get_with_tk())) {
while (p.curr_is_token(get_with_tk())) {
p.next();
auto pos = p.pos();
name g_name = p.check_id_next("invalid declaration, identifier expected");
p.check_token_next(get_colon_tk(), "invalid declaration, ':' expected");
expr g_type = p.parse_expr();
expr g = mk_local(g_name, g_type);
expr g = p.save_pos(mk_local(g_name, g_type), pos);
auxs.push_back(g_name);
fns.push_back(g);
}
@ -435,13 +436,14 @@ expr parse_equations(parser & p, name const & n, expr const & type, buffer<name>
}
validate_equation_lhs(p, lhs, locals);
lhs = merge_equation_lhs_vars(lhs, locals);
auto assign_pos = p.pos();
p.check_token_next(get_assign_tk(), "invalid declaration, ':=' expected");
{
parser::local_scope scope2(p);
for (expr const & local : locals)
p.add_local(local);
expr rhs = p.parse_expr();
eqns.push_back(Fun(fns, Fun(locals, mk_equation(lhs, rhs), p)));
eqns.push_back(Fun(fns, Fun(locals, p.save_pos(mk_equation(lhs, rhs), assign_pos), p)));
}
if (!p.curr_is_token(get_comma_tk()))
break;

2
src/frontends/lean/elaborator.cpp
View file

@ -1058,7 +1058,7 @@ expr elaborator::visit_equation(expr const & eq, constraint_seq & cs) {
pair<expr, constraint_seq> new_rhs_cs = ensure_has_type(new_rhs, rhs_type, lhs_type, j, m_relax_main_opaque);
new_rhs = new_rhs_cs.first;
cs += new_rhs_cs.second;
return mk_equation(new_lhs, new_rhs);
return copy_tag(eq, mk_equation(new_lhs, new_rhs));
}
expr elaborator::visit_inaccessible(expr const & e, constraint_seq & cs) {