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

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.

• 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.

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

Equations

• Lean.Compiler.LCNF.Simp.instReprFunDeclInfo = { reprPrec := Lean.Compiler.LCNF.Simp.reprFunDeclInfo✝ }

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

Equations

• Lean.Compiler.LCNF.Simp.instInhabitedFunDeclInfo = { default := Lean.Compiler.LCNF.Simp.FunDeclInfo.once }

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

Local function declaration statistics.

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

  Mapping from local function name to inlining information.

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

Equations

• Lean.Compiler.LCNF.Simp.instInhabitedFunDeclInfoMap = { default := { map := default } }

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

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

• { map := map }.addMustInline fvarId = { map := map.insert fvarId Lean.Compiler.LCNF.Simp.FunDeclInfo.mustInline }

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

Equations

• { map := map }.restore fvarId none = { map := map.erase fvarId }
• { map := map }.restore fvarId (some saved) = { map := map.insert fvarId saved }

def Lean.Compiler.LCNF.Simp.FunDeclInfoMap.update (s : Lean.Compiler.LCNF.Simp.FunDeclInfoMap) (code : Lean.Compiler.LCNF.Code) (mustInline : 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.

Equations

• s.update code mustInline = do let __discr ← (Lean.Compiler.LCNF.Simp.FunDeclInfoMap.update.go mustInline code).run s match __discr with | (fst, s) => pure s

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.Simp.FunDeclInfoMap.update.addArgOcc Lean.Compiler.LCNF.Arg.erased = pure ()
• Lean.Compiler.LCNF.Simp.FunDeclInfoMap.update.addArgOcc (Lean.Compiler.LCNF.Arg.type expr) = pure ()

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.Simp.FunDeclInfoMap.update.addLetValueOccs Lean.Compiler.LCNF.LetValue.erased = pure ()
• Lean.Compiler.LCNF.Simp.FunDeclInfoMap.update.addLetValueOccs (Lean.Compiler.LCNF.LetValue.value value) = pure ()
• Lean.Compiler.LCNF.Simp.FunDeclInfoMap.update.addLetValueOccs (Lean.Compiler.LCNF.LetValue.proj typeName idx struct) = pure ()
• Lean.Compiler.LCNF.Simp.FunDeclInfoMap.update.addLetValueOccs (Lean.Compiler.LCNF.LetValue.const declName us args) = Array.forM Lean.Compiler.LCNF.Simp.FunDeclInfoMap.update.addArgOcc args

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