Skip to content

Commit 30bf42a

Browse files
committed
fix: reduce cases where floatLetIn artificially blocks code motion
1 parent 52cfb7c commit 30bf42a

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

src/Lean/Compiler/LCNF/FloatLetIn.lean

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -229,10 +229,10 @@ def float (decl : CodeDecl) : FloatM Unit := do
229229
where
230230
goFVar (fvar : FVarId) (arm : Decision) : FloatM Unit := do
231231
let some decision := (← get).decision[fvar]? | return ()
232-
if decision != arm then
233-
modify fun s => { s with decision := s.decision.insert fvar .dont }
234-
else if decision == .unknown then
232+
if decision == .unknown then
235233
modify fun s => { s with decision := s.decision.insert fvar arm }
234+
else if decision != arm then
235+
modify fun s => { s with decision := s.decision.insert fvar .dont }
236236

237237
/--
238238
Iterate through `decl`, pushing local declarations that are only used in one

0 commit comments

Comments
 (0)