class Lean.Compiler.LCNF.MonadCodeBind (m : Type → Type) : Type

Helper class for lifting CompilerM.codeBind

• codeBind {pu : Purity} (c : Code pu) (f : FVarId → m (Code pu)) : m (Code pu)

@[reducible, inline]

abbrev Lean.Compiler.LCNF.Code.bind {m : Type → Type} {pu : Purity} [MonadCodeBind m] (c : Code pu) (f : FVarId → m (Code pu)) : m (Code pu)

Return code that is equivalent to c >>= f. That is, executes c, and then f x, where x is a variable that contains the result of c's computation.

If c contains a jump to a join point jp_i not declared in c, we throw an exception because an invalid block would be generated. It would be invalid because f would not be applied to jp_i. Note that, we could have decided to create a copy of jp_i where we apply f to it, by we decided to not do it to avoid code duplication.

def Lean.Compiler.LCNF.CompilerM.codeBind {pu : Purity} (c : Code pu) (f : FVarId → CompilerM (Code pu)) : CompilerM (Code pu)

@[instance_reducible]

instance Lean.Compiler.LCNF.instMonadCodeBindCompilerM : MonadCodeBind CompilerM

@[instance_reducible]

instance Lean.Compiler.LCNF.instMonadCodeBindReaderT {m : Type → Type} {ρ : Type} [MonadCodeBind m] : MonadCodeBind (ReaderT ρ m)

@[instance_reducible]

instance Lean.Compiler.LCNF.instMonadCodeBindStateRefT'OfSTWorld {ω : Type} {m : Type → Type} {σ : Type} [STWorld ω m] [MonadCodeBind m] : MonadCodeBind (StateRefT' ω σ m)

def Lean.Compiler.LCNF.mkNewParams {pu : Purity} (type : Expr) : CompilerM (Array (Param pu))

Create new parameters for the given arrow type. Example: if type is Nat → Bool → Int, the result is an array containing two new parameters with types Nat and Bool.

def Lean.Compiler.LCNF.isEtaExpandCandidateCore (type : Expr) (params : Array (Param Purity.pure)) : Bool

@[reducible, inline]

abbrev Lean.Compiler.LCNF.FunDecl.isEtaExpandCandidate (decl : FunDecl Purity.pure) : Bool

def Lean.Compiler.LCNF.etaExpandCore (type : Expr) (params : Array (Param Purity.pure)) (value : Code Purity.pure) : CompilerM (Array (Param Purity.pure) × Code Purity.pure)

def Lean.Compiler.LCNF.etaExpandCore? (type : Expr) (params : Array (Param Purity.pure)) (value : Code Purity.pure) : CompilerM (Option (Array (Param Purity.pure) × Code Purity.pure))

def Lean.Compiler.LCNF.FunDecl.etaExpand (decl : FunDecl Purity.pure) : CompilerM (FunDecl Purity.pure)

def Lean.Compiler.LCNF.Decl.etaExpand (decl : Decl Purity.pure) : CompilerM (Decl Purity.pure)