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

Local function declaration and join point being pulled.

• isFun : Bool
• decl : Lean.Compiler.LCNF.FunDecl
• used : Lean.FVarIdSet

instance Lean.Compiler.LCNF.PullFunDecls.instInhabitedToPull : Inhabited Lean.Compiler.LCNF.PullFunDecls.ToPull

Equations

• Lean.Compiler.LCNF.PullFunDecls.instInhabitedToPull = { default := { isFun := default, decl := default, used := default } }

@[reducible, inline]

abbrev Lean.Compiler.LCNF.PullFunDecls.PullM (α : Type) : Type

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

Equations

• Lean.Compiler.LCNF.PullFunDecls.PullM = StateRefT' IO.RealWorld (List Lean.Compiler.LCNF.PullFunDecls.ToPull) Lean.Compiler.LCNF.CompilerM

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.

Equations

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

def Lean.Compiler.LCNF.PullFunDecls.findFVarDirectDeps.go (fvarId : Lean.FVarId) (as keep dep : List Lean.Compiler.LCNF.PullFunDecls.ToPull) : Lean.CoreM (List Lean.Compiler.LCNF.PullFunDecls.ToPull × List Lean.Compiler.LCNF.PullFunDecls.ToPull)

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.PullFunDecls.findFVarDirectDeps.go fvarId [] keep dep = pure (keep, dep)

partial def Lean.Compiler.LCNF.PullFunDecls.findFVarDepsFixpoint (todo : List Lean.Compiler.LCNF.PullFunDecls.ToPull) (acc : Array Lean.Compiler.LCNF.PullFunDecls.ToPull := #[]) : Lean.Compiler.LCNF.PullFunDecls.PullM (Array Lean.Compiler.LCNF.PullFunDecls.ToPull)

def Lean.Compiler.LCNF.PullFunDecls.findFVarDeps (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.PullFunDecls.PullM (Array Lean.Compiler.LCNF.PullFunDecls.ToPull)

Equations

• Lean.Compiler.LCNF.PullFunDecls.findFVarDeps fvarId = do let ps ← Lean.Compiler.LCNF.PullFunDecls.findFVarDirectDeps fvarId Lean.Compiler.LCNF.PullFunDecls.findFVarDepsFixpoint ps

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.

Equations

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

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.

Equations

• p.attach k = if p.isFun = true then Lean.Compiler.LCNF.Code.fun p.decl k else Lean.Compiler.LCNF.Code.jp p.decl k

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.

Equations

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

def Lean.Compiler.LCNF.PullFunDecls.attach.go (ps : Array Lean.Compiler.LCNF.PullFunDecls.ToPull) : StateM (Lean.Compiler.LCNF.Code × Array Bool) Unit

Equations

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

def Lean.Compiler.LCNF.PullFunDecls.attach.visited (i : Nat) : StateM (Lean.Compiler.LCNF.Code × Array Bool) Bool

Equations

• Lean.Compiler.LCNF.PullFunDecls.attach.visited i = do let __do_lift ← get pure __do_lift.snd[i]!

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

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.

Equations

• Lean.Compiler.LCNF.PullFunDecls.attachFVarDeps fvarId k = do let ps ← Lean.Compiler.LCNF.PullFunDecls.findFVarDeps fvarId pure (Lean.Compiler.LCNF.PullFunDecls.attach ps k)

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.

Equations

• Lean.Compiler.LCNF.PullFunDecls.attachParamsDeps params k = do let ps ← Lean.Compiler.LCNF.PullFunDecls.findParamsDeps params pure (Lean.Compiler.LCNF.PullFunDecls.attach ps k)

def Lean.Compiler.LCNF.PullFunDecls.attachJps (k : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.PullFunDecls.PullM Lean.Compiler.LCNF.Code

Equations

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

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.

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.

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.

Equations

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

def Lean.Compiler.LCNF.pullFunDecls : Lean.Compiler.LCNF.Pass

Equations

• Lean.Compiler.LCNF.pullFunDecls = Lean.Compiler.LCNF.Pass.mkPerDeclaration `pullFunDecls Lean.Compiler.LCNF.Decl.pullFunDecls Lean.Compiler.LCNF.Phase.base