@[reducible, inline]

abbrev Lean.Compiler.LCNF.ExtractClosed.ExtractM (α : Type) : Type

Equations

• Lean.Compiler.LCNF.ExtractClosed.ExtractM = StateRefT' IO.RealWorld (Array (Lean.Compiler.LCNF.CodeDecl Lean.Compiler.LCNF.Purity.pure)) Lean.Compiler.LCNF.CompilerM

partial def Lean.Compiler.LCNF.ExtractClosed.extractLetValue (v : LetValue Purity.pure) : ExtractM Unit

partial def Lean.Compiler.LCNF.ExtractClosed.extractArg (arg : Arg Purity.pure) : ExtractM Unit

partial def Lean.Compiler.LCNF.ExtractClosed.extractFVar (fvarId : FVarId) : ExtractM Unit

def Lean.Compiler.LCNF.ExtractClosed.isIrrelevantArg (arg : Arg Purity.pure) : Bool

Equations

• Lean.Compiler.LCNF.ExtractClosed.isIrrelevantArg Lean.Compiler.LCNF.Arg.erased = true
• Lean.Compiler.LCNF.ExtractClosed.isIrrelevantArg (Lean.Compiler.LCNF.Arg.type expr ⋯) = true
• Lean.Compiler.LCNF.ExtractClosed.isIrrelevantArg (Lean.Compiler.LCNF.Arg.fvar fvarId) = false

structure Lean.Compiler.LCNF.ExtractClosed.Context : Type

• baseName : Name
• sccDecls : Array (Decl Purity.pure)

structure Lean.Compiler.LCNF.ExtractClosed.State : Type

• decls : Array (Decl Purity.pure)
• fvarDecisionCache : Std.HashMap FVarId Bool

  Cache for shouldExtractFVar in order to avoid superlinear behavior.

@[reducible, inline]

abbrev Lean.Compiler.LCNF.ExtractClosed.M (α : Type) : Type

Equations

• Lean.Compiler.LCNF.ExtractClosed.M = ReaderT Lean.Compiler.LCNF.ExtractClosed.Context (StateRefT' IO.RealWorld Lean.Compiler.LCNF.ExtractClosed.State Lean.Compiler.LCNF.CompilerM)

partial def Lean.Compiler.LCNF.ExtractClosed.shouldExtractLetValue (isRoot : Bool) (v : LetValue Purity.pure) : M Bool

partial def Lean.Compiler.LCNF.ExtractClosed.shouldExtractArg (arg : Arg Purity.pure) : M Bool

partial def Lean.Compiler.LCNF.ExtractClosed.shouldExtractFVar (fvarId : FVarId) : M Bool

def Lean.Compiler.LCNF.ExtractClosed.searchArrayLiteral (decl : LetDecl Purity.pure) (k : Code Purity.pure) : M (Option (LetDecl Purity.pure × Code Purity.pure))

Check if let decl; k forms an Array, ByteArray, or FloatArray literal. They consist of some initial allocation (Array.mkEmpty or Array.emptyWithCapacity) followed by a sequence of Array.push and for the scalar variants finally ByteArray.mk or FloatArray.mk.

We identify these literals by matching this pattern and ensuring that only the last push/mk from the sequence is used in the final continuation. If that is the case, we can pull out the entire literal as one closed declaration. This avoids the quadratic overhead of repeated Array.push calls on persistent Array objects during initialization.

Equations

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

partial def Lean.Compiler.LCNF.ExtractClosed.visitCode (code : Code Purity.pure) : M (Code Purity.pure)

def Lean.Compiler.LCNF.ExtractClosed.visitDecl (decl : Decl Purity.pure) : M (Decl Purity.pure)

Equations

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

def Lean.Compiler.LCNF.Decl.extractClosed (decl : Decl Purity.pure) (sccDecls : Array (Decl Purity.pure)) : CompilerM (Array (Decl Purity.pure))

Equations

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

def Lean.Compiler.LCNF.extractClosed : Pass

Equations

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