inductive Lean.Compiler.LCNF.Phase : Type

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

• base : Phase

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

• mono : Phase

  In this phase polymorphism has been eliminated.

• impure : Phase

@[implicit_reducible]

instance Lean.Compiler.LCNF.instInhabitedPhase : Inhabited Phase

def Lean.Compiler.LCNF.instInhabitedPhase.default : Phase

@[implicit_reducible]

instance Lean.Compiler.LCNF.instDecidableEqPhase : DecidableEq Phase

@[reducible]

def Lean.Compiler.LCNF.Phase.toPurity : Phase → Purity

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

The state managed by the CompilerM Monad.

• lctx : 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

def Lean.Compiler.LCNF.CompilerM.instInhabitedState.default : State

@[implicit_reducible]

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

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

• phase : Phase
• config : ConfigOptions

def Lean.Compiler.LCNF.CompilerM.instInhabitedContext.default : Context

@[implicit_reducible]

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

@[reducible, inline]

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

@[implicit_reducible, always_inline]

instance Lean.Compiler.LCNF.instMonadCompilerM : Monad CompilerM

@[inline]

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

def Lean.Compiler.LCNF.getPhase : CompilerM Phase

def Lean.Compiler.LCNF.getPurity : CompilerM Purity

def Lean.Compiler.LCNF.inBasePhase : CompilerM Bool

@[implicit_reducible]

instance Lean.Compiler.LCNF.instAddMessageContextCompilerM : AddMessageContext CompilerM

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

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

def Lean.Compiler.LCNF.findParam? {pu : Purity} (fvarId : FVarId) : CompilerM (Option (Param pu))

def Lean.Compiler.LCNF.findLetDecl? {pu : Purity} (fvarId : FVarId) : CompilerM (Option (LetDecl pu))

def Lean.Compiler.LCNF.findFunDecl? {pu : Purity} (fvarId : FVarId) : CompilerM (Option (FunDecl pu))

def Lean.Compiler.LCNF.findLetValue? {pu : Purity} (fvarId : FVarId) : CompilerM (Option (LetValue pu))

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

def Lean.Compiler.LCNF.Arg.isConstructorApp {pu : Purity} (arg : Arg pu) : CompilerM Bool

def Lean.Compiler.LCNF.getParam {pu : Purity} (fvarId : FVarId) : CompilerM (Param pu)

def Lean.Compiler.LCNF.getLetDecl {pu : Purity} (fvarId : FVarId) : CompilerM (LetDecl pu)

def Lean.Compiler.LCNF.getFunDecl {pu : Purity} (fvarId : FVarId) : CompilerM (FunDecl pu)

@[inline]

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

def Lean.Compiler.LCNF.eraseLetDecl {pu : Purity} (decl : LetDecl pu) : CompilerM Unit

def Lean.Compiler.LCNF.eraseFunDecl {pu : Purity} (decl : FunDecl pu) (recursive : Bool := true) : CompilerM Unit

def Lean.Compiler.LCNF.eraseCode {pu : Purity} (code : Code pu) : CompilerM Unit

def Lean.Compiler.LCNF.eraseParam {pu : Purity} (param : Param pu) : CompilerM Unit

def Lean.Compiler.LCNF.eraseParams {pu : Purity} (params : Array (Param pu)) : CompilerM Unit

def Lean.Compiler.LCNF.eraseCodeDecl {pu : Purity} (decl : CodeDecl pu) : CompilerM Unit

def Lean.Compiler.LCNF.eraseCodeDecls {pu : Purity} (decls : Array (CodeDecl pu)) : CompilerM Unit

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

def Lean.Compiler.LCNF.eraseDecl {pu : Purity} (decl : Decl pu) : CompilerM Unit

@[reducible, inline]

abbrev Lean.Compiler.LCNF.Decl.erase {pu : Purity} (decl : Decl pu) : CompilerM Unit

@[reducible, inline]

abbrev Lean.Compiler.LCNF.FVarSubst (pu : Purity) : 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

Result type for normFVar and normFVarImp.

• fvar (fvarId : FVarId) : NormFVarResult

  New free variable.

• erased : NormFVarResult

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

@[implicit_reducible]

instance Lean.Compiler.LCNF.instInhabitedNormFVarResult : Inhabited NormFVarResult

def Lean.Compiler.LCNF.instInhabitedNormFVarResult.default : NormFVarResult

partial def Lean.Compiler.LCNF.normFVarImp {pu : Purity} (s : FVarSubst pu) (fvarId : FVarId) (translator : Bool) : 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.

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

Interface for monads that have a free substitutions.

• getSubst : m (FVarSubst pu)

@[implicit_reducible]

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

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

• modifySubst : (FVarSubst pu → FVarSubst pu) → m Unit

@[implicit_reducible]

instance Lean.Compiler.LCNF.instMonadFVarSubstStateOfMonadLift {pu : Purity} (m n : Type → Type) [MonadLift m n] [MonadFVarSubstState m pu] : MonadFVarSubstState n pu

@[inline]

def Lean.Compiler.LCNF.addSubst {m : Type → Type} {pu : Purity} [MonadFVarSubstState m pu] (fvarId : FVarId) (arg : Arg pu) : m Unit

