# Documentation

Lean.Compiler.LCNF.CompilerM

The pipeline phase a certain Pass is supposed to happen in.

Instances For
Equations
• A LocalContext to store local declarations from let binders and other constructs in as we move through Exprs.

• Next auxiliary variable suffix

nextIdx : Nat

The state managed by the CompilerM Monad.

Instances For
Equations
Equations
@[inline]
Equations
@[always_inline]
Equations
@[inline]
Equations
• = withReader (fun ctx => { phase := phase, config := ctx.config }) x
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• = let __discr := arg; match __discr with | => | x => pure false
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
@[inline]
Equations
• = modify fun s => { lctx := f s.lctx, nextIdx := s.nextIdx }
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.

Erase all free variables occurring in decls from the local context.

Equations
@[inline]
Equations
@[inline]

A free variable substitution. We use these substitutions when inlining definitions and "internalizing" LCNF code into CompilerM. During the internalization process, we ensure all free variables in the LCNF code do not collide with existing ones at the CompilerM local context. Remark: in LCNF, (computationally relevant) data is in A-normal form, but this is not the case for types and type formers. So, when inlining we often want to replace a free variable with a type or type former.

The substitution contains entries fvarId ↦ e↦ e s.t., e is a valid LCNF argument. That is, it is a free variable, a type (or type former), or lcErased.

Check.lean contains a substitution validator.

Equations
• New free variable.

fvar:
• Free variable has been erased. This can happen when instantiating polymorphic code with computationally irrelant stuff.

erased: Lean.Compiler.LCNF.NormFVarResult

Result type for normFVar and normFVarImp.

Instances For
class Lean.Compiler.LCNF.MonadFVarSubst (m : ) (translator : ) :
• getSubst :

Interface for monads that have a free substitutions.

