From 69d83ecb86475d7346fedfe7b90a9dfdb8d65cf2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 22 Dec 2020 13:37:27 -0800 Subject: [PATCH] chore: make sure term and tactic parsers have disjoint infix operators --- src/Init/Notation.lean | 38 ++++++++++++++------------------ src/Lean/Elab/Tactic/Basic.lean | 4 ++-- tests/lean/run/allGoals.lean | 4 ++-- tests/lean/run/elab_cmd.lean | 2 +- tests/lean/run/newfrontend1.lean | 2 +- 5 files changed, 22 insertions(+), 28 deletions(-) diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index a3a9e5b46a..3444f27aa7 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -161,21 +161,16 @@ 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 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 " tacTerm : tactic -syntax (name := exact) "exact " tacTerm : tactic -syntax (name := refine) "refine " tacTerm : tactic -syntax (name := refine!) "refine! " tacTerm : 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 := case) "case " ident " => " tacticSeq : tactic syntax (name := allGoals) "allGoals " tacticSeq : tactic syntax (name := focus) "focus " tacticSeq : tactic @@ -187,9 +182,8 @@ syntax (name := generalize) "generalize " atomic(ident " : ")? term:51 " = " ide syntax (name := paren) "(" tacticSeq ")" : tactic syntax (name := withReducible) "withReducible " tacticSeq : tactic syntax (name := withReducibleAndInstances) "withReducibleAndInstances " tacticSeq : tactic -syntax:2 (name := orelse) tactic "<|>" tactic:1 : tactic -macro "try " t:tacticSeq : tactic => `(($t) <|> skip) - +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) @@ -201,10 +195,10 @@ syntax locationTarget := "⊢" <|> "|-" syntax locationHyp := (colGt ident)+ syntax location := withPosition("at " locationWildcard <|> locationTarget <|> locationHyp) -syntax (name := change) "change " tacTerm (location)? : tactic -syntax (name := changeWith) "change " term " with " tacTerm (location)? : tactic +syntax (name := change) "change " term (location)? : tactic +syntax (name := changeWith) "change " term " with " term (location)? : tactic -syntax rwRule := ("←" <|> "<-")? tacTerm +syntax rwRule := ("←" <|> "<-")? term syntax rwRuleSeq := "[" rwRule,+,? "]" syntax (name := rewrite) "rewrite " rwRule (location)? : tactic @@ -236,29 +230,29 @@ def expandERw : Macro := def expandERwSeq : Macro := fun stx => withCheapRefl (stx.setKind `Lean.Parser.Tactic.erewriteSeq |>.setArg 0 (mkAtomFrom stx "erewrite")) -syntax (name := injection) "injection " tacTerm (" with " (colGt (ident <|> "_"))+)? : tactic +syntax (name := injection) "injection " term (" with " (colGt (ident <|> "_"))+)? : tactic syntax (name := «have») "have " haveDecl : tactic syntax (name := «suffices») "suffices " sufficesDecl : tactic -syntax (name := «show») "show " tacTerm : tactic +syntax (name := «show») "show " term : 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 " tacTerm,+ (" using " ident)? ("generalizing " ident+)? (inductionAlts)? : tactic -syntax casesTarget := atomic(ident " : ")? tacTerm +syntax (name := induction) "induction " term,+ (" using " ident)? ("generalizing " ident+)? (inductionAlts)? : tactic +syntax casesTarget := atomic(ident " : ")? term syntax (name := cases) "cases " casesTarget,+ (" using " ident)? (inductionAlts)? : tactic -syntax (name := existsIntro) "exists " tacTerm : tactic +syntax (name := existsIntro) "exists " term : tactic /- We use a priority > default, to avoid ambiguity with the builtin `have` notation -/ -macro (priority := high) "have" x:ident " := " p:tacTerm : tactic => `(have $x:ident : _ := $p) +macro (priority := high) "have" x:ident " := " p:term : tactic => `(have $x:ident : _ := $p) syntax "repeat " tacticSeq : tactic macro_rules - | `(tactic| repeat $seq) => `(tactic| (($seq); repeat $seq) <|> skip) + | `(tactic| repeat $seq) => `(tactic| (($seq); repeat $seq) skip) end Parser.Tactic end Lean diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index af20fee660..5c920123a6 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -453,8 +453,8 @@ private def findTag? (gs : List MVarId) (tag : Name) : TacticM (Option MVarId) : @[builtinTactic «orelse»] def evalOrelse : Tactic := fun stx => match stx with - | `(tactic| $tac1 <|> $tac2) => evalTactic tac1 <|> evalTactic tac2 - | _ => throwUnsupportedSyntax + | `(tactic| $tac1 $tac2) => evalTactic tac1 <|> evalTactic tac2 + | _ => throwUnsupportedSyntax builtin_initialize registerTraceClass `Elab.tactic diff --git a/tests/lean/run/allGoals.lean b/tests/lean/run/allGoals.lean index 09f02101af..7801d0c1bd 100644 --- a/tests/lean/run/allGoals.lean +++ b/tests/lean/run/allGoals.lean @@ -39,10 +39,10 @@ theorem Weekday.nextOfPrevious'' (d : Weekday) : previous (next d) = d ∧ next apply And.intro <;> cases d <;> rfl open Lean.Parser.Tactic in -macro "rwd " x:tacTerm : tactic => `(rw $x:term; done) +macro "rwd " x:term : 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₂ + apply And.intro <;> try rwd h₁ rwd h₂ theorem idEq (a : α) : id a = a := rfl diff --git a/tests/lean/run/elab_cmd.lean b/tests/lean/run/elab_cmd.lean index 76a2754d5f..35e288ea16 100644 --- a/tests/lean/run/elab_cmd.lean +++ b/tests/lean/run/elab_cmd.lean @@ -20,7 +20,7 @@ elab "#check2" b:term : command => do #check2 10 elab "try" t:tactic : tactic => do - let t' ← `(tactic| $t <|> skip); + let t' ← `(tactic| $t skip); Lean.Elab.Tactic.evalTactic t' theorem tst (x y z : Nat) : y = z → x = x → x = y → x = z := diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean index 04a95ae060..2cec146844 100644 --- a/tests/lean/run/newfrontend1.lean +++ b/tests/lean/run/newfrontend1.lean @@ -111,7 +111,7 @@ intros h1 _ h3 traceState focus refine! Eq.trans ?pre ?post - (exact h1) <|> (exact y; exact h3; assumption) + (exact h1) (exact y; exact h3; assumption) namespace Foo def Prod.mk := 1