@[reducible, inline]

abbrev Lean.IR.ExpandResetReuse.ProjMap : Type

Mapping from variable to projections

Equations

• Lean.IR.ExpandResetReuse.ProjMap = Std.HashMap Lean.IR.VarId Lean.IR.Expr

@[reducible, inline]

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

Equations

• Lean.IR.ExpandResetReuse.CollectProjMap.Collector = (Lean.IR.ExpandResetReuse.ProjMap → Lean.IR.ExpandResetReuse.ProjMap)

@[inline]

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

Equations

• Lean.IR.ExpandResetReuse.CollectProjMap.collectVDecl x (Lean.IR.Expr.proj i x_1) m = Std.HashMap.insert m x (Lean.IR.Expr.proj i x_1)
• Lean.IR.ExpandResetReuse.CollectProjMap.collectVDecl x (Lean.IR.Expr.sproj n offset x_1) m = Std.HashMap.insert m x (Lean.IR.Expr.sproj n offset x_1)
• Lean.IR.ExpandResetReuse.CollectProjMap.collectVDecl x (Lean.IR.Expr.uproj i x_1) m = Std.HashMap.insert m x (Lean.IR.Expr.uproj i x_1)
• Lean.IR.ExpandResetReuse.CollectProjMap.collectVDecl x v m = m

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

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

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

Equations

• Lean.IR.ExpandResetReuse.mkProjMap (Lean.IR.Decl.fdecl f xs type b info) = Lean.IR.ExpandResetReuse.CollectProjMap.collectFnBody b ∅
• Lean.IR.ExpandResetReuse.mkProjMap d = ∅

structure Lean.IR.ExpandResetReuse.Context : Type

• projMap : Lean.IR.ExpandResetReuse.ProjMap

partial def Lean.IR.ExpandResetReuse.consumed (x : Lean.IR.VarId) : Lean.IR.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

Equations

• Lean.IR.ExpandResetReuse.Mask = Array (Option Lean.IR.VarId)

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

Auxiliary function for eraseProjIncFor

def Lean.IR.ExpandResetReuse.eraseProjIncFor (n : Nat) (y : Lean.IR.VarId) (bs : Array Lean.IR.FnBody) : Array Lean.IR.FnBody × Lean.IR.ExpandResetReuse.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.

Equations

• Lean.IR.ExpandResetReuse.eraseProjIncFor n y bs = Lean.IR.ExpandResetReuse.eraseProjIncForAux y bs (mkArray n none) #[]

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

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

def Lean.IR.ExpandResetReuse.mkSlowPath (x : Lean.IR.VarId) (y : Lean.IR.VarId) (mask : Lean.IR.ExpandResetReuse.Mask) (b : Lean.IR.FnBody) : Lean.IR.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 ....

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

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

Equations

• Lean.IR.ExpandResetReuse.M = ReaderT Lean.IR.ExpandResetReuse.Context (StateM Nat)

def Lean.IR.ExpandResetReuse.mkFresh : Lean.IR.ExpandResetReuse.M Lean.IR.VarId

Equations

• Lean.IR.ExpandResetReuse.mkFresh = modifyGet fun (n : Lean.IR.Index) => ({ idx := n }, n + 1)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.IR.ExpandResetReuse.setFields y zs b = Nat.fold (fun (i : Nat) (b : Lean.IR.FnBody) => Lean.IR.FnBody.set y i (zs.get! i) b) zs.size b

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

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

Equations

• Lean.IR.ExpandResetReuse.isSelfSet ctx x i (Lean.IR.Arg.var y_2) = match ctx.projMap[y_2]? with | some (Lean.IR.Expr.proj j w) => j == i && w == x | x => false
• Lean.IR.ExpandResetReuse.isSelfSet ctx x i y = false

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

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

Equations

• Lean.IR.ExpandResetReuse.isSelfUSet ctx x i y = match ctx.projMap[y]? with | some (Lean.IR.Expr.uproj j w) => j == i && w == x | x => false

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

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

Equations

• Lean.IR.ExpandResetReuse.isSelfSSet ctx x n i y = match ctx.projMap[y]? with | some (Lean.IR.Expr.sproj m j w) => n == m && j == i && w == x | x => false

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

Remove unnecessary set/uset/sset operations

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

def Lean.IR.ExpandResetReuse.mkFastPath (x : Lean.IR.VarId) (y : Lean.IR.VarId) (mask : Lean.IR.ExpandResetReuse.Mask) (b : Lean.IR.FnBody) : Lean.IR.ExpandResetReuse.M Lean.IR.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

Equations

• Lean.IR.ExpandResetReuse.mkFastPath x y mask b = do let ctx ← read let b : Lean.IR.FnBody := Lean.IR.ExpandResetReuse.reuseToSet ctx x y b Lean.IR.ExpandResetReuse.releaseUnreadFields y mask b

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.IR.ExpandResetReuse.main d = d

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

(Try to) expand reset and reuse instructions.

Equations

• d.expandResetReuse = (Lean.IR.ExpandResetReuse.main d).normalizeIds