Helper functions for backend code generators

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

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

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

structure Lean.IR.CollectUsedDecls.State : Type

• set : NameSet
• order : Array Name

@[reducible, inline]

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

@[inline]

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

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

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

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

def Lean.IR.CollectUsedDecls.collectDeclLoop (decls : List Decl) : M Unit

def Lean.IR.collectUsedDecls (env : Environment) (decls : List Decl) : Array Name

@[reducible, inline]

abbrev Lean.IR.VarTypeMap : Type

@[reducible, inline]

abbrev Lean.IR.JPParamsMap : Type

@[reducible, inline]

abbrev Lean.IR.CollectMaps.Collector : Type

@[inline]

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

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

@[inline]

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

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

collectFnBody assumes the variables in

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

def Lean.IR.mkVarJPMaps (d : Decl) : VarTypeMap × 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).