refactor: remove optional leading pipe from match, use `many1Indent…

…` instead of `sepBy1`

src/Lean/Elab/Binders.lean

@@ -4,9 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Elab.Term
+import Lean.Parser.Term
 
 namespace Lean.Elab.Term
 open Meta
+open Lean.Parser.Term
 
 /--
   Given syntax of the forms
@@ -350,10 +352,11 @@ def elabFunBinders {α} (binders : Array Syntax) (expectedType? : Option Expr) (
       x s.fvars s.expectedType?
 
 /- Helper function for `expandEqnsIntoMatch` -/
-private def getMatchAltNumPatterns (matchAlts : Syntax) : Nat :=
-  let alt0 := matchAlts[1][0]
-  let pats := alt0[0].getSepArgs
-  pats.size
+private def getMatchAltsNumPatterns : Syntax → Nat
+  | alts => match alts[0][0] with
+    | `(matchAltExpr| | $pats,* => $rhs) =>
+      pats.getElems.size
+    | _ => unreachable!
 
 private def mkMatch (ref : Syntax) (discrs : Array Syntax) (matchAlts : Syntax) (matchTactic := false) : Syntax :=
   Syntax.node (if matchTactic then `Lean.Parser.Tactic.match else `Lean.Parser.Term.match)
@@ -429,10 +432,10 @@ private def expandMatchAltsIntoMatchAux (ref : Syntax) (matchAlts : Syntax) (mat
     ```
  -/
 def expandMatchAltsIntoMatch (ref : Syntax) (matchAlts : Syntax) (tactic := false) : MacroM Syntax :=
-  expandMatchAltsIntoMatchAux ref matchAlts tactic (getMatchAltNumPatterns matchAlts) #[]
+  expandMatchAltsIntoMatchAux ref matchAlts tactic (getMatchAltsNumPatterns matchAlts) #[]
 
 def expandMatchAltsIntoMatchTactic (ref : Syntax) (matchAlts : Syntax) : MacroM Syntax :=
-  expandMatchAltsIntoMatchAux ref matchAlts true (getMatchAltNumPatterns matchAlts) #[]
+  expandMatchAltsIntoMatchAux ref matchAlts true (getMatchAltsNumPatterns matchAlts) #[]
 
 /--
   Similar to `expandMatchAltsIntoMatch`, but supports an optional `where` clause.
@@ -477,7 +480,7 @@ def expandMatchAltsWhereDecls (ref : Syntax) (matchAltsWhereDecls : Syntax) : Ma
       let x ← `(x)
       let body ← loop n (addDiscr ref discrs x)
       `(@fun $x => $body)
-  loop (getMatchAltNumPatterns matchAlts) #[]
+  loop (getMatchAltsNumPatterns matchAlts) #[]
 
 @[builtinTermElab «fun»] def elabFun : TermElab := fun stx expectedType? => match stx with
   | `(fun $binders* => $body) => do

src/Lean/Elab/Deriving/BEq.lean

@@ -8,7 +8,7 @@ import Lean.Elab.Deriving.Basic
 import Lean.Elab.Deriving.Util
 
 namespace Lean.Elab.Deriving.BEq
-
+open Lean.Parser.Term
 open Meta
 
 structure Header where
@@ -37,7 +37,7 @@ def mkHeader (ctx : Context) (indVal : InductiveVal) : TermElabM Header := do
 def mkMatch (ctx : Context) (header : Header) (indVal : InductiveVal) (auxFunName : Name) (argNames : Array Name) : TermElabM Syntax := do
   let discrs ← mkDiscrs
   let alts ← mkAlts
-  `(match $[$discrs],* with | $[$alts:matchAlt]|*)
+  `(match $[$discrs],* with $alts:matchAlt*)
 where
   mkDiscr (varName : Name) : TermElabM Syntax :=
     `(Parser.Term.matchDiscr| $(mkIdent varName):term)
@@ -57,7 +57,7 @@ where
     patterns := patterns.push (← `(_))
     patterns := patterns.push (← `(_))
     let altRhs ← `(false)
-    `(matchAltExpr| $[$patterns:term],* => $altRhs:term)
+    `(matchAltExpr| | $[$patterns:term],* => $altRhs:term)
 
   mkAlts : TermElabM (Array Syntax) := do
     let mut alts := #[]
@@ -93,7 +93,7 @@ where
               rhs ← `($rhs && $a:ident == $b:ident)
         patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs1:term*))
         patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs2:term*))
