Lean.Compiler.LCNF.Internalize

source

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

Instances For

source

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 }

source

instance Lean.Compiler.LCNF.Internalize.instMonadFVarSubstStateInternalizeM :

Lean.Compiler.LCNF.MonadFVarSubstState Lean.Compiler.LCNF.Internalize.InternalizeM

Equations

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

source

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.

source

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.

source

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

Lean.Compiler.LCNF.Internalize.InternalizeM Lean.Compiler.LCNF.FunDecl

source

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

Lean.Compiler.LCNF.Internalize.InternalizeM Lean.Compiler.LCNF.Code

source

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.

source

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

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

source

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

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

source

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.

source

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.

source

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)