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

fix(frontends/lean/parser): copy rec and initial fields when processing Exprs and ScopedExpr

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-13 01:24:55 +01:00
parent ea2fffc260
commit a31457efde
1 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -695,21 +695,22 @@ expr parser::parse_notation(parse_table t, expr * left) {
next(); next();
r_args.push_back(parse_expr(a.rbp())); r_args.push_back(parse_expr(a.rbp()));
} }
expr r = instantiate_rev(a.get_initial(), args.size(), args.data()); expr r = instantiate_rev(copy_with_new_pos(a.get_initial(), p), args.size(), args.data());
expr rec = copy_with_new_pos(a.get_rec(), p);
if (a.is_fold_right()) { if (a.is_fold_right()) {
unsigned i = r_args.size(); unsigned i = r_args.size();
while (i > 0) { while (i > 0) {
--i; --i;
args.push_back(r_args[i]); args.push_back(r_args[i]);
args.push_back(r); args.push_back(r);
r = instantiate_rev(a.get_rec(), args.size(), args.data()); r = instantiate_rev(rec, args.size(), args.data());
args.pop_back(); args.pop_back(); args.pop_back(); args.pop_back();
} }
} else { } else {
for (unsigned i = 0; i < r_args.size(); i++) { for (unsigned i = 0; i < r_args.size(); i++) {
args.push_back(r_args[i]); args.push_back(r_args[i]);
args.push_back(r); args.push_back(r);
r = instantiate_rev(a.get_rec(), args.size(), args.data()); r = instantiate_rev(rec, args.size(), args.data());
args.pop_back(); args.pop_back(); args.pop_back(); args.pop_back();
} }
} }
@ -725,10 +726,11 @@ expr parser::parse_notation(parse_table t, expr * left) {
lenv = parse_binders(ps); lenv = parse_binders(ps);
break; break;
case notation::action_kind::ScopedExpr: { case notation::action_kind::ScopedExpr: {
expr r = parse_scoped_expr(ps, lenv, a.rbp()); expr r = parse_scoped_expr(ps, lenv, a.rbp());
if (is_var(a.get_rec(), 0)) { if (is_var(a.get_rec(), 0)) {
r = abstract(ps, r, a.use_lambda_abstraction(), binder_pos); r = abstract(ps, r, a.use_lambda_abstraction(), binder_pos);
} else { } else {
expr rec = copy_with_new_pos(a.get_rec(), p);
unsigned i = ps.size(); unsigned i = ps.size();
while (i > 0) { while (i > 0) {
--i; --i;
@ -739,7 +741,7 @@ expr parser::parse_notation(parse_table t, expr * left) {
r = Pi(l, r); r = Pi(l, r);
r = save_pos(r, binder_pos); r = save_pos(r, binder_pos);
args.push_back(r); args.push_back(r);
r = instantiate_rev(a.get_rec(), args.size(), args.data()); r = instantiate_rev(rec, args.size(), args.data());
args.pop_back(); args.pop_back();
} }
} }