Helper functions for backend code generators

def Lean.IR.isTailCallTo (g : Lake.Name) (b : Lean.IR.FnBody) : Bool

Return true iff b is of the form let x := g ys; ret x

def Lean.IR.usesModuleFrom (env : Lean.Environment) (modulePrefix : Lake.Name) : Bool

@[inline, reducible]

abbrev Lean.IR.CollectUsedDecls.M (α : Type) : Type

@[inline]

def Lean.IR.CollectUsedDecls.collect (f : Lean.IR.FunId) : Lean.IR.CollectUsedDecls.M Unit

partial def Lean.IR.CollectUsedDecls.collectFnBody : Lean.IR.FnBody → Lean.IR.CollectUsedDecls.M Unit

def Lean.IR.CollectUsedDecls.collectInitDecl (fn : Lake.Name) : Lean.IR.CollectUsedDecls.M Unit

def Lean.IR.CollectUsedDecls.collectDecl : Lean.IR.Decl → Lean.IR.CollectUsedDecls.M Lean.NameSet

def Lean.IR.collectUsedDecls (env : Lean.Environment) (decl : Lean.IR.Decl) (used : optParam Lean.NameSet ∅) : Lean.NameSet

@[inline, reducible]

abbrev Lean.IR.VarTypeMap : Type

@[inline, reducible]

abbrev Lean.IR.JPParamsMap : Type

@[inline, reducible]

abbrev Lean.IR.CollectMaps.Collector : Type

@[inline]

def Lean.IR.CollectMaps.collectVar (x : Lean.IR.VarId) (t : Lean.IR.IRType) : Lean.IR.CollectMaps.Collector

def Lean.IR.CollectMaps.collectParams (ps : Array Lean.IR.Param) : Lean.IR.CollectMaps.Collector

@[inline]

def Lean.IR.CollectMaps.collectJP (j : Lean.IR.JoinPointId) (xs : Array Lean.IR.Param) : Lean.IR.CollectMaps.Collector

partial def Lean.IR.CollectMaps.collectFnBody : Lean.IR.FnBody → Lean.IR.CollectMaps.Collector

collectFnBody assumes the variables in

def Lean.IR.CollectMaps.collectDecl : Lean.IR.Decl → Lean.IR.CollectMaps.Collector

def Lean.IR.mkVarJPMaps (d : Lean.IR.Decl) : Lean.IR.VarTypeMap × Lean.IR.JPParamsMap

Return a pair (v, j), where v is a mapping from variable/parameter to type, and j is a mapping from join point to parameters. This function assumes d has normalized indexes (see normids.lean).