Lean.Compiler.LCNF.Simp.Used

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.markUsedLetValue letDecl.value

Instances For

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 __do_lift ← get pure (Lean.HashSet.contains __do_lift.used fvarId)

Instances For

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

Instances For

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.

Instances For