From 8912c759dda631b05affb7db6ef1211acfc1a21b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 3 Feb 2015 12:20:37 -0800
Subject: [PATCH] fix(frontends/lean/parse_rewrite_tactic): corner case
 "rewrite ?(t)"

The token '?(' is used to represent inaccessible terms in recursive
equations. In the rewriter tactic, we want "rewrite ?(t)" to be parsed
as "? (t)".
---
 src/frontends/lean/parse_rewrite_tactic.cpp | 12 ++++++++++++
 src/frontends/lean/tokens.cpp               |  4 ++++
 src/frontends/lean/tokens.h                 |  1 +
 3 files changed, 17 insertions(+)

diff --git a/src/frontends/lean/parse_rewrite_tactic.cpp b/src/frontends/lean/parse_rewrite_tactic.cpp
index ec680f7a7..117e8a732 100644
--- a/src/frontends/lean/parse_rewrite_tactic.cpp
+++ b/src/frontends/lean/parse_rewrite_tactic.cpp
@@ -52,6 +52,12 @@ expr parse_rewrite_element(parser & p) {
             expr H = parse_rule(p);
             location loc = parse_tactic_location(p);
             return mk_rewrite_at_most_n(pat, H, symm, n, loc);
+        } else if (p.curr_is_token(get_question_lp_tk())) {
+            p.next();
+            expr H = p.parse_expr();
+            p.check_token_next(get_rparen_tk(), "invalid rewrite pattern, ')' expected");
+            location loc = parse_tactic_location(p);
+            return mk_rewrite_at_most_n(optional<expr>(), H, symm, n, loc);
         } else if (p.curr_is_token(get_bang_tk())) {
             p.next();
             optional<expr> pat = parse_pattern(p);
@@ -70,6 +76,12 @@ expr parse_rewrite_element(parser & p) {
         expr H = parse_rule(p);
         location loc = parse_tactic_location(p);
         return mk_rewrite_zero_or_more(pat, H, symm, loc);
+    } else if (p.curr_is_token(get_question_lp_tk())) {
+        p.next();
+        expr H = p.parse_expr();
+        p.check_token_next(get_rparen_tk(), "invalid rewrite pattern, ')' expected");
+        location loc = parse_tactic_location(p);
+        return mk_rewrite_zero_or_more(optional<expr>(), H, symm, loc);
     } else if (p.curr_is_token(get_bang_tk())) {
         p.next();
         optional<expr> pat = parse_pattern(p);
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index 459bcbf74..48bd6a3f1 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -27,6 +27,7 @@ static name * g_comma        = nullptr;
 static name * g_add          = nullptr;
 static name * g_sub          = nullptr;
 static name * g_question     = nullptr;
+static name * g_question_lp  = nullptr;
 static name * g_bang         = nullptr;
 static name * g_slash        = nullptr;
 static name * g_star         = nullptr;
@@ -133,6 +134,7 @@ void initialize_tokens() {
     g_add          = new name("+");
     g_sub          = new name("-");
     g_question     = new name("?");
+    g_question_lp  = new name("?(");
     g_bang         = new name("!");
     g_slash        = new name("/");
     g_star         = new name("*");
@@ -303,6 +305,7 @@ void finalize_tokens() {
     delete g_add;
     delete g_sub;
     delete g_question;
+    delete g_question_lp;
     delete g_bang;
     delete g_slash;
     delete g_star;
@@ -346,6 +349,7 @@ name const & get_comma_tk() { return *g_comma; }
 name const & get_add_tk() { return *g_add; }
 name const & get_sub_tk() { return *g_sub; }
 name const & get_question_tk() { return *g_question; }
+name const & get_question_lp_tk() { return *g_question_lp; }
 name const & get_bang_tk() { return *g_bang; }
 name const & get_slash_tk() { return *g_slash; }
 name const & get_star_tk() { return *g_star; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index f28d4006f..511985113 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -29,6 +29,7 @@ name const & get_comma_tk();
 name const & get_add_tk();
 name const & get_sub_tk();
 name const & get_question_tk();
+name const & get_question_lp_tk();
 name const & get_bang_tk();
 name const & get_slash_tk();
 name const & get_star_tk();