Remark: in the paper "Counting Immutable Beans" the concepts of free and live variables coincide because the paper does not consider join points. For example, consider the function body `B`

    let x := ctor_0;
    jmp block_1 x

in a context where we have the join point `block_1` defined as

    block_1 (x : obj) : obj :=
    let z := ctor_0 x y;
    ret z

The variable `y` is live in the function body `B` since it occurs in `block_1` which is "invoked" by `B`.

source
@[reducible, inline]
abbrev Lean.IR.IsLive.M (α : Type) :
Type

We use `State Context` instead of `ReaderT Context Id` because we remove non local join points from `Context` whenever we visit them instead of maintaining a set of visited non local join points.

Remark: we don't need to track local join points because we assume there is no variable or join point shadowing in our IR.

Equations

- Lean.IR.IsLive.M = StateM Lean.IR.LocalContext

Instances For

source
@[reducible, inline]
abbrev Lean.IR.IsLive.visitVar (w : Index) (x : VarId) :
M Bool
Equations

- Lean.IR.IsLive.visitVar w x = pure (Lean.IR.HasIndex.visitVar w x)

Instances For

source
@[reducible, inline]
abbrev Lean.IR.IsLive.visitJP (w : Index) (x : JoinPointId) :
M Bool
Equations

- Lean.IR.IsLive.visitJP w x = pure (Lean.IR.HasIndex.visitJP w x)

Instances For

source
@[reducible, inline]
abbrev Lean.IR.IsLive.visitArg (w : Index) (a : Arg) :
M Bool
Equations

- Lean.IR.IsLive.visitArg w a = pure (Lean.IR.HasIndex.visitArg w a)

Instances For

source
@[reducible, inline]
abbrev Lean.IR.IsLive.visitArgs (w : Index) (as : Array Arg) :
M Bool
Equations

- Lean.IR.IsLive.visitArgs w as = pure (Lean.IR.HasIndex.visitArgs w as)

Instances For

source
@[reducible, inline]
abbrev Lean.IR.IsLive.visitExpr (w : Index) (e : Expr) :
M Bool
Equations

- Lean.IR.IsLive.visitExpr w e = pure (Lean.IR.HasIndex.visitExpr w e)

Instances For

source
partial def Lean.IR.IsLive.visitFnBody (w : Index) :
FnBody → M Bool
source
def Lean.IR.FnBody.hasLiveVar (b : FnBody) (ctx : LocalContext) (x : VarId) :
Bool

Return true if `x` is live in the function body `b` in the context `ctx`.

Remark: the context only needs to contain all (free) join point declarations.

Recall that we say that a join point `j` is free in `b` if `b` contains `FnBody.jmp j ys` and `j` is not local.

Equations

- b.hasLiveVar ctx x = StateT.run' (Lean.IR.IsLive.visitFnBody x.idx b) ctx

Instances For

source
@[reducible, inline]
abbrev Lean.IR.LiveVarSet :
Type
Equations

- Lean.IR.LiveVarSet = Lean.IR.VarIdSet

Instances For

source
@[reducible, inline]
abbrev Lean.IR.JPLiveVarMap :
Type
Equations

- Lean.IR.JPLiveVarMap = Std.TreeMap Lean.IR.JoinPointId Lean.IR.LiveVarSet fun (j₁ j₂ : Lean.IR.JoinPointId) => compare j₁.idx j₂.idx

Instances For

source
def Lean.IR.mkLiveVarSet (x : VarId) :
LiveVarSet
Equations

- Lean.IR.mkLiveVarSet x = Std.TreeSet.empty.insert x

Instances For

source
structure Lean.IR.LiveVars.State :
Type

- liveVars : LiveVarSet

Instances For

source
@[reducible, inline]
abbrev Lean.IR.LiveVars.M (α : Type) :
Type
Equations

- Lean.IR.LiveVars.M = StateM Lean.IR.LiveVars.State

Instances For

source
partial def Lean.IR.LiveVars.updateJPLiveVarMap (j : JoinPointId) (ys : Array Param) (v : FnBody) (m : JPLiveVarMap) :
JPLiveVarMap
source
def Lean.IR.updateLiveVars (e : Expr) (v : LiveVarSet) :
LiveVarSet
Equations

- Lean.IR.updateLiveVars e v = match StateT.run (Lean.IR.LiveVars.useExpr✝ e) { liveVars := v } with | (fst, { liveVars := liveVars }) => liveVars

Instances For

source
def Lean.IR.collectLiveVars (b : FnBody) (m : JPLiveVarMap) (v : LiveVarSet := ∅) :
LiveVarSet
Equations

- Lean.IR.collectLiveVars b m v = match StateT.run (Lean.IR.LiveVars.visitFnBody✝ b m) { liveVars := v } with | (fst, { liveVars := liveVars }) => liveVars

Instances For