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

chore: remove VarInfo defaults in IR RC pass (#9167)

Browse source 
These defaults don't make the code easier to understand.
This commit is contained in:
Cameron Zwarich 2025-07-02 20:15:07 -07:00 • committed by GitHub
parent 01d32aa408
commit 174b1301d8
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -16,9 +16,9 @@ that introduce the instructions `release` and `set`
-/
structure VarInfo where
ref : Bool := true -- true if the variable may be a reference (aka pointer) at runtime
persistent : Bool := false -- true if the variable is statically known to be marked a Persistent at runtime
consume : Bool := false -- true if the variable RC must be "consumed"
ref : Bool -- true if the variable may be a reference (aka pointer) at runtime
persistent : Bool -- true if the variable is statically known to be marked a Persistent at runtime
consume : Bool -- true if the variable RC must be "consumed"
deriving Inhabited
abbrev VarMap := RBMap VarId VarInfo (fun x y => compare x.idx y.idx)
@ -207,7 +207,7 @@ private def processVDecl (ctx : Context) (z : VarId) (t : IRType) (v : Expr) (b
def updateVarInfoWithParams (ctx : Context) (ps : Array Param) : Context :=
let m := ps.foldl (init := ctx.varMap) fun m p =>
m.insert p.x { ref := p.ty.isObj, consume := !p.borrow }
m.insert p.x { ref := p.ty.isObj, persistent := false, consume := !p.borrow }
{ ctx with varMap := m }
partial def visitFnBody : FnBody → Context → (FnBody × LiveVarSet)