@[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 : 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 : 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

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

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

Equations

• decl.internalize 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.

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