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.

@[reducible, inline]

abbrev Lean.IR.MaxIndex.Collector : Type

Equations

• Lean.IR.MaxIndex.Collector = (Lean.IR.Index → Lean.IR.Index)

instance Lean.IR.MaxIndex.instAndThenCollector : AndThen Lean.IR.MaxIndex.Collector

Equations

• Lean.IR.MaxIndex.instAndThenCollector = { andThen := fun (a : Lean.IR.MaxIndex.Collector) (b : Unit → Lean.IR.MaxIndex.Collector) => Lean.IR.MaxIndex.seq a (b ()) }

partial def Lean.IR.MaxIndex.collectFnBody : Lean.IR.FnBody → Lean.IR.MaxIndex.Collector

def Lean.IR.MaxIndex.collectDecl : Lean.IR.Decl → Lean.IR.MaxIndex.Collector

Equations

• Lean.IR.MaxIndex.collectDecl (Lean.IR.Decl.fdecl f xs type b info) = HAndThen.hAndThen (Lean.IR.MaxIndex.collectParams xs) fun (x : Unit) => Lean.IR.MaxIndex.collectFnBody b
• Lean.IR.MaxIndex.collectDecl (Lean.IR.Decl.extern f xs type ext) = Lean.IR.MaxIndex.collectParams xs

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

Equations

• b.maxIndex = Lean.IR.MaxIndex.collectFnBody b 0

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

Equations

• d.maxIndex = Lean.IR.MaxIndex.collectDecl d 0

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.

@[reducible, inline]

abbrev Lean.IR.FreeIndices.Collector : Type

Equations

• Lean.IR.FreeIndices.Collector = (Lean.IR.IndexSet → Lean.IR.IndexSet → Lean.IR.IndexSet)

def Lean.IR.FreeIndices.insertParams (s : Lean.IR.IndexSet) (ys : Array Lean.IR.Param) : Lean.IR.IndexSet

Equations

• Lean.IR.FreeIndices.insertParams s ys = Array.foldl (fun (s : Lean.IR.IndexSet) (p : Lean.IR.Param) => Lean.RBTree.insert s p.x.idx) s ys

instance Lean.IR.FreeIndices.instAndThenCollector : AndThen Lean.IR.FreeIndices.Collector

Equations

• Lean.IR.FreeIndices.instAndThenCollector = { andThen := fun (a : Lean.IR.FreeIndices.Collector) (b : Unit → Lean.IR.FreeIndices.Collector) => Lean.IR.FreeIndices.seq a (b ()) }

partial def Lean.IR.FreeIndices.collectFnBody : Lean.IR.FnBody → Lean.IR.FreeIndices.Collector

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

Equations

• b.collectFreeIndices vs = Lean.IR.FreeIndices.collectFnBody b ∅ vs

def Lean.IR.FnBody.freeIndices (b : Lean.IR.FnBody) : Lean.IR.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 : Lean.IR.Index) (x : Lean.IR.VarId) : Bool

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.IR.HasIndex.visitParams (w : Lean.IR.Index) (ps : Array Lean.IR.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 : Lean.IR.Index) : Lean.IR.Expr → Bool

Equations

• 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.reset n x_1) = Lean.IR.HasIndex.visitVar w x_1
• Lean.IR.HasIndex.visitExpr w (Lean.IR.Expr.reuse x_1 i updtHeader ys) = (Lean.IR.HasIndex.visitVar w x_1 || Lean.IR.HasIndex.visitArgs w ys)
• Lean.IR.HasIndex.visitExpr w (Lean.IR.Expr.proj i x_1) = Lean.IR.HasIndex.visitVar w x_1
• Lean.IR.HasIndex.visitExpr w (Lean.IR.Expr.uproj i x_1) = Lean.IR.HasIndex.visitVar w x_1
• Lean.IR.HasIndex.visitExpr w (Lean.IR.Expr.sproj n offset x_1) = Lean.IR.HasIndex.visitVar w x_1
• 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_1 ys) = (Lean.IR.HasIndex.visitVar w x_1 || Lean.IR.HasIndex.visitArgs w ys)
• Lean.IR.HasIndex.visitExpr w (Lean.IR.Expr.box ty x_1) = Lean.IR.HasIndex.visitVar w x_1
• Lean.IR.HasIndex.visitExpr w (Lean.IR.Expr.unbox x_1) = Lean.IR.HasIndex.visitVar w x_1
• Lean.IR.HasIndex.visitExpr w (Lean.IR.Expr.lit v) = false
• Lean.IR.HasIndex.visitExpr w (Lean.IR.Expr.isShared x_1) = Lean.IR.HasIndex.visitVar w x_1

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

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

Equations

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

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

Equations

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

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

Equations

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