- declName : Lake.Name
Name of the declaration being simplified. We currently use this information because we are generating phase1 declarations on demand, and it may trigger non-termination when trying to access the phase1 declaration.
- config : Lean.Compiler.LCNF.Simp.Config
Stack of global declarations being recursively inlined.
Mapping from declaration names to number of occurrences at
- subst : Lean.Compiler.LCNF.FVarSubst
Free variable substitution. We use it to implement inlining and removing redundant variables
let _x.i := _x.j
Track used local declarations to be able to eliminate dead variables.
- binderRenaming : Lean.Compiler.LCNF.Renaming
Mapping containing free variables ids that need to be renamed (i.e., the
binderName). We use this map to preserve user provide names.
- funDeclInfoMap : Lean.Compiler.LCNF.Simp.FunDeclInfoMap
Mapping used to decide whether a local function declaration must be inlined or not.
- simplified : Bool
trueif some simplification was performed in the current simplification pass.
- visited : Nat
Number of visited
let-declarationsand terminal values. This is a performance counter, and currently has no impact on code generation.
- inline : Nat
Number of definitions inlined. This is a performance counter.
- inlineLocal : Nat
Number of local functions inlined. This is a performance counter.
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.
LCNF "Beta-reduce". The equivalent of
(fun params => code) args.
mustInline is true, the local function declarations in the resulting code are marked as
See comment at
LCNF.addFVarSubst. That is, add the entry
fvarId ↦ fvarId' to the free variable substitution.
fvarId has a non-internal binder name
fvarId' does not,
this method also adds the entry
fvarId' ↦ n to the
The goal is to preserve user provided names.