Documentation

Lean.Compiler.LCNF.PullFunDecls

source
structure Lean.Compiler.LCNF.PullFunDecls.ToPull :
Type

Local function declaration and join point being pulled.

Instances For
    source
    @[implicit_reducible]
    instance Lean.Compiler.LCNF.PullFunDecls.instInhabitedToPull :
    Inhabited ToPull
    source
    def Lean.Compiler.LCNF.PullFunDecls.instInhabitedToPull.default :
    ToPull
    Instances For
      source
      @[reducible, inline]
      abbrev Lean.Compiler.LCNF.PullFunDecls.PullM (α : Type) :
      Type

      The PullM state contains the local function declarations and join points being pulled.

      Instances For
        source
        def Lean.Compiler.LCNF.PullFunDecls.findFVarDirectDeps (fvarId : FVarId) :
        PullM (List ToPull)

        Extract from the state any local function declarations that depends on the given free variable. The idea is that we have to stop pulling these declarations because they depend on fvarId.

        Instances For
          source
          partial def Lean.Compiler.LCNF.PullFunDecls.findFVarDepsFixpoint (todo : List ToPull) (acc : Array ToPull := #[]) :
          PullM (Array ToPull)
          source
          def Lean.Compiler.LCNF.PullFunDecls.findFVarDeps (fvarId : FVarId) :
          PullM (Array ToPull)
          Instances For
            source
            def Lean.Compiler.LCNF.PullFunDecls.findParamsDeps {pu : Purity} (params : Array (Param pu)) :
            PullM (Array ToPull)

            Similar to findFVarDeps. Extract from the state any local function declarations that depends on the given parameters.

            Instances For
              source
              def Lean.Compiler.LCNF.PullFunDecls.ToPull.attach (p : ToPull) (k : Code Purity.pure) :
              Code Purity.pure

              Construct the code fun p.decl k or jp p.decl k.

              Instances For
                source
                def Lean.Compiler.LCNF.PullFunDecls.attach (ps : Array ToPull) (k : Code Purity.pure) :
                Code Purity.pure

                Attach the given array of local function declarations and join points to k.

                Instances For
                  source
                  def Lean.Compiler.LCNF.PullFunDecls.attachFVarDeps (fvarId : FVarId) (k : Code Purity.pure) :
                  PullM (Code Purity.pure)

                  Extract from the state any local function declarations that depends on the given free variable, and attach to code k.

                  Instances For
                    source
                    def Lean.Compiler.LCNF.PullFunDecls.attachParamsDeps (params : Array (Param Purity.pure)) (k : Code Purity.pure) :
                    PullM (Code Purity.pure)

                    Similar to attachFVarDeps. Extract from the state any local function declarations that depends on the given parameters, and attach to code k.

                    Instances For
                      source
                      def Lean.Compiler.LCNF.PullFunDecls.attachJps (k : Code Purity.pure) :
                      PullM (Code Purity.pure)
                      Instances For
                        source
                        partial def Lean.Compiler.LCNF.PullFunDecls.addToPull (isFun : Bool) (decl : FunDecl Purity.pure) :
                        PullM Unit

                        Add local function declaration (or join point if isFun = false) to the state.

                        source
                        partial def Lean.Compiler.LCNF.PullFunDecls.pull (code : Code Purity.pure) :
                        PullM (Code Purity.pure)

                        Pull local function declarations and join points in code. The state contains the declarations being pulled.

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

                        Pull local function declarations and join points in the given declaration.

                        Instances For
                          source
                          def Lean.Compiler.LCNF.pullFunDecls :
                          Pass
                          Instances For