From 18aee9de30116f8cf4dc8f9f3d50237b03d3dbaf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 22 Dec 2020 11:39:10 -0800
Subject: [PATCH] fix: precedence issues at tactic DSL

---
 src/Init/Notation.lean       | 31 ++++++++++++++++++-------------
 tests/lean/run/allGoals.lean | 29 +++++++++++++++++++++++++++++
 2 files changed, 47 insertions(+), 13 deletions(-)

diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 3ba333907b..48d8180906 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -159,6 +159,10 @@ macro_rules
       `(%[ $elems,* | List.nil ])
 
 namespace Parser.Tactic
+/- The precedence 3 will "terminate" terms by
+   '<|>' (precedence 2) and '>>' (precedence 1). It should be used for any (potentially)
+   trailing expression parameters in the tactic DSL. -/
+def tacTerm : ParserDescr := ParserDescr.cat `term 3
 
 syntax (name := intro) "intro " notFollowedBy("|") (colGt term:max)* : tactic
 syntax (name := intros) "intros " (colGt (ident <|> "_"))* : tactic
@@ -166,10 +170,10 @@ syntax (name := revert) "revert " (colGt ident)+ : tactic
 syntax (name := clear) "clear " (colGt ident)+ : tactic
 syntax (name := subst) "subst " (colGt ident)+ : tactic
 syntax (name := assumption) "assumption" : tactic
-syntax (name := apply) "apply " term : tactic
-syntax (name := exact) "exact " term : tactic
-syntax (name := refine) "refine " term : tactic
-syntax (name := refine!) "refine! " term : tactic
+syntax (name := apply) "apply " tacTerm : tactic
+syntax (name := exact) "exact " tacTerm : tactic
+syntax (name := refine) "refine " tacTerm : tactic
+syntax (name := refine!) "refine! " tacTerm : tactic
 syntax (name := case) "case " ident " => " tacticSeq : tactic
 syntax (name := allGoals) "allGoals " tacticSeq : tactic
 syntax (name := focus) "focus " tacticSeq : tactic
@@ -184,6 +188,7 @@ syntax (name := withReducibleAndInstances) "withReducibleAndInstances " tacticSe
 syntax:2 (name := orelse) tactic "<|>" tactic:1 : tactic
 macro "try " t:tacticSeq : tactic => `(($t) <|> skip)
 
+macro:1 x:tactic " <;> " y:tactic:0 : tactic => `(tactic| focus ($x:tactic; allGoals $y:tactic))
 
 macro "rfl" : tactic => `(exact rfl)
 macro "decide!" : tactic => `(exact decide!)
@@ -194,10 +199,10 @@ syntax locationTarget   := "⊢" <|> "|-"
 syntax locationHyp      := (colGt ident)+
 syntax location         := withPosition("at " locationWildcard <|> locationTarget <|> locationHyp)
 
-syntax (name := change) "change " term (location)? : tactic
-syntax (name := changeWith) "change " term " with " term (location)? : tactic
+syntax (name := change) "change " tacTerm (location)? : tactic
+syntax (name := changeWith) "change " term " with " tacTerm (location)? : tactic
 
-syntax rwRule    := ("←" <|> "<-")? term
+syntax rwRule    := ("←" <|> "<-")? tacTerm
 syntax rwRuleSeq := "[" rwRule,+,? "]"
 
 syntax (name := rewrite) "rewrite " rwRule (location)? : tactic
@@ -229,25 +234,25 @@ def expandERw : Macro :=
 def expandERwSeq : Macro :=
   fun stx => withCheapRefl (stx.setKind `Lean.Parser.Tactic.erewriteSeq |>.setArg 0 (mkAtomFrom stx "erewrite"))
 
-syntax (name := injection) "injection " term (" with " (colGt (ident <|> "_"))+)? : tactic
+syntax (name := injection) "injection " tacTerm (" with " (colGt (ident <|> "_"))+)? : tactic
 
 syntax (name := «have») "have " haveDecl : tactic
 syntax (name := «suffices») "suffices " sufficesDecl : tactic
-syntax (name := «show») "show " term : tactic
+syntax (name := «show») "show " tacTerm : tactic
 syntax (name := «let») "let " letDecl : tactic
 syntax (name := «let!») "let! " letDecl : tactic
 syntax (name := letrec) withPosition(atomic(group("let " &"rec ")) letRecDecls) : tactic
 
 syntax inductionAlt  := "| " (ident <|> "_") (ident <|> "_")* " => " (hole <|> syntheticHole <|> tacticSeq)
 syntax inductionAlts := "with " withPosition( (colGe inductionAlt)+)
-syntax (name := induction) "induction " term,+ (" using " ident)?  ("generalizing " ident+)? (inductionAlts)? : tactic
-syntax casesTarget := atomic(ident " : ")? term
+syntax (name := induction) "induction " tacTerm,+ (" using " ident)?  ("generalizing " ident+)? (inductionAlts)? : tactic
+syntax casesTarget := atomic(ident " : ")? tacTerm
 syntax (name := cases) "cases " casesTarget,+ (" using " ident)? (inductionAlts)? : tactic
 
-syntax (name := existsIntro) "exists " term : tactic
+syntax (name := existsIntro) "exists " tacTerm : tactic
 
 /- We use a priority > default, to avoid ambiguity with the builtin `have` notation -/
-macro (priority := high) "have" x:ident " := " p:term : tactic => `(have $x:ident : _ := $p)
+macro (priority := high) "have" x:ident " := " p:tacTerm : tactic => `(have $x:ident : _ := $p)
 
 syntax "repeat " tacticSeq : tactic
 macro_rules
diff --git a/tests/lean/run/allGoals.lean b/tests/lean/run/allGoals.lean
index 5bd5f18da1..09f02101af 100644
--- a/tests/lean/run/allGoals.lean
+++ b/tests/lean/run/allGoals.lean
@@ -29,3 +29,32 @@ def Weekday.previous : Weekday -> Weekday
 theorem Weekday.nextOfPrevious (d : Weekday) : next (previous d) = d := by
   cases d
   allGoals rfl
+
+theorem Weekday.nextOfPrevious' (d : Weekday) : previous (next d) = d ∧ next (previous d) = d := by
+  apply And.intro
+  cases d <;> rfl
+  cases d <;> rfl
+
+theorem Weekday.nextOfPrevious'' (d : Weekday) : previous (next d) = d ∧ next (previous d) = d := by
+  apply And.intro <;> cases d <;> rfl
+
+open Lean.Parser.Tactic in
+macro "rwd " x:tacTerm : tactic => `(rw $x:term; done)
+
+theorem ex (a b c : α) (h₁ : a = b) (h₂ : a = c) : b = a ∧ c = a := by
+  apply And.intro <;> rwd h₁ <|> rwd h₂
+
+theorem idEq (a : α) : id a = a :=
+  rfl
+
+theorem Weekday.test (d : Weekday) : next (previous d) = id d := by
+  cases d
+  traceState
+  allGoals rw idEq
+  traceState
+  allGoals rfl
+
+theorem Weekday.test2 (d : Weekday) : next (previous d) = id d := by
+  cases d <;> rw idEq
+  traceState
+  allGoals rfl