Lean.Compiler.IR.ExpandResetReuse

source

@[inline]

abbrev Lean.IR.ExpandResetReuse.ProjMap:

Type

Equations

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

source

@[inline]

abbrev Lean.IR.ExpandResetReuse.CollectProjMap.Collector:

Type

Equations

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

source

@[inline]

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

Lean.IR.ExpandResetReuse.CollectProjMap.Collector

Equations

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

source

partial def Lean.IR.ExpandResetReuse.CollectProjMap.collectFnBody:

Lean.IR.FnBody → Lean.IR.ExpandResetReuse.CollectProjMap.Collector

source

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

Lean.IR.ExpandResetReuse.ProjMap

Equations

Lean.IR.ExpandResetReuse.mkProjMap d = match d with | Lean.IR.Decl.fdecl f xs type b info => Lean.IR.ExpandResetReuse.CollectProjMap.collectFnBody b ∅ | x => ∅

source

structure Lean.IR.ExpandResetReuse.Context:

Type

projMap : Lean.IR.ExpandResetReuse.ProjMap

source

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

Lean.IR.FnBody → Bool

source

@[inline]

abbrev Lean.IR.ExpandResetReuse.Mask:

Type

Equations

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

source

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

source

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

Array Lean.IR.FnBody × Lean.IR.ExpandResetReuse.Mask

Equations

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

source

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

Lean.IR.FnBody → Lean.IR.FnBody

source

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

Equations

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

source

@[inline]

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

Type

Equations

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

source

def Lean.IR.ExpandResetReuse.mkFresh:

Lean.IR.ExpandResetReuse.M Lean.IR.VarId

Equations

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

source

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.

source

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 b => Lean.IR.FnBody.set y i (Array.get! zs i) b) (Array.size zs) b

source

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

Bool

Equations

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

source

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

Bool

Equations

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

source

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

Bool

Equations

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

source

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

Lean.IR.FnBody → Lean.IR.FnBody

source

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

source

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

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

source

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.

source

partial def Lean.IR.ExpandResetReuse.searchAndExpand:

Lean.IR.FnBody → Array Lean.IR.FnBody → Lean.IR.ExpandResetReuse.M Lean.IR.FnBody

source

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.

source

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

Lean.IR.Decl

(Try to) expand reset and reuse instructions.

Equations

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