Lean.Compiler.IR.NormIds

source

@[inline, reducible]

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

Type

Instances For

source

def Lean.IR.UniqueIds.checkId (id : Lean.IR.Index) :

Lean.IR.UniqueIds.M Bool

Instances For

source

def Lean.IR.UniqueIds.checkParams (ps : Array Lean.IR.Param) :

Lean.IR.UniqueIds.M Bool

Instances For

source

partial def Lean.IR.UniqueIds.checkFnBody :

Lean.IR.FnBody → Lean.IR.UniqueIds.M Bool

source

def Lean.IR.UniqueIds.checkDecl :

Lean.IR.Decl → Lean.IR.UniqueIds.M Bool

Instances For

source

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

Bool

Return true if variable, parameter and join point ids are unique

Instances For

source

@[inline, reducible]

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

Type

Instances For

source

def Lean.IR.NormalizeIds.normIndex (x : Lean.IR.Index) :

Lean.IR.NormalizeIds.M Lean.IR.Index

Instances For

source

def Lean.IR.NormalizeIds.normVar (x : Lean.IR.VarId) :

Lean.IR.NormalizeIds.M Lean.IR.VarId

Instances For

source

def Lean.IR.NormalizeIds.normJP (x : Lean.IR.JoinPointId) :

Lean.IR.NormalizeIds.M Lean.IR.JoinPointId

Instances For

source

def Lean.IR.NormalizeIds.normArg :

Lean.IR.Arg → Lean.IR.NormalizeIds.M Lean.IR.Arg

Instances For

source

def Lean.IR.NormalizeIds.normArgs (as : Array Lean.IR.Arg) :

Lean.IR.NormalizeIds.M (Array Lean.IR.Arg)

Instances For

source

def Lean.IR.NormalizeIds.normExpr :

Lean.IR.Expr → Lean.IR.NormalizeIds.M Lean.IR.Expr

Instances For

source

@[inline, reducible]

abbrev Lean.IR.NormalizeIds.N (α : Type) :

Type

Instances For

source

@[inline]

def Lean.IR.NormalizeIds.withVar {α : Type} (x : Lean.IR.VarId) (k : Lean.IR.VarId → Lean.IR.NormalizeIds.N α) :

Lean.IR.NormalizeIds.N α

Instances For

source

@[inline]

def Lean.IR.NormalizeIds.withJP {α : Type} (x : Lean.IR.JoinPointId) (k : Lean.IR.JoinPointId → Lean.IR.NormalizeIds.N α) :

Lean.IR.NormalizeIds.N α

Instances For

source

@[inline]

def Lean.IR.NormalizeIds.withParams {α : Type} (ps : Array Lean.IR.Param) (k : Array Lean.IR.Param → Lean.IR.NormalizeIds.N α) :

Lean.IR.NormalizeIds.N α

Instances For

source

instance Lean.IR.NormalizeIds.instMonadLiftMN :

MonadLift Lean.IR.NormalizeIds.M Lean.IR.NormalizeIds.N

source

partial def Lean.IR.NormalizeIds.normFnBody :

Lean.IR.FnBody → Lean.IR.NormalizeIds.N Lean.IR.FnBody

source

def Lean.IR.NormalizeIds.normDecl (d : Lean.IR.Decl) :

Lean.IR.NormalizeIds.N Lean.IR.Decl

Instances For

source

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

Lean.IR.Decl

Create a declaration equivalent to d s.t. d.normalizeIds.uniqueIds == true

Instances For

Apply a function f : VarId → VarId to variable occurrences. The following functions assume the IR code does not have variable shadowing.

source

@[inline]

def Lean.IR.MapVars.mapArg (f : Lean.IR.VarId → Lean.IR.VarId) :

Lean.IR.Arg → Lean.IR.Arg

Instances For

source

def Lean.IR.MapVars.mapArgs (f : Lean.IR.VarId → Lean.IR.VarId) (as : Array Lean.IR.Arg) :

Array Lean.IR.Arg

Instances For

source

def Lean.IR.MapVars.mapExpr (f : Lean.IR.VarId → Lean.IR.VarId) :

Lean.IR.Expr → Lean.IR.Expr

Instances For

source

partial def Lean.IR.MapVars.mapFnBody (f : Lean.IR.VarId → Lean.IR.VarId) :

Lean.IR.FnBody → Lean.IR.FnBody

source

@[inline]

def Lean.IR.FnBody.mapVars (f : Lean.IR.VarId → Lean.IR.VarId) (b : Lean.IR.FnBody) :

Lean.IR.FnBody

Instances For

source

def Lean.IR.FnBody.replaceVar (x : Lean.IR.VarId) (y : Lean.IR.VarId) (b : Lean.IR.FnBody) :

Lean.IR.FnBody

Replace x with y in b. This function assumes b does not shadow x

Instances For