@[reducible, inline]

abbrev Lean.IR.ExpandResetReuse.ProjMap : Type

Mapping from variable to projections

@[reducible, inline]

abbrev Lean.IR.ExpandResetReuse.CollectProjMap.Collector : Type

@[inline]

def Lean.IR.ExpandResetReuse.CollectProjMap.collectVDecl (x : VarId) (v : Expr) : Collector

partial def Lean.IR.ExpandResetReuse.CollectProjMap.collectFnBody : FnBody → Collector

def Lean.IR.ExpandResetReuse.mkProjMap (d : Decl) : ProjMap

Create a mapping from variables to projections. This function assumes variable ids have been normalized

structure Lean.IR.ExpandResetReuse.Context : Type

• projMap : ProjMap

partial def Lean.IR.ExpandResetReuse.consumed (x : VarId) : FnBody → Bool

Return true iff x is consumed in all branches of the current block. Here consumption means the block contains a dec x or reuse x ....

@[reducible, inline]

abbrev Lean.IR.ExpandResetReuse.Mask : Type

partial def Lean.IR.ExpandResetReuse.eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (keep : Array FnBody) : Array FnBody × Mask

Auxiliary function for eraseProjIncFor

def Lean.IR.ExpandResetReuse.eraseProjIncFor (n : Nat) (y : VarId) (bs : Array FnBody) : Array FnBody × Mask

Try to erase inc instructions on projections of y occurring in the tail of bs. Return the updated bs and a bit mask specifying which incs have been removed.

partial def Lean.IR.ExpandResetReuse.reuseToCtor (x : VarId) : FnBody → FnBody

Replace reuse x ctor ... with ctor ..., and remove dec x

def Lean.IR.ExpandResetReuse.mkSlowPath (x y : VarId) (mask : Mask) (b : FnBody) : FnBody

replace

x := reset y; b

with

inc z_1; ...; inc z_i; dec y; b'

where z_i's are the variables in mask, and b' is b where we removed dec x and replaced reuse x ctor_i ... with ctor_i ....

@[reducible, inline]

abbrev Lean.IR.ExpandResetReuse.M (α : Type) : Type

def Lean.IR.ExpandResetReuse.mkFresh : M VarId

def Lean.IR.ExpandResetReuse.releaseUnreadFields (y : VarId) (mask : Mask) (b : FnBody) : M FnBody

def Lean.IR.ExpandResetReuse.setFields (y : VarId) (zs : Array Arg) (b : FnBody) : FnBody

def Lean.IR.ExpandResetReuse.isSelfSet (ctx : Context) (x : VarId) (i : Nat) (y : Arg) : Bool

Given set x[i] := y, return true iff y := proj[i] x

def Lean.IR.ExpandResetReuse.isSelfUSet (ctx : Context) (x : VarId) (i : Nat) (y : VarId) : Bool

Given uset x[i] := y, return true iff y := uproj[i] x

def Lean.IR.ExpandResetReuse.isSelfSSet (ctx : Context) (x : VarId) (n i : Nat) (y : VarId) : Bool

Given sset x[n, i] := y, return true iff y := sproj[n, i] x

partial def Lean.IR.ExpandResetReuse.removeSelfSet (ctx : Context) : FnBody → FnBody

Remove unnecessary set/uset/sset operations

partial def Lean.IR.ExpandResetReuse.reuseToSet (ctx : Context) (x y : VarId) : FnBody → FnBody

def Lean.IR.ExpandResetReuse.mkFastPath (x y : VarId) (mask : Mask) (b : FnBody) : M FnBody

replace

x := reset y; b

with

let f_i_1 := proj[i_1] y;
...
let f_i_k := proj[i_k] y;
b'

where i_js are the field indexes that the code did not touch immediately before the reset. That is mask[j] == none. b' is b where y dec x is replaced with del y, and z := reuse x ctor_i ws; F is replaced with set x i ws[i] operations, and we replace z with x in F

def Lean.IR.ExpandResetReuse.expand (mainFn : FnBody → Array FnBody → M FnBody) (bs : Array FnBody) (x : VarId) (n : Nat) (y : VarId) (b : FnBody) : M FnBody

partial def Lean.IR.ExpandResetReuse.searchAndExpand : FnBody → Array FnBody → M FnBody

def Lean.IR.ExpandResetReuse.main (d : Decl) : Decl

def Lean.IR.Decl.expandResetReuse (d : Decl) : Decl

(Try to) expand reset and reuse instructions.