Documentation

Lean.Compiler.LCNF.PullFunDecls

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

Local function declaration and join point being pulled.

Instances For
    source
    instance Lean.Compiler.LCNF.PullFunDecls.instInhabitedToPull :
    Inhabited Lean.Compiler.LCNF.PullFunDecls.ToPull
    source
    @[inline, reducible]
    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 : Lean.FVarId) :
      Lean.Compiler.LCNF.PullFunDecls.PullM (List Lean.Compiler.LCNF.PullFunDecls.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
        def Lean.Compiler.LCNF.PullFunDecls.findFVarDirectDeps.go (fvarId : Lean.FVarId) (as : List Lean.Compiler.LCNF.PullFunDecls.ToPull) (keep : List Lean.Compiler.LCNF.PullFunDecls.ToPull) (dep : List Lean.Compiler.LCNF.PullFunDecls.ToPull) :
        Lean.CoreM (List Lean.Compiler.LCNF.PullFunDecls.ToPull × List Lean.Compiler.LCNF.PullFunDecls.ToPull)
        Equations
        Instances For
          source
          partial def Lean.Compiler.LCNF.PullFunDecls.findFVarDepsFixpoint (todo : List Lean.Compiler.LCNF.PullFunDecls.ToPull) (acc : optParam (Array Lean.Compiler.LCNF.PullFunDecls.ToPull) #[]) :
          Lean.Compiler.LCNF.PullFunDecls.PullM (Array Lean.Compiler.LCNF.PullFunDecls.ToPull)
          source
          def Lean.Compiler.LCNF.PullFunDecls.findFVarDeps (fvarId : Lean.FVarId) :
          Lean.Compiler.LCNF.PullFunDecls.PullM (Array Lean.Compiler.LCNF.PullFunDecls.ToPull)
          Instances For
            source
            def Lean.Compiler.LCNF.PullFunDecls.findParamsDeps (params : Array Lean.Compiler.LCNF.Param) :
            Lean.Compiler.LCNF.PullFunDecls.PullM (Array Lean.Compiler.LCNF.PullFunDecls.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 : Lean.Compiler.LCNF.PullFunDecls.ToPull) (k : Lean.Compiler.LCNF.Code) :
              Lean.Compiler.LCNF.Code

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

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

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

                Instances For
                  source
                  def Lean.Compiler.LCNF.PullFunDecls.attach.go (ps : Array Lean.Compiler.LCNF.PullFunDecls.ToPull) :
                  StateM (Lean.Compiler.LCNF.Code × Array Bool) Unit
                  Instances For
                    source
                    def Lean.Compiler.LCNF.PullFunDecls.attach.visited (i : Nat) :
                    StateM (Lean.Compiler.LCNF.Code × Array Bool) Bool
                    Instances For
                      source
                      partial def Lean.Compiler.LCNF.PullFunDecls.attach.visit (ps : Array Lean.Compiler.LCNF.PullFunDecls.ToPull) (i : Nat) :
                      StateM (Lean.Compiler.LCNF.Code × Array Bool) Unit
                      source
                      def Lean.Compiler.LCNF.PullFunDecls.attachFVarDeps (fvarId : Lean.FVarId) (k : Lean.Compiler.LCNF.Code) :
                      Lean.Compiler.LCNF.PullFunDecls.PullM Lean.Compiler.LCNF.Code

                      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 Lean.Compiler.LCNF.Param) (k : Lean.Compiler.LCNF.Code) :
                        Lean.Compiler.LCNF.PullFunDecls.PullM Lean.Compiler.LCNF.Code

                        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 : Lean.Compiler.LCNF.Code) :
                          Lean.Compiler.LCNF.PullFunDecls.PullM Lean.Compiler.LCNF.Code
                          Instances For
                            source
                            partial def Lean.Compiler.LCNF.PullFunDecls.addToPull (isFun : Bool) (decl : Lean.Compiler.LCNF.FunDecl) :
                            Lean.Compiler.LCNF.PullFunDecls.PullM Unit

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

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

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

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

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

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