refactor: adapt raw syntax manipulations to TSyntax

Sometimes there's just no structure to work on

src/Init/Notation.lean

@@ -214,11 +214,12 @@ namespace Lean
 
 macro_rules
   | `([ $elems,* ]) => do
-    let rec expandListLit (i : Nat) (skip : Bool) (result : Syntax) : MacroM Syntax := do
+    -- NOTE: we do not have `TSepArray.getElems` yet at this point
+    let rec expandListLit (i : Nat) (skip : Bool) (result : TSyntax `term) : MacroM Syntax := do
       match i, skip with
       | 0,   _     => pure result
       | i+1, true  => expandListLit i false result
-      | i+1, false => expandListLit i true  (← ``(List.cons $(elems.elemsAndSeps[i]) $result))
+      | i+1, false => expandListLit i true  (← ``(List.cons $(⟨elems.elemsAndSeps[i]⟩) $result))
     if elems.elemsAndSeps.size < 64 then
       expandListLit elems.elemsAndSeps.size false (← ``(List.nil))
     else

src/Lean/Elab/App.lean

@@ -401,7 +401,7 @@ mutual
         | Except.error err       => throwError err
         | Except.ok tacticSyntax =>
           -- TODO(Leo): does this work correctly for tactic sequences?
-          let tacticBlock ← `(by $tacticSyntax)
+          let tacticBlock ← `(by $(⟨tacticSyntax⟩))
           let argNew := Arg.stx tacticBlock
           propagateExpectedType argNew
           elabAndAddNewArg argName argNew

src/Lean/Elab/BuiltinNotation.lean

@@ -195,8 +195,8 @@ private partial def hasCDot : Syntax → Bool
   - `f · · b` => `fun _a_1 _a_2 => f _a_1 _a_2 b` -/
 partial def expandCDot? (stx : TSyntax `term) : MacroM (Option (TSyntax `term)) := do
   if hasCDot stx then
-    let (newStx, binders) ← (go stx).run #[];
-    `(fun $binders* => $newStx)
+    let (newStx, binders) ← (go stx).run #[]
+    `(fun $binders* => $(⟨newStx⟩))
   else
     pure none
 where
@@ -264,7 +264,7 @@ where
   | stx =>
     if !stx[1][0].isMissing && stx[1][1].isMissing then
       -- parsed `(` and `term`, assume it's a basic parenthesis to get any elaboration output at all
-      `(($(stx[1][0])))
+      `(($(⟨stx[1][0]⟩)))
     else
       throw <| Macro.Exception.error stx "unexpected parentheses notation"
 

src/Lean/Elab/ElabRules.lean

@@ -32,7 +32,7 @@ def elabElabRulesAux (doc? : Option (TSyntax ``docComment)) (attrKind : TSyntax
          | none        => throwErrorAt alt "invalid elab_rules alternative, expected syntax node kind '{k}'"
          | some quoted =>
            let pat := pat.setArg 1 quoted
-           let pats := pats.elemsAndSeps.set! 0 pat
+           let pats := ⟨pats.elemsAndSeps.set! 0 pat⟩
            `(matchAltExpr| | $pats,* => $rhs)
       else
         throwErrorAt alt "invalid elab_rules alternative, unexpected syntax node kind '{k'}'"

src/Lean/Elab/Macro.lean

@@ -22,16 +22,17 @@ open Lean.Parser.Command
       | none => liftMacroM <| mkNameFromParserSyntax cat.getId (mkNullNode stxParts)
     /- The command `syntax [<kind>] ...` adds the current namespace to the syntax node kind.
       So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/
-    let pat := mkNode ((← getCurrNamespace) ++ name) patArgs
+    let pat := ⟨mkNode ((← getCurrNamespace) ++ name) patArgs⟩
     let stxCmd ← `($[$doc?:docComment]? $attrKind:attrKind
-      syntax%$tk$[:$prec?]? (name := $(← mkIdentFromRef name)) (priority := $(quote prio)) $[$stxParts]* : $cat)
+      syntax%$tk$[:$prec?]? (name := $(← mkIdentFromRef name)) (priority := $(quote prio):num) $[$stxParts]* : $cat)
+    let rhs := rhs.raw
     let macroRulesCmd ← if rhs.getArgs.size == 1 then
       -- `rhs` is a `term`
-      let rhs := rhs[0]
+      let rhs := ⟨rhs[0]⟩
       `($[$doc?:docComment]? macro_rules%$tk | `($pat) => $rhs)
     else
       -- `rhs` is of the form `` `( $body ) ``
-      let rhsBody := rhs[1]
+      let rhsBody := ⟨rhs[1]⟩
       `($[$doc?:docComment]? macro_rules%$tk | `($pat) => `($rhsBody))
     elabCommand <| mkNullNode #[stxCmd, macroRulesCmd]
   | _ => throwUnsupportedSyntax

