feat: add DoElem and DoSeq syntax abbreviations (#14025)

This PR adds `Lean.DoElem` and `Lean.DoSeq` as abbreviations for
``TSyntax `doElem`` and ``TSyntax `Lean.Parser.Term.doSeq``, mirroring
`Lean.Term`, and uses them throughout the `do` elaborator.

Author: sgraf812

src/Init/Meta/Defs.lean

@@ -407,6 +407,14 @@ Syntax that represents a tactic.
 -/
 protected abbrev Tactic := TSyntax `tactic
 /--
+Syntax that represents an element of a `do` sequence.
+-/
+abbrev DoElem := TSyntax `doElem
+/--
+Syntax that represents a sequence of `do` elements.
+-/
+abbrev DoSeq := TSyntax `Lean.Parser.Term.doSeq
+/--
 Syntax that represents a precedence (e.g. for an operator).
 -/
 abbrev Prec := TSyntax `prec
@@ -449,7 +457,7 @@ abbrev HexNum := TSyntax hexnumKind
 
 end Syntax
 
-export Syntax (Term Command Prec Prio Ident StrLit CharLit NameLit ScientificLit NumLit HygieneInfo)
+export Syntax (Term Command DoElem DoSeq Prec Prio Ident StrLit CharLit NameLit ScientificLit NumLit HygieneInfo)
 
 namespace TSyntax
 

src/Lean/Elab/BuiltinDo/Basic.lean

@@ -16,7 +16,7 @@ namespace Lean.Elab.Do
 open Lean.Parser.Term
 open Lean.Meta
 
-def elabDoIdDecl (x : Ident) (xType? : Option Term) (rhs : TSyntax `doElem) (k : DoElabM Expr)
+def elabDoIdDecl (x : Ident) (xType? : Option Term) (rhs : DoElem) (k : DoElabM Expr)
     (kind : DoElemContKind := .nonDuplicable) : DoElabM Expr := do
   let xType ← Term.elabType (xType?.getD (mkHole x))
   let lctx ← getLCtx

src/Lean/Elab/BuiltinDo/Match.lean

@@ -23,7 +23,7 @@ open Lean.Parser.Term
 open Lean.Meta
 open Lean.Meta.Match
 
-private def elabDoSeqWithRefinedType (type : Expr) (doSeq : TSyntax ``doSeq) (dec : DoElemCont) : DoElabM Expr := do
+private def elabDoSeqWithRefinedType (type : Expr) (doSeq : DoSeq) (dec : DoElemCont) : DoElabM Expr := do
   let newDoBlockResultType ← withNewMCtxDepth do
     let γ ← mkFreshExprMVar (mkSort (← read).monadInfo.u.succ)
     unless ← isDefEqGuarded type (← mkMonadApp γ) do

src/Lean/Elab/Do/Basic.lean

@@ -217,7 +217,7 @@ It is ``elabTerm `(do $e; $rest) = elabDoElem e dec``, where `elabDoElem e ·` i
 `do` element `e`, and `dec` is the `DoElemCont` describing the elaboration of the rest of the block
 `rest`.
 -/
-abbrev DoElab := TSyntax `doElem → DoElemCont → DoElabM Expr
+abbrev DoElab := DoElem → DoElemCont → DoElabM Expr
 
 structure ReturnCont where
   resultType : Expr
@@ -830,7 +830,7 @@ private partial def hasNestedActionsToLift : Syntax → Bool
     else args.any hasNestedActionsToLift
   | _ => false
 
-private partial def expandNestedActionsAux (baseId : Name) (inQuot : Bool) (inBinder : Bool) : Syntax → StateT (Array (TSyntax `doElem)) DoElabM Syntax
+private partial def expandNestedActionsAux (baseId : Name) (inQuot : Bool) (inBinder : Bool) : Syntax → StateT (Array DoElem) DoElabM Syntax
   | stx@(Syntax.node i k args) =>
     if k == choiceKind then do
       -- choice node: check that lifts are consistent
