feat: split ControlInfo.deadCode from syntactic numRegularExits

This PR separates the semantic dead-code flag from the syntactic
continuation-wiring count on `ControlInfo`. `numRegularExits` is now
documented as purely syntactic: the number of times the block wires
its enclosing continuation into its elaborated expression, consumed
by `withDuplicableCont` to decide whether to introduce a join point
(`> 1`). The new `deadCode : Bool` field holds the conservative
semantic estimate: `true` iff every path through the block provably
fails to reach the end normally.

Invariant: `numRegularExits = 0 → deadCode`. The converse does not
hold — for example a `repeat` without `break` has `numRegularExits = 1`
(the loop elaborator wires its continuation once for the normal-exit
path) yet `deadCode = true` (the loop never terminates normally). The
`repeat` handler now reports exactly that.

`ControlInfo.sequence` previously used `if a.numRegularExits == 0` to
absorb `b`, conflating the two notions. It now aggregates the
syntactic fields unconditionally and derives `deadCode` as
`a.deadCode || b.deadCode`. `ControlInfo.alternative` derives it as
`a.deadCode && b.deadCode`. The dead-code warning gate in
`withDuplicableCont` and `ControlLifter.ofCont` now reads `deadCode`
instead of `numRegularExits == 0`, so it fires on all semantic
dead-code paths (including `repeat` without `break`) rather than only
when the continuation is also syntactically unwired.

src/Lean/Elab/Do/Basic.lean

@@ -587,7 +587,7 @@ def DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : Control
     withLocalDeclD nondupDec.resultName nondupDec.resultType fun r => do
     withLocalDeclsDND (mutDecls.map fun (d : LocalDecl) => (d.userName, d.type)) fun muts => do
     for (x, newX) in mutVars.zip muts do Term.addTermInfo' x newX
-    withDeadCode (if callerInfo.numRegularExits > 0 then .alive else .deadSemantically) do
+    withDeadCode (if callerInfo.deadCode then .deadSemantically else .alive) do
     let e ← nondupDec.k
     mkLambdaFVars (#[r] ++ muts) e
   unless ← joinRhsMVar.mvarId!.checkedAssign joinRhs do

src/Lean/Elab/Do/Control.lean

@@ -232,9 +232,8 @@ def ControlLifter.ofCont (info : ControlInfo) (dec : DoElemCont) : DoElabM Contr
     breakBase?,
     continueBase?,
     pureBase := controlStack,
-    -- The success continuation `origCont` is dead code iff the `ControlInfo` says that there is no
-    -- regular exit.
-    pureDeadCode := if info.numRegularExits > 0 then .alive else .deadSemantically,
+    -- The success continuation `origCont` is dead code iff the `ControlInfo` says so semantically.
+    pureDeadCode := if info.deadCode then .deadSemantically else .alive,
     liftedDoBlockResultType := (← controlStack.stM dec.resultType),
   }
 

src/Lean/Elab/Do/InferControlInfo.lean

@@ -16,48 +16,77 @@ namespace Lean.Elab.Do
 
 open Lean Meta Parser.Term
 
-/-- Represents information about what control effects a `do` block has. -/
+/--
+Represents information about what control effects a `do` block has.
+
+The fields split by flavor:
+
+* `breaks`, `continues`, `returnsEarly`, and `reassigns` are **syntactic**: `true`/non-empty iff
+  the corresponding construct appears anywhere in the source text of the block, independent of
+  whether it is semantically reachable. Downstream elaborators must assume every such syntactic
+  effect may occur, because the elaborator visits every doElem (only top-level
+  `return`/`break`/`continue` short-circuit via `elabAsSyntacticallyDeadCode`).
+* `numRegularExits` is also **syntactic**: the number of times the block wires the enclosing
+  continuation into its elaborated expression. `withDuplicableCont` reads it as a join-point
+  duplication trigger (`> 1`).
+* `deadCode` is **semantic**: a conservative over-approximation of "every path through the block
+  fails to reach the end normally". It drives the dead-code warning.
+
+Invariant: `numRegularExits = 0 → deadCode = true`. The converse does not hold — for example a
+`repeat` with no `break` has `numRegularExits = 1` (the loop elaborator wires its continuation
+once for the normal-exit path) but `deadCode = true` (the loop never terminates normally).
+-/
 structure ControlInfo where
-  /-- The `do` block may `break`. -/
+  /-- The `do` block syntactically contains a `break`. -/
   breaks : Bool := false
