inductive Lean.Compiler.LCNF.Phase : Type

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

  base: Lean.Compiler.LCNF.Phase

• In this phase polymorphism has been eliminated.

  mono: Lean.Compiler.LCNF.Phase

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

  impure: Lean.Compiler.LCNF.Phase

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

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

Equations

• Lean.Compiler.LCNF.instInhabitedPhase = { default := Lean.Compiler.LCNF.Phase.base }

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

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

  lctx : Lean.Compiler.LCNF.LCtx

• Next auxiliary variable suffix

  nextIdx : Nat

The state managed by the CompilerM Monad.

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

Equations

• Lean.Compiler.LCNF.CompilerM.instInhabitedState = { default := { lctx := default, nextIdx := default } }

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

Equations

• Lean.Compiler.LCNF.CompilerM.instInhabitedContext = { default := { phase := default, config := default } }

@[inline]

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

Equations

• Lean.Compiler.LCNF.CompilerM = ReaderT Lean.Compiler.LCNF.CompilerM.Context (StateRefT' IO.RealWorld Lean.Compiler.LCNF.CompilerM.State Lean.CoreM)

@[inline]

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

Equations

• Lean.Compiler.LCNF.withPhase phase x = withReader (fun ctx => { phase := phase, config := ctx.config }) x

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

Equations

• Lean.Compiler.LCNF.getPhase = do let a ← read pure a.phase

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Compiler.LCNF.findParam? fvarId = do let a ← get pure (Lean.HashMap.find? a.lctx.params fvarId)

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

Equations

• Lean.Compiler.LCNF.findLetDecl? fvarId = do let a ← get pure (Lean.HashMap.find? a.lctx.letDecls fvarId)

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

Equations

• Lean.Compiler.LCNF.findFunDecl? fvarId = do let a ← get pure (Lean.HashMap.find? a.lctx.funDecls fvarId)

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

Equations

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

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

Equations

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

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

Equations

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

@[inline]

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

Equations

• Lean.Compiler.LCNF.modifyLCtx f = modify fun s => { lctx := f s.lctx, nextIdx := s.nextIdx }

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

Equations

• Lean.Compiler.LCNF.eraseLetDecl decl = Lean.Compiler.LCNF.modifyLCtx fun lctx => Lean.Compiler.LCNF.LCtx.eraseLetDecl lctx decl

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

Equations

• Lean.Compiler.LCNF.eraseFunDecl decl recursive = Lean.Compiler.LCNF.modifyLCtx fun lctx => Lean.Compiler.LCNF.LCtx.eraseFunDecl lctx decl recursive

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

Equations

• Lean.Compiler.LCNF.eraseCode code = Lean.Compiler.LCNF.modifyLCtx fun lctx => Lean.Compiler.LCNF.LCtx.eraseCode code lctx

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

Equations

• Lean.Compiler.LCNF.eraseParam param = Lean.Compiler.LCNF.modifyLCtx fun lctx => Lean.Compiler.LCNF.LCtx.eraseParam lctx param

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

Equations

• Lean.Compiler.LCNF.eraseParams params = Lean.Compiler.LCNF.modifyLCtx fun lctx => Lean.Compiler.LCNF.LCtx.eraseParams lctx params

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

Equations

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

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.

Equations

• Lean.Compiler.LCNF.eraseCodeDecls decls = Array.forM (fun decl => Lean.Compiler.LCNF.eraseCodeDecl decl) decls 0 (Array.size decls)

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

Equations

• Lean.Compiler.LCNF.eraseDecl decl = do Lean.Compiler.LCNF.eraseParams decl.params Lean.Compiler.LCNF.eraseCode decl.value

@[inline]

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.

Equations

• Lean.Compiler.LCNF.FVarSubst = Lean.HashMap Lean.FVarId Lean.Expr

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) [inst : MonadLift m n] [inst : Lean.Compiler.LCNF.MonadFVarSubst m t] : Lean.Compiler.LCNF.MonadFVarSubst n t

Equations

• Lean.Compiler.LCNF.instMonadFVarSubst m n = { getSubst := liftM Lean.Compiler.LCNF.getSubst }

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) [inst : MonadLift m n] [inst : Lean.Compiler.LCNF.MonadFVarSubstState m] : Lean.Compiler.LCNF.MonadFVarSubstState n

Equations

• Lean.Compiler.LCNF.instMonadFVarSubstState m n = { modifySubst := fun f => liftM (Lean.Compiler.LCNF.modifySubst f) }

@[inline]

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

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

Equations

