Documentation

Lean.Compiler.IR.EmitUtil

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

Equations

Lean.IR.isTailCallTo g b = match b with | Lean.IR.FnBody.vdecl x x_1 (Lean.IR.Expr.fap f x_2) (Lean.IR.FnBody.ret (Lean.IR.Arg.var y)) => x == y && f == g | x => false

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

Equations

Lean.IR.usesModuleFrom env modulePrefix = List.any (Array.toList (Lean.Environment.allImportedModuleNames env)) fun modName => Lean.Name.isPrefixOf modulePrefix modName

@[inline]

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

Type

Equations

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

@[inline]

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

Lean.IR.CollectUsedDecls.M Unit

Equations

Lean.IR.CollectUsedDecls.collect f = modify fun s => Lean.NameSet.insert s f

partial def Lean.IR.CollectUsedDecls.collectFnBody :

Lean.IR.FnBody → Lean.IR.CollectUsedDecls.M Unit

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

Lean.IR.CollectUsedDecls.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 ()

def Lean.IR.CollectUsedDecls.collectDecl :

Lean.IR.Decl → Lean.IR.CollectUsedDecls.M Lean.NameSet

Equations

Lean.IR.CollectUsedDecls.collectDecl x = match x with | Lean.IR.Decl.fdecl f x x_1 b x_2 => SeqRight.seqRight (SeqRight.seqRight (Lean.IR.CollectUsedDecls.collectInitDecl f) fun x => Lean.IR.CollectUsedDecls.collectFnBody b) fun x => get | Lean.IR.Decl.extern f x x_1 x_2 => SeqRight.seqRight (Lean.IR.CollectUsedDecls.collectInitDecl f) fun x => get

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

Equations

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

@[inline]

abbrev Lean.IR.VarTypeMap :

Type

Equations

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

@[inline]

abbrev Lean.IR.JPParamsMap :

Type

Equations

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

@[inline]

abbrev Lean.IR.CollectMaps.Collector :

Type

Equations

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

@[inline]

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

Lean.IR.CollectMaps.Collector

Equations

Lean.IR.CollectMaps.collectVar x t x = match x with | (vs, js) => (Std.HashMap.insert vs x t, js)

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

Lean.IR.CollectMaps.Collector

Equations

Lean.IR.CollectMaps.collectParams ps s = Array.foldl (fun s p => Lean.IR.CollectMaps.collectVar p.x p.ty s) s ps 0 (Array.size ps)

@[inline]

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

Lean.IR.CollectMaps.Collector

Equations

Lean.IR.CollectMaps.collectJP j xs x = match x with | (vs, js) => (vs, Std.HashMap.insert js j xs)

partial def Lean.IR.CollectMaps.collectFnBody :

Lean.IR.FnBody → Lean.IR.CollectMaps.Collector

def Lean.IR.CollectMaps.collectDecl :

Lean.IR.Decl → Lean.IR.CollectMaps.Collector

Equations

Lean.IR.CollectMaps.collectDecl x = match x with | Lean.IR.Decl.fdecl x xs x_1 b x_2 => Lean.IR.CollectMaps.collectParams xs ∘ Lean.IR.CollectMaps.collectFnBody b | x => id

def Lean.IR.mkVarJPMaps (d : Lean.IR.Decl) :

Lean.IR.VarTypeMap × Lean.IR.JPParamsMap

Equations

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