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

perf: avoid ref count increments for borrowed array accesses (#9866)

Browse source
This commit is contained in:
Cameron Zwarich 2025-08-11 22:27:35 -07:00 • committed by GitHub
parent 954957c456
commit e9df183e87
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 13 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -70,6 +70,12 @@ private partial def visitFnBody (b : FnBody) : M Unit := do
match e with
| .proj _ parent =>
addDerivedValue parent x
| .fap ``Array.getInternal args =>
if let .var parent := args[1]! then
addDerivedValue parent x
| .fap ``Array.get!Internal args =>
if let .var parent := args[2]! then
addDerivedValue parent x
| .reset _ x =>
removeFromParent x
| _ => pure ()
@ -351,7 +357,13 @@ private def processVDecl (ctx : Context) (z : VarId) (t : IRType) (v : Expr) (b
| .fap f ys =>
let ps := (getDecl ctx f).params
let b := addDecAfterFullApp ctx ys ps b bLiveVars
let b := .vdecl z t v b
let v :=
if f == ``Array.getInternal && bLiveVars.borrows.contains z then
.fap ``Array.getInternalBorrowed ys
else if f == ``Array.get!Internal && bLiveVars.borrows.contains z then
.fap ``Array.get!InternalBorrowed ys
else v
let b := .vdecl z t v b
addIncBefore ctx ys ps b bLiveVars
| .ap x ys =>
let ysx := ys.push (.var x) -- TODO: avoid temporary array allocation