From a31457efde892fa1c6098151e50b895bd6e7bf15 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 13 Jul 2014 01:24:55 +0100
Subject: [PATCH] fix(frontends/lean/parser): copy rec and initial fields when
 processing Exprs and ScopedExpr

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/parser.cpp | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 6ad3d6cd9..5157798e0 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -695,21 +695,22 @@ expr parser::parse_notation(parse_table t, expr * left) {
                 next();
                 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()) {
                 unsigned i = r_args.size();
                 while (i > 0) {
                     --i;
                     args.push_back(r_args[i]);
                     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();
                 }
             } else {
                 for (unsigned i = 0; i < r_args.size(); i++) {
                     args.push_back(r_args[i]);
                     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();
                 }
             }
@@ -725,10 +726,11 @@ expr parser::parse_notation(parse_table t, expr * left) {
             lenv = parse_binders(ps);
             break;
         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)) {
                 r = abstract(ps, r, a.use_lambda_abstraction(), binder_pos);
             } else {
+                expr rec = copy_with_new_pos(a.get_rec(), p);
                 unsigned i = ps.size();
                 while (i > 0) {
                     --i;
@@ -739,7 +741,7 @@ expr parser::parse_notation(parse_table t, expr * left) {
                         r = Pi(l, r);
                     r = save_pos(r, binder_pos);
                     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();
                 }
             }