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.

Equations

• c.bind f = Lean.Compiler.LCNF.MonadCodeBind.codeBind c f

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

Equations

• Lean.Compiler.LCNF.CompilerM.codeBind c f = (Lean.Compiler.LCNF.CompilerM.codeBind.go✝ f c).run ∅

@[instance_reducible]

instance Lean.Compiler.LCNF.instMonadCodeBindCompilerM : MonadCodeBind CompilerM

Equations

• Lean.Compiler.LCNF.instMonadCodeBindCompilerM = { codeBind := fun {pu : Lean.Compiler.LCNF.Purity} => Lean.Compiler.LCNF.CompilerM.codeBind }

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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.

Equations

• Lean.Compiler.LCNF.mkNewParams type = Lean.Compiler.LCNF.mkNewParams.go✝ type #[] #[]

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

Equations

• Lean.Compiler.LCNF.isEtaExpandCandidateCore type params = decide (Lean.Compiler.LCNF.getArrowArity type > params.size)

@[reducible, inline]

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

Equations

• decl.isEtaExpandCandidate = Lean.Compiler.LCNF.isEtaExpandCandidateCore decl.type decl.params

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

Equations

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

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))

Equations

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

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

Equations

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

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

Equations

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