inductive Lean.Compiler.LCNF.Simp.FunDeclInfo : Type

• once: Lean.Compiler.LCNF.Simp.FunDeclInfo

  Local function is applied once, and must be inlined.

• many: Lean.Compiler.LCNF.Simp.FunDeclInfo

  Local function is applied many times or occur as an argument of another function, and will only be inlined if it is small.

• mustInline: Lean.Compiler.LCNF.Simp.FunDeclInfo

  Function must be inlined.

Local function usage information used to decide whether it should be inlined or not. The information is an approximation, but it is on the "safe" side. That is, if we tagged a function with .once, then it is applied only once. A local function may be marked as .many, but after simplifications the number of applications may reduce to 1. This is not a big problem in practice because we run the simplifier multiple times, and this information is recomputed from scratch at the beginning of each simplification step.

instance Lean.Compiler.LCNF.Simp.instReprFunDeclInfo : Repr Lean.Compiler.LCNF.Simp.FunDeclInfo

instance Lean.Compiler.LCNF.Simp.instInhabitedFunDeclInfo : Inhabited Lean.Compiler.LCNF.Simp.FunDeclInfo

structure Lean.Compiler.LCNF.Simp.FunDeclInfoMap : Type

• map : Lean.HashMap Lean.FVarId Lean.Compiler.LCNF.Simp.FunDeclInfo

  Mapping from local function name to inlining information.

Local function declaration statistics.

instance Lean.Compiler.LCNF.Simp.instInhabitedFunDeclInfoMap : Inhabited Lean.Compiler.LCNF.Simp.FunDeclInfoMap

def Lean.Compiler.LCNF.Simp.FunDeclInfoMap.format (s : Lean.Compiler.LCNF.Simp.FunDeclInfoMap) : Lean.Compiler.LCNF.CompilerM Lean.Format

def Lean.Compiler.LCNF.Simp.FunDeclInfoMap.add (s : Lean.Compiler.LCNF.Simp.FunDeclInfoMap) (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.Simp.FunDeclInfoMap

Add new occurrence for the local function with binder name key.

def Lean.Compiler.LCNF.Simp.FunDeclInfoMap.addHo (s : Lean.Compiler.LCNF.Simp.FunDeclInfoMap) (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.Simp.FunDeclInfoMap

Add new occurrence for the local function occurring as an argument for another function.

def Lean.Compiler.LCNF.Simp.FunDeclInfoMap.addMustInline (s : Lean.Compiler.LCNF.Simp.FunDeclInfoMap) (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.Simp.FunDeclInfoMap

Add new occurrence for the local function with binder name key.

def Lean.Compiler.LCNF.Simp.FunDeclInfoMap.restore (s : Lean.Compiler.LCNF.Simp.FunDeclInfoMap) (fvarId : Lean.FVarId) (saved? : Option Lean.Compiler.LCNF.Simp.FunDeclInfo) : Lean.Compiler.LCNF.Simp.FunDeclInfoMap

def Lean.Compiler.LCNF.Simp.FunDeclInfoMap.update (s : Lean.Compiler.LCNF.Simp.FunDeclInfoMap) (code : Lean.Compiler.LCNF.Code) (mustInline : optParam Bool false) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Simp.FunDeclInfoMap

Traverse code and update function occurrence map. This map is used to decide whether we inline local functions or not. If mustInline := true, then all local function declarations occurring in code are tagged as .mustInline. Recall that we use .mustInline for local function declarations occurring in type class instances.

def Lean.Compiler.LCNF.Simp.FunDeclInfoMap.update.addArgOcc (arg : Lean.Compiler.LCNF.Arg) : StateRefT' IO.RealWorld Lean.Compiler.LCNF.Simp.FunDeclInfoMap Lean.Compiler.LCNF.CompilerM Unit

def Lean.Compiler.LCNF.Simp.FunDeclInfoMap.update.addLetValueOccs (e : Lean.Compiler.LCNF.LetValue) : StateRefT' IO.RealWorld Lean.Compiler.LCNF.Simp.FunDeclInfoMap Lean.Compiler.LCNF.CompilerM Unit

partial def Lean.Compiler.LCNF.Simp.FunDeclInfoMap.update.go (mustInline : optParam Bool false) (code : Lean.Compiler.LCNF.Code) : StateRefT' IO.RealWorld Lean.Compiler.LCNF.Simp.FunDeclInfoMap Lean.Compiler.LCNF.CompilerM Unit