This file implements an auxiliary algorithm to determine whether a variable is live (that is, might be used during execution) in a piece of impure LCNF code. This information is relevant to determine potential reset-reuse pairs. Note that this algorithm assumes the piece of code it is operating on has already been internalized.

The key difference of this algorithm compared to dependsOn is that it also considers non-syntactic uses.

For example, given a piece of code B:

let x : = ...;
jmp jp1 x

where jp1 is defined to be:

jp jp1 x :=
  let res := f x y
  return res;

this algorithm will identify y as being live in B because it is used through the jump to jp1.

def Lean.Compiler.LCNF.Code.isFVarLiveIn (c : Code Purity.impure) (fvarId : FVarId) : CompilerM Bool

Determine whether fvarId is live in c. Assumes that c and all of its transitively reachable join-points are internalized.

Equations

• c.isFVarLiveIn fvarId = (ReaderT.run (Lean.Compiler.LCNF.Code.isFVarLiveIn.go✝ fvarId c) { targetSet := {fvarId}, targetId := fvarId }).run' { }