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

• codeBind : Lean.Compiler.LCNF.Code → (Lean.FVarId → m Lean.Compiler.LCNF.Code) → m Lean.Compiler.LCNF.Code

Helper class for lifting CompilerM.codeBind

@[inline]

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

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

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

def Lean.Compiler.LCNF.CompilerM.codeBind (c : Lean.Compiler.LCNF.Code) (f : Lean.FVarId → Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Code

Equations

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

partial def Lean.Compiler.LCNF.CompilerM.codeBind.go (f : Lean.FVarId → Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Code) (c : Lean.Compiler.LCNF.Code) : ReaderT Lean.FVarIdSet Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Code

instance Lean.Compiler.LCNF.instMonadCodeBindCompilerM : Lean.Compiler.LCNF.MonadCodeBind Lean.Compiler.LCNF.CompilerM

Equations

• Lean.Compiler.LCNF.instMonadCodeBindCompilerM = { codeBind := Lean.Compiler.LCNF.CompilerM.codeBind }

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

Equations

• Lean.Compiler.LCNF.instMonadCodeBindReaderT = { codeBind := fun c f ctx => Lean.Compiler.LCNF.Code.bind c fun fvarId => f fvarId ctx }

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

Equations

• Lean.Compiler.LCNF.instMonadCodeBindStateRefT' = { codeBind := fun c f sref => Lean.Compiler.LCNF.Code.bind c fun fvarId => f fvarId sref }

def Lean.Compiler.LCNF.Code.ensureAnyType (c : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Code

Ensure resulting code has type ⊤.

Equations

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

def Lean.Compiler.LCNF.mkNewParams (type : Lean.Expr) : Lean.Compiler.LCNF.CompilerM (Array Lean.Compiler.LCNF.Param)

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 #[] #[]

partial def Lean.Compiler.LCNF.mkNewParams.go (type : Lean.Expr) (xs : Array Lean.Expr) (ps : Array Lean.Compiler.LCNF.Param) : Lean.Compiler.LCNF.CompilerM (Array Lean.Compiler.LCNF.Param)

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

Equations

• Lean.Compiler.LCNF.isEtaExpandCandidateCore type params = let typeArity := Lean.Compiler.LCNF.getArrowArity type; let valueArity := Array.size params; decide (typeArity > valueArity)

@[inline]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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