-        `(matchAltExpr| $[$patterns:term],* => $rhs:term)
+        `(matchAltExpr| | $[$patterns:term],* => $rhs:term)
       alts := alts.push alt
     alts := alts.push (← mkElseAlt)
     return alts

src/Lean/Elab/Deriving/Util.lean

@@ -12,7 +12,6 @@ open Meta
 def implicitBinderF := Parser.Term.implicitBinder
 def instBinderF     := Parser.Term.instBinder
 def explicitBinderF := Parser.Term.explicitBinder
-def matchAltExpr    := Parser.Term.matchAlt
 
 def mkInductArgNames (indVal : InductiveVal) : TermElabM (Array Name) := do
   forallTelescopeReducing indVal.type fun xs _ => do

src/Lean/Elab/Do.lean

@@ -7,6 +7,7 @@ import Lean.Elab.Term
 import Lean.Elab.Binders
 import Lean.Elab.Match
 import Lean.Elab.Quotation.Util
+import Lean.Parser.Do
 
 namespace Lean.Elab.Term
 open Meta
@@ -1016,15 +1017,12 @@ partial def toTerm : Code → M Syntax
   | Code.seq stx k          => do seqToTerm stx (← toTerm k)
   | Code.ite ref _ o c t e  => do mkIte ref o c (← toTerm t) (← toTerm e)
   | Code.«match» ref discrs optType alts => do
-    let mut termSepAlts := #[]
+    let mut termAlts := #[]
     for alt in alts do
-      termSepAlts := termSepAlts.push $ mkAtomFrom alt.ref "|"
       let rhs ← toTerm alt.rhs
-      let termAlt  := mkNode `Lean.Parser.Term.matchAlt #[alt.patterns, mkAtomFrom alt.ref "=>", rhs]
-      termSepAlts := termSepAlts.push termAlt
-    let firstVBar     := termSepAlts[0]
-    let termSepAlts   := mkNullNode termSepAlts[1:termSepAlts.size]
-    let termMatchAlts := mkNode `Lean.Parser.Term.matchAlts #[mkNullNode #[firstVBar], termSepAlts]
+      let termAlt := mkNode `Lean.Parser.Term.matchAlt #[mkAtomFrom alt.ref "|", alt.patterns, mkAtomFrom alt.ref "=>", rhs]
+      termAlts := termAlts.push termAlt
+    let termMatchAlts := mkNode `Lean.Parser.Term.matchAlts #[mkNullNode termAlts]
     pure $ mkNode `Lean.Parser.Term.«match» #[mkAtomFrom ref "match", discrs, optType, mkAtomFrom ref "with", termMatchAlts]
 
 def run (code : Code) (m : Syntax) (uvars : Array Name := #[]) (kind := Kind.regular) : MacroM Syntax := do
@@ -1328,22 +1326,16 @@ def doForToCode (doSeqToCode : List Syntax → M CodeBlock) (doFor : Syntax) (do
       let auxDo ← `(do let r ← $forInTerm:term; $uvarsTuple:term := r)
       doSeqToCode (getDoSeqElems (getDoSeq auxDo) ++ doElems)
 
-/--
-  Generate `CodeBlock` for `doMatch; doElems`
-  ```
-  def doMatchAlt   := sepBy1 termParser ", " >> darrow >> doSeq
-  def doMatchAlts  := parser! optional "| " >> sepBy1 doMatchAlt "|"
-  def doMatch      := parser! "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> doMatchAlts
-  ``` -/
+/-- Generate `CodeBlock` for `doMatch; doElems` -/
 def doMatchToCode (doSeqToCode : List Syntax → M CodeBlock) (doMatch : Syntax) (doElems: List Syntax) : M CodeBlock := do
   let ref       := doMatch
   let discrs    := doMatch[1]
   let optType   := doMatch[2]
-  let matchAlts := doMatch[4][1].getSepArgs -- Array of `doMatchAlt`
+  let matchAlts := doMatch[4][0].getArgs -- Array of `doMatchAlt`
   let alts ←  matchAlts.mapM fun matchAlt => do
-    let patterns := matchAlt[0]
+    let patterns := matchAlt[1]
     let vars ← getPatternsVarsEx patterns.getSepArgs
-    let rhs  := matchAlt[2]
+    let rhs  := matchAlt[3]
     let rhs ← doSeqToCode (getDoSeqElems rhs)
     pure { ref := matchAlt, vars := vars, patterns := patterns, rhs := rhs : Alt CodeBlock }
   let matchCode ← mkMatch ref discrs optType alts

src/Lean/Elab/Match.lean

