Documentation

Lean.Compiler.LCNF.Bind

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

Helper class for lifting CompilerM.codeBind

Instances
    source
    @[inline, reducible]
    abbrev Lean.Compiler.LCNF.Code.bind {m : Type → Type} [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.

    Instances For
      source
      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
      Instances For
        source
        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
        source
        instance Lean.Compiler.LCNF.instMonadCodeBindCompilerM :
        Lean.Compiler.LCNF.MonadCodeBind Lean.Compiler.LCNF.CompilerM
        source
        instance Lean.Compiler.LCNF.instMonadCodeBindReaderT {m : Type → Type} {ρ : Type} [Lean.Compiler.LCNF.MonadCodeBind m] :
        Lean.Compiler.LCNF.MonadCodeBind (ReaderT ρ m)
        source
        instance Lean.Compiler.LCNF.instMonadCodeBindStateRefT' {ω : Type} {m : Type → Type} {σ : Type} [STWorld ω m] [Lean.Compiler.LCNF.MonadCodeBind m] :
        Lean.Compiler.LCNF.MonadCodeBind (StateRefT' ω σ m)
        source
        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.

        Instances For
          source
          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)
          source
          def Lean.Compiler.LCNF.isEtaExpandCandidateCore (type : Lean.Expr) (params : Array Lean.Compiler.LCNF.Param) :
          Bool
          Instances For
            source
            @[inline, reducible]
            abbrev Lean.Compiler.LCNF.FunDeclCore.isEtaExpandCandidate (decl : Lean.Compiler.LCNF.FunDecl) :
            Bool
            Instances For
              source
              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)
              Instances For
                source
                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))
                Instances For
                  source
                  def Lean.Compiler.LCNF.FunDeclCore.etaExpand (decl : Lean.Compiler.LCNF.FunDecl) :
                  Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.FunDecl
                  Instances For
                    source
                    def Lean.Compiler.LCNF.Decl.etaExpand (decl : Lean.Compiler.LCNF.Decl) :
                    Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Decl
                    Instances For