• Lean.Compiler.LCNF.addFVarSubst fvarId fvarId' = Lean.Compiler.LCNF.modifySubst fun s => Lean.HashMap.insert s fvarId (Lean.Expr.fvar fvarId')

@[inline]

def Lean.Compiler.LCNF.addSubst {m : Type → Type} [inst : 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.

Equations

• Lean.Compiler.LCNF.addSubst fvarId e = Lean.Compiler.LCNF.modifySubst fun s => Lean.HashMap.insert s fvarId e

@[inline]

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

• Lean.Compiler.LCNF.normFVar fvarId = do let a ← Lean.Compiler.LCNF.getSubst pure (Lean.Compiler.LCNF.normFVarImp a fvarId t)

@[inline]

def Lean.Compiler.LCNF.normExpr {m : Type → Type} {t : Bool} [inst : Lean.Compiler.LCNF.MonadFVarSubst m t] [inst : 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.

Equations

• Lean.Compiler.LCNF.normExpr e = do let a ← Lean.Compiler.LCNF.getSubst pure (Lean.Compiler.LCNF.normExprImp a e t)

def Lean.Compiler.LCNF.normExprs {m : Type → Type} {t : Bool} [inst : Lean.Compiler.LCNF.MonadFVarSubst m t] [inst : Monad m] (es : Array Lean.Expr) : m (Array Lean.Expr)

Normalize the given expressions using the current substitution.

Equations

• Lean.Compiler.LCNF.normExprs es = Array.mapMonoM es Lean.Compiler.LCNF.normExpr

def Lean.Compiler.LCNF.mkFreshBinderName (binderName : optParam Lean.Name (Lean.Name.mkStr1 "_x")) : Lean.Compiler.LCNF.CompilerM Lean.Name

Equations

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

@[inline]

abbrev Lean.Compiler.LCNF.Internalize.InternalizeM (α : Type) : Type

Equations

• Lean.Compiler.LCNF.Internalize.InternalizeM = StateRefT' IO.RealWorld Lean.Compiler.LCNF.FVarSubst Lean.Compiler.LCNF.CompilerM

instance Lean.Compiler.LCNF.Internalize.instMonadFVarSubstInternalizeMTrue : Lean.Compiler.LCNF.MonadFVarSubst Lean.Compiler.LCNF.Internalize.InternalizeM true

The InternalizeM monad is a translator. It "translates" the free variables in the input expressions and Code, into new fresh free variables in the local context.

Equations

• Lean.Compiler.LCNF.Internalize.instMonadFVarSubstInternalizeMTrue = { getSubst := get }

instance Lean.Compiler.LCNF.Internalize.instMonadFVarSubstStateInternalizeM : Lean.Compiler.LCNF.MonadFVarSubstState Lean.Compiler.LCNF.Internalize.InternalizeM

Equations

• Lean.Compiler.LCNF.Internalize.instMonadFVarSubstStateInternalizeM = { modifySubst := modify }

def Lean.Compiler.LCNF.Internalize.internalizeParam (p : Lean.Compiler.LCNF.Param) : Lean.Compiler.LCNF.Internalize.InternalizeM Lean.Compiler.LCNF.Param

Equations

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

def Lean.Compiler.LCNF.Internalize.internalizeLetDecl (decl : Lean.Compiler.LCNF.LetDecl) : Lean.Compiler.LCNF.Internalize.InternalizeM Lean.Compiler.LCNF.LetDecl

Equations

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

partial def Lean.Compiler.LCNF.Internalize.internalizeFunDecl (decl : Lean.Compiler.LCNF.FunDecl) : Lean.Compiler.LCNF.Internalize.InternalizeM Lean.Compiler.LCNF.FunDecl

partial def Lean.Compiler.LCNF.Internalize.internalizeCode (code : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.Internalize.InternalizeM Lean.Compiler.LCNF.Code

def Lean.Compiler.LCNF.Internalize.internalizeCodeDecl (decl : Lean.Compiler.LCNF.CodeDecl) : Lean.Compiler.LCNF.Internalize.InternalizeM Lean.Compiler.LCNF.CodeDecl

Equations

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

def Lean.Compiler.LCNF.Code.internalize (code : Lean.Compiler.LCNF.Code) (s : optParam Lean.Compiler.LCNF.FVarSubst ∅) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Code

Refresh free variables ids in code, and store their declarations in the local context.

Equations

• Lean.Compiler.LCNF.Code.internalize code s = StateRefT'.run' (Lean.Compiler.LCNF.Internalize.internalizeCode code) s

def Lean.Compiler.LCNF.Decl.internalize (decl : Lean.Compiler.LCNF.Decl) (s : optParam Lean.Compiler.LCNF.FVarSubst ∅) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Decl

Equations

• Lean.Compiler.LCNF.Decl.internalize decl s = StateRefT'.run' (Lean.Compiler.LCNF.Decl.internalize.go decl) s

def Lean.Compiler.LCNF.Decl.internalize.go (decl : Lean.Compiler.LCNF.Decl) : Lean.Compiler.LCNF.Internalize.InternalizeM Lean.Compiler.LCNF.Decl

Equations

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

Helper functions for creating LCNF local declarations.

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

Equations

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

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

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 : Array Lean.Compiler.LCNF.Param) (value : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.FunDecl

Equations

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

@[implementedBy _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

@[implementedBy _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.Expr) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.LetDecl

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

Equations

• Lean.Compiler.LCNF.LetDecl.updateValue decl value = Lean.Compiler.LCNF.LetDecl.update decl decl.type value

@[implementedBy _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]

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

Equations

• Lean.Compiler.LCNF.FunDeclCore.update' decl type value = Lean.Compiler.LCNF.FunDeclCore.update decl type decl.params value

@[inline]

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

Equations

• Lean.Compiler.LCNF.FunDeclCore.updateValue decl value = Lean.Compiler.LCNF.FunDeclCore.update decl decl.type decl.params value

@[inline]

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

Equations

• Lean.Compiler.LCNF.normParam p = do let a ← Lean.Compiler.LCNF.normExpr p.type liftM (Lean.Compiler.LCNF.Param.update p a)

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

Equations

• Lean.Compiler.LCNF.normParams ps = Array.mapMonoM ps Lean.Compiler.LCNF.normParam

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

Equations

• Lean.Compiler.LCNF.normLetDecl decl = do let a ← Lean.Compiler.LCNF.normExpr decl.type let a_1 ← Lean.Compiler.LCNF.normExpr decl.value liftM (Lean.Compiler.LCNF.LetDecl.update decl a a_1)

@[inline]

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

Equations

• Lean.Compiler.LCNF.NormalizerM _translator = ReaderT Lean.Compiler.LCNF.FVarSubst Lean.Compiler.LCNF.CompilerM

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

Equations

• Lean.Compiler.LCNF.instMonadFVarSubstNormalizerM = { getSubst := read }

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} [inst : MonadLiftT Lean.Compiler.LCNF.CompilerM m] [inst : Monad m] [inst : Lean.Compiler.LCNF.MonadFVarSubst m t] (decl : Lean.Compiler.LCNF.FunDecl) : m Lean.Compiler.LCNF.FunDecl

Equations

• Lean.Compiler.LCNF.normFunDecl decl = do let a ← Lean.Compiler.LCNF.getSubst liftM (Lean.Compiler.LCNF.normFunDeclImp decl a)

@[inline]

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

Similar to internalize, but does not refresh FVarIds.

Equations

• Lean.Compiler.LCNF.normCode code = do let a ← Lean.Compiler.LCNF.getSubst liftM (Lean.Compiler.LCNF.normCodeImp code a)

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

Equations

• Lean.Compiler.LCNF.replaceExprFVars e s translator = ReaderT.run (Lean.Compiler.LCNF.normExpr e) s

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

Equations

• Lean.Compiler.LCNF.replaceFVars code s translator = ReaderT.run (Lean.Compiler.LCNF.normCode code) s

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

Equations

• Lean.Compiler.LCNF.mkFreshJpName = Lean.Compiler.LCNF.mkFreshBinderName (Lean.Name.mkStr1 "_jp")

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

Equations

• Lean.Compiler.LCNF.mkAuxParam type borrow = do let a ← Lean.Compiler.LCNF.mkFreshBinderName (Lean.Name.mkStr1 "_y") Lean.Compiler.LCNF.mkParam a type borrow

def Lean.Compiler.LCNF.cleanup (decl : Array Lean.Compiler.LCNF.Decl) : Lean.Compiler.LCNF.CompilerM (Array Lean.Compiler.LCNF.Decl)

Create a fresh local context and internalize the given decls.

Equations

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

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

Equations

• Lean.Compiler.LCNF.getConfig = do let a ← read pure a.config

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 α

Equations

• Lean.Compiler.LCNF.CompilerM.run x s phase = do let a ← Lean.getOptions StateRefT'.run' (x { phase := phase, config := Lean.Compiler.LCNF.toConfigOptions a }) s