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

instance Lean.IR.MaxIndex.instAndThenCollector : AndThen Collector

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

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

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

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

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

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

instance Lean.IR.FreeIndices.instAndThenCollector : AndThen Collector

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

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

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

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

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

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

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

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

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

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

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

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

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