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

fix: move structProjCases pass before extendJoinPointContext (#8752)

Browse source 
This PR fixes an issue where the `extendJoinPointContext` pass can lift
join points containing projections to the top level, as siblings of
`cases` constructs matching on other projections of the same base value.
This prevents the `structProjCases` pass from projecting both at once,
extending the lifetime of the parent value and breaking linearity at
runtime.

This would theoretically be possible to fix in `structProjCases`, but it
would require some better infrastructure for handling join points. It's
also likely that the IR passes dealing with reference counting would
have similar bugs that pessimize the code. For this reason, the simplest
thing is to just perform the `structProjCases` pass earlier, which
prevents `extendJoinPointContext` from lifting these join points.
This commit is contained in:
Cameron Zwarich 2025-06-12 14:52:02 -07:00 • committed by GitHub
parent 6a698c1c22
commit 8aa003bdfc
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Compiler/LCNF/Passes.lean
View file

@ -68,6 +68,7 @@ def builtinPassManager : PassManager := {
toMono,
simp (occurrence := 3) (phase := .mono),
reduceJpArity (phase := .mono),
structProjCases,
extendJoinPointContext (phase := .mono) (occurrence := 0),
floatLetIn (phase := .mono) (occurrence := 1),
reduceArity,
@ -78,7 +79,6 @@ def builtinPassManager : PassManager := {
lambdaLifting,
extendJoinPointContext (phase := .mono) (occurrence := 1),
simp (occurrence := 5) (phase := .mono),
structProjCases,
cse (occurrence := 2) (phase := .mono),
saveMono, -- End of mono phase
extractClosed