From 08dcc9e2fc5f96171078c20c25265de86de8fc6d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 Feb 2015 19:19:19 -0800 Subject: [PATCH] feat(frontends/lean/parse_rewrite_tactic): polish rewrite tactic notation --- src/frontends/lean/parse_rewrite_tactic.cpp | 28 ++++----------------- src/frontends/lean/tokens.cpp | 8 ++++++ src/frontends/lean/tokens.h | 2 ++ 3 files changed, 15 insertions(+), 23 deletions(-) diff --git a/src/frontends/lean/parse_rewrite_tactic.cpp b/src/frontends/lean/parse_rewrite_tactic.cpp index 117e8a732..75b8a29f1 100644 --- a/src/frontends/lean/parse_rewrite_tactic.cpp +++ b/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 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(), H, symm, n, loc); - } else if (p.curr_is_token(get_bang_tk())) { - p.next(); - optional 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 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 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())) { - 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(), H, symm, loc); - } else if (p.curr_is_token(get_bang_tk())) { + } else if (p.curr_is_token(get_plus_tk())) { p.next(); optional 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_question_tk()) && + !p.curr_is_token(get_plus_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()) && diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index 48bd6a3f1..117380c8a 100644 --- a/src/frontends/lean/tokens.cpp +++ b/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; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index 511985113..8899f733b 100644 --- a/src/frontends/lean/tokens.h +++ b/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();