feat(frontends/lean/parse_tactic_location): make rewrite notation more uniform

src/frontends/lean/parse_tactic_location.cpp

@@ -11,37 +11,28 @@ Author: Leonardo de Moura
 
 namespace lean {
 static occurrence parse_occurrence(parser & p) {
+    bool is_pos = true;
+    if (p.curr_is_token(get_sub_tk())) {
+        p.next();
+        is_pos = false;
+        if (!p.curr_is_token(get_lcurly_tk()))
+            throw parser_error("invalid tactic location, '{' expected", p.pos());
+    }
     if (p.curr_is_token(get_lcurly_tk())) {
         p.next();
-        bool has_pos = false;
-        bool has_neg = false;
         buffer<unsigned> occs;
         while (true) {
-            if (p.curr_is_token(get_sub_tk())) {
+            auto pos   = p.pos();
-                if (has_pos)
+            unsigned i = p.parse_small_nat();
-                    throw parser_error("invalid tactic location, cannot mix positive and negative occurrences", p.pos());
+            if (i == 0)
-                has_neg = true;
+                throw parser_error("invalid tactic location, first occurrence is 1", pos);
-                p.next();
+            occs.push_back(i);
-                auto pos   = p.pos();
+            if (!p.curr_is_token(get_comma_tk()))
-                unsigned i = p.parse_small_nat();
-                if (i == 0)
-                    throw parser_error("invalid tactic location, first occurrence is 1", pos);
-                occs.push_back(i);
-            } else {
-                auto pos   = p.pos();
-                unsigned i = p.parse_small_nat();
-                if (i == 0)
-                    throw parser_error("invalid tactic location, first occurrence is 1", pos);
-                occs.push_back(i);
-                if (has_neg)
-                    throw parser_error("invalid tactic location, cannot mix positive and negative occurrences", pos);
-                has_pos = true;
-            }
-            if (p.curr_is_token(get_rcurly_tk()))
                 break;
+            p.next();
         }
-        p.next();
+        p.check_token_next(get_rcurly_tk(), "invalid tactic location, '}' or ',' expected");
-        if (has_pos)
+        if (is_pos)
             return occurrence::mk_occurrences(occs);
         else
             return occurrence::mk_except_occurrences(occs);
@@ -88,7 +79,7 @@ location parse_tactic_location(parser & p) {
             } else {
                 return location::mk_hypotheses_at(hyps, hyp_occs);
             }
-        } else if (p.curr_is_token(get_lcurly_tk())) {
+        } else if (p.curr_is_token(get_lcurly_tk()) || p.curr_is_token(get_sub_tk())) {
             occurrence o = parse_occurrence(p);
             return location::mk_goal_at(o);
         } else {

tests/lean/hott/rewriter1.hlean

@@ -6,7 +6,7 @@ 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
+    add_right_id at {1, 3}, -- rewrite 1st and 3rd occurrences
     {0 + _}add_comm]   -- apply commutativity to (0 + _)
 end
 

tests/lean/run/rewrite12.lean

@@ -0,0 +1,9 @@
+import data.nat
+open nat
+variables (f : nat → nat → nat → nat) (a b c : nat)
+
+example (H₁ : a = b) (H₂ : f b a b = 0) : f a a a = 0 :=
+by rewrite ⟨H₁ at -{2}, H₂⟩
+
+example (H₁ : a = b) (H₂ : f b a b = 0) (H₃ : c = f a a a) : c = 0 :=
+by rewrite ⟨H₁ at H₃ -{2}, H₂ at H₃, H₃⟩

tests/lean/run/rewriter2.lean

@@ -5,7 +5,7 @@ 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
+  rewrite [add_zero at {1, 3}, -- rewrite 1st and 3rd occurrences
            {0 + _}add.comm]   -- apply commutativity to (0 + _)
 end
 
@@ -16,7 +16,7 @@ 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
+    -(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