@[reducible, inline]

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

Equations

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

@[implicit_reducible]

instance Lean.Compiler.LCNF.Internalize.instMonadFVarSubstInternalizeMTrue {pu : Purity} : MonadFVarSubst (InternalizeM pu) pu 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 }

@[implicit_reducible]

instance Lean.Compiler.LCNF.Internalize.instMonadFVarSubstStateInternalizeM {pu : Purity} : MonadFVarSubstState (InternalizeM pu) pu

Equations

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

def Lean.Compiler.LCNF.Internalize.internalizeParam {pu : Purity} (p : Param pu) : InternalizeM pu (Param pu)

Equations

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

def Lean.Compiler.LCNF.Internalize.internalizeArg {pu : Purity} (arg : Arg pu) : InternalizeM pu (Arg pu)

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.Internalize.internalizeArg Lean.Compiler.LCNF.Arg.erased = pure Lean.Compiler.LCNF.Arg.erased

def Lean.Compiler.LCNF.Internalize.internalizeArgs {pu : Purity} (args : Array (Arg pu)) : InternalizeM pu (Array (Arg pu))

Equations

• Lean.Compiler.LCNF.Internalize.internalizeArgs args = Array.mapM Lean.Compiler.LCNF.Internalize.internalizeArg args

def Lean.Compiler.LCNF.Internalize.internalizeLetDecl {pu : Purity} (decl : LetDecl pu) : InternalizeM pu (LetDecl pu)

Equations

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

partial def Lean.Compiler.LCNF.Internalize.internalizeFunDecl {pu : Purity} (decl : FunDecl pu) : InternalizeM pu (FunDecl pu)

partial def Lean.Compiler.LCNF.Internalize.internalizeCode {pu : Purity} (code : Code pu) : InternalizeM pu (Code pu)

def Lean.Compiler.LCNF.Internalize.internalizeCodeDecl {pu : Purity} (decl : CodeDecl pu) : InternalizeM pu (CodeDecl pu)

Equations

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

def Lean.Compiler.LCNF.Code.internalize {pu : Purity} (code : Code pu) (s : FVarSubst pu := ∅) : CompilerM (Code pu)

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

Equations

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

def Lean.Compiler.LCNF.Decl.internalize {pu : Purity} (decl : Decl pu) (s : FVarSubst pu := ∅) : CompilerM (Decl pu)

Equations

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

def Lean.Compiler.LCNF.cleanup {pu : Purity} (decl : Array (Decl pu)) : CompilerM (Array (Decl pu))

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.normalizeFVarIds {pu : Purity} (decl : Decl pu) : CoreM (Decl pu)

Equations

• Lean.Compiler.LCNF.normalizeFVarIds decl = do let ngenSaved ← Lean.getNGen Lean.setNGen { } tryFinally decl.internalize.run (Lean.setNGen ngenSaved)