max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: reduce code duplication (#9742)

Browse source
This commit is contained in:
Cameron Zwarich 2025-08-05 13:42:56 -07:00 • committed by GitHub
parent eb5399445a
commit 6846a5179b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 9 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/Lean/Compiler/IR/RC.lean
View file

@ -180,25 +180,24 @@ private def addDecIfNeeded (ctx : Context) (x : VarId) (b : FnBody) (bLiveVars :
private def processVDecl (ctx : Context) (z : VarId) (t : IRType) (v : Expr) (b : FnBody) (bLiveVars : LiveVarSet) : FnBody × LiveVarSet :=
let b := match v with
| .ctor _ ys => addIncBeforeConsumeAll ctx ys (.vdecl z t v b) bLiveVars
| .reuse _ _ _ ys => addIncBeforeConsumeAll ctx ys (.vdecl z t v b) bLiveVars
| .proj _ x =>
| .ctor _ ys | .reuse _ _ _ ys | .pap _ ys =>
addIncBeforeConsumeAll ctx ys (.vdecl z t v b) bLiveVars
| .proj _ x =>
let b := addDecIfNeeded ctx x b bLiveVars
let b := if (getVarInfo ctx x).consume then addInc ctx z b else b
.vdecl z t v b
| .uproj _ x => .vdecl z t v (addDecIfNeeded ctx x b bLiveVars)
| .sproj _ _ x => .vdecl z t v (addDecIfNeeded ctx x b bLiveVars)
| .fap f ys =>
| .uproj _ x | .sproj _ _ x | .unbox x =>
.vdecl z t v (addDecIfNeeded ctx x b bLiveVars)
| .fap f ys =>
let ps := (getDecl ctx f).params
let b := addDecAfterFullApp ctx ys ps b bLiveVars
let b := .vdecl z t v b
addIncBefore ctx ys ps b bLiveVars
| .pap _ ys => addIncBeforeConsumeAll ctx ys (.vdecl z t v b) bLiveVars
| .ap x ys =>
| .ap x ys =>
let ysx := ys.push (.var x) -- TODO: avoid temporary array allocation
addIncBeforeConsumeAll ctx ysx (.vdecl z t v b) bLiveVars
| .unbox x => .vdecl z t v (addDecIfNeeded ctx x b bLiveVars)
| _ => .vdecl z t v b -- Expr.reset, Expr.box, Expr.lit are handled here
| .lit _ | .box .. | .reset .. | .isShared _ =>
.vdecl z t v b
let liveVars := updateLiveVars v bLiveVars
let liveVars := liveVars.erase z
⟨b, liveVars⟩