@@ -7,22 +7,14 @@ import Lean.Meta.Match.MatchPatternAttr
 import Lean.Meta.Match.Match
 import Lean.Elab.SyntheticMVars
 import Lean.Elab.App
+import Lean.Parser.Term
 
 namespace Lean.Elab.Term
 open Meta
 
 /- This modules assumes "match"-expressions use the following syntax.
 
 ```lean
-def matchAlt : Parser :=
-nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $
-  sepBy1 termParser ", " >> darrow >> termParser
-
-def matchAlts (optionalFirstBar := true) : Parser :=
-group $ withPosition $ fun pos =>
-  (if optionalFirstBar then optional "| " else "| ") >>
-  sepBy1 matchAlt (checkColGe pos.column "alternatives must be indented" >> "|")
-
 def matchDiscr := parser! optional (try (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> termParser
 
 def «match» := parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> matchAlts
@@ -34,12 +26,6 @@ structure MatchAltView where
   patterns : Array Syntax
   rhs      : Syntax
 
-def mkMatchAltView (ref : Syntax) (matchAlt : Syntax) : MatchAltView := {
-  ref      := ref
-  patterns := matchAlt[0].getSepArgs
-  rhs      := matchAlt[2]
-}
-
 private def expandSimpleMatch (stx discr lhsVar rhs : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
   let newStx ← `(let $lhsVar := $discr; $rhs)
   withMacroExpansion stx newStx $ elabTerm newStx expectedType?
