chore: give a proper node to matchAlts

src/Lean/Elab/Binders.lean

@@ -373,7 +373,7 @@ else
 
 /- Helper function for `expandEqnsIntoMatch` -/
 private def getMatchAltNumPatterns (matchAlts : Syntax) : Nat :=
-let alt0 := matchAlts.getArg 0;
+let alt0 := (matchAlts.getArg 1).getArg 0;
 let pats := (alt0.getArg 0).getArgs.getSepElems;
 pats.size
 
@@ -381,7 +381,7 @@ pats.size
 private def expandMatchAltsIntoMatchAux (ref : Syntax) (matchAlts : Syntax) (matchTactic : Bool) : Nat → Array Syntax → MacroM Syntax
 | 0,   discrs =>
   pure $ Syntax.node (if matchTactic then `Lean.Parser.Tactic.match else `Lean.Parser.Term.match)
-    #[mkAtomFrom ref "match ", mkNullNode discrs, mkNullNode, mkAtomFrom ref " with ", mkNullNode, matchAlts]
+    #[mkAtomFrom ref "match ", mkNullNode discrs, mkNullNode, mkAtomFrom ref " with ", matchAlts]
 | n+1, discrs => withFreshMacroScope do
   x ← `(x);
   let discrs := if discrs.isEmpty then discrs else discrs.push $ mkAtomFrom ref ", ";
@@ -425,7 +425,7 @@ fun stx expectedType? =>
 -- "fun " >> ((many1 funBinder >> darrow >> termParser) <|> funMatchAlts)
 -- funMatchAlts := parser! matchAlts false
 if (stx.getArg 1).isOfKind `Lean.Parser.Term.funMatchAlts then do
-  stxNew ← liftMacroM $ expandMatchAltsIntoMatch stx ((stx.getArg 1).getArg 1);
+  stxNew ← liftMacroM $ expandMatchAltsIntoMatch stx ((stx.getArg 1).getArg 0);
   withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
 else do
   let binders := (stx.getArg 1).getArgs;

src/Lean/Elab/Match.lean

@@ -21,7 +21,7 @@ nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $
   sepBy1 termParser ", " >> darrow >> termParser
 
 def matchAlts (optionalFirstBar := true) : Parser :=
-withPosition $ fun pos =>
+group $ withPosition $ fun pos =>
   (if optionalFirstBar then optional "| " else "| ") >>
   sepBy1 matchAlt (checkColGe pos.column "alternatives must be indented" >> "|")
 
@@ -92,7 +92,7 @@ matchAlts.mapM fun matchAlt => do
 
 /- Given `stx` a match-expression, return its alternatives. -/
 private def getMatchAlts (stx : Syntax) : Array MatchAltView :=
-let alts : Array Syntax := (stx.getArg 5).getArgs.filter fun alt => alt.getKind == `Lean.Parser.Term.matchAlt;
+let alts : Array Syntax := ((stx.getArg 4).getArg 1).getArgs.filter fun alt => alt.getKind == `Lean.Parser.Term.matchAlt;
 alts.map mkMatchAltView
 
 /--

src/Lean/Elab/Tactic/Basic.lean

@@ -304,7 +304,7 @@ fun stx => match_syntax stx with
 
 @[builtinTactic Lean.Parser.Tactic.introMatch] def evalIntroMatch : Tactic :=
 fun stx => do
-  let matchAlts := stx.getArg 2;
+  let matchAlts := stx.getArg 1;
   stxNew ← liftMacroM $ Term.expandMatchAltsIntoMatchTactic stx matchAlts;
   withMacroExpansion stx stxNew $ evalTactic stxNew
 

src/Lean/Elab/Tactic/Match.lean

@@ -16,7 +16,8 @@ structure AuxMatchTermState :=
 (cases   : Array Syntax := #[])
 
 private def mkAuxiliaryMatchTermAux (parentTag : Name) (matchTac : Syntax) : StateT AuxMatchTermState MacroM Syntax := do
-let alts := (matchTac.getArg 5).getArgs;
+let matchAlts := matchTac.getArg 4;
+let alts      := (matchAlts.getArg 1).getArgs;
 newAlts ← alts.mapSepElemsM fun alt => do {
   let alt    := alt.updateKind `Lean.Parser.Term.matchAlt;
   let holeOrTactic := alt.getArg 2;
@@ -36,7 +37,7 @@ newAlts ← alts.mapSepElemsM fun alt => do {
     pure $ alt.setArg 2 newHole
 };
 let result  := matchTac.updateKind `Lean.Parser.Term.match;
-let result  := result.setArg 5 (mkNullNode newAlts);
+let result  := result.setArg 4 (matchAlts.setArg 1 (mkNullNode newAlts));
 pure result
 
 private def mkAuxiliaryMatchTerm (parentTag : Name) (matchTac : Syntax) : MacroM (Syntax × Array Syntax) := do

src/Lean/Parser/Tactic.lean

@@ -57,7 +57,7 @@ def generalizingVars := optional (" generalizing " >> many1 ident)
 def withIds : Parser := optional (" with " >> many1 ident')
 
 def matchAlt  : Parser := parser! sepBy1 termParser ", " >> darrow >> holeOrTactic
-def matchAlts : Parser := withPosition $ fun pos => (optional "| ") >> sepBy1 matchAlt (checkColGe pos.column "alternatives must be indented" >> "|")
+def matchAlts : Parser := group $ withPosition $ fun pos => (optional "| ") >> sepBy1 matchAlt (checkColGe pos.column "alternatives must be indented" >> "|")
 @[builtinTacticParser] def «match»      := parser! nonReservedSymbol "match " >> sepBy1 Term.matchDiscr ", " >> Term.optType >> " with " >> matchAlts
 @[builtinTacticParser] def «introMatch» := parser! nonReservedSymbol "intro " >> matchAlts
 

src/Lean/Parser/Term.lean

@@ -99,7 +99,7 @@ nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $
   sepBy1 termParser ", " >> darrow >> termParser
 
 def matchAlts (optionalFirstBar := true) : Parser :=
-withPosition $ fun pos =>
+parser! withPosition $ fun pos =>
   (if optionalFirstBar then optional "| " else "| ") >>
   sepBy1 matchAlt (checkColGe pos.column "alternatives must be indented" >> "|")
 
@@ -110,8 +110,7 @@ def matchDiscr := parser! optional (try (ident >> checkNoWsBefore "no space befo
 
 def funImplicitBinder := try (lookahead ("{" >> many1 binderIdent >> (" : " <|> "}"))) >> implicitBinder
 def funBinder : Parser := funImplicitBinder <|> instBinder <|> termParser maxPrec
-def funMatchAlts := parser! matchAlts false
-@[builtinTermParser] def «fun» := parser!:maxPrec unicodeSymbol "λ " "fun " >> ((many1 funBinder >> darrow >> termParser) <|> funMatchAlts)
+@[builtinTermParser] def «fun» := parser!:maxPrec unicodeSymbol "λ " "fun " >> ((many1 funBinder >> darrow >> termParser) <|> matchAlts false)
 
 def optExprPrecedence := optional (try ":" >> termParser maxPrec)
 @[builtinTermParser] def «parser!»  := parser!:leadPrec "parser! " >> optExprPrecedence >> termParser