From dfad24e3f56b3ae222a0cdeeee9732ca20e67e82 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Feb 2015 10:15:58 -0800 Subject: [PATCH] feat(frontends/lean): polish rewrite tactic notation --- src/frontends/lean/parse_rewrite_tactic.cpp | 10 +++++++--- src/frontends/lean/token_table.cpp | 2 +- src/frontends/lean/tokens.cpp | 20 ++++++++++++++++++++ src/frontends/lean/tokens.h | 5 +++++ tests/lean/run/rewrite4.lean | 13 +++++++++++++ 5 files changed, 46 insertions(+), 4 deletions(-) create mode 100644 tests/lean/run/rewrite4.lean diff --git a/src/frontends/lean/parse_rewrite_tactic.cpp b/src/frontends/lean/parse_rewrite_tactic.cpp index b92418e7b..126a6ce26 100644 --- a/src/frontends/lean/parse_rewrite_tactic.cpp +++ b/src/frontends/lean/parse_rewrite_tactic.cpp @@ -33,7 +33,7 @@ static expr parse_rule(parser & p) { } expr parse_rewrite_element(parser & p) { - if (p.curr_is_token(get_slash_tk())) { + if (p.curr_is_token(get_up_tk()) || p.curr_is_token(get_caret_tk())) { p.next(); name n = p.check_id_next("invalid unfold rewrite step, identifier expected"); location loc = parse_tactic_location(p); @@ -80,7 +80,8 @@ expr parse_rewrite_element(parser & p) { expr parse_rewrite_tactic(parser & p) { buffer elems; - if (p.curr_is_token(get_lbracket_tk())) { + bool lbraket = p.curr_is_token(get_lbracket_tk()); + if (lbraket || p.curr_is_token(get_langle_tk())) { p.next(); while (true) { auto pos = p.pos(); @@ -89,7 +90,10 @@ expr parse_rewrite_tactic(parser & p) { break; p.next(); } - p.check_token_next(get_rbracket_tk(), "invalid rewrite tactic, ']' expected"); + if (lbraket) + p.check_token_next(get_rbracket_tk(), "invalid rewrite tactic, ']' expected"); + else + p.check_token_next(get_rangle_tk(), "invalid rewrite tactic, '⟩' expected"); } else { auto pos = p.pos(); elems.push_back(p.save_pos(parse_rewrite_element(p), pos)); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 1fdd87288..68dea0c80 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -78,7 +78,7 @@ void init_token_table(token_table & t) { {"if", 0}, {"then", 0}, {"else", 0}, {"by", 0}, {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec}, {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, - {"{|", g_max_prec}, {"|}", 0}, {"⊢", 0}, + {"{|", g_max_prec}, {"|}", 0}, {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0}, {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0}, {"with", 0}, {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {":=", 0}, {"--", 0}, {"#", 0}, {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec}, diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index 117380c8a..ee3a4416a 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -22,6 +22,11 @@ static name * g_lcurlybar = nullptr; static name * g_rcurlybar = nullptr; static name * g_lbracket = nullptr; static name * g_rbracket = nullptr; +static name * g_langle = nullptr; +static name * g_rangle = nullptr; +static name * g_triangle = nullptr; +static name * g_caret = nullptr; +static name * g_up = nullptr; static name * g_bar = nullptr; static name * g_comma = nullptr; static name * g_add = nullptr; @@ -131,6 +136,11 @@ void initialize_tokens() { g_rcurlybar = new name("|}"); g_lbracket = new name("["); g_rbracket = new name("]"); + g_langle = new name("⟨"); + g_rangle = new name("⟩"); + g_triangle = new name("▸"); + g_caret = new name("^"); + g_up = new name("↑"); g_bar = new name("|"); g_comma = new name(","); g_add = new name("+"); @@ -318,6 +328,11 @@ void finalize_tokens() { delete g_turnstile; delete g_comma; delete g_bar; + delete g_langle; + delete g_rangle; + delete g_triangle; + delete g_caret; + delete g_up; delete g_rbracket; delete g_lbracket; delete g_rdcurly; @@ -339,6 +354,11 @@ name const & get_period_tk() { return *g_period; } name const & get_placeholder_tk() { return *g_placeholder; } name const & get_colon_tk() { return *g_colon; } name const & get_dcolon_tk() { return *g_dcolon; } +name const & get_langle_tk() { return *g_langle; } +name const & get_rangle_tk() { return *g_rangle; } +name const & get_triangle_tk() { return *g_triangle; } +name const & get_caret_tk() { return *g_caret; } +name const & get_up_tk() { return *g_up; } name const & get_lparen_tk() { return *g_lparen; } name const & get_rparen_tk() { return *g_rparen; } name const & get_llevel_curly_tk() { return *g_llevel_curly; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index 8899f733b..7976798ef 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -24,6 +24,11 @@ name const & get_lcurlybar_tk(); name const & get_rcurlybar_tk(); name const & get_lbracket_tk(); name const & get_rbracket_tk(); +name const & get_langle_tk(); +name const & get_rangle_tk(); +name const & get_triangle_tk(); +name const & get_caret_tk(); +name const & get_up_tk(); name const & get_bar_tk(); name const & get_comma_tk(); name const & get_add_tk(); diff --git a/tests/lean/run/rewrite4.lean b/tests/lean/run/rewrite4.lean new file mode 100644 index 000000000..01dad3705 --- /dev/null +++ b/tests/lean/run/rewrite4.lean @@ -0,0 +1,13 @@ +import data.nat +open algebra + +constant f {A : Type} : A → A → A + +theorem test1 {A : Type} [s : comm_ring A] (a b c : A) (H : a + 0 = 0) : f a a = f 0 0 := +by rewrite ⟨add_zero at H, H⟩ + +theorem test2 {A : Type} [s : comm_ring A] (a b c : A) (H : a + 0 = 0) : f a a = f 0 0 := +by rewrite ⟨add_zero at *, H⟩ + +theorem test3 {A : Type} [s : comm_ring A] (a b c : A) (H : a + 0 = 0 + 0) : f a a = f 0 0 := +by rewrite ⟨add_zero at H, zero_add at H, H⟩