Lean.Compiler.LCNF.Simp.Used

source

def Lean.Compiler.LCNF.Simp.markUsedFVar (fvarId : Lean.FVarId) :

Lean.Compiler.LCNF.Simp.SimpM Unit

Mark fvarId as an used free variable. This is information is used to eliminate dead local declarations.

Equations

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

source

def Lean.Compiler.LCNF.Simp.markUsedExpr (e : Lean.Expr) :

Lean.Compiler.LCNF.Simp.SimpM Unit

Mark all free variables occurring in e as used. This is information is used to eliminate dead local declarations.

Equations

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

source

def Lean.Compiler.LCNF.Simp.markUsedLetDecl (letDecl : Lean.Compiler.LCNF.LetDecl) :

Lean.Compiler.LCNF.Simp.SimpM Unit

Mark all free variables occurring on the right-hand side of the given let declaration as used. This is information is used to eliminate dead local declarations.

Equations

Lean.Compiler.LCNF.Simp.markUsedLetDecl letDecl = Lean.Compiler.LCNF.Simp.markUsedExpr letDecl.value

source

partial def Lean.Compiler.LCNF.Simp.markUsedCode (code : Lean.Compiler.LCNF.Code) :

Lean.Compiler.LCNF.Simp.SimpM Unit

Mark all free variables occurring in code as used.

source

partial def Lean.Compiler.LCNF.Simp.markUsedFunDecl (funDecl : Lean.Compiler.LCNF.FunDecl) :

Lean.Compiler.LCNF.Simp.SimpM Unit

Mark all free variables occurring in funDecl as used.

source

def Lean.Compiler.LCNF.Simp.isUsed (fvarId : Lean.FVarId) :

Lean.Compiler.LCNF.Simp.SimpM Bool

Return true if fvarId is in the used set.

Equations

Lean.Compiler.LCNF.Simp.isUsed fvarId = do let a ← get pure (Lean.HashSet.contains a.used fvarId)

source

def Lean.Compiler.LCNF.Simp.attachCodeDecls (decls : Array Lean.Compiler.LCNF.CodeDecl) (code : Lean.Compiler.LCNF.Code) :

Lean.Compiler.LCNF.Simp.SimpM Lean.Compiler.LCNF.Code

Attach the given decls to code. For example, assume decls is #[.let _x.1 := 10, .let _x.2 := true], then the result is

let _x.1 := 10
let _x.2 := true

Equations

Lean.Compiler.LCNF.Simp.attachCodeDecls decls code = Lean.Compiler.LCNF.Simp.attachCodeDecls.go decls (Array.size decls) code

source

def
Lean.Compiler.LCNF.Simp.attachCodeDecls.go
(decls : Array Lean.Compiler.LCNF.CodeDecl)

(i : Nat)

(code : Lean.Compiler.LCNF.Code)
 :Lean.Compiler.LCNF.Simp.SimpM Lean.Compiler.LCNF.Code

Equations

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