From bf348ae60f5bace12f79576c9e0bb03b538f261b Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Mon, 11 Aug 2025 16:56:50 -0700 Subject: [PATCH] refactor: use more helper functions (#9862) --- src/Lean/Compiler/IR/RC.lean | 36 +++++++++++++++++++++--------------- 1 file changed, 21 insertions(+), 15 deletions(-) diff --git a/src/Lean/Compiler/IR/RC.lean b/src/Lean/Compiler/IR/RC.lean index a71ef09bf6..3743b4a751 100644 --- a/src/Lean/Compiler/IR/RC.lean +++ b/src/Lean/Compiler/IR/RC.lean @@ -45,27 +45,33 @@ private def visitParam (p : Param) : M Unit := else s.borrowedParams } +private partial def addDerivedValue (parent : VarId) (child : VarId) : M Unit := do + modify fun s => { s with + varMap := s.varMap.modify parent fun info => + { info with children := info.children.insert child } + } + modify fun s => { s with + varMap := s.varMap.insert child { + parent? := some parent + children := {} + } + } + +private partial def removeFromParent (child : VarId) : M Unit := do + if let some (some parent) := (← get).varMap.get? child |>.map (·.parent?) then + modify fun s => { s with + varMap := s.varMap.modify parent fun info => + { info with children := info.children.erase child } + } + private partial def visitFnBody (b : FnBody) : M Unit := do match b with | .vdecl x _ e b => match e with | .proj _ parent => - modify fun s => { s with - varMap := s.varMap.modify parent fun info => - { info with children := info.children.insert x } - } - modify fun s => { s with - varMap := s.varMap.insert x { - parent? := some parent - children := {} - } - } + addDerivedValue parent x | .reset _ x => - if let some (some parent) := (← get).varMap.get? x |>.map (·.parent?) then - modify fun s => { s with - varMap := s.varMap.modify parent fun info => - { info with children := info.children.erase x } - } + removeFromParent x | _ => pure () visitFnBody b | .jdecl _ ps v b =>