Documentation

Lean.Compiler.IR.FreeVars

@[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 b => 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

One or more equations did not get rendered due to their size.

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

Equations

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

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

Equations

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

@[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 p => Std.RBTree.insert s p.x.idx) s ys 0 (Array.size ys)

instance Lean.IR.FreeIndices.instAndThenCollector:

AndThen Lean.IR.FreeIndices.Collector

Equations

Lean.IR.FreeIndices.instAndThenCollector = { andThen := fun a b => 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

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

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

Lean.IR.IndexSet

Equations

Lean.IR.FnBody.freeIndices b = Lean.IR.FnBody.collectFreeIndices b ∅

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

Equations

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

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

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 _fun_discr = match _fun_discr with | Lean.IR.Arg.var x => Lean.IR.HasIndex.visitVar w x | x => false

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

Equations

Lean.IR.HasIndex.visitArgs w xs = Array.any xs (Lean.IR.HasIndex.visitArg w) 0 (Array.size xs)

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

Equations

Lean.IR.HasIndex.visitParams w ps = Array.any ps (fun p => w == p.x.idx) 0 (Array.size ps)

def Lean.IR.HasIndex.visitExpr (w : Lean.IR.Index) :

Lean.IR.Expr → Bool

Equations

One or more equations did not get rendered due to their size.

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) :

Equations

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

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

Equations

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

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

Equations

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