- declName : Lake.NameName 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. 
- inlineStackOccs : Lean.PHashMap Lake.Name NatMapping from declaration names to number of occurrences at inlineStack
Instances For
- subst : Lean.Compiler.LCNF.FVarSubstFree 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.RenamingMapping 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.FunDeclInfoMapMapping used to decide whether a local function declaration must be inlined or not. 
- simplified : Booltrueif some simplification was performed in the current simplification pass.
- visited : NatNumber of visited let-declarationsand terminal values. This is a performance counter, and currently has no impact on code generation.
- inline : NatNumber of definitions inlined. This is a performance counter. 
- inlineLocal : NatNumber of local functions inlined. This is a performance counter. 
Instances For
Set the simplified flag to true.
Instances For
Increment visited performance counter.
Instances For
Increment inline performance counter. It is the number of inlined global declarations.
Instances For
Increment inlineLocal performance counter. It is the number of inlined local function and join point declarations.
Instances For
Mark the local function declaration or join point with the given id as a "must inline".
Instances For
Add a new occurrence of local function fvarId.
Instances For
Add a new occurrence of local function fvarId in argument position .
Instances For
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.
Instances For
Execute x with an updated inlineStack. If value is of the form const ..., add const to the stack.
Otherwise, do not change the inlineStack.
Instances For
Instances For
Similar to the default Lean.withIncRecDepth, but include the inlineStack in the error messsage.
Instances For
Instances For
Execute x with fvarId set as mustInline.
After execution the original setting is restored.
Instances For
Return true if the given local function declaration or join point id is marked as
once or mustInline. We use this information to decide whether to inline them.
Instances For
Return true if the given code is considered "small".
Instances For
Return true if the given local function declaration should be inlined.
Instances For
LCNF "Beta-reduce". The equivalent of (fun params => code) args.
If mustInline is true, the local function declarations in the resulting code are marked as .mustInline.
See comment at updateFunDeclInfo.
Instances For
Erase the given let-declaration from the local context,
and set the simplified flag to true.
Instances For
Erase the given local function declaration from the local context,
and set the simplified flag to true.
Instances For
Similar to LCNF.addFVarSubst. That is, add the entry
fvarId ↦ fvarId' to the free variable substitution.
If fvarId has a non-internal binder name n, but fvarId' does not,
this method also adds the entry fvarId' ↦ n to the binderRenaming map.
The goal is to preserve user provided names.