From 93090baa82cd37e4ed81e30f7d586ee0e7be88fd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 28 Sep 2020 13:27:24 -0700
Subject: [PATCH] chore: cleanup `tactic` syntax

---
 src/Lean/Parser/Tactic.lean | 15 +++++++--------
 src/Lean/Parser/Term.lean   | 16 +++++++++++++---
 2 files changed, 20 insertions(+), 11 deletions(-)

diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean
index ee08d9b94e..a2f8f41338 100644
--- a/src/Lean/Parser/Tactic.lean
+++ b/src/Lean/Parser/Tactic.lean
@@ -9,9 +9,6 @@ namespace Lean
 namespace Parser
 namespace Tactic
 
-def seq  := node `Lean.Parser.Tactic.seq $ sepBy tacticParser "; " true
-def seq1 := node `Lean.Parser.Tactic.seq $ sepBy1 tacticParser "; " true
-
 def underscoreFn : ParserFn :=
 fun c s =>
   let s   := symbolFn "_" c s;
@@ -38,13 +35,13 @@ def ident' : Parser := ident <|> underscore
 @[builtinTacticParser] def «exact»      := parser! nonReservedSymbol "exact " >> termParser
 @[builtinTacticParser] def «refine»     := parser! nonReservedSymbol "refine " >> termParser
 @[builtinTacticParser] def «refine!»    := parser! nonReservedSymbol "refine! " >> termParser
-@[builtinTacticParser] def «case»       := parser! nonReservedSymbol "case " >> ident >> darrow >> indentedNonEmptySeq
-@[builtinTacticParser] def «allGoals»   := parser! nonReservedSymbol "allGoals " >> indentedNonEmptySeq
+@[builtinTacticParser] def «case»       := parser! nonReservedSymbol "case " >> ident >> darrow >> tacticSeq1
+@[builtinTacticParser] def «allGoals»   := parser! nonReservedSymbol "allGoals " >> tacticSeq1
 @[builtinTacticParser] def «skip»       := parser! nonReservedSymbol "skip"
 @[builtinTacticParser] def «done»       := parser! nonReservedSymbol "done"
 @[builtinTacticParser] def «admit»      := parser! nonReservedSymbol "admit"
 @[builtinTacticParser] def «traceState» := parser! nonReservedSymbol "traceState"
-@[builtinTacticParser] def «failIfSuccess» := parser! nonReservedSymbol "failIfSuccess " >> indentedNonEmptySeq
+@[builtinTacticParser] def «failIfSuccess» := parser! nonReservedSymbol "failIfSuccess " >> tacticSeq1
 @[builtinTacticParser] def «generalize» := parser! nonReservedSymbol "generalize " >> optional (try (ident >> " : ")) >> termParser 51 >> " = " >> ident
 
 def locationWildcard := parser! "*"
@@ -61,7 +58,7 @@ def rwRuleSeq := parser! "[" >> sepBy1 rwRule ", " true >> "]"
 @[builtinTacticParser] def «rewriteSeq» := parser! (nonReservedSymbol "rewrite" <|> nonReservedSymbol "rw") >> rwRuleSeq >> optional location
 
 def majorPremise := parser! optional (try (ident >> " : ")) >> termParser
-def altRHS := Term.hole <|> Term.syntheticHole <|> indentedNonEmptySeq
+def altRHS := Term.hole <|> Term.syntheticHole <|> tacticSeq1
 def inductionAlt  : Parser := nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident' >> many ident' >> darrow >> altRHS
 def inductionAlts : Parser := withPosition $ "|" >> sepBy1 inductionAlt (checkColGe "alternatives must be indented" >> "|")
 def withAlts : Parser := optional (" with " >> inductionAlts)
@@ -77,8 +74,10 @@ def matchAlts : Parser := group $ withPosition $ (optional "| ") >> sepBy1 match
 
 def withIds : Parser := optional (" with " >> many1 ident')
 @[builtinTacticParser] def «injection»  := parser! nonReservedSymbol "injection " >> termParser >> withIds
+def seq  := node `Lean.Parser.Tactic.seq $ sepBy tacticParser "; " true
+def seq1 := node `Lean.Parser.Tactic.seq $ sepBy1 tacticParser "; " true
 @[builtinTacticParser] def paren        := parser! "(" >> seq1 >> ")"
-@[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> seq >> "}"
+@[builtinTacticParser] def nestedTactic := parser! "{" >> seq >> "}"
 @[builtinTacticParser] def orelse := tparser!:2 " <|> " >> tacticParser 1
 
 /- Term binders as tactics. They are all implemented as macros using the triad: named holes, hygiene, and `refine` tactic. -/
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index a43eb56a4a..6a897af147 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -19,9 +19,19 @@ registerBuiltinDynamicParserAttribute `tacticParser `tactic
 @[inline] def tacticParser (rbp : Nat := 0) : Parser :=
 categoryParser `tactic rbp
 
-def Tactic.indentedNonEmptySeq : Parser :=
+namespace Tactic
+
+def tacticSeq1Indented : Parser :=
 nodeWithAntiquot "tacticSeq" `Lean.Parser.Tactic.seq $ withPosition $
   sepBy1 tacticParser (try ("; " >>  checkColGe "tatic must be indented"))
+def tacticSeq1Bracketed : Parser :=
+  parser! "{" >> sepBy1 tacticParser "; " true >> "}"
+def tacticSeq1 := tacticSeq1Bracketed <|> tacticSeq1Indented
+
+def tacticSeqBracketed : Parser :=
+  parser! "{" >> sepBy tacticParser "; " true >> "}"
+
+end Tactic
 
 def darrow : Parser := " => "
 
@@ -43,7 +53,7 @@ checkPrec prec >> symbol sym >> termParser (prec+1)
 
 /- Built-in parsers -/
 
-@[builtinTermParser] def byTactic := parser!:leadPrec "by " >> Tactic.indentedNonEmptySeq
+@[builtinTermParser] def byTactic := parser!:leadPrec "by " >> Tactic.tacticSeq1
 
 -- `checkPrec` necessary for the pretty printer
 @[builtinTermParser] def ident := checkPrec maxPrec >> Parser.ident
@@ -85,7 +95,7 @@ def optType : Parser := optional typeSpec
 @[builtinTermParser] def inaccessible := parser! ".(" >> termParser >> ")"
 def binderIdent : Parser  := ident <|> hole
 def binderType (requireType := false) : Parser := if requireType then group (" : " >> termParser) else optional (" : " >> termParser)
-def binderTactic  := parser! try (" := " >> " by ") >> Tactic.indentedNonEmptySeq
+def binderTactic  := parser! try (" := " >> " by ") >> Tactic.tacticSeq1
 def binderDefault := parser! " := " >> termParser
 def explicitBinder (requireType := false) := ppGroup $ parser! "(" >> many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault) >> ")"
 def implicitBinder (requireType := false) := ppGroup $ parser! "{" >> many1 binderIdent >> binderType requireType >> "}"