feat(frontends/lean/parse_rewrite_tactic): polish rewrite tactic notation

src/frontends/lean/parse_rewrite_tactic.cpp

@@ -46,43 +46,25 @@ expr parse_rewrite_element(parser & p) {
     }
     if (p.curr_is_numeral()) {
         unsigned n = p.parse_small_nat();
-        if (p.curr_is_token(get_question_tk())) {
+        if (p.curr_is_token(get_greater_tk())) {
             p.next();
             optional<expr> pat = parse_pattern(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);
-            expr H = parse_rule(p);
-            location loc = parse_tactic_location(p);
-            return mk_rewrite_exactly_n(pat, H, symm, n, loc);
         } else {
             optional<expr> pat = parse_pattern(p);
             expr H = parse_rule(p);
             location loc = parse_tactic_location(p);
             return mk_rewrite_exactly_n(pat, H, symm, n, loc);
         }
-    } else if (p.curr_is_token(get_question_tk())) {
+    } else if (p.curr_is_token(get_star_tk())) {
         p.next();
         optional<expr> pat = parse_pattern(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())) {
+    } else if (p.curr_is_token(get_plus_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);
         expr H = parse_rule(p);
@@ -103,8 +85,8 @@ expr parse_rewrite_tactic(parser & p) {
         elems.push_back(p.save_pos(parse_rewrite_element(p), pos));
         if (!p.curr_is_token(get_sub_tk()) &&
             !p.curr_is_numeral() &&
-            !p.curr_is_token(get_bang_tk()) &&
+            !p.curr_is_token(get_plus_tk()) &&
-            !p.curr_is_token(get_question_tk()) &&
+            !p.curr_is_token(get_star_tk()) &&
             !p.curr_is_token(get_slash_tk()) &&
             !p.curr_is_identifier() &&
             !p.curr_is_token(get_lbracket_tk()) &&

src/frontends/lean/tokens.cpp

@@ -26,11 +26,13 @@ static name * g_bar          = nullptr;
 static name * g_comma        = nullptr;
 static name * g_add          = nullptr;
 static name * g_sub          = nullptr;
+static name * g_greater      = 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;
+static name * g_plus         = nullptr;
 static name * g_turnstile    = nullptr;
 static name * g_max          = nullptr;
 static name * g_imax         = nullptr;
@@ -133,10 +135,12 @@ void initialize_tokens() {
     g_comma        = new name(",");
     g_add          = new name("+");
     g_sub          = new name("-");
+    g_greater      = new name(">");
     g_question     = new name("?");
     g_question_lp  = new name("?(");
     g_bang         = new name("!");
     g_slash        = new name("/");
+    g_plus         = new name("+");
     g_star         = new name("*");
     g_turnstile    = new name("⊢");
     g_max          = new name("max");
@@ -304,10 +308,12 @@ void finalize_tokens() {
     delete g_max;
     delete g_add;
     delete g_sub;
+    delete g_greater;
     delete g_question;
     delete g_question_lp;
     delete g_bang;
     delete g_slash;
+    delete g_plus;
     delete g_star;
     delete g_turnstile;
     delete g_comma;
@@ -348,11 +354,13 @@ name const & get_bar_tk() { return *g_bar; }
 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_greater_tk() { return *g_greater; }
 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; }
+name const & get_plus_tk() { return *g_plus; }
 name const & get_turnstile_tk() { return *g_turnstile; }
 name const & get_max_tk() { return *g_max; }
 name const & get_imax_tk() { return *g_imax; }

src/frontends/lean/tokens.h

@@ -33,6 +33,8 @@ name const & get_question_lp_tk();
 name const & get_bang_tk();
 name const & get_slash_tk();
 name const & get_star_tk();
+name const & get_plus_tk();
+name const & get_greater_tk();
 name const & get_turnstile_tk();
 name const & get_max_tk();
 name const & get_imax_tk();