From f0b5ec8dfa034fdd672f875c9b4f2618155d7985 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 19 Aug 2013 16:14:19 -0700
Subject: [PATCH] Fix bug in parse_arrow

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontend/parser.cpp       | 7 +++++++
 src/tests/frontend/parser.cpp | 2 ++
 2 files changed, 9 insertions(+)

diff --git a/src/frontend/parser.cpp b/src/frontend/parser.cpp
index f0ee47675b..ac53f63321 100644
--- a/src/frontend/parser.cpp
+++ b/src/frontend/parser.cpp
@@ -59,6 +59,11 @@ static name g_overload_name(name(name(name(0u), "parser"), "overload"));
 static expr g_overload = mk_constant(g_overload_name);
 // ==========================================
 
+// A name that can't be created by the user.
+// It is used as placeholder for parsing A -> B expressions which
+// are syntax sugar for (Pi (_ : A), B)
+static name g_unused(name(0u), "parser");
+
 /**
     \brief Functional object for parsing
 
@@ -471,6 +476,8 @@ class parser_fn {
     /** \brief Parse <tt>expr '->' expr</tt>. */
     expr parse_arrow(expr const & left) {
         next();
+        mk_scope scope(*this);
+        register_binding(g_unused);
         // The -1 is a trick to get right associativity in Pratt's parsers
         expr right = parse_expr(g_arrow_precedence-1);
         return mk_arrow(left, right);
diff --git a/src/tests/frontend/parser.cpp b/src/tests/frontend/parser.cpp
index 039e53e5ef..dc27241ddd 100644
--- a/src/tests/frontend/parser.cpp
+++ b/src/tests/frontend/parser.cpp
@@ -34,6 +34,8 @@ static void tst1() {
     parse(fe, "Show true && false Eval true && false");
     parse(fe, "Infixl 35 & and Show true & false & false Eval true & false");
     parse(fe, "Mixfixc 100 if then fi implies Show if true then false fi");
+    parse(fe, "Show Pi (A : Type), A -> A");
+    parse(fe, "Check Pi (A : Type), A -> A");
 }
 
 static void check(frontend const & fe, char const * str, expr const & expected) {