-  /-- The `do` block may `continue`. -/
+  /-- The `do` block syntactically contains a `continue`. -/
   continues : Bool := false
-  /-- The `do` block may `return` early. -/
+  /-- The `do` block syntactically contains an early `return`. -/
   returnsEarly : Bool := false
   /--
-  The number of regular exit paths the `do` block has.
-  Corresponds to the number of jumps to an ambient join point.
+  The number of times the block wires the enclosing continuation into its elaborated expression.
+  Consumed by `withDuplicableCont` to decide whether to introduce a join point (`> 1`).
   -/
   numRegularExits : Nat := 1
-  /-- The variables that are reassigned in the `do` block. -/
+  /--
+  Conservative semantic flag: `true` iff every path through the block provably fails to reach the
+  end normally. Implied by `numRegularExits = 0`, but not equivalent (e.g. a `repeat` without
+  `break` has `numRegularExits = 1` yet is dead).
+  -/
+  deadCode : Bool := false
+  /-- The variables that are syntactically reassigned somewhere in the `do` block. -/
   reassigns : NameSet := {}
   deriving Inhabited
 
 def ControlInfo.pure : ControlInfo := {}
 
 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
+    -- `elabAsSyntacticallyDeadCode`).
     breaks := a.breaks || b.breaks,
     continues := a.continues || b.continues,
     returnsEarly := a.returnsEarly || b.returnsEarly,
-    -- Once `a` has no regular exits, `b` is statically unreachable, so no regular exit survives.
-    -- We still aggregate the other effects because the elaborator keeps visiting `b` unless it is
-    -- skipped via `elabAsSyntacticallyDeadCode`.
-    numRegularExits := if a.numRegularExits == 0 then 0 else b.numRegularExits,
     reassigns := a.reassigns ++ b.reassigns,
+    numRegularExits := b.numRegularExits,
+    -- Semantic: the sequence is dead if either part is dead.
+    deadCode := a.deadCode || b.deadCode,
   }
 
 def ControlInfo.alternative (a b : ControlInfo) : ControlInfo := {
     breaks := a.breaks || b.breaks,
     continues := a.continues || b.continues,
     returnsEarly := a.returnsEarly || b.returnsEarly,
-    numRegularExits := a.numRegularExits + b.numRegularExits,
     reassigns := a.reassigns ++ b.reassigns,
+    numRegularExits := a.numRegularExits + b.numRegularExits,
+    -- Semantic: alternatives are dead only if all branches are dead.
+    deadCode := a.deadCode && b.deadCode,
   }
 
 instance : ToMessageData ControlInfo where
   toMessageData info := m!"breaks: {info.breaks}, continues: {info.continues},
-    returnsEarly: {info.returnsEarly}, exitsRegularly: {info.numRegularExits},
-    reassigns: {info.reassigns.toList}"
+    returnsEarly: {info.returnsEarly}, numRegularExits: {info.numRegularExits},
+    deadCode: {info.deadCode}, 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
@@ -91,9 +120,9 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
     return ← ofElem ⟨stxNew⟩
 
   match stx with
-  | `(doElem| break) => return { breaks := true, numRegularExits := 0 }
-  | `(doElem| continue) => return { continues := true, numRegularExits := 0 }
-  | `(doElem| return $[$_]?) => return { returnsEarly := true, numRegularExits := 0 }
+  | `(doElem| break) => return { breaks := true, numRegularExits := 0, deadCode := true }
+  | `(doElem| continue) => return { continues := true, numRegularExits := 0, deadCode := true }
+  | `(doElem| return $[$_]?) => return { returnsEarly := true, numRegularExits := 0, deadCode := true }
   | `(doExpr| $_:term) => return { numRegularExits := 1 }
   | `(doElem| do $doSeq) => ofSeq doSeq
   -- Let
@@ -137,14 +166,18 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
     return { info with  -- keep only reassigns and earlyReturn
       numRegularExits := 1,
       continues := false,
-      breaks := false
+      breaks := false,
+      deadCode := false,
     }
   | `(doRepeat| repeat $bodySeq) =>
     let info ← ofSeq bodySeq
     return { info with
-      numRegularExits := if info.breaks then 1 else 0,
+      -- Syntactically the loop elaborator wires the continuation once (for the break path).
+      numRegularExits := 1,
       continues := false,
-      breaks := false
+      breaks := false,
+      -- Semantically the loop never terminates normally unless the body may `break`.
+      deadCode := !info.breaks,
     }
   -- Try
   | `(doElem| try $trySeq:doSeq $[$catches]* $[finally $finSeq?]?) =>