structure Lean.Compiler.LCNF.Internalize.Context : Type

• uniqueIdents : Bool

@[reducible, inline]

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

Equations

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

@[inline]

def Lean.Compiler.LCNF.Internalize.InternalizeM.run {pu : Purity} {α : Type} (x : InternalizeM pu α) (state : FVarSubst pu) (ctx : Context := { }) : CompilerM (α × FVarSubst pu)

Equations

• x.run state ctx = (ReaderT.run x ctx).run state

@[inline]

def Lean.Compiler.LCNF.Internalize.InternalizeM.run' {pu : Purity} {α : Type} (x : InternalizeM pu α) (state : FVarSubst pu) (ctx : Context := { }) : CompilerM α

Equations

• x.run' state ctx = (ReaderT.run x ctx).run' state

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

@[instance_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 := ∅) (uniqueIdents : Bool := false) : CompilerM (Code pu)

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

Equations

• code.internalize s uniqueIdents = (Lean.Compiler.LCNF.Internalize.internalizeCode code).run' s { uniqueIdents := uniqueIdents }

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

Equations

• decl.internalize s uniqueIdents = (Lean.Compiler.LCNF.Decl.internalize.go✝ decl).run' s { uniqueIdents := uniqueIdents }

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)