From 15efadfbdcb528b1dd53d9cd36690fe9aebe9a00 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 Feb 2015 20:16:24 -0800 Subject: [PATCH] feat(frontends/lean/parse_rewrite_tactic): cleanup rewrite tactic notation Make a rewrite command sequence explicit. --- src/frontends/lean/parse_rewrite_tactic.cpp | 25 +++++++++++---------- tests/lean/hott/rewriter1.hlean | 10 ++++----- tests/lean/run/rewriter1.lean | 2 +- tests/lean/run/rewriter2.lean | 23 +++++++++---------- tests/lean/run/rewriter3.lean | 3 +-- 5 files changed, 31 insertions(+), 32 deletions(-) diff --git a/src/frontends/lean/parse_rewrite_tactic.cpp b/src/frontends/lean/parse_rewrite_tactic.cpp index 75b8a29f1..b92418e7b 100644 --- a/src/frontends/lean/parse_rewrite_tactic.cpp +++ b/src/frontends/lean/parse_rewrite_tactic.cpp @@ -11,10 +11,10 @@ Author: Leonardo de Moura namespace lean { static optional parse_pattern(parser & p) { - if (p.curr_is_token(get_lbracket_tk())) { + if (p.curr_is_token(get_lcurly_tk())) { p.next(); expr r = p.parse_expr(); - p.check_token_next(get_rbracket_tk(), "invalid rewrite pattern, ']' expected"); + p.check_token_next(get_rcurly_tk(), "invalid rewrite pattern, '}' expected"); return some_expr(r); } else { return none_expr(); @@ -80,18 +80,19 @@ expr parse_rewrite_element(parser & p) { expr parse_rewrite_tactic(parser & p) { buffer elems; - while (true) { + if (p.curr_is_token(get_lbracket_tk())) { + p.next(); + while (true) { + auto pos = p.pos(); + elems.push_back(p.save_pos(parse_rewrite_element(p), pos)); + if (!p.curr_is_token(get_comma_tk())) + break; + p.next(); + } + p.check_token_next(get_rbracket_tk(), "invalid rewrite tactic, ']' expected"); + } else { auto pos = p.pos(); 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_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()) && - !p.curr_is_token(get_lparen_tk())) - break; } return mk_rewrite_tactic_expr(elems); } diff --git a/tests/lean/hott/rewriter1.hlean b/tests/lean/hott/rewriter1.hlean index ecc6e97d3..42fef7fb2 100644 --- a/tests/lean/hott/rewriter1.hlean +++ b/tests/lean/hott/rewriter1.hlean @@ -5,15 +5,15 @@ constant f {A : Type} : A → A → A theorem test1 {A : Type} [s : add_comm_group A] (a b c : A) : f (a + 0) (f (a + 0) (a + 0)) = f a (f (0 + a) a) := begin - rewrite - add_right_id at {1 3} -- rewrite 1st and 3rd occurrences - [0 + _]add_comm -- apply commutativity to (0 + _) + rewrite [ + add_right_id at {1 3}, -- rewrite 1st and 3rd occurrences + {0 + _}add_comm] -- apply commutativity to (0 + _) end axiom Ax {A : Type} [s₁ : has_mul A] [s₂ : has_one A] (a : A) : f (a * 1) (a * 1) = 1 theorem test2 {A : Type} [s : comm_group A] (a b c : A) : f a a = 1 := begin - rewrite -(mul_right_id a) -- - means apply symmetry, rewrite 0 ==> a * 0 at 1st and 2nd occurrences - Ax -- use Ax as rewrite rule + rewrite [-(mul_right_id a), -- - means apply symmetry, rewrite 0 ==> a * 0 at 1st and 2nd occurrences + Ax] -- use Ax as rewrite rule end diff --git a/tests/lean/run/rewriter1.lean b/tests/lean/run/rewriter1.lean index dc5a347f0..009782810 100644 --- a/tests/lean/run/rewriter1.lean +++ b/tests/lean/run/rewriter1.lean @@ -3,7 +3,7 @@ open algebra theorem test {A : Type} [s : comm_ring A] (a b c : A) : a + b + c = a + c + b := begin - rewrite add.assoc [b + _]add.comm -add.assoc, + rewrite [add.assoc, {b + _}add.comm, -add.assoc] end print definition test diff --git a/tests/lean/run/rewriter2.lean b/tests/lean/run/rewriter2.lean index 92684a611..cf56993dc 100644 --- a/tests/lean/run/rewriter2.lean +++ b/tests/lean/run/rewriter2.lean @@ -5,9 +5,8 @@ constant f {A : Type} : A → A → A theorem test1 {A : Type} [s : comm_ring A] (a b c : A) : f (a + 0) (f (a + 0) (a + 0)) = f a (f (0 + a) a) := begin - rewrite - add_zero at {1 3} -- rewrite 1st and 3rd occurrences - [0 + _]add.comm -- apply commutativity to (0 + _) + rewrite [add_zero at {1 3}, -- rewrite 1st and 3rd occurrences + {0 + _}add.comm] -- apply commutativity to (0 + _) end check @mul_zero @@ -16,27 +15,27 @@ axiom Ax {A : Type} [s₁ : has_mul A] [s₂ : has_zero A] (a : A) : f (a * 0) ( theorem test2 {A : Type} [s : comm_ring A] (a b c : A) : f 0 0 = 0 := begin - rewrite - -(mul_zero a) at {1 2} -- - means apply symmetry, rewrite 0 ==> a * 0 at 1st and 2nd occurrences - Ax -- use Ax as rewrite rule + rewrite [ + -(mul_zero a) at {1 2}, -- - means apply symmetry, rewrite 0 ==> a * 0 at 1st and 2nd occurrences + Ax] -- use Ax as rewrite rule end theorem test3 {A : Type} [s : comm_ring A] (a b c : A) : a * 0 + 0 * b + c * 0 + 0 * a = 0 := begin - rewrite +mul_zero +zero_mul +add_zero -- in rewrite rules, + is notation for one or more + rewrite [+mul_zero, +zero_mul, +add_zero] -- in rewrite rules, + is notation for one or more end print definition test3 theorem test4 {A : Type} [s : comm_ring A] (a b c : A) : a * 0 + 0 * b + c * 0 + 0 * a = 0 := begin - rewrite *mul_zero *zero_mul *add_zero *zero_add -- in rewrite rules, * is notation for zero or more + rewrite [*mul_zero, *zero_mul, *add_zero, *zero_add] -- in rewrite rules, * is notation for zero or more end theorem test5 {A : Type} [s : comm_ring A] (a b c : A) : a * 0 + 0 * b + c * 0 + 0 * a = 0 := begin - rewrite - 2 mul_zero -- apply mul_zero exactly twice - 2 zero_mul -- apply zero_mul exactly twice - 5>add_zero -- apply add_zero at most 5 times + rewrite [ + 2 mul_zero, -- apply mul_zero exactly twice + 2 zero_mul, -- apply zero_mul exactly twice + 5>add_zero] -- apply add_zero at most 5 times end diff --git a/tests/lean/run/rewriter3.lean b/tests/lean/run/rewriter3.lean index 1b253d8c0..752db2fd2 100644 --- a/tests/lean/run/rewriter3.lean +++ b/tests/lean/run/rewriter3.lean @@ -17,7 +17,6 @@ end theorem test3 {A : Type} [s : comm_ring A] (a b c : A) (H : a + 0 = 0 + 0) : f a a = f 0 0 := begin - rewrite add_zero at H, - rewrite zero_add at H, + rewrite [add_zero at H, zero_add at H], rewrite H end