source
structure Lean.Compiler.LCNF.Simp.Context :
Type

- declName : 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 : Config
- inlineStack : List Name

  Stack of global declarations being recursively inlined.

- inlineStackOccs : PHashMap Name Nat

  Mapping from declaration names to number of occurrences at `inlineStack`

Instances For

source
structure Lean.Compiler.LCNF.Simp.State :
Type

- subst : FVarSubst

  Free variable substitution. We use it to implement inlining and removing redundant variables `let _x.i := _x.j`

- used : UsedLocalDecls

  Track used local declarations to be able to eliminate dead variables.

- binderRenaming : 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 : FunDeclInfoMap

  Mapping used to decide whether a local function declaration must be inlined or not.

- simplified : Bool

  `true` if some simplification was performed in the current simplification pass.

- visited : Nat

  Number of visited `let-declarations` and 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.

Instances For

source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.Simp.SimpM (α : Type) :
Type
Equations

- Lean.Compiler.LCNF.Simp.SimpM = ReaderT Lean.Compiler.LCNF.Simp.Context (StateRefT' IO.RealWorld Lean.Compiler.LCNF.Simp.State Lean.Compiler.LCNF.Simp.DiscrM)

Instances For

source
@[always_inline]
instance Lean.Compiler.LCNF.Simp.instMonadSimpM :
Monad SimpM
Equations

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

source
instance Lean.Compiler.LCNF.Simp.instMonadFVarSubstSimpMFalse :
MonadFVarSubst SimpM false
Equations

- Lean.Compiler.LCNF.Simp.instMonadFVarSubstSimpMFalse = { getSubst := do let __do_lift ← get pure __do_lift.subst }

source
instance Lean.Compiler.LCNF.Simp.instMonadFVarSubstStateSimpM :
MonadFVarSubstState SimpM
Equations

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

source
def Lean.Compiler.LCNF.Simp.markSimplified :
SimpM Unit

Set the `simplified` flag to `true`.

Equations

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

Instances For

source
def Lean.Compiler.LCNF.Simp.incVisited :
SimpM Unit

Increment `visited` performance counter.

Equations

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

Instances For

source
def Lean.Compiler.LCNF.Simp.incInline :
SimpM Unit

Increment `inline` performance counter. It is the number of inlined global declarations.

Equations

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

Instances For

source
def Lean.Compiler.LCNF.Simp.incInlineLocal :
SimpM Unit

Increment `inlineLocal` performance counter. It is the number of inlined local function and join point declarations.

Equations

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

Instances For

source
def Lean.Compiler.LCNF.Simp.addMustInline (fvarId : FVarId) :
SimpM Unit

Mark the local function declaration or join point with the given id as a "must inline".

Equations

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

Instances For

source
def Lean.Compiler.LCNF.Simp.addFunOcc (fvarId : FVarId) :
SimpM Unit

Add a new occurrence of local function `fvarId`.

Equations

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

Instances For

source
def Lean.Compiler.LCNF.Simp.addFunHoOcc (fvarId : FVarId) :
SimpM Unit

Add a new occurrence of local function `fvarId` in argument position .

Equations

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

Instances For

source
def Lean.Compiler.LCNF.Simp.updateFunDeclInfo (code : Code) (mustInline : Bool := false) :
SimpM Unit

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

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

Instances For

source
@[inline]
def Lean.Compiler.LCNF.Simp.withInlining {α : Type} (value : LetValue) (recursive : Bool) (x : SimpM α) :
SimpM α

Execute `x` with an updated `inlineStack`. If `value` is of the form `const ...`, add `const` to the stack. Otherwise, do not change the `inlineStack`.

Equations

- One or more equations did not get rendered due to their size.
- Lean.Compiler.LCNF.Simp.withInlining value recursive x = x

Instances For

source
@[inline]
def Lean.Compiler.LCNF.Simp.withIncRecDepth {α : Type} (x : SimpM α) :
SimpM α

Similar to the default `Lean.withIncRecDepth`, but include the `inlineStack` in the error message.

Equations

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

Instances For

source
def Lean.Compiler.LCNF.Simp.withAddMustInline {α : Type} (fvarId : FVarId) (x : SimpM α) :
SimpM α

Execute `x` with `fvarId` set as `mustInline`. After execution the original setting is restored.

Equations

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

Instances For

source
def Lean.Compiler.LCNF.Simp.isOnceOrMustInline (fvarId : FVarId) :
SimpM Bool

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.

Equations

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

Instances For

source
def Lean.Compiler.LCNF.Simp.isSmall (code : Code) :
SimpM Bool

Return `true` if the given code is considered "small".

Equations

- Lean.Compiler.LCNF.Simp.isSmall code = do let __do_lift ← liftM Lean.Compiler.LCNF.getConfig pure (code.sizeLe __do_lift.smallThreshold)

Instances For

source
def Lean.Compiler.LCNF.Simp.shouldInlineLocal (decl : FunDecl) :
SimpM Bool

Return `true` if the given local function declaration should be inlined.

Equations

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

Instances For

source
def Lean.Compiler.LCNF.Simp.betaReduce (params : Array Param) (code : Code) (args : Array Arg) (mustInline : Bool := false) :
SimpM Code

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

Equations

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

Instances For

source
def Lean.Compiler.LCNF.Simp.eraseLetDecl (decl : LetDecl) :
SimpM Unit

Erase the given let-declaration from the local context, and set the `simplified` flag to true.

Equations

- Lean.Compiler.LCNF.Simp.eraseLetDecl decl = do liftM (Lean.Compiler.LCNF.eraseLetDecl decl) Lean.Compiler.LCNF.Simp.markSimplified

Instances For

source
def Lean.Compiler.LCNF.Simp.eraseFunDecl (decl : FunDecl) :
SimpM Unit

Erase the given local function declaration from the local context, and set the `simplified` flag to true.

Equations

- Lean.Compiler.LCNF.Simp.eraseFunDecl decl = do liftM (Lean.Compiler.LCNF.eraseFunDecl decl) Lean.Compiler.LCNF.Simp.markSimplified

Instances For

source
def Lean.Compiler.LCNF.Simp.addFVarSubst (fvarId fvarId' : FVarId) :
SimpM Unit

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.

Equations

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

Instances For