@[reducible, inline]

abbrev Lean.Compiler.LCNF.UsedLocalDecls : Type

Equations

• Lean.Compiler.LCNF.UsedLocalDecls = Lean.FVarIdHashSet

def Lean.Compiler.LCNF.collectLocalDeclsType (s : UsedLocalDecls) (type : Expr) : UsedLocalDecls

Collect set of (let) free variables in a LCNF value. This code exploits the LCNF property that local declarations do not occur in types.

Equations

• Lean.Compiler.LCNF.collectLocalDeclsType s type = Lean.Compiler.LCNF.collectLocalDeclsType.go s type

def Lean.Compiler.LCNF.collectLocalDeclsType.go (s : UsedLocalDecls) (e : Expr) : UsedLocalDecls

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.collectLocalDeclsType.go s (Lean.Expr.forallE binderName binderType body binderInfo) = s
• Lean.Compiler.LCNF.collectLocalDeclsType.go s (Lean.Expr.lam binderName binderType b binderInfo) = Lean.Compiler.LCNF.collectLocalDeclsType.go s b
• Lean.Compiler.LCNF.collectLocalDeclsType.go s (f.app a) = Lean.Compiler.LCNF.collectLocalDeclsType.go (Lean.Compiler.LCNF.collectLocalDeclsType.go s a) f
• Lean.Compiler.LCNF.collectLocalDeclsType.go s (Lean.Expr.fvar fvarId) = Std.HashSet.insert s fvarId
• Lean.Compiler.LCNF.collectLocalDeclsType.go s e = s

def Lean.Compiler.LCNF.collectLocalDeclsArg (s : UsedLocalDecls) (arg : Arg) : UsedLocalDecls

Equations

• Lean.Compiler.LCNF.collectLocalDeclsArg s Lean.Compiler.LCNF.Arg.erased = s
• Lean.Compiler.LCNF.collectLocalDeclsArg s (Lean.Compiler.LCNF.Arg.type e) = Lean.Compiler.LCNF.collectLocalDeclsType s e
• Lean.Compiler.LCNF.collectLocalDeclsArg s (Lean.Compiler.LCNF.Arg.fvar fvarId) = Std.HashSet.insert s fvarId

def Lean.Compiler.LCNF.collectLocalDeclsArgs (s : UsedLocalDecls) (args : Array Arg) : UsedLocalDecls

Equations

• Lean.Compiler.LCNF.collectLocalDeclsArgs s args = Array.foldl Lean.Compiler.LCNF.collectLocalDeclsArg s args

def Lean.Compiler.LCNF.collectLocalDeclsLetValue (s : UsedLocalDecls) (e : LetValue) : UsedLocalDecls

Equations

• Lean.Compiler.LCNF.collectLocalDeclsLetValue s Lean.Compiler.LCNF.LetValue.erased = s
• Lean.Compiler.LCNF.collectLocalDeclsLetValue s (Lean.Compiler.LCNF.LetValue.lit value) = s
• Lean.Compiler.LCNF.collectLocalDeclsLetValue s (Lean.Compiler.LCNF.LetValue.proj typeName idx fvarId) = Std.HashSet.insert s fvarId
• Lean.Compiler.LCNF.collectLocalDeclsLetValue s (Lean.Compiler.LCNF.LetValue.const declName us args) = Lean.Compiler.LCNF.collectLocalDeclsArgs s args
• Lean.Compiler.LCNF.collectLocalDeclsLetValue s (Lean.Compiler.LCNF.LetValue.fvar fvarId args) = Lean.Compiler.LCNF.collectLocalDeclsArgs (Std.HashSet.insert s fvarId) args

@[reducible, inline]

abbrev Lean.Compiler.LCNF.ElimDead.M (α : Type) : Type

Equations

• Lean.Compiler.LCNF.ElimDead.M = StateRefT' IO.RealWorld Lean.Compiler.LCNF.UsedLocalDecls Lean.Compiler.LCNF.CompilerM

partial def Lean.Compiler.LCNF.ElimDead.visitFunDecl (funDecl : FunDecl) : M FunDecl

partial def Lean.Compiler.LCNF.ElimDead.elimDead (code : Code) : M Code

def Lean.Compiler.LCNF.Code.elimDead (code : Code) : CompilerM Code

Equations

• code.elimDead = StateRefT'.run' (Lean.Compiler.LCNF.ElimDead.elimDead code) ∅

def Lean.Compiler.LCNF.Decl.elimDead (decl : Decl) : CompilerM Decl

Equations

• One or more equations did not get rendered due to their size.