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

fix: use the fvar subst for erased code in LCNF simp (#8717)

Browse source 
This PR uses the fvar substitution mechanism to replace erased code.
This isn't entirely satisfactory, since LCNF's `.return` doesn't support
a general `Arg` (which has a `.erased` constructor), it only supports an
`FVarId`. This is in contrast to the IR `.ret`, which does support a
general `Arg`.
This commit is contained in:
Cameron Zwarich 2025-06-10 22:46:39 -07:00 • committed by GitHub
parent eccc472e8d
commit a92890ec84
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 8 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Lean/Compiler/LCNF/Simp/Main.lean
View file

@ -224,13 +224,17 @@ partial def simp (code : Code) : SimpM Code := withIncRecDepth do
let mut decl ← normLetDecl baseDecl
if baseDecl != decl then
markSimplified
if decl.type.isErased && decl.value != .erased then
markSimplified
decl ← decl.updateValue .erased
if let some value ← simpValue? decl.value then
markSimplified
decl ← decl.updateValue value
if let some decls ← ConstantFold.foldConstants decl then
-- This `decl.value != .erased` check is required because `.return` takes
-- and `FVarId` rather than `Arg`, and the substitution will end up
-- creating a new erased let decl in that case.
if decl.type.isErased && decl.value != .erased then
modifySubst fun s => s.insert decl.fvarId (.const ``lcErased [])
eraseLetDecl decl
simp k
else if let some decls ← ConstantFold.foldConstants decl then
markSimplified
let k ← simp k
attachCodeDecls decls k