@[reducible, inline]

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

Equations

• Lean.IR.UniqueIds.M = StateT Lean.IR.IndexSet Id

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

Equations

• Lean.IR.UniqueIds.checkId id = modifyGet fun (s : Lean.IR.IndexSet) => if Lean.RBTree.contains s id = true then (false, s) else (true, Lean.RBTree.insert s id)

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

Equations

• Lean.IR.UniqueIds.checkParams ps = Array.allM (fun (p : Lean.IR.Param) => Lean.IR.UniqueIds.checkId p.x.idx) ps

partial def Lean.IR.UniqueIds.checkFnBody : FnBody → M Bool

def Lean.IR.UniqueIds.checkDecl : Decl → M Bool

Equations

• Lean.IR.UniqueIds.checkDecl (Lean.IR.Decl.fdecl f xs type b info) = (Lean.IR.UniqueIds.checkParams xs <&&> Lean.IR.UniqueIds.checkFnBody b)
• Lean.IR.UniqueIds.checkDecl (Lean.IR.Decl.extern f xs type ext) = Lean.IR.UniqueIds.checkParams xs

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

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

Equations

• d.uniqueIds = StateT.run' (Lean.IR.UniqueIds.checkDecl d) ∅

@[reducible, inline]

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

Equations

• Lean.IR.NormalizeIds.M = ReaderT Lean.IR.IndexRenaming Id

Instances For

• Lean.IR.NormalizeIds.instMonadLiftMN

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

Equations

• Lean.IR.NormalizeIds.normIndex x m = match Lean.RBMap.find? m x with | some y => y | none => x

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

Equations

• Lean.IR.NormalizeIds.normVar x = Lean.IR.VarId.mk <$> Lean.IR.NormalizeIds.normIndex x.idx

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

Equations

• Lean.IR.NormalizeIds.normJP x = Lean.IR.JoinPointId.mk <$> Lean.IR.NormalizeIds.normIndex x.idx

def Lean.IR.NormalizeIds.normArg : Arg → M Arg

Equations

• Lean.IR.NormalizeIds.normArg (Lean.IR.Arg.var x_1) = Lean.IR.Arg.var <$> Lean.IR.NormalizeIds.normVar x_1
• Lean.IR.NormalizeIds.normArg x✝ = pure x✝

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

Equations

• Lean.IR.NormalizeIds.normArgs as m = Array.map (fun (a : Lean.IR.Arg) => Lean.IR.NormalizeIds.normArg a m) as

def Lean.IR.NormalizeIds.normExpr : Expr → M Expr

Equations

• Lean.IR.NormalizeIds.normExpr (Lean.IR.Expr.ctor c ys) x✝ = Lean.IR.Expr.ctor c (Lean.IR.NormalizeIds.normArgs ys x✝)
• Lean.IR.NormalizeIds.normExpr (Lean.IR.Expr.reset n x_2) x✝ = Lean.IR.Expr.reset n (Lean.IR.NormalizeIds.normVar x_2 x✝)
• Lean.IR.NormalizeIds.normExpr (Lean.IR.Expr.reuse x_2 c u ys) x✝ = Lean.IR.Expr.reuse (Lean.IR.NormalizeIds.normVar x_2 x✝) c u (Lean.IR.NormalizeIds.normArgs ys x✝)
• Lean.IR.NormalizeIds.normExpr (Lean.IR.Expr.proj i x_2) x✝ = Lean.IR.Expr.proj i (Lean.IR.NormalizeIds.normVar x_2 x✝)
• Lean.IR.NormalizeIds.normExpr (Lean.IR.Expr.uproj i x_2) x✝ = Lean.IR.Expr.uproj i (Lean.IR.NormalizeIds.normVar x_2 x✝)
• Lean.IR.NormalizeIds.normExpr (Lean.IR.Expr.sproj n o x_2) x✝ = Lean.IR.Expr.sproj n o (Lean.IR.NormalizeIds.normVar x_2 x✝)
• Lean.IR.NormalizeIds.normExpr (Lean.IR.Expr.fap c ys) x✝ = Lean.IR.Expr.fap c (Lean.IR.NormalizeIds.normArgs ys x✝)
• Lean.IR.NormalizeIds.normExpr (Lean.IR.Expr.pap c ys) x✝ = Lean.IR.Expr.pap c (Lean.IR.NormalizeIds.normArgs ys x✝)
• Lean.IR.NormalizeIds.normExpr (Lean.IR.Expr.ap x_2 ys) x✝ = Lean.IR.Expr.ap (Lean.IR.NormalizeIds.normVar x_2 x✝) (Lean.IR.NormalizeIds.normArgs ys x✝)
• Lean.IR.NormalizeIds.normExpr (Lean.IR.Expr.box t x_2) x✝ = Lean.IR.Expr.box t (Lean.IR.NormalizeIds.normVar x_2 x✝)
• Lean.IR.NormalizeIds.normExpr (Lean.IR.Expr.unbox x_2) x✝ = Lean.IR.Expr.unbox (Lean.IR.NormalizeIds.normVar x_2 x✝)
• Lean.IR.NormalizeIds.normExpr (Lean.IR.Expr.isShared x_2) x✝ = Lean.IR.Expr.isShared (Lean.IR.NormalizeIds.normVar x_2 x✝)
• Lean.IR.NormalizeIds.normExpr (Lean.IR.Expr.lit v) x✝ = Lean.IR.Expr.lit v

