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.

@[reducible, inline]

abbrev Lean.IR.IsLive.M (α : Type) : Type

We use State Context instead of ReaderT Context Id because we remove non local joint 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

@[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)

@[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)

@[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)

@[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)

@[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)

partial def Lean.IR.IsLive.visitFnBody (w : Index) : FnBody → M Bool

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

@[reducible, inline]

abbrev Lean.IR.LiveVarSet : Type

Equations

• Lean.IR.LiveVarSet = Lean.IR.VarIdSet

@[reducible, inline]

abbrev Lean.IR.JPLiveVarMap : Type

Equations

• Lean.IR.JPLiveVarMap = Lean.RBMap Lean.IR.JoinPointId Lean.IR.LiveVarSet fun (j₁ j₂ : Lean.IR.JoinPointId) => compare j₁.idx j₂.idx

instance Lean.IR.instInhabitedLiveVarSet : Inhabited LiveVarSet

Equations

• Lean.IR.instInhabitedLiveVarSet = { default := ∅ }

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

Equations

• Lean.IR.mkLiveVarSet x = Lean.RBTree.empty.insert x

@[reducible, inline]

abbrev Lean.IR.LiveVars.Collector : Type

Equations

• Lean.IR.LiveVars.Collector = (Lean.IR.LiveVarSet → Lean.IR.LiveVarSet)

def Lean.IR.LiveVars.collectExpr : Expr → Collector

Equations

• Lean.IR.LiveVars.collectExpr (Lean.IR.Expr.ctor i ys) = Lean.IR.LiveVars.collectArgs✝ ys
• Lean.IR.LiveVars.collectExpr (Lean.IR.Expr.reset n x_1) = Lean.IR.LiveVars.collectVar✝ x_1
• Lean.IR.LiveVars.collectExpr (Lean.IR.Expr.reuse x_1 i updtHeader ys) = Lean.IR.LiveVars.collectVar✝ x_1 ∘ Lean.IR.LiveVars.collectArgs✝ ys
• Lean.IR.LiveVars.collectExpr (Lean.IR.Expr.proj i x_1) = Lean.IR.LiveVars.collectVar✝ x_1
• Lean.IR.LiveVars.collectExpr (Lean.IR.Expr.uproj i x_1) = Lean.IR.LiveVars.collectVar✝ x_1
• Lean.IR.LiveVars.collectExpr (Lean.IR.Expr.sproj n offset x_1) = Lean.IR.LiveVars.collectVar✝ x_1
• Lean.IR.LiveVars.collectExpr (Lean.IR.Expr.fap c ys) = Lean.IR.LiveVars.collectArgs✝ ys
• Lean.IR.LiveVars.collectExpr (Lean.IR.Expr.pap c ys) = Lean.IR.LiveVars.collectArgs✝ ys
• Lean.IR.LiveVars.collectExpr (Lean.IR.Expr.ap x_1 ys) = Lean.IR.LiveVars.collectVar✝ x_1 ∘ Lean.IR.LiveVars.collectArgs✝ ys
• Lean.IR.LiveVars.collectExpr (Lean.IR.Expr.box ty x_1) = Lean.IR.LiveVars.collectVar✝ x_1
• Lean.IR.LiveVars.collectExpr (Lean.IR.Expr.unbox x_1) = Lean.IR.LiveVars.collectVar✝ x_1
• Lean.IR.LiveVars.collectExpr (Lean.IR.Expr.lit v) = Lean.IR.LiveVars.skip✝
• Lean.IR.LiveVars.collectExpr (Lean.IR.Expr.isShared x_1) = Lean.IR.LiveVars.collectVar✝ x_1

partial def Lean.IR.LiveVars.collectFnBody : FnBody → JPLiveVarMap → Collector

def Lean.IR.LiveVars.updateJPLiveVarMap (j : JoinPointId) (ys : Array Param) (v : FnBody) (m : JPLiveVarMap) : JPLiveVarMap

Equations

• Lean.IR.updateJPLiveVarMap j ys v m = Lean.RBMap.insert m j ((Lean.IR.LiveVars.bindParams✝ ys ∘ Lean.IR.LiveVars.collectFnBody v m) ∅)

def Lean.IR.updateLiveVars (e : Expr) (v : LiveVarSet) : LiveVarSet

Equations

• Lean.IR.updateLiveVars e v = Lean.IR.LiveVars.collectExpr e v

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

Equations

• Lean.IR.collectLiveVars b m v = Lean.IR.LiveVars.collectFnBody b m v