- 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.
Add new occurrence for the local function with binder name
code and update function occurrence map.
This map is used to decide whether we inline local functions or not.
mustInline := true, then all local function declarations occurring in
code are tagged as
Recall that we use
.mustInline for local function declarations occurring in type class instances.