diff --git a/library/init/lean/compiler/elimdead.lean b/library/init/lean/compiler/elimdead.lean index a1ce8d79fb..7ce008bebd 100644 --- a/library/init/lean/compiler/elimdead.lean +++ b/library/init/lean/compiler/elimdead.lean @@ -32,12 +32,13 @@ reshapeWithoutDeadAux bs term term.freeVars partial def FnBody.elimDead : FnBody → FnBody | b := let (bs, term) := b.flatten in + let bs := modifyJPVals bs FnBody.elimDead in let term := match term with | FnBody.case tid x alts := let alts := alts.hmap $ λ alt, alt.modifyBody $ λ b, FnBody.elimDead b in FnBody.case tid x alts | other := other in - reshape bs term + reshapeWithoutDead bs term /-- Eliminate dead let-declarations and join points -/ @[export lean.ir.decl_elim_dead_core] diff --git a/library/init/lean/compiler/ir.lean b/library/init/lean/compiler/ir.lean index 7566ab7a7b..7eda612961 100644 --- a/library/init/lean/compiler/ir.lean +++ b/library/init/lean/compiler/ir.lean @@ -281,6 +281,11 @@ partial def reshapeAux : Array FnBody → Nat → FnBody → FnBody def reshape (bs : Array FnBody) (term : FnBody) : FnBody := reshapeAux bs bs.size term +@[inline] def modifyJPVals (bs : Array FnBody) (f : FnBody → FnBody) : Array FnBody := +bs.hmap $ λ b, match b with + | FnBody.jdecl j xs t v k := FnBody.jdecl j xs t (f v) k + | other := other + @[export lean.ir.mk_alt_core] def mkAlt (n : Name) (cidx : Nat) (size : Nat) (usize : Nat) (ssize : Nat) (b : FnBody) : Alt := Alt.ctor ⟨n, cidx, size, usize, ssize⟩ b inductive Decl diff --git a/library/init/lean/compiler/pushproj.lean b/library/init/lean/compiler/pushproj.lean index eb5c14f63a..4373fa3d27 100644 --- a/library/init/lean/compiler/pushproj.lean +++ b/library/init/lean/compiler/pushproj.lean @@ -36,6 +36,7 @@ partial def pushProjs : Array FnBody → Array Alt → Array IndexSet → Array partial def FnBody.pushProj : FnBody → FnBody | b := let (bs, term) := b.flatten in + let bs := modifyJPVals bs FnBody.pushProj in match term with | FnBody.case tid x alts := let afvs := alts.map $ λ alt, alt.body.freeVars in