@@ -122,28 +108,20 @@ private def elabMatchTypeAndDiscrs (discrStxs : Array Syntax) (matchOptType : Sy
     let discrs ← elabDiscrsWitMatchType discrStxs matchType expectedType
     pure (discrs, matchType, matchAltViews)
 
-/-
-nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $ sepBy1 termParser ", " >> darrow >> termParser
--/
 def expandMacrosInPatterns (matchAlts : Array MatchAltView) : MacroM (Array MatchAltView) := do
   matchAlts.mapM fun matchAlt => do
     let patterns ← matchAlt.patterns.mapM expandMacros
     pure { matchAlt with patterns := patterns }
 
-  /- Given `stx` a match-expression, return its alternatives. -/
-  private def getMatchAlts (stx : Syntax) : Array MatchAltView := do
-  let matchAlts  := stx[4]
-  let firstVBar  := matchAlts[0]
-  let mut ref    := firstVBar
-  let mut result := #[]
-  for arg in matchAlts[1].getArgs do
-    if ref.isNone then
-      ref := arg -- The first vertical bar is optional
-    if arg.getKind == `Lean.Parser.Term.matchAlt then
-      result := result.push (mkMatchAltView ref arg)
-    else
-      ref := arg -- current `arg` is a vertical bar
-  pure result
+/- Given `stx` a match-expression, return its alternatives. -/
+private def getMatchAlts : Syntax → Array MatchAltView
+  | `(match $discrs,* $[: $ty?]? with $[| $patternss,* => $rhss]*) =>
+    patternss.zipWith rhss fun patterns rhs => {
+      ref      := patterns[0],
+      patterns := patterns,
+      rhs      := rhs
+    }
+  | stx => dbgTrace s!"{stx}" fun _ => unreachable!
 
 /--
   Auxiliary annotation used to mark terms marked with the "inaccessible" annotation `.(t)` and
@@ -894,9 +872,7 @@ private def elabMatchCore (stx : Syntax) (expectedType? : Option Expr) : TermEla
 -- parser! "match " >> sepBy1 termParser ", " >> optType >> " with " >> matchAlts
 @[builtinTermElab «match»] def elabMatch : TermElab := fun stx expectedType? =>
   match stx with
-  | `(match $discr:term with $y:ident => $rhs:term)           => expandSimpleMatch stx discr y rhs expectedType?
   | `(match $discr:term with | $y:ident => $rhs:term)         => expandSimpleMatch stx discr y rhs expectedType?
-  | `(match $discr:term : $type with $y:ident => $rhs:term)   => expandSimpleMatchWithType stx discr y type rhs expectedType?
   | `(match $discr:term : $type with | $y:ident => $rhs:term) => expandSimpleMatchWithType stx discr y type rhs expectedType?
   | _ => do
     match (← expandNonAtomicDiscrs? stx) with

src/Lean/Elab/MutualDef.lean

@@ -166,10 +166,6 @@ private def expandWhereDeclsAsStructInst (whereDecls : Syntax) : MacroM Syntax :
 /-
 Recall that
 ```
-def matchAlts (optionalFirstBar := true) : Parser :=
-withPosition $ fun pos =>
-  (if optionalFirstBar then optional "| " else "| ") >>
-  sepBy1 matchAlt (checkColGe pos.column "alternatives must be indented" >> "|")
 def declValSimple    := parser! " :=\n" >> termParser >> optional Term.whereDecls
 def declValEqns      := parser! Term.matchAltsWhereDecls
 def declVal          := declValSimple <|> declValEqns <|> Term.whereDecls

src/Lean/Elab/Quotation.lean

@@ -10,6 +10,7 @@ import Lean.Syntax
 import Lean.ResolveName
 import Lean.Elab.Term
 import Lean.Elab.Quotation.Util
+import Lean.Parser.Term
 
 namespace Lean.Elab.Term.Quotation
 
@@ -343,7 +344,7 @@ private def letBindRhss (cont : List Alt → TermElabM Syntax) : List Alt → Li
 
 def match_syntax.expand (stx : Syntax) : TermElabM Syntax := do
   match stx with
-  | `(match $[$discrs:term],* with $[|]? $[$[$patss],* => $rhss]|*) => do
+  | `(match $[$discrs:term],* with $[| $[$patss],* => $rhss]*) => do
     -- letBindRhss ...
     if patss.all (·.all (!·.isQuot)) then
       -- no quotations => fall back to regular `match`

src/Lean/Elab/Syntax.lean

@@ -172,6 +172,7 @@ end Term
 
 namespace Command
 open Lean.Syntax
+open Lean.Parser.Term hiding macroArg
 open Lean.Parser.Command
 
 private def getCatSuffix (catName : Name) : String :=
@@ -329,54 +330,56 @@ def syntaxAbbrev  := parser! "syntax " >> ident >> " := " >> many1 syntaxParser
   Recall that syntax node kinds contain the current namespace.
 -/
 def elabMacroRulesAux (k : SyntaxNodeKind) (alts : Array Syntax) : CommandElabM Syntax := do
-  let alts ← alts.mapSepElemsM fun alt => do
-    let lhs := alt[0]
-    let pat := lhs[0]
-    if !pat.isQuot then
-      throwUnsupportedSyntax
-    let quot := pat[1]
-    let k' := quot.getKind
-    if k' == k then
-      pure alt
-    else if k' == choiceKind then
-       match quot.getArgs.find? fun quotAlt => quotAlt.getKind == k with
-       | none      => throwErrorAt! alt "invalid macro_rules alternative, expected syntax node kind '{k}'"
-       | some quot =>
-         let pat := pat.setArg 1 quot
-         let lhs := lhs.setArg 0 pat
-         pure $ alt.setArg 0 lhs
-    else
-      throwErrorAt! alt "invalid macro_rules alternative, unexpected syntax node kind '{k'}'"
+  let alts ← alts.mapM fun alt => match alt with
+    | `(matchAltExpr| | $pats,* => $rhs) => do
+      let pat := pats.elemsAndSeps[0]
+      if !pat.isQuot then
+        throwUnsupportedSyntax
+      let quoted := getQuotContent pat
+      let k' := quoted.getKind
+      if k' == k then
+        pure alt
+      else if k' == choiceKind then
+         match quoted.getArgs.find? fun quotAlt => quotAlt.getKind == k with
+         | none        => throwErrorAt! alt "invalid macro_rules alternative, expected syntax node kind '{k}'"
+         | some quoted =>
+           let pat := pat.setArg 1 quoted
+           let pats := pats.elemsAndSeps.set! 0 pat
+           `(matchAltExpr| | $pats,* => $rhs)
+      else
+        throwErrorAt! alt "invalid macro_rules alternative, unexpected syntax node kind '{k'}'"
+    | _ => throwUnsupportedSyntax
   `(@[macro $(Lean.mkIdent k)] def myMacro : Macro :=
-     fun | $(SepArray.mk alts):matchAlt|* | _ => throw Lean.Macro.Exception.unsupportedSyntax)
+     fun $alts:matchAlt* | _ => throw Lean.Macro.Exception.unsupportedSyntax)
 
