@[inline]
Equations
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)
Equations
- Lean.IR.UniqueIds.checkParams ps = Array.allM (fun p => Lean.IR.UniqueIds.checkId p.x.idx) ps 0 (Array.size ps)
Equations
- Lean.IR.UniqueIds.checkDecl x = match x with | Lean.IR.Decl.fdecl x xs x_1 b x_2 => Lean.IR.UniqueIds.checkParams xs <&&> Lean.IR.UniqueIds.checkFnBody b | Lean.IR.Decl.extern x xs x_1 x_2 => Lean.IR.UniqueIds.checkParams xs
Equations
@[inline]
Equations
Equations
- Lean.IR.NormalizeIds.normIndex x m = match Std.RBMap.find? m x with | some y => y | none => x
Equations
- Lean.IR.NormalizeIds.normArg x = match x with | Lean.IR.Arg.var x => Lean.IR.Arg.var <$> Lean.IR.NormalizeIds.normVar x | other => pure other
Equations
- Lean.IR.NormalizeIds.normArgs as m = Array.map (fun a => Lean.IR.NormalizeIds.normArg a m) as
Equations
- Lean.IR.NormalizeIds.normExpr x x = match x, x with | Lean.IR.Expr.ctor c ys, m => Lean.IR.Expr.ctor c (Lean.IR.NormalizeIds.normArgs ys m) | Lean.IR.Expr.reset n x, m => Lean.IR.Expr.reset n (Lean.IR.NormalizeIds.normVar x m) | Lean.IR.Expr.reuse x c u ys, m => Lean.IR.Expr.reuse (Lean.IR.NormalizeIds.normVar x m) c u (Lean.IR.NormalizeIds.normArgs ys m) | Lean.IR.Expr.proj i x, m => Lean.IR.Expr.proj i (Lean.IR.NormalizeIds.normVar x m) | Lean.IR.Expr.uproj i x, m => Lean.IR.Expr.uproj i (Lean.IR.NormalizeIds.normVar x m) | Lean.IR.Expr.sproj n o x, m => Lean.IR.Expr.sproj n o (Lean.IR.NormalizeIds.normVar x m) | Lean.IR.Expr.fap c ys, m => Lean.IR.Expr.fap c (Lean.IR.NormalizeIds.normArgs ys m) | Lean.IR.Expr.pap c ys, m => Lean.IR.Expr.pap c (Lean.IR.NormalizeIds.normArgs ys m) | Lean.IR.Expr.ap x ys, m => Lean.IR.Expr.ap (Lean.IR.NormalizeIds.normVar x m) (Lean.IR.NormalizeIds.normArgs ys m) | Lean.IR.Expr.box t x, m => Lean.IR.Expr.box t (Lean.IR.NormalizeIds.normVar x m) | Lean.IR.Expr.unbox x, m => Lean.IR.Expr.unbox (Lean.IR.NormalizeIds.normVar x m) | Lean.IR.Expr.isShared x, m => Lean.IR.Expr.isShared (Lean.IR.NormalizeIds.normVar x m) | Lean.IR.Expr.isTaggedPtr x, m => Lean.IR.Expr.isTaggedPtr (Lean.IR.NormalizeIds.normVar x m) | e@h:(Lean.IR.Expr.lit v), m => e
@[inline]
Equations
@[inline]
def
Lean.IR.NormalizeIds.withVar
{α : Type}
(x : Lean.IR.VarId)
(k : Lean.IR.VarId → 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)
@[inline]
def
Lean.IR.NormalizeIds.withJP
{α : Type}
(x : Lean.IR.JoinPointId)
(k : Lean.IR.JoinPointId → 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)
@[inline]
def
Lean.IR.NormalizeIds.withParams
{α : Type}
(ps : Array Lean.IR.Param)
(k : Array Lean.IR.Param → Lean.IR.NormalizeIds.N α)
:
Equations
- Lean.IR.NormalizeIds.withParams ps k m = do let m ← Array.foldlM (fun m p => do let n ← getModify fun n => n + 1 pure (Std.RBMap.insert m p.x.idx n)) m ps 0 (Array.size ps) let ps : Array Lean.IR.Param := Array.map (fun p => { x := Lean.IR.NormalizeIds.normVar p.x m, borrow := p.borrow, ty := p.ty }) ps k ps m
Equations
- Lean.IR.NormalizeIds.instMonadLiftMN = { monadLift := fun {α} x m => pure (x m) }
Equations
- Lean.IR.NormalizeIds.normDecl d = match d with | Lean.IR.Decl.fdecl x xs x_1 b x_2 => Lean.IR.NormalizeIds.withParams xs fun xs => do let a ← Lean.IR.NormalizeIds.normFnBody b pure (Lean.IR.Decl.updateBody! d a) | other => pure other
Equations
@[inline]
Equations
- Lean.IR.MapVars.mapArg f x = match x with | Lean.IR.Arg.var x => Lean.IR.Arg.var (f x) | a => a
Equations
- Lean.IR.MapVars.mapArgs f as = Array.map (Lean.IR.MapVars.mapArg f) as
Equations
- Lean.IR.MapVars.mapExpr f x = match x with | Lean.IR.Expr.ctor c ys => Lean.IR.Expr.ctor c (Lean.IR.MapVars.mapArgs f ys) | Lean.IR.Expr.reset n x => Lean.IR.Expr.reset n (f x) | Lean.IR.Expr.reuse x c u ys => Lean.IR.Expr.reuse (f x) c u (Lean.IR.MapVars.mapArgs f ys) | Lean.IR.Expr.proj i x => Lean.IR.Expr.proj i (f x) | Lean.IR.Expr.uproj i x => Lean.IR.Expr.uproj i (f x) | Lean.IR.Expr.sproj n o x => Lean.IR.Expr.sproj n o (f x) | Lean.IR.Expr.fap c ys => Lean.IR.Expr.fap c (Lean.IR.MapVars.mapArgs f ys) | Lean.IR.Expr.pap c ys => Lean.IR.Expr.pap c (Lean.IR.MapVars.mapArgs f ys) | Lean.IR.Expr.ap x ys => Lean.IR.Expr.ap (f x) (Lean.IR.MapVars.mapArgs f ys) | Lean.IR.Expr.box t x => Lean.IR.Expr.box t (f x) | Lean.IR.Expr.unbox x => Lean.IR.Expr.unbox (f x) | Lean.IR.Expr.isShared x => Lean.IR.Expr.isShared (f x) | Lean.IR.Expr.isTaggedPtr x => Lean.IR.Expr.isTaggedPtr (f x) | e@h:(Lean.IR.Expr.lit v) => e
@[inline]
Equations
Equations
- Lean.IR.FnBody.replaceVar x y b = Lean.IR.FnBody.mapVars (fun z => if (x == z) = true then y else z) b