@@ -856,7 +856,7 @@ private partial def expandNestedActionsAux (baseId : Name) (inQuot : Bool) (inBi
       -- Wrap raw terms in `doExpr` so the subsequent `let _ ← _` quotation parses correctly.
       let isDoElem :=
         (Parser.getParserCategory? (← getEnv) `doElem).any (·.kinds.contains arg.getKind)
-      let act : TSyntax `doElem ←
+      let act : DoElem ←
         if isDoElem then pure ⟨arg⟩
         else let t : Term := ⟨arg⟩; `(doElem| $t:term)
       -- keep name deterministic across choice branches
@@ -871,7 +871,7 @@ private partial def expandNestedActionsAux (baseId : Name) (inQuot : Bool) (inBi
       return Syntax.node i k args
   | stx => return stx
 
-def expandNestedActions (stx : TSyntax kind) : DoElabM (Array (TSyntax `doElem) × TSyntax kind) := do
+def expandNestedActions (stx : TSyntax kind) : DoElabM (Array DoElem × TSyntax kind) := do
   if !hasNestedActionsToLift stx then
     return (#[], stx)
   else
@@ -907,7 +907,7 @@ private def withTermInfoContext' (elaborator : Name) (stx : Syntax) (expectedTyp
   controlAtTermElabM fun runInBase =>
     Term.withTermInfoContext' elaborator stx (expectedType? := expectedType) (runInBase x)
 
-private def elabDoElemFns (stx : TSyntax `doElem) (cont : DoElemCont)
+private def elabDoElemFns (stx : DoElem) (cont : DoElemCont)
     (fns : List (KeyedDeclsAttribute.AttributeEntry DoElab)) (catchExPostpone : Bool := true) : DoElabM Expr := do
   let s ← saveState
   match fns with
@@ -935,7 +935,7 @@ private def DoElemCont.mkUnit (k : DoElabM Expr) : DoElabM DoElemCont := do
   return DoElemCont.mk r unit k .nonDuplicable
 
 mutual
-partial def elabDoElem (stx : TSyntax `doElem) (cont : DoElemCont) (catchExPostpone : Bool := true) : DoElabM Expr := do
+partial def elabDoElem (stx : DoElem) (cont : DoElemCont) (catchExPostpone : Bool := true) : DoElabM Expr := do
   let k := stx.raw.getKind
   trace[Elab.do.step] "do element: {stx}"
   checkSystem "do element elaborator"
@@ -963,7 +963,7 @@ partial def elabDoElem (stx : TSyntax `doElem) (cont : DoElemCont) (catchExPostp
   | []      => throwError "elaboration function for `{k}` has not been implemented{indentD stx}"
   | elabFns => elabDoElemFns stx cont elabFns catchExPostpone
 
-partial def elabDoElems1 (doElems : Array (TSyntax `doElem)) (cont : DoElemCont) (catchExPostpone : Bool := true) : DoElabM Expr := do
+partial def elabDoElems1 (doElems : Array DoElem) (cont : DoElemCont) (catchExPostpone : Bool := true) : DoElabM Expr := do
   if h : doElems.size = 0 then
     throwError "Empty array of `do` elements passed to `elabDoElems1`."
   else