-def inferMacroRulesAltKind (alt : Syntax) : CommandElabM SyntaxNodeKind := do
-  let lhs := alt[0]
-  let pat := lhs[0]
-  if !pat.isQuot then
-    throwUnsupportedSyntax
-  let quot := pat[1]
-  pure quot.getKind
+def inferMacroRulesAltKind : Syntax → CommandElabM SyntaxNodeKind
+  | `(matchAltExpr| | $pats,* => $rhs) => do
+    let pat := pats.elemsAndSeps[0]
+    if !pat.isQuot then
+      throwUnsupportedSyntax
+    let quoted := getQuotContent pat
+    pure quoted.getKind
+  | _ => throwUnsupportedSyntax
 
 def elabNoKindMacroRulesAux (alts : Array Syntax) : CommandElabM Syntax := do
-  let k ← inferMacroRulesAltKind (alts.get! 0)
+  let k ← inferMacroRulesAltKind alts[0]
   if k == choiceKind then
     throwErrorAt! alts[0]
       "invalid macro_rules alternative, multiple interpretations for pattern (solution: specify node kind using `macro_rules [<kind>] ...`)"
   else
-    let altsK    ← alts.filterSepElemsM fun alt => do pure $ k == (← inferMacroRulesAltKind alt)
-    let altsNotK ← alts.filterSepElemsM fun alt => do pure $ k != (← inferMacroRulesAltKind alt)
+    let altsK    ← alts.filterM fun alt => do pure $ k == (← inferMacroRulesAltKind alt)
+    let altsNotK ← alts.filterM fun alt => do pure $ k != (← inferMacroRulesAltKind alt)
     let defCmd   ← elabMacroRulesAux k altsK
     if altsNotK.isEmpty then
       pure defCmd
     else
-      `($defCmd:command macro_rules $(SepArray.mk altsNotK):matchAlt|*)
+      `($defCmd:command macro_rules $altsNotK:matchAlt*)
 
 @[builtinCommandElab «macro_rules»] def elabMacroRules : CommandElab :=
   adaptExpander fun stx => match stx with
-  | `(macro_rules $[|]? $alts:matchAlt|*)         => elabNoKindMacroRulesAux alts.elemsAndSeps
-  | `(macro_rules [$kind] $[|]? $alts:matchAlt|*) => do elabMacroRulesAux ((← getCurrNamespace) ++ kind.getId) alts.elemsAndSeps
-  | _                                             => throwUnsupportedSyntax
+  | `(macro_rules $alts:matchAlt*)         => elabNoKindMacroRulesAux alts
+  | `(macro_rules [$kind] $alts:matchAlt*) => do elabMacroRulesAux ((← getCurrNamespace) ++ kind.getId) alts
+  | _                                      => throwUnsupportedSyntax
 
 -- TODO: cleanup after we have support for optional syntax at `match_syntax`
 @[builtinMacro Lean.Parser.Command.mixfix] def expandMixfix : Macro := fun stx =>

src/Lean/Elab/Tactic/Basic.lean

@@ -326,7 +326,9 @@ private def introStep (n : Name) : TacticM Unit :=
   | `(tactic| intro $h:ident)  => introStep h.getId
   | `(tactic| intro _)         => introStep `_
   | `(tactic| intro $pat:term) => do
-    let stxNew ← `(tactic| intro h; match h with | $pat:term => _; clear h)
+    let m ← `(match h with | $pat:term => _)
+    let m := m.setKind ``Lean.Parser.Tactic.match
+    let stxNew ← `(tactic| intro h; $m; clear h)
     withMacroExpansion stx stxNew $ evalTactic stxNew
   | `(tactic| intro $hs:term*) => do
     let h0 := hs.get! 0

src/Lean/Elab/Tactic/Induction.lean

@@ -23,13 +23,13 @@ open Meta
   ```
 -/
 private def getAltName (alt : Syntax) : Name :=
-  getNameOfIdent' alt[0] |>.eraseMacroScopes
+  getNameOfIdent' alt[1] |>.eraseMacroScopes
 private def getAltVarNames (alt : Syntax) : Array Name :=
-  alt[1].getArgs.map getNameOfIdent'
+  alt[2].getArgs.map getNameOfIdent'
 private def getAltRHS (alt : Syntax) : Syntax :=
-  alt[3]
+  alt[4]
 private def getAltDArrow (alt : Syntax) : Syntax :=
-  alt[2]
+  alt[3]
 
 -- Return true if `stx` is a term occurring in the RHS of the induction/cases tactic
 def isHoleRHS (rhs : Syntax) : Bool :=
@@ -241,7 +241,7 @@ private def generalizeVars (stx : Syntax) (targets : Array Expr) : TacticM Nat :
     pure (fvarIds.size, [mvarId'])
 
 private def getAltsOfInductionAlts (inductionAlts : Syntax) : Array Syntax :=
-  inductionAlts[2].getSepArgs
+  inductionAlts[1].getArgs
 
 private def getAltsOfOptInductionAlts (optInductionAlts : Syntax) : Array Syntax :=
   if optInductionAlts.isNone then #[] else getAltsOfInductionAlts optInductionAlts[0]