Lean.Compiler.IR.NormIds

source

@[inline]

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

Type

Equations

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

source

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

Lean.IR.UniqueIds.M Bool

Equations

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

source

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

Lean.IR.UniqueIds.M Bool

Equations

Lean.IR.UniqueIds.checkParams ps = Array.allM (fun p => Lean.IR.UniqueIds.checkId p.x.idx) ps 0 (Array.size ps)

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

Equations

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

source

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

Bool

Equations

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

source

@[inline]

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

Type

Equations

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

source

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

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

Equations

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

source

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

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

Equations

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

source

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

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

Equations

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

source

def Lean.IR.NormalizeIds.normArg:

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

Equations

Lean.IR.NormalizeIds.normArg _fun_discr = match _fun_discr with | Lean.IR.Arg.var x => Lean.IR.Arg.var <$> Lean.IR.NormalizeIds.normVar x | other => pure other

source

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

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

Equations

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

source

def Lean.IR.NormalizeIds.normExpr:

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

Equations

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

source

@[inline]

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

Type

Equations

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

source

@[inline]

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

Lean.IR.NormalizeIds.N α

Equations

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

source

@[inline]

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

Lean.IR.NormalizeIds.N α

Equations

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

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 α

Equations

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

source

instance Lean.IR.NormalizeIds.instMonadLiftMN:

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

Equations

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

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

Equations

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

source

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

Lean.IR.Decl

Equations

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

source

@[inline]

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

Lean.IR.Arg → Lean.IR.Arg

Equations

Lean.IR.MapVars.mapArg f _fun_discr = match _fun_discr with | Lean.IR.Arg.var x => Lean.IR.Arg.var (f x) | a => a

source

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

Array Lean.IR.Arg

Equations

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

source

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

Lean.IR.Expr → Lean.IR.Expr

Equations

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

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

Equations

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

source

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

Lean.IR.FnBody

Equations

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