Documentation

Lean.Compiler.IR.LiveVars

@[inline]

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

Type

Equations

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

@[inline]

abbrev Lean.IR.IsLive.visitVar (w : Lean.IR.Index) (x : Lean.IR.VarId) :

Lean.IR.IsLive.M Bool

Equations

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

@[inline]

abbrev Lean.IR.IsLive.visitJP (w : Lean.IR.Index) (x : Lean.IR.JoinPointId) :

Lean.IR.IsLive.M Bool

Equations

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

@[inline]

abbrev Lean.IR.IsLive.visitArg (w : Lean.IR.Index) (a : Lean.IR.Arg) :

Lean.IR.IsLive.M Bool

Equations

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

@[inline]

abbrev Lean.IR.IsLive.visitArgs (w : Lean.IR.Index) (as : Array Lean.IR.Arg) :

Lean.IR.IsLive.M Bool

Equations

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

@[inline]

abbrev Lean.IR.IsLive.visitExpr (w : Lean.IR.Index) (e : Lean.IR.Expr) :

Lean.IR.IsLive.M Bool

Equations

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

partial def Lean.IR.IsLive.visitFnBody (w : Lean.IR.Index) :

Lean.IR.FnBody → Lean.IR.IsLive.M Bool

def Lean.IR.FnBody.hasLiveVar (b : Lean.IR.FnBody) (ctx : Lean.IR.LocalContext) (x : Lean.IR.VarId) :

Equations

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

@[inline]

abbrev Lean.IR.LiveVarSet :

Type

Equations

Lean.IR.LiveVarSet = Lean.IR.VarIdSet

@[inline]

abbrev Lean.IR.JPLiveVarMap :

Type

Equations

Lean.IR.JPLiveVarMap = Std.RBMap Lean.IR.JoinPointId Lean.IR.LiveVarSet fun j₁ j₂ => compare j₁.idx j₂.idx

instance Lean.IR.instInhabitedLiveVarSet :

Inhabited Lean.IR.LiveVarSet

Equations

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

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

Lean.IR.LiveVarSet

Equations

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

@[inline]

abbrev Lean.IR.LiveVars.Collector :

Type

Equations

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

def Lean.IR.LiveVars.collectExpr :

Lean.IR.Expr → Lean.IR.LiveVars.Collector

Equations

Lean.IR.LiveVars.collectExpr x = match x with | Lean.IR.Expr.ctor x ys => Lean.IR.LiveVars.collectArgs ys | Lean.IR.Expr.reset x x_1 => Lean.IR.LiveVars.collectVar x_1 | Lean.IR.Expr.reuse x x_1 x_2 ys => Lean.IR.LiveVars.collectVar x ∘ Lean.IR.LiveVars.collectArgs ys | Lean.IR.Expr.proj x x_1 => Lean.IR.LiveVars.collectVar x_1 | Lean.IR.Expr.uproj x x_1 => Lean.IR.LiveVars.collectVar x_1 | Lean.IR.Expr.sproj x x_1 x_2 => Lean.IR.LiveVars.collectVar x_2 | Lean.IR.Expr.fap x ys => Lean.IR.LiveVars.collectArgs ys | Lean.IR.Expr.pap x ys => Lean.IR.LiveVars.collectArgs ys | Lean.IR.Expr.ap x ys => Lean.IR.LiveVars.collectVar x ∘ Lean.IR.LiveVars.collectArgs ys | Lean.IR.Expr.box x x_1 => Lean.IR.LiveVars.collectVar x_1 | Lean.IR.Expr.unbox x => Lean.IR.LiveVars.collectVar x | Lean.IR.Expr.lit v => Lean.IR.LiveVars.skip | Lean.IR.Expr.isShared x => Lean.IR.LiveVars.collectVar x | Lean.IR.Expr.isTaggedPtr x => Lean.IR.LiveVars.collectVar x

partial def Lean.IR.LiveVars.collectFnBody :

Lean.IR.FnBody → Lean.IR.JPLiveVarMap → Lean.IR.LiveVars.Collector

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

Lean.IR.JPLiveVarMap

Equations

Lean.IR.updateJPLiveVarMap j ys v m = let jLiveVars := Function.comp (Lean.IR.LiveVars.bindParams ys) (Lean.IR.LiveVars.collectFnBody v m) ∅; Std.RBMap.insert m j jLiveVars

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

Lean.IR.LiveVarSet

Equations

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

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

Lean.IR.LiveVarSet

Equations

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