doc: fix stale references in do elaborator docs (#14026)

This PR fixes doc typos and stale references in the `do` elaborator and
parser: the `CodeLiveness.deadSyntactically` docstring describes
syntactically dead code, the `Context.doBlockResultType` docstring
references `ReturnCont.resultType`, `ControlInfo` comments reference the
`returnsEarly` field, the `DoElemContKind` docstring drops a stale
remark about `pure` continuations, the `doElem_control_info` docstring
markup is repaired, the `ControlInfo.pure`/`sequence`/`alternative`
docstrings are rewritten in the style of `ControlInfo.empty`, the
`EffectForwarder.lift` docstring references
`ControlStack.mkBreak`/`mkContinue`/`mkReturn`, and grammar typos in
`withLCtxKeepingMutVarDefs`, `expandToTermMatch` and the `doFor`/`idbg`
parser docstrings are fixed.

Author: sgraf812

src/Lean/Elab/BuiltinDo/Match.lean

@@ -36,7 +36,7 @@ private def elabDoSeqWithRefinedType (type : Expr) (doSeq : DoSeq) (dec : DoElem
   withDoBlockResultType newDoBlockResultType (elabDoSeq doSeq dec)
 
 /--
-Expand a `doMatch` into a term `match` term. We do this for `match_syntax` and
+Expand a `doMatch` into a term-level `match`. We do this for `match_syntax` and
 `match (dependent := true)`. For the latter, the functionality is very restricted to effectively
 ban join points.
 Reason: In case of a dependent match, it is hard to guarantee that generalization of join points and

src/Lean/Elab/Do/Basic.lean

@@ -56,7 +56,7 @@ instance : Nonempty DoOpsRef :=
 
 /-- Whether a code block is alive or dead. -/
 inductive CodeLiveness where
-  /-- We inferred the code is semantically dead and don't need to elaborate it at all. -/
+  /-- We inferred the code is syntactically dead and don't need to elaborate it at all. -/
   | deadSyntactically
   /-- We inferred the code is semantically dead, but we need to elaborate it to produce a program. -/
   | deadSemantically
@@ -115,7 +115,7 @@ structure Context where
   mutVarDefs : Std.HashMap Name MutVar := {}
   /--
   The expected type of the current `do` block.
-  This can be different from `earlyReturnType` in `for` loop `do` blocks, for example.
+  This can be different from `ReturnCont.resultType` in `for` loop `do` blocks, for example.
   -/
   doBlockResultType : Expr
   /-- Information about `return`, `break` and `continue` continuations. -/
@@ -160,9 +160,8 @@ unsafe def DoOpsRef.toDoOpsImpl (r : DoOpsRef) : DoOps :=
 opaque DoOpsRef.toDoOps (r : DoOpsRef) : DoOps
 
 /--
-Whether the continuation of a `do` element is duplicable and if so whether it is just `pure r` for
-the result variable `r`. Saying `nonDuplicable` is always safe; `duplicable` allows for more
-optimizations.
+Whether the continuation of a `do` element is duplicable. Saying `nonDuplicable` is always safe;
+`duplicable` allows for more optimizations.
 -/
 inductive DoElemContKind
   | nonDuplicable
@@ -224,7 +223,7 @@ structure ReturnCont where
   /--
   The elaborator constructing a jump site to the return continuation,
   given some return value. The type of this return value determines the type of the jump expression;
-  this could very well be different than the `resultType` in case an intervening `match` as refined
+  this could very well be different than the `resultType` in case an intervening `match` has refined
   `resultType`. So `k` must *not* hardcode the type `resultType` into its definition; rather it
   should infer the type of the return value argument.
   -/
@@ -450,7 +449,7 @@ pure (x + y + z)
 ```
 Note that the continuation of the `let z ← ...` bind, roughly
 ``k := .cont `z _ `(let y := y + 3; pure (x + y + z))``,
-needs to elaborated in a local context that contains the reassignment of `x`, but not the shadowing
+needs to be elaborated in a local context that contains the reassignment of `x`, but not the shadowing
 mut var definition of `y`.
 -/
 def withLCtxKeepingMutVarDefs (oldLCtx : LocalContext) (oldCtx : Context) (resultName : Name) (k : DoElabM α) : DoElabM α := do

src/Lean/Elab/Do/Control.lean

@@ -248,7 +248,7 @@ handlers funnelling into `liftedStack` and set the doBlock result type to
 `liftedDoBlockResultType`. Semantically
 `MonadControl.liftWith fun runInBase => elabElem (runInBase pure)`. Conts
 passed to `elabElem` are implicitly wrapped in `runInBase`, realised later by
-`ControlStack.synthesizeConts` once the transformer stack `t` is fixed by
+`ControlStack.mkBreak`/`mkContinue`/`mkReturn` once the transformer stack `t` is fixed by
 aggregating effects across *all* `lift` sites for this lifter.
 -/
 def EffectForwarder.lift (l : EffectForwarder) (elabElem : DoElemCont → DoElabM Expr) : DoElabM Expr := do

src/Lean/Elab/Do/InferControlInfo.lean

@@ -57,7 +57,10 @@ structure ControlInfo where
   reassigns : NameSet := {}
   deriving Inhabited
 
-/-- A `ControlInfo` for an element that always falls through normally with a single exit. -/
+/--
+The left identity of `ControlInfo.sequence`: a `ControlInfo` describing an element that always
+falls through normally with a single regular exit.
+-/
 def ControlInfo.pure : ControlInfo := {}
 
 /--
@@ -66,7 +69,10 @@ at all (so no regular exits and the next element is trivially unreachable).
 -/
 def ControlInfo.empty : ControlInfo := { numRegularExits := 0, noFallthrough := true }
 
-/-- Combine info for `a; b`: union effect flags, exits/dead follow `b`/either. -/
+/--
+The `ControlInfo` of a sequence `a; b`: effect flags are unioned, the regular exits are those of
+`b`, and the sequence falls through iff both parts fall through.
+-/
 def ControlInfo.sequence (a b : ControlInfo) : ControlInfo := {
     -- Syntactic fields aggregate unconditionally; the elaborator keeps visiting `b` unless `a` is
     -- a syntactically-terminal element (only top-level `return`/`break`/`continue` are, via
@@ -80,7 +86,10 @@ def ControlInfo.sequence (a b : ControlInfo) : ControlInfo := {
     noFallthrough := a.noFallthrough || b.noFallthrough,
   }
 
-/-- Combine info for branches `a | b`: union flags, sum exits, dead iff both dead. -/
+/--
+The `ControlInfo` of branches `a | b`: effect flags are unioned, the regular exits are summed, and
+the alternative falls through iff at least one branch falls through.
+-/
 def ControlInfo.alternative (a b : ControlInfo) : ControlInfo := {
     breaks := a.breaks || b.breaks,
     continues := a.continues || b.continues,
@@ -178,7 +187,7 @@ partial def ofElem (stx : DoElem) : TermElabM ControlInfo := do
   -- For/Repeat
   | `(doElem| for $[$[$_ :]? $_ in $_],* do $bodySeq) =>
     let info ← ofSeq bodySeq
-    return { info with  -- keep only reassigns and earlyReturn
+    return { info with  -- keep only reassigns and returnsEarly
       numRegularExits := 1,
       continues := false,
       breaks := false,
@@ -189,7 +198,7 @@ partial def ofElem (stx : DoElem) : TermElabM ControlInfo := do
     -- surrounding continuation still has a polymorphic value to hand back, and any dead-code
     -- warning on subsequent elements is actionable.
     let info ← ofSeq bodySeq
-    return { info with  -- keep only reassigns and earlyReturn
+    return { info with  -- keep only reassigns and returnsEarly
       numRegularExits := if info.breaks then 1 else 0,
       continues := false,
       breaks := false,

src/Lean/Parser/Do.lean

@@ -177,9 +177,9 @@ def doIfCond    :=
 def doForDecl := leading_parser
   optional (atomic (ident >> " : ")) >> termParser >> " in " >> withForbidden "do" termParser
 /--
-`for x in e do s`  iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass.
+`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass.
 `break` and `continue` are supported inside `for` loops.
-`for x in e, x2 in e2, ... do s` iterates of the given collections in parallel,
+`for x in e, x2 in e2, ... do s` iterates over the given collections in parallel,
 until at least one of them is exhausted.
 The types of `e2` etc. must implement the `Std.ToStream` typeclass.
 -/
@@ -271,11 +271,11 @@ the program need to be recompiled and restarted.
 
 # Known Limitations
 
-* The program will poll for the server for up to 10 minutes and needs to be killed manually
+* The program will poll the server for up to 10 minutes and needs to be killed manually
   otherwise.
 * Use of multiple `idbg` at once untested, likely too much overhead from overlapping imports without
   further changes.
-* `LEAN_PATH` must be properly set up so compiled program can import its origin module.
+* `LEAN_PATH` must be properly set up so the compiled program can import its origin module.
 * Untested on Windows and macOS.
 -/
 @[builtin_doElem_parser] def doIdbg      := leading_parser:leadPrec