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

fix: revert #8023 now that it is redundant (#8371)

Browse source 
This PR reverts #8023 now that it has been made redundant by the more
general fix in #8367.
This commit is contained in:
Cameron Zwarich 2025-05-15 17:53:30 -07:00 • committed by GitHub
parent 73509d03f3
commit fcb6bcee67
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 5 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/Lean/Compiler/IR/ExpandResetReuse.lean
View file

@ -49,23 +49,11 @@ partial def consumed (x : VarId) : FnBody → Bool
| e => !e.isTerminal && consumed x e.body
abbrev Mask := Array (Option VarId)
abbrev ProjCounts := Std.HashMap (VarId × Nat) Nat
partial def computeProjCounts (bs : Array FnBody) : ProjCounts :=
let incrementCountIfProj r b :=
if let .vdecl _ _ (.proj i v) _ := b then
r.alter (v, i) fun
| some n => some (n + 1)
| none => some 1
else
r
bs.foldl incrementCountIfProj Std.HashMap.emptyWithCapacity
/-- Auxiliary function for eraseProjIncFor -/
partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (projCounts : ProjCounts)
(mask : Mask) (keep : Array FnBody) : Array FnBody × Mask :=
partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (keep : Array FnBody) : Array FnBody × Mask :=
let done (_ : Unit) := (bs ++ keep.reverse, mask)
let keepInstr (b : FnBody) := eraseProjIncForAux y bs.pop projCounts mask (keep.push b)
let keepInstr (b : FnBody) := eraseProjIncForAux y bs.pop mask (keep.push b)
if h : bs.size < 2 then done ()
else
let b := bs.back!
@ -77,10 +65,7 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (projCounts : Pro
let b' := bs[bs.size - 2]
match b' with
| .vdecl w _ (.proj i x) _ =>
-- We disable the inc optimization if there are multiple projections with the same base
-- and index, because the downstream transformations are incapable of correctly handling
-- the aliasing.
if w == z && y == x && projCounts[(x, i)]! == 1 then
if w == z && y == x then
/- Found
```
let z := proj[i] y
@ -92,7 +77,7 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (projCounts : Pro
let mask := mask.set! i (some z)
let keep := keep.push b'
let keep := if n == 1 then keep else keep.push (FnBody.inc z (n-1) c p FnBody.nil)
eraseProjIncForAux y bs projCounts mask keep
eraseProjIncForAux y bs mask keep
else done ()
| _ => done ()
| _ => done ()
@ -100,7 +85,7 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (projCounts : Pro
/-- Try to erase `inc` instructions on projections of `y` occurring in the tail of `bs`.
Return the updated `bs` and a bit mask specifying which `inc`s have been removed. -/
def eraseProjIncFor (n : Nat) (y : VarId) (bs : Array FnBody) : Array FnBody × Mask :=
eraseProjIncForAux y bs (computeProjCounts bs) (.replicate n none) #[]
eraseProjIncForAux y bs (.replicate n none) #[]
/-- Replace `reuse x ctor ...` with `ctor ...`, and remove `dec x` -/
partial def reuseToCtor (x : VarId) : FnBody → FnBody