@[reducible, inline]

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

Equations

• Lean.IR.NormalizeIds.N = ReaderT Lean.IR.IndexRenaming (StateM Nat)

Instances For

• Lean.IR.NormalizeIds.instMonadLiftMN

@[inline]

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

Equations

• Lean.IR.NormalizeIds.withVar x k m = do let n ← getModify fun (n : Nat) => n + 1 k { idx := n } (Lean.RBMap.insert m x.idx n)

@[inline]

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

Equations

• Lean.IR.NormalizeIds.withJP x k m = do let n ← getModify fun (n : Nat) => n + 1 k { idx := n } (Lean.RBMap.insert m x.idx n)

@[inline]

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

Equations

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

instance Lean.IR.NormalizeIds.instMonadLiftMN : MonadLift M N

Equations

• Lean.IR.NormalizeIds.instMonadLiftMN = { monadLift := fun {α : Type} (x : Lean.IR.NormalizeIds.M α) (m : Lean.IR.IndexRenaming) => pure (x m) }

partial def Lean.IR.NormalizeIds.normFnBody : FnBody → N FnBody

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.IR.NormalizeIds.normDecl d = pure d

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

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

Equations

• d.normalizeIds = StateT.run' (Lean.IR.NormalizeIds.normDecl d ∅) 1

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

@[inline]

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

Equations

• Lean.IR.MapVars.mapArg f (Lean.IR.Arg.var x_1) = Lean.IR.Arg.var (f x_1)
• Lean.IR.MapVars.mapArg f x✝ = x✝

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

Equations

• Lean.IR.MapVars.mapArgs f as = Array.map (Lean.IR.MapVars.mapArg f) as

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

Equations

• Lean.IR.MapVars.mapExpr f (Lean.IR.Expr.ctor c ys) = Lean.IR.Expr.ctor c (Lean.IR.MapVars.mapArgs f ys)
• Lean.IR.MapVars.mapExpr f (Lean.IR.Expr.reset n x_1) = Lean.IR.Expr.reset n (f x_1)
• Lean.IR.MapVars.mapExpr f (Lean.IR.Expr.reuse x_1 c u ys) = Lean.IR.Expr.reuse (f x_1) c u (Lean.IR.MapVars.mapArgs f ys)
• Lean.IR.MapVars.mapExpr f (Lean.IR.Expr.proj i x_1) = Lean.IR.Expr.proj i (f x_1)
• Lean.IR.MapVars.mapExpr f (Lean.IR.Expr.uproj i x_1) = Lean.IR.Expr.uproj i (f x_1)
• Lean.IR.MapVars.mapExpr f (Lean.IR.Expr.sproj n o x_1) = Lean.IR.Expr.sproj n o (f x_1)
• Lean.IR.MapVars.mapExpr f (Lean.IR.Expr.fap c ys) = Lean.IR.Expr.fap c (Lean.IR.MapVars.mapArgs f ys)
• Lean.IR.MapVars.mapExpr f (Lean.IR.Expr.pap c ys) = Lean.IR.Expr.pap c (Lean.IR.MapVars.mapArgs f ys)
• Lean.IR.MapVars.mapExpr f (Lean.IR.Expr.ap x_1 ys) = Lean.IR.Expr.ap (f x_1) (Lean.IR.MapVars.mapArgs f ys)
• Lean.IR.MapVars.mapExpr f (Lean.IR.Expr.box t x_1) = Lean.IR.Expr.box t (f x_1)
• Lean.IR.MapVars.mapExpr f (Lean.IR.Expr.unbox x_1) = Lean.IR.Expr.unbox (f x_1)
• Lean.IR.MapVars.mapExpr f (Lean.IR.Expr.isShared x_1) = Lean.IR.Expr.isShared (f x_1)
• Lean.IR.MapVars.mapExpr f (Lean.IR.Expr.lit v) = Lean.IR.Expr.lit v

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

@[inline]

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

Equations

• Lean.IR.FnBody.mapVars f b = Lean.IR.MapVars.mapFnBody f b

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

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

Equations

• Lean.IR.FnBody.replaceVar x y b = Lean.IR.FnBody.mapVars (fun (z : Lean.IR.VarId) => if (x == z) = true then y else z) b