Instances
instance Lean.Compiler.LCNF.instMonadFVarSubst {t : Bool} (m : ) (n : ) [inst : ] [inst : ] :
Equations
• = { getSubst := liftM Lean.Compiler.LCNF.getSubst }
• modifySubst :
Instances
instance Lean.Compiler.LCNF.instMonadFVarSubstState (m : ) (n : ) [inst : ] [inst : ] :
Equations
• = { modifySubst := fun f => }
@[inline]
def Lean.Compiler.LCNF.addFVarSubst {m : } [inst : ] (fvarId : Lean.FVarId) (fvarId' : Lean.FVarId) :

Add the entry fvarId ↦ fvarId'↦ fvarId' to the free variable substitution.

Equations
@[inline]
def Lean.Compiler.LCNF.addSubst {m : } [inst : ] (fvarId : Lean.FVarId) (e : Lean.Expr) :

Add the substitution fvarId ↦ e↦ e, e must be a valid LCNF argument. That is, it must be a free variable, type (or type former), or lcErased.

See Check.lean for the free variable substitution checker.

Equations
@[inline]
def Lean.Compiler.LCNF.normFVar {m : } {t : Bool} [inst : ] [inst : ] (fvarId : Lean.FVarId) :

Normalize the given free variable. See normExprImp for documentation on the translator parameter. This function is meant to be used in contexts where the input free-variable is computationally relevant. This function panics if the substitution is mapping fvarId to an expression that is not another free variable. That is, it is not a type (or type former), nor lcErased. Recall that a valid FVarSubst contains only expressions that are free variables, lcErased, or type formers.

Equations
@[inline]
def Lean.Compiler.LCNF.normExpr {m : } {t : Bool} [inst : ] [inst : ] (e : Lean.Expr) :

Replace the free variables in e using the given substitution.

If translator = true, then we assume the free variables occurring in the range of the substitution are in another local context. For example, translator = true during internalization where we are making sure all free variables in a given expression are replaced with new ones that do not collide with the ones in the current local context.

If translator = false, we assume the substitution contains free variable replacements in the same local context, and given entries such as x₁ ↦ x₂↦ x₂, x₂ ↦ x₃↦ x₃, ..., xₙ₋₁ ↦ xₙ₋₁ ↦ xₙ↦ xₙ, and the expression f x₁ x₂, we want the resulting expression to be f xₙ xₙ. We use this setting, for example, in the simplifier.

Equations
@[inline]
def Lean.Compiler.LCNF.normArg {m : } {t : Bool} [inst : ] [inst : ] (arg : Lean.Compiler.LCNF.Arg) :

Replace the free variables in arg using the given substitution.

See normExprImp

Equations
@[inline]
def Lean.Compiler.LCNF.normLetValue {m : } {t : Bool} [inst : ] [inst : ] :

Replace the free variables in e using the given substitution.

See normExprImp

Equations
@[inline]

Replace the free variables in e using the given substitution.

If translator = true, then we assume the free variables occurring in the range of the substitution are in another local context. For example, translator = true during internalization where we are making sure all free variables in a given expression are replaced with new ones that do not collide with the ones in the current local context.

If translator = false, we assume the substitution contains free variable replacements in the same local context, and given entries such as x₁ ↦ x₂↦ x₂, x₂ ↦ x₃↦ x₃, ..., xₙ₋₁ ↦ xₙ₋₁ ↦ xₙ↦ xₙ, and the expression f x₁ x₂, we want the resulting expression to be f xₙ xₙ. We use this setting, for example, in the simplifier.

Equations
def Lean.Compiler.LCNF.normArgs {m : } {t : Bool} [inst : ] [inst : ] (args : ) :

Normalize the given arguments using the current substitution.

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

Helper functions for creating LCNF local declarations.

def Lean.Compiler.LCNF.mkParam (binderName : Lean.Name) (type : Lean.Expr) (borrow : Bool) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
def Lean.Compiler.LCNF.mkFunDecl (binderName : Lean.Name) (type : Lean.Expr) (params : ) (value : Lean.Compiler.LCNF.Code) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
@[implemented_by _private.Lean.Compiler.LCNF.CompilerM.0.Lean.Compiler.LCNF.updateParamImp]
@[implemented_by _private.Lean.Compiler.LCNF.CompilerM.0.Lean.Compiler.LCNF.updateLetDeclImp]
Equations
@[implemented_by _private.Lean.Compiler.LCNF.CompilerM.0.Lean.Compiler.LCNF.updateFunDeclImp]
@[inline]
Equations
@[inline]
Equations
@[inline]
def Lean.Compiler.LCNF.normParam {m : } {t : Bool} [inst : ] [inst : ] [inst : ] :
Equations
def Lean.Compiler.LCNF.normParams {m : } {t : Bool} [inst : ] [inst : ] [inst : ] :
Equations
def Lean.Compiler.LCNF.normLetDecl {m : } {t : Bool} [inst : ] [inst : ] [inst : ] (decl : Lean.Compiler.LCNF.LetDecl) :
Equations
• One or more equations did not get rendered due to their size.
@[inline]
abbrev Lean.Compiler.LCNF.NormalizerM (_translator : Bool) (α : Type) :
Equations
Equations
@[inline]
def Lean.Compiler.LCNF.withNormFVarResult {m : TypeType u_1} [inst : ] [inst : ] (result : Lean.Compiler.LCNF.NormFVarResult) (x : ) :

If result is .fvar fvarId, then return x fvarId. Otherwise, it is .erased, and method returns let _x.i := .erased; return _x.i.

Equations
• One or more equations did not get rendered due to their size.
@[inline]
def Lean.Compiler.LCNF.normFunDecl {m : } {t : Bool} [inst : ] [inst : ] [inst : ] (decl : Lean.Compiler.LCNF.FunDecl) :
Equations
@[inline]
def Lean.Compiler.LCNF.normCode {m : } {t : Bool} [inst : ] [inst : ] [inst : ] (code : Lean.Compiler.LCNF.Code) :

Similar to internalize, but does not refresh FVarIds.

Equations
def Lean.Compiler.LCNF.mkAuxParam (type : Lean.Expr) (borrow : ) :
Equations
Equations
def Lean.Compiler.LCNF.CompilerM.run {α : Type} (x : ) (s : optParam Lean.Compiler.LCNF.CompilerM.State { lctx := { params := , letDecls := , funDecls := }, nextIdx := 1 }) :
Equations