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 ToPull
Equations
source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.PullFunDecls.PullM (α : Type) :
Type

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

Equations
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.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.PullFunDecls.findFVarDirectDeps.go (fvarId : FVarId) (as keep dep : List ToPull) :
CoreM (List ToPull × List ToPull)
Equations
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)
Equations
source
def Lean.Compiler.LCNF.PullFunDecls.findParamsDeps (params : Array Param) :
PullM (Array 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.
source
def Lean.Compiler.LCNF.PullFunDecls.ToPull.attach (p : ToPull) (k : Code) :
Code

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

Equations
source
def Lean.Compiler.LCNF.PullFunDecls.attach (ps : Array ToPull) (k : Code) :
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.
source
def Lean.Compiler.LCNF.PullFunDecls.attach.go (ps : Array ToPull) :
StateM (Code × Array Bool) Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.PullFunDecls.attach.visited (i : Nat) :
StateM (Code × Array Bool) Bool
Equations
source
partial def Lean.Compiler.LCNF.PullFunDecls.attach.visit (ps : Array ToPull) (i : Nat) :
StateM (Code × Array Bool) Unit
source
def Lean.Compiler.LCNF.PullFunDecls.attachFVarDeps (fvarId : FVarId) (k : Code) :
PullM Code

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

Equations
source
def Lean.Compiler.LCNF.PullFunDecls.attachParamsDeps (params : Array Param) (k : Code) :
PullM Code

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

Equations
source
def Lean.Compiler.LCNF.PullFunDecls.attachJps (k : Code) :
PullM Code
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Compiler.LCNF.PullFunDecls.addToPull (isFun : Bool) (decl : FunDecl) :
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) :
PullM 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 : Decl) :
CompilerM 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.
source
def Lean.Compiler.LCNF.pullFunDecls :
Pass
Equations