Skip to content

Commit

Permalink
feat: enable reuse across types
Browse files Browse the repository at this point in the history
  • Loading branch information
bollu committed Apr 3, 2024
1 parent b8bf735 commit ca9cdc9
Showing 1 changed file with 3 additions and 2 deletions.
5 changes: 3 additions & 2 deletions src/Lean/Compiler/IR/ResetReuse.lean
Original file line number Diff line number Diff line change
Expand Up @@ -27,11 +27,11 @@ namespace Lean.IR.ResetReuse
-/

private def mayReuse (c₁ c₂ : CtorInfo) : Bool :=
c₁.size == c₂.size && c₁.usize == c₂.usize && c₁.ssize == c₂.ssize &&
c₁.size == c₂.size && c₁.usize == c₂.usize && c₁.ssize == c₂.ssize
/- The following condition is a heuristic.
We don't want to reuse cells from different types even when they are compatible
because it produces counterintuitive behavior. -/
c₁.name.getPrefix == c₂.name.getPrefix
-- c₁.name.getPrefix == c₂.name.getPrefix

private partial def S (w : VarId) (c : CtorInfo) : FnBody → FnBody
| FnBody.vdecl x t v@(Expr.ctor c' ys) b =>
Expand Down Expand Up @@ -76,6 +76,7 @@ private def argsContainsVar (ys : Array Arg) (x : VarId) : Bool :=
private def isCtorUsing (b : FnBody) (x : VarId) : Bool :=
match b with
| (FnBody.vdecl _ _ (Expr.ctor _ ys) _) => argsContainsVar ys x
| (FnBody.vdecl _ _ (Expr.reset _ y) _) => x == y
| _ => false

/-- Given `Dmain b`, the resulting pair `(new_b, flag)` contains the new body `new_b`,
Expand Down

0 comments on commit ca9cdc9

Please sign in to comment.