@@ -976,7 +976,7 @@ partial def elabDoElems1 (doElems : Array (TSyntax `doElem)) (cont : DoElemCont)
   res
 end
 
-partial def elabDoSeq (doSeq : TSyntax ``doSeq) (cont : DoElemCont) (catchExPostpone : Bool := true) : DoElabM Expr := do
+partial def elabDoSeq (doSeq : DoSeq) (cont : DoElemCont) (catchExPostpone : Bool := true) : DoElabM Expr := do
   let s ← saveState
   try
     elabDoElems1 (getDoElems doSeq) cont catchExPostpone
@@ -996,7 +996,7 @@ def elabNestedAction : Term.TermElab := fun stx _ty? => do
   throwErrorAt stx "Nested action `{stx}` must be nested inside a `do` expression."
 
 /-- Elaborate `doSeq` using `ops` for pure/bind construction. -/
-def elabDoWith (ops : DoOps) (doSeq : TSyntax ``doSeq)
+def elabDoWith (ops : DoOps) (doSeq : DoSeq)
     (expectedType? : Option Expr) : TermElabM Expr := do
   Term.tryPostponeIfNoneOrMVar expectedType?
   let ctx ← mkContext expectedType? (ops := ops)

src/Lean/Elab/Do/ForwardSyntax.lean

@@ -21,7 +21,7 @@ form.
 -/
 public structure ForwardArg where
   binders : Array (TSyntax ``funBinder)
-  body    : TSyntax ``doSeq
+  body    : DoSeq
 
 /--
 If `e` is a function application whose last argument effect-forwards into the enclosing `do`

src/Lean/Elab/Do/InferControlInfo.lean

@@ -97,7 +97,7 @@ instance : ToMessageData ControlInfo where
     noFallthrough: {info.noFallthrough}, reassigns: {info.reassigns.toList}"
 
 /-- A handler for inferring `ControlInfo` from a `doElem` syntax. Register with `@[doElem_control_info parserName]`. -/
-abbrev ControlInfoHandler := TSyntax `doElem → TermElabM ControlInfo
+abbrev ControlInfoHandler := DoElem → TermElabM ControlInfo
 
 unsafe def mkControlInfoElemAttributeUnsafe (ref : Name) : IO (KeyedDeclsAttribute ControlInfoHandler) :=
   mkElabAttribute ControlInfoHandler `builtin_doElem_control_info `doElem_control_info
@@ -109,7 +109,7 @@ opaque mkControlInfoElemAttribute (ref : Name) : IO (KeyedDeclsAttribute Control
 /--
 Registers a `ControlInfo` inference handler for the given `doElem` syntax node kind.
 
-A handler should have type `ControlInfoHandler` (i.e. `TSyntax \`doElem → TermElabM ControlInfo`).
+A handler should have type `ControlInfoHandler` (i.e. `DoElem → TermElabM ControlInfo`).
 For pure handlers, use `fun stx => return ControlInfo.pure`.
 -/
 @[builtin_doc]
@@ -121,7 +121,7 @@ namespace InferControlInfo
 open InternalSyntax in
 mutual
 
-partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
+partial def ofElem (stx : DoElem) : TermElabM ControlInfo := do
   let env ← getEnv
   if let some (_decl, stxNew?) ← liftMacroM (expandMacroImpl? env stx) then
     let stxNew ← liftMacroM <| liftExcept stxNew?
@@ -251,7 +251,7 @@ partial def ofLetOrReassignArrow (reassignment : Bool) (decl : TSyntax [``doIdDe
     ofLetOrReassign reassigns rhs otherwise? body??.join
   | _ => throwError "Not a let or reassignment declaration: {toString decl}"
 
-partial def ofLetOrReassign (reassigned : Array Ident) (rhs? : Option (TSyntax `doElem))
+partial def ofLetOrReassign (reassigned : Array Ident) (rhs? : Option DoElem)
     (otherwise? : Option (TSyntax ``doSeqIndent)) (body? : Option (TSyntax ``doSeqIndent))
     : TermElabM ControlInfo := do
   let rhs ← match rhs? with | none => pure { : ControlInfo } | some rhs => ofElem rhs
@@ -260,23 +260,23 @@ partial def ofLetOrReassign (reassigned : Array Ident) (rhs? : Option (TSyntax `
   let info := rhs.sequence (body.alternative otherwise)
   return { info with reassigns := (reassigned.map TSyntax.getId).foldl NameSet.insert info.reassigns }
 
-partial def ofSeq (stx : TSyntax ``doSeq) : TermElabM ControlInfo := do
+partial def ofSeq (stx : DoSeq) : TermElabM ControlInfo := do
   let mut info : ControlInfo := {}
   for elem in getDoElems stx do
     info := info.sequence (← ofElem elem)
   return info
 
-partial def ofOptionSeq (stx? : Option (TSyntax ``doSeq)) : TermElabM ControlInfo := do
+partial def ofOptionSeq (stx? : Option DoSeq) : TermElabM ControlInfo := do
   match stx? with | none => pure { : ControlInfo } | some stx => ofSeq stx
 
 end
 
 end InferControlInfo
 
 /-- Infer the `ControlInfo` of `doSeq`. -/
-def inferControlInfoSeq (doSeq : TSyntax ``doSeq) : TermElabM ControlInfo :=
+def inferControlInfoSeq (doSeq : DoSeq) : TermElabM ControlInfo :=
   InferControlInfo.ofSeq doSeq
 
 /-- Infer the `ControlInfo` of a single doElem. -/
-def inferControlInfoElem (doElem : TSyntax `doElem) : TermElabM ControlInfo :=
+def inferControlInfoElem (doElem : DoElem) : TermElabM ControlInfo :=
   InferControlInfo.ofElem doElem

src/Lean/Meta/Sym/SymM.lean

@@ -301,7 +301,7 @@ def reportIssue (msg : MessageData) : SymM Unit := do
   if (← getConfig).verbose then
     reportIssue msg
 
-private meta def expandReportIssueMacro (s : Syntax) : MacroM (TSyntax `doElem) := do
+private meta def expandReportIssueMacro (s : Syntax) : MacroM DoElem := do
   let msg ← if s.getKind == interpolatedStrKind then `(m! $(⟨s⟩)) else `(($(⟨s⟩) : MessageData))
   `(doElem| Sym.reportIssueIfVerbose $msg)
 
@@ -315,7 +315,7 @@ macro "reportIssue!" s:(interpolatedStr(term) <|> term) : doElem => do
     if sym.debug.get (← getOptions) then
       reportIssue msg
 
-meta def expandReportDbgIssueMacro (s : Syntax) : MacroM (TSyntax `doElem) := do
+meta def expandReportDbgIssueMacro (s : Syntax) : MacroM DoElem := do
   let msg ← if s.getKind == interpolatedStrKind then `(m! $(⟨s⟩)) else `(($(⟨s⟩) : MessageData))
   `(doElem| Sym.reportDbgIssue $msg)
 

src/Lean/Parser/Do.lean

@@ -49,7 +49,7 @@ builtin_initialize
   register_parser_alias doSeq
   register_parser_alias termBeforeDo
 
-def getDoElems (doSeq : TSyntax ``doSeq) : Array (TSyntax `doElem) :=
+def getDoElems (doSeq : DoSeq) : Array DoElem :=
   if doSeq.raw.getKind == ``Parser.Term.doSeqBracketed then
     doSeq.raw[1].getArgs.map fun arg => ⟨arg[0]⟩
   else if doSeq.raw.getKind == ``Parser.Term.doSeqIndent then

src/Lean/Util/Trace.lean

@@ -387,7 +387,7 @@ def registerTraceClass (traceClassName : Name) (inherited := false) (ref : Name
   if inherited then
     inheritedTraceOptions.modify (·.insert optionName)
 
-private meta def expandTraceMacro (id : Syntax) (s : Syntax) : MacroM (TSyntax `doElem) := do
+private meta def expandTraceMacro (id : Syntax) (s : Syntax) : MacroM DoElem := do
   let msg ← if s.getKind == interpolatedStrKind then `(m! $(⟨s⟩)) else `(($(⟨s⟩) : MessageData))
   `(doElem| do
     let cls := $(quote id.getId.eraseMacroScopes)