From e16e2b2ffa1c9d60d2c75b1508508ee7b38894e0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 23 Feb 2026 15:06:28 +0100
Subject: [PATCH] refactor: use Code.forM more (#12649)

---
 src/Lean/Compiler/LCNF/SplitSCC.lean | 22 +++++++---------------
 src/Lean/Compiler/LCNF/Toposort.lean | 16 +++++-----------
 2 files changed, 12 insertions(+), 26 deletions(-)

diff --git a/src/Lean/Compiler/LCNF/SplitSCC.lean b/src/Lean/Compiler/LCNF/SplitSCC.lean
index e0e4429e2c..d5fb4410ff 100644
--- a/src/Lean/Compiler/LCNF/SplitSCC.lean
+++ b/src/Lean/Compiler/LCNF/SplitSCC.lean
@@ -21,21 +21,13 @@ partial def findSccCalls (scc : Std.HashMap Name (Decl pu)) (decl : Decl pu) : B
   | .extern .. => return {}
 where
   goCode (c : Code pu) : StateRefT (Std.HashSet Name) BaseIO Unit := do
-    match c with
-    | .let decl k =>
-      match decl.value with
-      | .const name .. | .fap name .. | .pap name .. =>
-        if scc.contains name then
-          modify fun s => s.insert name
-      | _ => pure ()
-      goCode k
-    | .fun decl k _ | .jp decl k =>
-      goCode decl.value
-      goCode k
-    | .cases cases => cases.alts.forM (·.forCodeM goCode)
-    | .jmp .. | .return .. | .unreach .. => return ()
-    | .uset (k := k) .. | .sset (k := k) .. | .inc (k := k) .. | .dec (k := k) .. =>
-      goCode k
+    c.forM fun c => do
+      if let .let decl _ := c then
+        match decl.value with
+        | .const name .. | .fap name .. | .pap name .. =>
+          if scc.contains name then
+            modify fun s => s.insert name
+        | _ => return
 
 end SplitScc
 
diff --git a/src/Lean/Compiler/LCNF/Toposort.lean b/src/Lean/Compiler/LCNF/Toposort.lean
index 106586de08..ee710dc246 100644
--- a/src/Lean/Compiler/LCNF/Toposort.lean
+++ b/src/Lean/Compiler/LCNF/Toposort.lean
@@ -43,24 +43,18 @@ where
       return ()
 
     modify fun s => { s with seen := s.seen.insert decl.name }
-    decl.value.forCodeM visit
+    decl.value.forCodeM (·.forM visitConsts)
     modify fun s => { s with order := s.order.push decl }
 
-  visit (code : Code pu) : ToposortM pu Unit := do
+  visitConsts (code : Code pu) : ToposortM pu Unit := do
     match code with
-    | .let decl k =>
+    | .let decl _ =>
       match decl.value with
       | .const declName .. | .fap declName .. | .pap declName .. =>
         if let some d := (← read).declsMap[declName]? then
           process d
-      | _ => pure ()
-      visit k
-    | .jp decl k | .fun decl k .. =>
-      visit decl.value
-      visit k
-    | .cases c => c.alts.forM fun alt => visit alt.getCode
-    | .jmp .. | .return .. | .unreach .. => return ()
-    | .uset (k := k) .. | .sset (k := k) .. | .inc (k := k) .. | .dec (k := k) .. => visit k
+      | _ => return ()
+    | _ => return ()
 
 public def toposortDecls (decls : Array (Decl pu)) : CompilerM (Array (Decl pu)) := do
   let (externDecls, otherDecls) := decls.partition (fun decl => decl.value matches .extern ..)