This module contains a pass for propagating user provided borrows as far forward in the function as possible. This analysis is used to inform the reset-reuse insertion as to avoid inserting reset-reuse on values that the user explicitly requested to be borrowed.

inductive Lean.Compiler.LCNF.Ownedness : Type

• bot : Ownedness
• borrow : Ownedness
• own : Ownedness
• top : Ownedness

def Lean.Compiler.LCNF.instInhabitedOwnedness.default : Ownedness

Equations

• Lean.Compiler.LCNF.instInhabitedOwnedness.default = Lean.Compiler.LCNF.Ownedness.bot

@[implicit_reducible]

instance Lean.Compiler.LCNF.instInhabitedOwnedness : Inhabited Ownedness

Equations

• Lean.Compiler.LCNF.instInhabitedOwnedness = { default := Lean.Compiler.LCNF.instInhabitedOwnedness.default }

@[implicit_reducible]

instance Lean.Compiler.LCNF.instBEqOwnedness : BEq Ownedness

Equations

• Lean.Compiler.LCNF.instBEqOwnedness = { beq := Lean.Compiler.LCNF.instBEqOwnedness.beq }

def Lean.Compiler.LCNF.instBEqOwnedness.beq : Ownedness → Ownedness → Bool

Equations

• Lean.Compiler.LCNF.instBEqOwnedness.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Lean.Compiler.LCNF.Decl.analyzePropagatedBorrows (decl : Decl Purity.impure) : CompilerM (Std.HashMap FVarId Ownedness)

Equations

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

def Lean.Compiler.LCNF.Decl.applyOwnedness (decl : Decl Purity.impure) (values : Std.HashMap FVarId Ownedness) : CompilerM (Decl Purity.impure)

Equations

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