Add the substitution fvarId ↦ e, e must be a valid LCNF Arg.

See Check.lean for the free variable substitution checker.

@[inline]

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

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

@[inline]

def Lean.Compiler.LCNF.normFVar {m : Type → Type} {pu : Purity} {t : Bool} [MonadFVarSubst m pu t] [Monad m] (fvarId : FVarId) : m 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} {pu : Purity} {t : Bool} [MonadFVarSubst m pu t] [Monad m] (e : Expr) : m 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} {pu : Purity} {t : Bool} [MonadFVarSubst m pu t] [Monad m] (arg : Arg pu) : m (Arg pu)

Replace the free variables in arg using the given substitution.

See normExprImp

@[inline]

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

Replace the free variables in e using the given substitution.

See normExprImp

@[inline]

def Lean.Compiler.LCNF.normExprCore {pu : Purity} (s : FVarSubst pu) (e : Expr) (translator : Bool) : 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} {pu : Purity} {t : Bool} [MonadFVarSubst m pu t] [Monad m] (args : Array (Arg pu)) : m (Array (Arg pu))

Normalize the given arguments using the current substitution.

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

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

Helper functions for creating LCNF local declarations.

def Lean.Compiler.LCNF.mkParam {pu : Purity} (binderName : Name) (type : Expr) (borrow : Bool) : CompilerM (Param pu)

def Lean.Compiler.LCNF.mkLetDecl {pu : Purity} (binderName : Name) (type : Expr) (value : LetValue pu) : CompilerM (LetDecl pu)

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

def Lean.Compiler.LCNF.mkLetDeclErased {pu : Purity} : CompilerM (LetDecl pu)

def Lean.Compiler.LCNF.mkReturnErased {pu : Purity} : CompilerM (Code pu)

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

opaque Lean.Compiler.LCNF.Param.update {pu : Purity} (p : Param pu) (type : Expr) : CompilerM (Param pu)

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

opaque Lean.Compiler.LCNF.Param.updateBorrow {pu : Purity} (p : Param pu) (borrow : Bool) : CompilerM (Param pu)

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

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

def Lean.Compiler.LCNF.LetDecl.updateValue {pu : Purity} (decl : LetDecl pu) (value : LetValue pu) : CompilerM (LetDecl pu)

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

opaque Lean.Compiler.LCNF.FunDecl.update {pu : Purity} (decl : FunDecl pu) (type : Expr) (params : Array (Param pu)) (value : Code pu) : CompilerM (FunDecl pu)

@[reducible, inline]

abbrev Lean.Compiler.LCNF.FunDecl.update' {pu : Purity} (decl : FunDecl pu) (type : Expr) (value : Code pu) : CompilerM (FunDecl pu)

@[reducible, inline]

abbrev Lean.Compiler.LCNF.FunDecl.updateValue {pu : Purity} (decl : FunDecl pu) (value : Code pu) : CompilerM (FunDecl pu)

@[inline]

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

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

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

@[reducible, inline]

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

@[implicit_reducible]

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

@[inline]

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

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 {pu : Purity} {t : Bool} (decl : FunDecl pu) : NormalizerM pu t (FunDecl pu)

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

@[inline]

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

@[inline]

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

Similar to internalize, but does not refresh FVarIds.

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

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

def Lean.Compiler.LCNF.mkFreshJpName : CompilerM Name

def Lean.Compiler.LCNF.mkAuxParam {pu : Purity} (type : Expr) (borrow : Bool := false) : CompilerM (Param pu)

def Lean.Compiler.LCNF.getConfig : CompilerM ConfigOptions

def Lean.Compiler.LCNF.CompilerM.run {α : Type} (x : CompilerM α) (s : State := { }) (phase : Phase := Phase.base) : CoreM α

structure Lean.Compiler.LCNF.CacheExtension (α β : Type) [BEq α] [Hashable α] extends Lean.EnvExtension (List α × Lean.PHashMap α β) : Type

Environment extension for local caching of key-value pairs, not persisted in .olean files.

• idx : Nat
• mkInitial : IO (List α × PHashMap α β)
• asyncMode : AsyncMode
• replay? : Option (ReplayFn (List α × PHashMap α β))

def Lean.Compiler.LCNF.instInhabitedCacheExtension.default {a✝ a✝¹ : Type} {a✝² : BEq a✝} {a✝³ : Hashable a✝} : CacheExtension a✝ a✝¹

@[implicit_reducible]

instance Lean.Compiler.LCNF.instInhabitedCacheExtension {a✝ a✝¹ : Type} {a✝² : BEq a✝} {a✝³ : Hashable a✝} : Inhabited (CacheExtension a✝ a✝¹)

def Lean.Compiler.LCNF.CacheExtension.register {α β : Type} [BEq α] [Hashable α] [Inhabited β] : IO (CacheExtension α β)

def Lean.Compiler.LCNF.CacheExtension.insert {α β : Type} [BEq α] [Hashable α] [Inhabited β] (ext : CacheExtension α β) (a : α) (b : β) : CoreM Unit

def Lean.Compiler.LCNF.CacheExtension.find? {α β : Type} [BEq α] [Hashable α] [Inhabited β] (ext : CacheExtension α β) (a : α) : CoreM (Option β)