From 7c5377707cfedaba3d08c518aa85885bd39bb377 Mon Sep 17 00:00:00 2001 From: Anton Lorenzen Date: Mon, 1 Apr 2024 15:00:16 +0100 Subject: [PATCH] fix: recursive call also on delete and re-enable reuse specialization --- src/Lean/Compiler/IR/ExpandResetReuse.lean | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/Lean/Compiler/IR/ExpandResetReuse.lean b/src/Lean/Compiler/IR/ExpandResetReuse.lean index 98e8658e345c..9260793ea287 100644 --- a/src/Lean/Compiler/IR/ExpandResetReuse.lean +++ b/src/Lean/Compiler/IR/ExpandResetReuse.lean @@ -187,12 +187,14 @@ partial def searchAndSpecialize : FnBody → Array FnBody → Array VarId → Ha let b ← searchAndSpecialize b #[] (tokens.push x) (subst.insert x y) let b ← specializeReset x y mask b return reshape bs b - -- | FnBody.vdecl z t (Expr.reuse w c u zs) b, bs, tokens, subst => do - -- let b ← searchAndSpecialize b #[] tokens subst - -- let b ← specializeReuse z w (subst.find! w) c u t zs b - -- return reshape bs b + | FnBody.vdecl z t (Expr.reuse w c u zs) b, bs, tokens, subst => do + let b ← searchAndSpecialize b #[] tokens subst + let b ← specializeReuse z w (subst.find! w) c u t zs b + return reshape bs b | FnBody.dec z n c p b, bs, tokens, subst => - if tokens.contains z then return FnBody.del z b + if tokens.contains z then do + let b ← searchAndSpecialize b #[] tokens subst + return reshape bs (FnBody.del z b) else do let b ← searchAndSpecialize b #[] tokens subst return reshape bs (FnBody.dec z n c p b)