inductive Lean.Compiler.LCNF.Phase : Type

• base: Lean.Compiler.LCNF.Phase

  Here we still carry most of the original type information, most of the dependent portion is already (partially) erased though.

• mono: Lean.Compiler.LCNF.Phase

  In this phase polymorphism has been eliminated.

• impure: Lean.Compiler.LCNF.Phase

  In this phase impure stuff such as RC or efficient BaseIO transformations happen.

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

instance Lean.Compiler.LCNF.instInhabitedPhase : Inhabited Lean.Compiler.LCNF.Phase

structure Lean.Compiler.LCNF.CompilerM.State : Type

• lctx : Lean.Compiler.LCNF.LCtx

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

• nextIdx : Nat

  Next auxiliary variable suffix

The state managed by the CompilerM Monad.

instance Lean.Compiler.LCNF.CompilerM.instInhabitedState : Inhabited Lean.Compiler.LCNF.CompilerM.State

structure Lean.Compiler.LCNF.CompilerM.Context : Type

• phase : Lean.Compiler.LCNF.Phase
• config : Lean.Compiler.LCNF.ConfigOptions

instance Lean.Compiler.LCNF.CompilerM.instInhabitedContext : Inhabited Lean.Compiler.LCNF.CompilerM.Context

@[inline, reducible]

abbrev Lean.Compiler.LCNF.CompilerM (α : Type) : Type

@[always_inline]

instance Lean.Compiler.LCNF.instMonadCompilerM : Monad Lean.Compiler.LCNF.CompilerM

@[inline]

def Lean.Compiler.LCNF.withPhase {α : Type} (phase : Lean.Compiler.LCNF.Phase) (x : Lean.Compiler.LCNF.CompilerM α) : Lean.Compiler.LCNF.CompilerM α

def Lean.Compiler.LCNF.getPhase : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Phase

def Lean.Compiler.LCNF.inBasePhase : Lean.Compiler.LCNF.CompilerM Bool

instance Lean.Compiler.LCNF.instAddMessageContextCompilerM : Lean.AddMessageContext Lean.Compiler.LCNF.CompilerM