src/Lean/Elab/MacroArgUtil.lean

@@ -20,8 +20,8 @@ partial def expandMacroArg (stx : TSyntax ``macroArg) : CommandElabM (TSyntax `s
 where
   mkSyntaxAndPat id? id stx := do
     let pat ← match stx with
-    | `(stx| $s:str)         => pure <| mkNode `token_antiquot #[← liftMacroM <| strLitToPattern s, mkAtom "%", mkAtom "$", id]
-    | `(stx| &$s:str)        => pure <| mkNode `token_antiquot #[← liftMacroM <| strLitToPattern s, mkAtom "%", mkAtom "$", id]
+    | `(stx| $s:str)         => pure ⟨mkNode `token_antiquot #[← liftMacroM <| strLitToPattern s, mkAtom "%", mkAtom "$", id]⟩
+    | `(stx| &$s:str)        => pure ⟨mkNode `token_antiquot #[← liftMacroM <| strLitToPattern s, mkAtom "%", mkAtom "$", id]⟩
     | `(stx| optional($stx)) => mkSplicePat `optional stx id "?"
     | `(stx| many($stx))     => mkSplicePat `many stx id "*"
     | `(stx| many1($stx))    => mkSplicePat `many stx id "*"
@@ -30,7 +30,7 @@ where
     | `(stx| sepBy1($stx, $sep:str $[, $stxsep]? $[, allowTrailingSep]?)) =>
       mkSplicePat `sepBy stx id ((isStrLit? sep).get! ++ "*")
     -- NOTE: all `interpolatedStr(·)` reuse the same node kind
-    | `(stx| interpolatedStr(term)) => pure <| Syntax.mkAntiquotNode interpolatedStrKind id
+    | `(stx| interpolatedStr(term)) => pure ⟨Syntax.mkAntiquotNode interpolatedStrKind id⟩
     -- bind through withPosition
     | `(stx| withPosition($stx)) =>
       return (← mkSyntaxAndPat id? id stx)
@@ -40,9 +40,9 @@ where
       -- otherwise `group` the syntax to enforce arity 1, e.g. for `noWs`
       | none    => return (← `(stx| group($stx)), (← mkAntiquotNode stx id))
     pure (stx, pat)
-  mkSplicePat kind stx id suffix :=
-    return mkNullNode #[mkAntiquotSuffixSpliceNode kind (← mkAntiquotNode stx id) suffix]
-  mkAntiquotNode
+  mkSplicePat kind stx id suffix : CommandElabM (TSyntax `term) :=
+    return ⟨mkNullNode #[mkAntiquotSuffixSpliceNode kind (← mkAntiquotNode stx id) suffix]⟩
+  mkAntiquotNode : TSyntax `stx → TSyntax `term → CommandElabM (TSyntax `term)
     | `(stx| ($stx)), term => mkAntiquotNode stx term
     | `(stx| $id:ident$[:$p:prec]?), term => do
       let kind ← match (← Elab.Term.resolveParserName id) with
@@ -55,13 +55,13 @@ where
         | [] =>
           let id := id.getId.eraseMacroScopes
           if Parser.isParserCategory (← getEnv) id then
-            return Syntax.mkAntiquotNode id term (isPseudoKind := true)
+            return ⟨Syntax.mkAntiquotNode id term (isPseudoKind := true)⟩
           else if (← Parser.isParserAlias id) then
             pure <| (← Parser.getSyntaxKindOfParserAlias? id).getD Name.anonymous
           else
             throwError "unknown parser declaration/category/alias '{id}'"
-      pure <| Syntax.mkAntiquotNode kind term
+      pure ⟨Syntax.mkAntiquotNode kind term⟩
     | stx, term =>
-      pure <| Syntax.mkAntiquotNode Name.anonymous term (isPseudoKind := true)
+      pure ⟨Syntax.mkAntiquotNode Name.anonymous term (isPseudoKind := true)⟩
 
 end Lean.Elab.Command

src/Lean/Elab/MacroRules.lean

@@ -31,7 +31,7 @@ def elabMacroRulesAux (doc? : Option (TSyntax ``docComment)) (attrKind : TSyntax
          | some quoted =>
            let pat := pat.setArg 1 quoted
            let pats := pats.elemsAndSeps.set! 0 pat
-           `(matchAltExpr| | $pats,* => $rhs)
+           `(matchAltExpr| | $(⟨pats⟩),* => $rhs)
       else
         throwErrorAt alt "invalid macro_rules alternative, unexpected syntax node kind '{k'}'"
     | _ => throwUnsupportedSyntax

src/Lean/Elab/Mixfix.lean

@@ -30,6 +30,6 @@ where
     let attrKind := stx[0]
     let stx  := stx.setArg 0 mkAttrKindGlobal
     let stx ← f stx
-    return stx.setArg 0 attrKind
+    return stx.raw.setArg 0 attrKind
 
 end Lean.Elab.Command

src/Lean/Elab/Notation.lean

@@ -123,22 +123,25 @@ private def expandNotationAux (ref : Syntax)
     | some name => pure name.getId
     | none => mkNameFromParserSyntax `term (mkNullNode syntaxParts)
   -- build macro rules
-  let vars := items.filter fun item => item.getKind == `Lean.Parser.Command.identPrec
-  let vars := vars.map fun var => var[0]
-  let qrhs := antiquote vars rhs
+  let vars := items.filter fun item => item.raw.getKind == `Lean.Parser.Command.identPrec
+  let vars := vars.map fun var => var.raw[0]
+  let qrhs := ⟨antiquote vars rhs⟩
   let patArgs ← items.mapM expandNotationItemIntoPattern
   /- The command `syntax [<kind>] ...` adds the current namespace to the syntax node kind.
      So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/
   let fullName := currNamespace ++ name
-  let pat := mkNode fullName patArgs
+  let pat : TSyntax `term := ⟨mkNode fullName patArgs⟩
   let stxDecl ← `($attrKind:attrKind syntax $[: $prec?]? (name := $(mkIdent name)) (priority := $(quote prio):num) $[$syntaxParts]* : $cat)
-  let mut macroDecl ← `(macro_rules | `($pat) => ``($qrhs))
-  if isLocalAttrKind attrKind then
-    -- Make sure the quotation pre-checker takes section variables into account for local notation.
-    macroDecl ← `(section set_option quotPrecheck.allowSectionVars true $macroDecl end)
+  let macroDecl ← `(macro_rules | `($pat) => ``($qrhs))
+  let macroDecls ←
+    if isLocalAttrKind attrKind then
+      -- Make sure the quotation pre-checker takes section variables into account for local notation.
+      `(section set_option quotPrecheck.allowSectionVars true $macroDecl end)
+    else
+      pure ⟨mkNullNode #[macroDecl]⟩
   match (← mkSimpleDelab attrKind pat qrhs |>.run) with
-  | some delabDecl => return mkNullNode #[stxDecl, macroDecl, delabDecl]
-  | none           => return mkNullNode #[stxDecl, macroDecl]
+  | some delabDecl => return mkNullNode #[stxDecl, macroDecls, delabDecl]
+  | none           => return mkNullNode #[stxDecl, macroDecls]
 
 @[builtinMacro Lean.Parser.Command.notation] def expandNotation : Macro
   | stx@`($attrKind:attrKind notation $[: $prec? ]? $[(name := $name?)]? $[(priority := $prio?)]? $items* => $rhs) => do

src/Lean/Elab/Quotation/Precheck.lean

@@ -109,7 +109,7 @@ private def isSectionVariable (e : Expr) : TermElabM Bool := do
 @[builtinQuotPrecheck Lean.Parser.Term.app] def precheckApp : Precheck
   | `($f $args*) => do
     precheck f
-    for arg in args do
+    for arg in args.raw do
       match arg with
       | `(argument| ($_ := $e)) => precheck e
       | `(argument| $e:term)    => precheck e
@@ -125,7 +125,7 @@ private def isSectionVariable (e : Expr) : TermElabM Bool := do
   | `(($e))         => precheck e
   | `(($e, $es,*))  => do
     precheck e
-    es.getElems.forM precheck
+    es.getElems.raw.forM precheck
   | _ => throwUnsupportedSyntax
 
 @[builtinQuotPrecheck choice] def precheckChoice : Precheck := fun stx => do

src/Lean/Elab/Quotation/Util.lean

@@ -18,7 +18,7 @@ def getAntiquotationIds (stx : Syntax) : TermElabM (Array (TSyntax identKind)) :
   for stx in stx.topDown (firstChoiceOnly := true) do
     if (isAntiquot stx || isTokenAntiquot stx) && !isEscapedAntiquot stx then
       let anti := getAntiquotTerm stx
-      if anti.isIdent then ids := ids.push anti
+      if anti.isIdent then ids := ids.push ⟨anti⟩
       else if anti.isOfKind ``Parser.Term.hole then pure ()
       else throwErrorAt stx "complex antiquotation not allowed here"
   return ids

src/Lean/Elab/Tactic/Match.lean

@@ -35,7 +35,7 @@ private def mkAuxiliaryMatchTerm (parentTag : Name) (matchTac : Syntax) : MacroM
         alt := alt.setArg 3 newHole
       else
         let newHole ← withFreshMacroScope `(?rhs)
-        let newHoleId := newHole[1]
+        let newHoleId := newHole.raw[1]
         let newCase ← `(tactic|
           case $newHoleId =>%$(alt[2])
             -- annotate `| ... =>` with state after `case`

src/Lean/Parser/Module.lean

@@ -134,7 +134,7 @@ def testParseModule (env : Environment) (fname contents : String) : IO Syntax :=
   let (header, state, messages) ← parseHeader inputCtx
   let cmds ← testParseModuleAux env inputCtx state messages #[]
   let stx := mkNode `Lean.Parser.Module.module #[header, mkListNode cmds]
-  pure stx.updateLeading
+  pure stx.raw.updateLeading
 
 def testParseFile (env : Environment) (fname : System.FilePath) : IO Syntax := do
   let contents ← IO.FS.readFile fname

src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -334,17 +334,17 @@ def parserOfStack.parenthesizer (offset : Nat) (_prec : Nat := 0) : Parenthesize
 
 @[builtinCategoryParenthesizer term]
 def term.parenthesizer : CategoryParenthesizer | prec => do
-  maybeParenthesize `term true (fun stx => Unhygienic.run `(($stx))) prec $
+  maybeParenthesize `term true (fun stx => Unhygienic.run `(($(⟨stx⟩)))) prec $
     parenthesizeCategoryCore `term prec
 
 @[builtinCategoryParenthesizer tactic]
 def tactic.parenthesizer : CategoryParenthesizer | prec => do
-  maybeParenthesize `tactic false (fun stx => Unhygienic.run `(tactic|($stx))) prec $
+  maybeParenthesize `tactic false (fun stx => Unhygienic.run `(tactic|($(⟨stx⟩)))) prec $
     parenthesizeCategoryCore `tactic prec
 
 @[builtinCategoryParenthesizer level]
 def level.parenthesizer : CategoryParenthesizer | prec => do
-  maybeParenthesize `level false (fun stx => Unhygienic.run `(level|($stx))) prec $
+  maybeParenthesize `level false (fun stx => Unhygienic.run `(level|($(⟨stx⟩)))) prec $
     parenthesizeCategoryCore `level prec
 
 @[builtinCategoryParenthesizer rawStx]

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -256,7 +256,7 @@ partial def handleDocumentSymbol (_ : DocumentSymbolParams)
     | [] => ([], [])
     | stx::stxs => match stx with
       | `(namespace $id)  => sectionLikeToDocumentSymbols text stx stxs (id.getId.toString) SymbolKind.namespace id
-      | `(section $(id)?) => sectionLikeToDocumentSymbols text stx stxs ((·.getId.toString) <$> id |>.getD "<section>") SymbolKind.namespace (id.getD stx)
+      | `(section $(id)?) => sectionLikeToDocumentSymbols text stx stxs ((·.getId.toString) <$> id |>.getD "<section>") SymbolKind.namespace (id.map (·.raw) |>.getD stx)
       | `(end $(_id)?) => ([], stx::stxs)
       | _ => Id.run do
         let (syms, stxs') := toDocumentSymbols text stxs
@@ -265,7 +265,7 @@ partial def handleDocumentSymbol (_ : DocumentSymbolParams)
         if let some stxRange := stx.getRange? then
           let (name, selection) := match stx with
             | `($_:declModifiers $_:attrKind instance $[$np:namedPrio]? $[$id:ident$[.{$ls,*}]?]? $sig:declSig $_) =>
-              ((·.getId.toString) <$> id |>.getD s!"instance {sig.reprint.getD ""}", id.getD sig)
+              ((·.getId.toString) <$> id |>.getD s!"instance {sig.raw.reprint.getD ""}", id.map (·.raw) |>.getD sig)
             | _ => match stx[1][1] with
               | `(declId|$id:ident$[.{$ls,*}]?) => (id.getId.toString, id)
               | _                               => (stx[1][0].isIdOrAtom?.getD "<unknown>", stx[1][0])
@@ -423,7 +423,7 @@ partial def handleFoldingRange (_ : FoldingRangeParams)
           addRanges text sections stxs
       | `(mutual $body* end) => do
         addRangeFromSyntax text FoldingRangeKind.region stx
-        addRanges text [] body.toList
+        addRanges text [] body.raw.toList
         addRanges text sections stxs
       | _ => do
         if isImport stx then
@@ -444,7 +444,7 @@ partial def handleFoldingRange (_ : FoldingRangeParams)
         -- separately to the main definition.
         -- We never fold other modifiers, such as annotations.
         if let `($dm:declModifiers $decl) := stx then
-          if let some comment := dm[0].getOptional? then
+          if let some comment := dm.raw[0].getOptional? then
             addRangeFromSyntax text FoldingRangeKind.comment comment
 
           addRangeFromSyntax text FoldingRangeKind.region decl