@[reducible, inline]

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

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

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

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.

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)

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

def Lean.Compiler.LCNF.extractClosed : Pass