@[reducible, 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 : MonadFVarSubst 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 : MonadFVarSubstState InternalizeM

Equations

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

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

Equations

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

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

Equations

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

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

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

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

Equations

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

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

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 (decl : Decl) (s : FVarSubst := ∅) : CompilerM Decl

Equations

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

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

Equations

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

def Lean.Compiler.LCNF.cleanup (decl : Array Decl) : CompilerM (Array 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.normalizeFVarIds (decl : Decl) : CoreM Decl

Equations

• Lean.Compiler.LCNF.normalizeFVarIds decl = do let ngenSaved ← Lean.getNGen Lean.setNGen { namePrefix := `_uniq, idx := 1 } tryFinally decl.internalize.run (Lean.setNGen ngenSaved)