# Helper functions for backend code generators #

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

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

Equations

- Lean.IR.isTailCallTo g (Lean.IR.FnBody.vdecl x ty (Lean.IR.Expr.fap f ys) (Lean.IR.FnBody.ret (Lean.IR.Arg.var y))) = (x == y && f == g)
- Lean.IR.isTailCallTo g b = false

Instances For

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

- Lean.IR.usesModuleFrom env modulePrefix = env.allImportedModuleNames.toList.any fun (modName : Lean.Name) => modulePrefix.isPrefixOf modName

Instances For

source
@[reducible, inline]
abbrev Lean.IR.CollectUsedDecls.M (α : Type) :
Type
Equations

- Lean.IR.CollectUsedDecls.M = ReaderT Lean.Environment (StateM Lean.NameSet)

Instances For

source
@[inline]
def Lean.IR.CollectUsedDecls.collect (f : FunId) :
M Unit
Equations

- Lean.IR.CollectUsedDecls.collect f = modify fun (s : Lean.NameSet) => s.insert f

Instances For

source
partial def Lean.IR.CollectUsedDecls.collectFnBody :
FnBody → M Unit
source
def Lean.IR.CollectUsedDecls.collectInitDecl (fn : Name) :
M Unit
Equations

- Lean.IR.CollectUsedDecls.collectInitDecl fn = do let env ← read match Lean.getInitFnNameFor? env fn with | some initFn => Lean.IR.CollectUsedDecls.collect initFn | x => pure ()

Instances For

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

- Lean.IR.CollectUsedDecls.collectDecl (Lean.IR.Decl.fdecl f xs type b info) = Lean.IR.CollectUsedDecls.collectInitDecl f *> Lean.IR.CollectUsedDecls.collectFnBody b *> get
- Lean.IR.CollectUsedDecls.collectDecl (Lean.IR.Decl.extern f xs type ext) = Lean.IR.CollectUsedDecls.collectInitDecl f *> get

Instances For

source
def Lean.IR.collectUsedDecls (env : Environment) (decl : Decl) (used : NameSet := ∅) :
NameSet
Equations

- Lean.IR.collectUsedDecls env decl used = StateT.run' (Lean.IR.CollectUsedDecls.collectDecl decl env) used

Instances For

source
@[reducible, inline]
abbrev Lean.IR.VarTypeMap :
Type
Equations

- Lean.IR.VarTypeMap = Std.HashMap Lean.IR.VarId Lean.IR.IRType

Instances For

source
@[reducible, inline]
abbrev Lean.IR.JPParamsMap :
Type
Equations

- Lean.IR.JPParamsMap = Std.HashMap Lean.IR.JoinPointId (Array Lean.IR.Param)

Instances For

source
@[reducible, inline]
abbrev Lean.IR.CollectMaps.Collector :
Type
Equations

- Lean.IR.CollectMaps.Collector = (Lean.IR.VarTypeMap × Lean.IR.JPParamsMap → Lean.IR.VarTypeMap × Lean.IR.JPParamsMap)

Instances For

source
@[inline]
def Lean.IR.CollectMaps.collectVar (x : VarId) (t : IRType) :
Collector
Equations

- Lean.IR.CollectMaps.collectVar x t (vs, js) = (Std.HashMap.insert vs x t, js)

Instances For

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

- Lean.IR.CollectMaps.collectParams ps s = Array.foldl (fun (s : Lean.IR.VarTypeMap × Lean.IR.JPParamsMap) (p : Lean.IR.Param) => Lean.IR.CollectMaps.collectVar p.x p.ty s) s ps

Instances For

source
@[inline]
def Lean.IR.CollectMaps.collectJP (j : JoinPointId) (xs : Array Param) :
Collector
Equations

- Lean.IR.CollectMaps.collectJP j xs (vs, js) = (vs, Std.HashMap.insert js j xs)

Instances For

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

`collectFnBody` assumes the variables in

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

- Lean.IR.CollectMaps.collectDecl (Lean.IR.Decl.fdecl f xs type b info) = Lean.IR.CollectMaps.collectParams xs ∘ Lean.IR.CollectMaps.collectFnBody b
- Lean.IR.CollectMaps.collectDecl x✝ = id

Instances For

source
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`).

Equations

- Lean.IR.mkVarJPMaps d = Lean.IR.CollectMaps.collectDecl d (∅, ∅)

Instances For