Compute the maximum index M used in a declaration. We M to initialize the fresh index generator used to create fresh variable and join point names.

Recall that we variable and join points share the same namespace in our implementation.

structure Lean.IR.MaxIndex.State : Type

• currentMax : Nat

@[reducible, inline]

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

Equations

• Lean.IR.MaxIndex.M = StateM Lean.IR.MaxIndex.State

partial def Lean.IR.MaxIndex.visitFnBody (fnBody : FnBody) : M Unit

def Lean.IR.FnBody.maxIndex (b : FnBody) : Index

Equations

• b.maxIndex = (match StateT.run (Lean.IR.MaxIndex.visitFnBody b) { } with | (fst, { currentMax := currentMax }) => pure currentMax).run

def Lean.IR.Decl.maxIndex (d : Decl) : Index

Equations

• d.maxIndex = (match StateT.run (Lean.IR.MaxIndex.visitDecl✝ d) { } with | (fst, { currentMax := currentMax }) => pure currentMax).run

We say a variable (join point) index (aka name) is free in a function body if there isn't a FnBody.vdecl (Fnbody.jdecl) binding it.

structure Lean.IR.FreeIndices.State : Type

• freeIndices : IndexSet

@[reducible, inline]

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

Equations

• Lean.IR.FreeIndices.M = StateM Lean.IR.FreeIndices.State

partial def Lean.IR.FreeIndices.visitFnBody (fnBody : FnBody) : M Unit

def Lean.IR.FnBody.collectFreeIndices (b : FnBody) (init : IndexSet) : IndexSet

Equations

• b.collectFreeIndices init = (match StateT.run (Lean.IR.FreeIndices.visitFnBody b) { freeIndices := init } with | (fst, { freeIndices := freeIndices }) => pure freeIndices).run

def Lean.IR.FnBody.freeIndices (b : FnBody) : IndexSet

Equations

• b.freeIndices = b.collectFreeIndices ∅

In principle, we can check whether a function body b contains an index i using b.freeIndices.contains i, but it is more efficient to avoid the construction of the set of freeIndices and just search whether i occurs in b or not.

def Lean.IR.HasIndex.visitVar (w : Index) (x : VarId) : Bool

Equations

• Lean.IR.HasIndex.visitVar w x = (w == x.idx)

def Lean.IR.HasIndex.visitJP (w : Index) (x : JoinPointId) : Bool

Equations

• Lean.IR.HasIndex.visitJP w x = (w == x.idx)

def Lean.IR.HasIndex.visitArg (w : Index) : Arg → Bool

Equations

• Lean.IR.HasIndex.visitArg w (Lean.IR.Arg.var x) = Lean.IR.HasIndex.visitVar w x
• Lean.IR.HasIndex.visitArg w Lean.IR.Arg.erased = false

def Lean.IR.HasIndex.visitArgs (w : Index) (xs : Array Arg) : Bool

Equations

• Lean.IR.HasIndex.visitArgs w xs = xs.any (Lean.IR.HasIndex.visitArg w)

def Lean.IR.HasIndex.visitParams (w : Index) (ps : Array Param) : Bool

Equations

• Lean.IR.HasIndex.visitParams w ps = ps.any fun (p : Lean.IR.Param) => w == p.x.idx

def Lean.IR.HasIndex.visitExpr (w : Index) : Expr → Bool

Equations

• Lean.IR.HasIndex.visitExpr w (Lean.IR.Expr.proj i x) = Lean.IR.HasIndex.visitVar w x
• Lean.IR.HasIndex.visitExpr w (Lean.IR.Expr.uproj i x) = Lean.IR.HasIndex.visitVar w x
• Lean.IR.HasIndex.visitExpr w (Lean.IR.Expr.sproj n offset x) = Lean.IR.HasIndex.visitVar w x
• Lean.IR.HasIndex.visitExpr w (Lean.IR.Expr.box ty x) = Lean.IR.HasIndex.visitVar w x
• Lean.IR.HasIndex.visitExpr w (Lean.IR.Expr.unbox x) = Lean.IR.HasIndex.visitVar w x
• Lean.IR.HasIndex.visitExpr w (Lean.IR.Expr.reset n x) = Lean.IR.HasIndex.visitVar w x
• Lean.IR.HasIndex.visitExpr w (Lean.IR.Expr.isShared x) = Lean.IR.HasIndex.visitVar w x
• Lean.IR.HasIndex.visitExpr w (Lean.IR.Expr.ctor i ys) = Lean.IR.HasIndex.visitArgs w ys
• Lean.IR.HasIndex.visitExpr w (Lean.IR.Expr.fap c ys) = Lean.IR.HasIndex.visitArgs w ys
• Lean.IR.HasIndex.visitExpr w (Lean.IR.Expr.pap c ys) = Lean.IR.HasIndex.visitArgs w ys
• Lean.IR.HasIndex.visitExpr w (Lean.IR.Expr.ap x ys) = (Lean.IR.HasIndex.visitVar w x || Lean.IR.HasIndex.visitArgs w ys)
• Lean.IR.HasIndex.visitExpr w (Lean.IR.Expr.reuse x i updtHeader ys) = (Lean.IR.HasIndex.visitVar w x || Lean.IR.HasIndex.visitArgs w ys)
• Lean.IR.HasIndex.visitExpr w (Lean.IR.Expr.lit v) = false

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

def Lean.IR.Arg.hasFreeVar (arg : Arg) (x : VarId) : Bool

Equations

• arg.hasFreeVar x = Lean.IR.HasIndex.visitArg x.idx arg

def Lean.IR.Expr.hasFreeVar (e : Expr) (x : VarId) : Bool

Equations

• e.hasFreeVar x = Lean.IR.HasIndex.visitExpr x.idx e

def Lean.IR.FnBody.hasFreeVar (b : FnBody) (x : VarId) : Bool

Equations

• b.hasFreeVar x = Lean.IR.HasIndex.visitFnBody x.idx b