feat: add matchExprPat parser

src/Lean/Elab/Do.lean

@@ -1146,7 +1146,8 @@ where
       for alt in alts do
         let rhs ← toTerm alt.rhs
         let optVar := if let some var := alt.var? then mkNullNode #[var, mkAtomFrom var "@"] else mkNullNode #[]
-        let termAlt := mkNode ``Parser.Term.matchExprAlt #[mkAtomFrom alt.ref "|", optVar, alt.funName, mkNullNode alt.pvars, mkAtomFrom alt.ref "=>", rhs]
+        let pat := mkNode ``Parser.Term.matchExprPat #[optVar, alt.funName, mkNullNode alt.pvars]
+        let termAlt := mkNode ``Parser.Term.matchExprAlt #[mkAtomFrom alt.ref "|", pat, mkAtomFrom alt.ref "=>", rhs]
         termAlts := termAlts.push termAlt
       let elseBranch := mkNode ``Parser.Term.matchExprElseAlt #[mkAtomFrom ref "|", mkHole ref, mkAtomFrom ref "=>", (← toTerm elseBranch)]
       let termMatchExprAlts := mkNode ``Parser.Term.matchExprAlts #[mkNullNode termAlts, elseBranch]
@@ -1614,10 +1615,11 @@ mutual
     let discr     := doMatchExpr[2]
     let alts      := doMatchExpr[4][0].getArgs -- Array of `doMatchExprAlt`
     let alts ← alts.mapM fun alt => do
-      let var? := if alt[1].isNone then none else some alt[1][0]
-      let funName  := alt[2]
-      let pvars    := alt[3].getArgs
-      let rhs      := alt[5]
+      let pat      := alt[1]
+      let var?     := if pat[0].isNone then none else some pat[0][0]
+      let funName  := pat[1]
+      let pvars    := pat[2].getArgs
+      let rhs      := alt[3]
       let rhs ← doSeqToCode (getDoSeqElems rhs)
       pure { ref, var?, funName, pvars, rhs }
     let elseBranch ← doSeqToCode (getDoSeqElems doMatchExpr[4][1][3])

src/Lean/Elab/MatchExpr.lean

@@ -52,23 +52,22 @@ Converts syntax representing a `match_expr` else-alternative into an `ElseAlt`.
 -/
 def toElseAlt? (stx : Syntax) : Option ElseAlt :=
   if !stx.isOfKind ``matchExprElseAlt then none else
-  some { rhs := stx.getArg 3 }
+  some { rhs := stx[3] }
 
 /--
 Converts syntax representing a `match_expr` alternative into an `Alt`.
 -/
 def toAlt? (stx : Syntax) : Option Alt :=
   if !stx.isOfKind ``matchExprAlt then none else
-  let var? : Option Ident :=
-    let optVar := stx.getArg 1
-    if optVar.isNone then none else some ⟨optVar.getArg 0⟩
-  let funName := ⟨stx.getArg 2⟩
-  let pvars := stx.getArg 3 |>.getArgs.toList.reverse.map fun arg =>
-    match arg with
-    | `(_) => none
-    | _ => some ⟨arg⟩
-  let rhs := stx.getArg 5
-  some { var?, funName, pvars, rhs }
+  match stx[1] with
+  | `(matchExprPat| $[$var? @]? $funName:ident $pvars*) =>
+    let pvars := pvars.toList.reverse.map fun arg =>
+      match arg.raw with
+      | `(_) => none
+      | _ => some ⟨arg⟩
+    let rhs := stx[3]
+    some { var?, funName, pvars, rhs }
+  | _ => none
 
 /--
 Returns the function names of alternatives that do not have any pattern variable left.
@@ -198,7 +197,7 @@ end MatchExpr
 @[builtin_macro Lean.Parser.Term.matchExpr] def expandMatchExpr : Macro := fun stx =>
   match stx with
   | `(match_expr $discr:term with $alts) =>
-    MatchExpr.main discr (alts.raw.getArg 0).getArgs (alts.raw.getArg 1)
+    MatchExpr.main discr alts.raw[0].getArgs alts.raw[1]
   | _ => Macro.throwUnsupported
 
 end Lean.Elab.Term

src/Lean/Parser/Term.lean

@@ -826,7 +826,8 @@ Implementation of the `show_term` term elaborator.
 `match_expr` support.
 -/
 
-def matchExprAlt (rhsParser : Parser) := leading_parser "| " >> ppIndent (optional (atomic (ident >> "@")) >> ident >> many binderIdent >> " => " >> rhsParser)
+def matchExprPat := leading_parser optional (atomic (ident >> "@")) >> ident >> many binderIdent
+def matchExprAlt (rhsParser : Parser) := leading_parser "| " >> ppIndent (matchExprPat >> " => " >> rhsParser)
 def matchExprElseAlt (rhsParser : Parser) := leading_parser "| " >> ppIndent (hole >> " => " >> rhsParser)
 def matchExprAlts (rhsParser : Parser) :=
   leading_parser withPosition $

stage0/src/stdlib_flags.h

@@ -8,7 +8,7 @@ options get_default_options() {
     // switch to `true` for ABI-breaking changes affecting meta code
     opts = opts.update({"interpreter", "prefer_native"}, false);
     // switch to `true` for changing built-in parsers used in quotations
-    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
+    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
     // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax
     // with custom precheck hooks were affected
     opts = opts.update({"quotPrecheck"}, true);