def Lean.Compiler.LCNF.getType (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.CompilerM Lean.Expr

def Lean.Compiler.LCNF.getBinderName (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.CompilerM Lake.Name

def Lean.Compiler.LCNF.findParam? (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.CompilerM (Option Lean.Compiler.LCNF.Param)

def Lean.Compiler.LCNF.findLetDecl? (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.CompilerM (Option Lean.Compiler.LCNF.LetDecl)

def Lean.Compiler.LCNF.findFunDecl? (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.CompilerM (Option Lean.Compiler.LCNF.FunDecl)

def Lean.Compiler.LCNF.findLetValue? (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.CompilerM (Option Lean.Compiler.LCNF.LetValue)

def Lean.Compiler.LCNF.isConstructorApp (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.CompilerM Bool

def Lean.Compiler.LCNF.Arg.isConstructorApp (arg : Lean.Compiler.LCNF.Arg) : Lean.Compiler.LCNF.CompilerM Bool

def Lean.Compiler.LCNF.getParam (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Param

def Lean.Compiler.LCNF.getLetDecl (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.LetDecl

def Lean.Compiler.LCNF.getFunDecl (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.FunDecl

@[inline]

def Lean.Compiler.LCNF.modifyLCtx (f : Lean.Compiler.LCNF.LCtx → Lean.Compiler.LCNF.LCtx) : Lean.Compiler.LCNF.CompilerM Unit

def Lean.Compiler.LCNF.eraseLetDecl (decl : Lean.Compiler.LCNF.LetDecl) : Lean.Compiler.LCNF.CompilerM Unit

def Lean.Compiler.LCNF.eraseFunDecl (decl : Lean.Compiler.LCNF.FunDecl) (recursive : optParam Bool true) : Lean.Compiler.LCNF.CompilerM Unit

def Lean.Compiler.LCNF.eraseCode (code : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.CompilerM Unit

def Lean.Compiler.LCNF.eraseParam (param : Lean.Compiler.LCNF.Param) : Lean.Compiler.LCNF.CompilerM Unit

def Lean.Compiler.LCNF.eraseParams (params : Array Lean.Compiler.LCNF.Param) : Lean.Compiler.LCNF.CompilerM Unit

def Lean.Compiler.LCNF.eraseCodeDecl (decl : Lean.Compiler.LCNF.CodeDecl) : Lean.Compiler.LCNF.CompilerM Unit

def Lean.Compiler.LCNF.eraseCodeDecls (decls : Array Lean.Compiler.LCNF.CodeDecl) : Lean.Compiler.LCNF.CompilerM Unit

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

def Lean.Compiler.LCNF.eraseDecl (decl : Lean.Compiler.LCNF.Decl) : Lean.Compiler.LCNF.CompilerM Unit

@[inline, reducible]

abbrev Lean.Compiler.LCNF.Decl.erase (decl : Lean.Compiler.LCNF.Decl) : Lean.Compiler.LCNF.CompilerM Unit

@[inline, reducible]

abbrev Lean.Compiler.LCNF.FVarSubst : Type

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

inductive Lean.Compiler.LCNF.NormFVarResult : Type

• fvar: Lean.FVarId → Lean.Compiler.LCNF.NormFVarResult

  New free variable.

• erased: Lean.Compiler.LCNF.NormFVarResult

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

Result type for normFVar and normFVarImp.

instance Lean.Compiler.LCNF.instInhabitedNormFVarResult : Inhabited Lean.Compiler.LCNF.NormFVarResult

class Lean.Compiler.LCNF.MonadFVarSubst (m : Type → Type) (translator : outParam Bool) : Type

• getSubst : m Lean.Compiler.LCNF.FVarSubst

Interface for monads that have a free substitutions.

instance Lean.Compiler.LCNF.instMonadFVarSubst {t : Bool} (m : Type → Type) (n : Type → Type) [MonadLift m n] [Lean.Compiler.LCNF.MonadFVarSubst m t] : Lean.Compiler.LCNF.MonadFVarSubst n t

class Lean.Compiler.LCNF.MonadFVarSubstState (m : Type → Type) : Type

• modifySubst : (Lean.Compiler.LCNF.FVarSubst → Lean.Compiler.LCNF.FVarSubst) → m Unit

instance Lean.Compiler.LCNF.instMonadFVarSubstState (m : Type → Type) (n : Type → Type) [MonadLift m n] [Lean.Compiler.LCNF.MonadFVarSubstState m] : Lean.Compiler.LCNF.MonadFVarSubstState n

@[inline]

def Lean.Compiler.LCNF.addFVarSubst {m : Type → Type} [Lean.Compiler.LCNF.MonadFVarSubstState m] (fvarId : Lean.FVarId) (fvarId' : Lean.FVarId) : m Unit

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

@[inline]

def Lean.Compiler.LCNF.addSubst {m : Type → Type} [Lean.Compiler.LCNF.MonadFVarSubstState m] (fvarId : Lean.FVarId) (e : Lean.Expr) : m Unit

Add the substitution fvarId ↦ 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.

@[inline]

def Lean.Compiler.LCNF.normFVar {m : Type → Type} {t : Bool} [Lean.Compiler.LCNF.MonadFVarSubst m t] [Monad m] (fvarId : Lean.FVarId) : m Lean.Compiler.LCNF.NormFVarResult

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.

@[inline]

def Lean.Compiler.LCNF.normExpr {m : Type → Type} {t : Bool} [Lean.Compiler.LCNF.MonadFVarSubst m t] [Monad m] (e : Lean.Expr) : m 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ₙ, 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.

@[inline]

def Lean.Compiler.LCNF.normArg {m : Type → Type} {t : Bool} [Lean.Compiler.LCNF.MonadFVarSubst m t] [Monad m] (arg : Lean.Compiler.LCNF.Arg) : m Lean.Compiler.LCNF.Arg

Replace the free variables in arg using the given substitution.

See normExprImp

@[inline]

def Lean.Compiler.LCNF.normLetValue {m : Type → Type} {t : Bool} [Lean.Compiler.LCNF.MonadFVarSubst m t] [Monad m] (e : Lean.Compiler.LCNF.LetValue) : m Lean.Compiler.LCNF.LetValue

Replace the free variables in e using the given substitution.

See normExprImp

@[inline, reducible]

abbrev Lean.Compiler.LCNF.normExprCore (s : Lean.Compiler.LCNF.FVarSubst) (e : Lean.Expr) (translator : Bool) : 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ₙ, 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.

def Lean.Compiler.LCNF.normArgs {m : Type → Type} {t : Bool} [Lean.Compiler.LCNF.MonadFVarSubst m t] [Monad m] (args : Array Lean.Compiler.LCNF.Arg) : m (Array Lean.Compiler.LCNF.Arg)

Normalize the given arguments using the current substitution.

def Lean.Compiler.LCNF.mkFreshBinderName (binderName : optParam Lake.Name `_x) : Lean.Compiler.LCNF.CompilerM Lake.Name

def Lean.Compiler.LCNF.ensureNotAnonymous (binderName : Lake.Name) (baseName : Lake.Name) : Lean.Compiler.LCNF.CompilerM Lake.Name

Helper functions for creating LCNF local declarations.

def Lean.Compiler.LCNF.mkParam (binderName : Lake.Name) (type : Lean.Expr) (borrow : Bool) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Param

def Lean.Compiler.LCNF.mkLetDecl (binderName : Lake.Name) (type : Lean.Expr) (value : Lean.Compiler.LCNF.LetValue) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.LetDecl

def Lean.Compiler.LCNF.mkFunDecl (binderName : Lake.Name) (type : Lean.Expr) (params : Array Lean.Compiler.LCNF.Param) (value : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.FunDecl

def Lean.Compiler.LCNF.mkLetDeclErased : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.LetDecl

def Lean.Compiler.LCNF.mkReturnErased : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Code

@[implemented_by _private.Lean.Compiler.LCNF.CompilerM.0.Lean.Compiler.LCNF.updateParamImp]

opaque Lean.Compiler.LCNF.Param.update (p : Lean.Compiler.LCNF.Param) (type : Lean.Expr) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Param

@[implemented_by _private.Lean.Compiler.LCNF.CompilerM.0.Lean.Compiler.LCNF.updateLetDeclImp]

opaque Lean.Compiler.LCNF.LetDecl.update (decl : Lean.Compiler.LCNF.LetDecl) (type : Lean.Expr) (value : Lean.Compiler.LCNF.LetValue) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.LetDecl

def Lean.Compiler.LCNF.LetDecl.updateValue (decl : Lean.Compiler.LCNF.LetDecl) (value : Lean.Compiler.LCNF.LetValue) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.LetDecl

@[implemented_by _private.Lean.Compiler.LCNF.CompilerM.0.Lean.Compiler.LCNF.updateFunDeclImp]

opaque Lean.Compiler.LCNF.FunDeclCore.update (decl : Lean.Compiler.LCNF.FunDecl) (type : Lean.Expr) (params : Array Lean.Compiler.LCNF.Param) (value : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.FunDecl

@[inline, reducible]

abbrev Lean.Compiler.LCNF.FunDeclCore.update' (decl : Lean.Compiler.LCNF.FunDecl) (type : Lean.Expr) (value : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.FunDecl

@[inline, reducible]

abbrev Lean.Compiler.LCNF.FunDeclCore.updateValue (decl : Lean.Compiler.LCNF.FunDecl) (value : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.FunDecl

@[inline]

def Lean.Compiler.LCNF.normParam {m : Type → Type} {t : Bool} [MonadLiftT Lean.Compiler.LCNF.CompilerM m] [Monad m] [Lean.Compiler.LCNF.MonadFVarSubst m t] (p : Lean.Compiler.LCNF.Param) : m Lean.Compiler.LCNF.Param

def Lean.Compiler.LCNF.normParams {m : Type → Type} {t : Bool} [MonadLiftT Lean.Compiler.LCNF.CompilerM m] [Monad m] [Lean.Compiler.LCNF.MonadFVarSubst m t] (ps : Array Lean.Compiler.LCNF.Param) : m (Array Lean.Compiler.LCNF.Param)

def Lean.Compiler.LCNF.normLetDecl {m : Type → Type} {t : Bool} [MonadLiftT Lean.Compiler.LCNF.CompilerM m] [Monad m] [Lean.Compiler.LCNF.MonadFVarSubst m t] (decl : Lean.Compiler.LCNF.LetDecl) : m Lean.Compiler.LCNF.LetDecl

@[inline, reducible]

abbrev Lean.Compiler.LCNF.NormalizerM (_translator : Bool) (α : Type) : Type

instance Lean.Compiler.LCNF.instMonadFVarSubstNormalizerM {t : Bool} : Lean.Compiler.LCNF.MonadFVarSubst (Lean.Compiler.LCNF.NormalizerM t) t

@[inline]

def Lean.Compiler.LCNF.withNormFVarResult {m : Type → Type u_1} [MonadLiftT Lean.Compiler.LCNF.CompilerM m] [Monad m] (result : Lean.Compiler.LCNF.NormFVarResult) (x : Lean.FVarId → m Lean.Compiler.LCNF.Code) : m Lean.Compiler.LCNF.Code

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

partial def Lean.Compiler.LCNF.normFunDeclImp {t : Bool} (decl : Lean.Compiler.LCNF.FunDecl) : Lean.Compiler.LCNF.NormalizerM t Lean.Compiler.LCNF.FunDecl

partial def Lean.Compiler.LCNF.normCodeImp {t : Bool} (code : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.NormalizerM t Lean.Compiler.LCNF.Code

@[inline]

def Lean.Compiler.LCNF.normFunDecl {m : Type → Type} {t : Bool} [MonadLiftT Lean.Compiler.LCNF.CompilerM m] [Monad m] [Lean.Compiler.LCNF.MonadFVarSubst m t] (decl : Lean.Compiler.LCNF.FunDecl) : m Lean.Compiler.LCNF.FunDecl

@[inline]

def Lean.Compiler.LCNF.normCode {m : Type → Type} {t : Bool} [MonadLiftT Lean.Compiler.LCNF.CompilerM m] [Monad m] [Lean.Compiler.LCNF.MonadFVarSubst m t] (code : Lean.Compiler.LCNF.Code) : m Lean.Compiler.LCNF.Code

Similar to internalize, but does not refresh FVarIds.

def Lean.Compiler.LCNF.replaceExprFVars (e : Lean.Expr) (s : Lean.Compiler.LCNF.FVarSubst) (translator : Bool) : Lean.Compiler.LCNF.CompilerM Lean.Expr

def Lean.Compiler.LCNF.replaceFVars (code : Lean.Compiler.LCNF.Code) (s : Lean.Compiler.LCNF.FVarSubst) (translator : Bool) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Code

def Lean.Compiler.LCNF.mkFreshJpName : Lean.Compiler.LCNF.CompilerM Lake.Name

def Lean.Compiler.LCNF.mkAuxParam (type : Lean.Expr) (borrow : optParam Bool false) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Param

def Lean.Compiler.LCNF.getConfig : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.ConfigOptions

def Lean.Compiler.LCNF.CompilerM.run {α : Type} (x : Lean.Compiler.LCNF.CompilerM α) (s : optParam Lean.Compiler.LCNF.CompilerM.State { lctx := { params := ∅, letDecls := ∅, funDecls := ∅ }, nextIdx := 1 }) (phase : optParam Lean.Compiler.LCNF.Phase Lean.Compiler.LCNF.Phase.base) : Lean.CoreM α