Implements (extended) λPure and λRc proposed in the article "Counting Immutable Beans", Sebastian Ullrich and Leonardo de Moura.

The Lean to IR transformation produces λPure code, and this part is implemented in C++. The procedures described in the paper above are implemented in Lean.

@[reducible, inline]

abbrev Lean.IR.FunId : Type

Function identifier

Equations

• Lean.IR.FunId = Lean.Name

@[reducible, inline]

abbrev Lean.IR.Index : Type

Equations

• Lean.IR.Index = Nat

structure Lean.IR.VarId : Type

Variable identifier

• idx : Index

instance Lean.IR.instInhabitedVarId : Inhabited VarId

Equations

• Lean.IR.instInhabitedVarId = { default := { idx := default } }

instance Lean.IR.instBEqVarId : BEq VarId

Equations

• Lean.IR.instBEqVarId = { beq := Lean.IR.beqVarId✝ }

instance Lean.IR.instHashableVarId : Hashable VarId

Equations

• Lean.IR.instHashableVarId = { hash := Lean.IR.hashVarId✝ }

instance Lean.IR.instReprVarId : Repr VarId

Equations

• Lean.IR.instReprVarId = { reprPrec := Lean.IR.reprVarId✝ }

structure Lean.IR.JoinPointId : Type

Join point identifier

• idx : Index

instance Lean.IR.instInhabitedJoinPointId : Inhabited JoinPointId

Equations

• Lean.IR.instInhabitedJoinPointId = { default := { idx := default } }

instance Lean.IR.instBEqJoinPointId : BEq JoinPointId

Equations

• Lean.IR.instBEqJoinPointId = { beq := Lean.IR.beqJoinPointId✝ }

instance Lean.IR.instHashableJoinPointId : Hashable JoinPointId

Equations

• Lean.IR.instHashableJoinPointId = { hash := Lean.IR.hashJoinPointId✝ }

instance Lean.IR.instReprJoinPointId : Repr JoinPointId

Equations

• Lean.IR.instReprJoinPointId = { reprPrec := Lean.IR.reprJoinPointId✝ }

@[reducible, inline]

abbrev Lean.IR.Index.lt (a b : Index) : Bool

Equations

• a.lt b = decide (a < b)

instance Lean.IR.instToStringVarId : ToString VarId

Equations

• Lean.IR.instToStringVarId = { toString := fun (a : Lean.IR.VarId) => "x_" ++ toString a.idx }

instance Lean.IR.instToStringJoinPointId : ToString JoinPointId

Equations

• Lean.IR.instToStringJoinPointId = { toString := fun (a : Lean.IR.JoinPointId) => "block_" ++ toString a.idx }

inductive Lean.IR.IRType : Type

Low Level IR types. Most are self explanatory.

• usize represents the C++ size_t Type. We have it here because it is 32-bit in 32-bit machines, and 64-bit in 64-bit machines, and we want the C++ backend for our Compiler to generate platform independent code.

• erased for Lean types, propositions and proofs.

• object a pointer to a value in the heap.

• tagged a tagged pointer (i.e., the least significant bit is 1) storing a scalar value.

• tobject an object or a tagged pointer

• struct and union are used to return small values (e.g., Option, Prod, Except) on the stack.

Remark: the RC operations for tobject are slightly more expensive because we first need to test whether the tobject is really a pointer or not.

Remark: the Lean runtime assumes that sizeof(void*) == sizeof(sizeT). Lean cannot be compiled on old platforms where this is not True.

Since values of type struct and union are only used to return values, We assume they must be used/consumed "linearly". We use the term "linear" here to mean "exactly once" in each execution. That is, given x : S, where S is a struct, then one of the following must hold in each (execution) branch. 1- x occurs only at a single ret x instruction. That is, it is being consumed by being returned. 2- x occurs only at a single ctor. That is, it is being "consumed" by being stored into another struct/union. 3- We extract (aka project) every single field of x exactly once. That is, we are consuming x by consuming each of one of its components. Minor refinement: we don't need to consume scalar fields or struct/union fields that do not contain object fields.

• float : IRType
• uint8 : IRType
• uint16 : IRType
• uint32 : IRType
• uint64 : IRType
• usize : IRType
• erased : IRType
• object : IRType
• tobject : IRType
• float32 : IRType
• struct (leanTypeName : Option Name) (types : Array IRType) : IRType
• union (leanTypeName : Name) (types : Array IRType) : IRType
• tagged : IRType

instance Lean.IR.instInhabitedIRType : Inhabited IRType

Equations

• Lean.IR.instInhabitedIRType = { default := Lean.IR.IRType.float }

instance Lean.IR.instBEqIRType : BEq IRType

Equations

• Lean.IR.instBEqIRType = { beq := Lean.IR.beqIRType✝ }

instance Lean.IR.instReprIRType : Repr IRType

Equations

• Lean.IR.instReprIRType = { reprPrec := Lean.IR.reprIRType✝ }

def Lean.IR.IRType.isScalar : IRType → Bool

Equations

• Lean.IR.IRType.float.isScalar = true
• Lean.IR.IRType.float32.isScalar = true
• Lean.IR.IRType.uint8.isScalar = true
• Lean.IR.IRType.uint16.isScalar = true
• Lean.IR.IRType.uint32.isScalar = true
• Lean.IR.IRType.uint64.isScalar = true
• Lean.IR.IRType.usize.isScalar = true
• x✝.isScalar = false

def Lean.IR.IRType.isObj : IRType → Bool

Equations

• Lean.IR.IRType.object.isObj = true
• Lean.IR.IRType.tagged.isObj = true
• Lean.IR.IRType.tobject.isObj = true
• x✝.isObj = false

def Lean.IR.IRType.isPossibleRef : IRType → Bool

Equations

• Lean.IR.IRType.object.isPossibleRef = true
• Lean.IR.IRType.tobject.isPossibleRef = true
• x✝.isPossibleRef = false

def Lean.IR.IRType.isDefiniteRef : IRType → Bool

Equations

• Lean.IR.IRType.object.isDefiniteRef = true
• x✝.isDefiniteRef = false

def Lean.IR.IRType.isErased : IRType → Bool

Equations

• Lean.IR.IRType.erased.isErased = true
• x✝.isErased = false

def Lean.IR.IRType.boxed : IRType → IRType

Equations

• Lean.IR.IRType.object.boxed = Lean.IR.IRType.object
• Lean.IR.IRType.float.boxed = Lean.IR.IRType.object
• Lean.IR.IRType.float32.boxed = Lean.IR.IRType.object
• Lean.IR.IRType.tagged.boxed = Lean.IR.IRType.tagged
• Lean.IR.IRType.uint8.boxed = Lean.IR.IRType.tagged
• Lean.IR.IRType.uint16.boxed = Lean.IR.IRType.tagged
• x✝.boxed = Lean.IR.IRType.tobject

inductive Lean.IR.Arg : Type

Arguments to applications, constructors, etc. We use erased for Lean types, propositions and proofs that have been erased. Recall that for a Function f, we also generate f._rarg which does not take erased arguments. However, f._rarg is only safe to be used in full applications.

• var (id : VarId) : Arg
• erased : Arg

instance Lean.IR.instInhabitedArg : Inhabited Arg

Equations

• Lean.IR.instInhabitedArg = { default := Lean.IR.Arg.var default }

instance Lean.IR.instBEqArg : BEq Arg

Equations

• Lean.IR.instBEqArg = { beq := Lean.IR.beqArg✝ }

instance Lean.IR.instReprArg : Repr Arg

Equations

• Lean.IR.instReprArg = { reprPrec := Lean.IR.reprArg✝ }

def Lean.IR.Arg.beq : Arg → Arg → Bool

Equations

• (Lean.IR.Arg.var a).beq (Lean.IR.Arg.var b) = (a == b)
• Lean.IR.Arg.erased.beq Lean.IR.Arg.erased = true
• x✝¹.beq x✝ = false

inductive Lean.IR.LitVal : Type

• num (v : Nat) : LitVal
• str (v : String) : LitVal

instance Lean.IR.instInhabitedLitVal : Inhabited LitVal

Equations

• Lean.IR.instInhabitedLitVal = { default := Lean.IR.LitVal.num default }

instance Lean.IR.instBEqLitVal : BEq LitVal

Equations

• Lean.IR.instBEqLitVal = { beq := Lean.IR.beqLitVal✝ }

structure Lean.IR.CtorInfo : Type

Constructor information.

• name is the Name of the Constructor in Lean.
• cidx is the Constructor index (aka tag).
• size is the number of arguments of type object/tobject.
• usize is the number of arguments of type usize.
• ssize is the number of bytes used to store scalar values.

Recall that a Constructor object contains a header, then a sequence of pointers to other Lean objects, a sequence of USize (i.e., size_t) scalar values, and a sequence of other scalar values.

• name : Name
• cidx : Nat
• size : Nat
• usize : Nat
• ssize : Nat

instance Lean.IR.instInhabitedCtorInfo : Inhabited CtorInfo

Equations

• Lean.IR.instInhabitedCtorInfo = { default := { name := default, cidx := default, size := default, usize := default, ssize := default } }

instance Lean.IR.instBEqCtorInfo : BEq CtorInfo

Equations

• Lean.IR.instBEqCtorInfo = { beq := Lean.IR.beqCtorInfo✝ }

instance Lean.IR.instReprCtorInfo : Repr CtorInfo

Equations

• Lean.IR.instReprCtorInfo = { reprPrec := Lean.IR.reprCtorInfo✝ }

def Lean.IR.CtorInfo.isRef (info : CtorInfo) : Bool

Equations

• info.isRef = (decide (info.size > 0) || decide (info.usize > 0) || decide (info.ssize > 0))

def Lean.IR.CtorInfo.isScalar (info : CtorInfo) : Bool

Equations

• info.isScalar = !info.isRef

def Lean.IR.CtorInfo.type (info : CtorInfo) : IRType

Equations

• info.type = if info.isRef = true then Lean.IR.IRType.object else Lean.IR.IRType.tagged

inductive Lean.IR.Expr : Type

• ctor (i : CtorInfo) (ys : Array Arg) : Expr

  We use ctor mainly for constructing Lean object/tobject values lean_ctor_object in the runtime. This instruction is also used to creat struct and union return values. For union, only i.cidx is relevant. For struct, i is irrelevant.

• reset (n : Nat) (x : VarId) : Expr
• reuse (x : VarId) (i : CtorInfo) (updtHeader : Bool) (ys : Array Arg) : Expr

  reuse x in ctor_i ys instruction in the paper.

• proj (i : Nat) (x : VarId) : Expr

  Extract the tobject value at Position sizeof(void*)*i from x. We also use proj for extracting fields from struct return values, and casting union return values.

• uproj (i : Nat) (x : VarId) : Expr

  Extract the Usize value at Position sizeof(void*)*i from x.

• sproj (n offset : Nat) (x : VarId) : Expr

  Extract the scalar value at Position sizeof(void*)*n + offset from x.

• fap (c : FunId) (ys : Array Arg) : Expr

  Full application.

• pap (c : FunId) (ys : Array Arg) : Expr

  Partial application that creates a pap value (aka closure in our nonstandard terminology).

• ap (x : VarId) (ys : Array Arg) : Expr

  Application. x must be a pap value.

• box (ty : IRType) (x : VarId) : Expr

  Given x : ty where ty is a scalar type, this operation returns a value of Type tobject. For small scalar values, the Result is a tagged pointer, and no memory allocation is performed.

• unbox (x : VarId) : Expr

  Given x : [t]object, obtain the scalar value.

• lit (v : LitVal) : Expr
• isShared (x : VarId) : Expr

  Return 1 : uint8 Iff RC(x) > 1

instance Lean.IR.instInhabitedExpr : Inhabited Expr

Equations

• Lean.IR.instInhabitedExpr = { default := Lean.IR.Expr.ctor default default }

structure Lean.IR.Param : Type

• x : VarId
• borrow : Bool
• ty : IRType

instance Lean.IR.instInhabitedParam : Inhabited Param

Equations

• Lean.IR.instInhabitedParam = { default := { x := default, borrow := default, ty := default } }

instance Lean.IR.instReprParam : Repr Param

Equations

• Lean.IR.instReprParam = { reprPrec := Lean.IR.reprParam✝ }

inductive Lean.IR.Alt : Type

• ctor (info : CtorInfo) (b : FnBody) : Alt
• default (b : FnBody) : Alt

inductive Lean.IR.FnBody : Type

• vdecl (x : VarId) (ty : IRType) (e : Expr) (b : FnBody) : FnBody

  let x : ty := e; b

• jdecl (j : JoinPointId) (xs : Array Param) (v b : FnBody) : FnBody

  Join point Declaration block_j (xs) := e; b

• set (x : VarId) (i : Nat) (y : Arg) (b : FnBody) : FnBody

  Store y at Position sizeof(void*)*i in x. x must be a Constructor object and RC(x) must be 1. This operation is not part of λPure is only used during optimization.

• setTag (x : VarId) (cidx : Nat) (b : FnBody) : FnBody
• uset (x : VarId) (i : Nat) (y : VarId) (b : FnBody) : FnBody

  Store y : Usize at Position sizeof(void*)*i in x. x must be a Constructor object and RC(x) must be 1.

• sset (x : VarId) (i offset : Nat) (y : VarId) (ty : IRType) (b : FnBody) : FnBody

  Store y : ty at Position sizeof(void*)*i + offset in x. x must be a Constructor object and RC(x) must be 1. ty must not be object, tobject, erased nor Usize.

• inc (x : VarId) (n : Nat) (c persistent : Bool) (b : FnBody) : FnBody

  RC increment for object. If c == true, then inc must check whether x is a tagged pointer or not. If persistent == true then x is statically known to be a persistent object.

• dec (x : VarId) (n : Nat) (c persistent : Bool) (b : FnBody) : FnBody

  RC decrement for object. If c == true, then inc must check whether x is a tagged pointer or not. If persistent == true then x is statically known to be a persistent object.

• del (x : VarId) (b : FnBody) : FnBody
• case (tid : Name) (x : VarId) (xType : IRType) (cs : Array Alt) : FnBody
• ret (x : Arg) : FnBody
• jmp (j : JoinPointId) (ys : Array Arg) : FnBody

  Jump to join point j

• unreachable : FnBody

instance Lean.IR.instInhabitedFnBody : Inhabited FnBody

Equations

• Lean.IR.instInhabitedFnBody = { default := Lean.IR.FnBody.case default default default default }

instance Lean.IR.instInhabitedAlt : Inhabited Alt

Equations

• Lean.IR.instInhabitedAlt = { default := Lean.IR.Alt.ctor default default }

@[reducible, inline]

abbrev Lean.IR.FnBody.nil : FnBody

Equations

• Lean.IR.FnBody.nil = Lean.IR.FnBody.unreachable

def Lean.IR.FnBody.isTerminal : FnBody → Bool

Equations

• (Lean.IR.FnBody.case tid x_1 xType cs).isTerminal = true
• (Lean.IR.FnBody.ret x_1).isTerminal = true
• (Lean.IR.FnBody.jmp j ys).isTerminal = true
• Lean.IR.FnBody.unreachable.isTerminal = true
• x✝.isTerminal = false

def Lean.IR.FnBody.body : FnBody → FnBody

Equations

• (Lean.IR.FnBody.vdecl x_1 ty e b).body = b
• (Lean.IR.FnBody.jdecl j xs v b).body = b
• (Lean.IR.FnBody.set x_1 i y b).body = b
• (Lean.IR.FnBody.uset x_1 i y b).body = b
• (Lean.IR.FnBody.sset x_1 i offset y ty b).body = b
• (Lean.IR.FnBody.setTag x_1 cidx b).body = b
• (Lean.IR.FnBody.inc x_1 n c persistent b).body = b
• (Lean.IR.FnBody.dec x_1 n c persistent b).body = b
• (Lean.IR.FnBody.del x_1 b).body = b
• x✝.body = x✝

def Lean.IR.FnBody.setBody : FnBody → FnBody → FnBody

Equations

• (Lean.IR.FnBody.vdecl x_2 t v b).setBody x✝ = Lean.IR.FnBody.vdecl x_2 t v x✝
• (Lean.IR.FnBody.jdecl j xs v b).setBody x✝ = Lean.IR.FnBody.jdecl j xs v x✝
• (Lean.IR.FnBody.set x_2 i y b).setBody x✝ = Lean.IR.FnBody.set x_2 i y x✝
• (Lean.IR.FnBody.uset x_2 i y b).setBody x✝ = Lean.IR.FnBody.uset x_2 i y x✝
• (Lean.IR.FnBody.sset x_2 i o y t b).setBody x✝ = Lean.IR.FnBody.sset x_2 i o y t x✝
• (Lean.IR.FnBody.setTag x_2 i b).setBody x✝ = Lean.IR.FnBody.setTag x_2 i x✝
• (Lean.IR.FnBody.inc x_2 n c p b).setBody x✝ = Lean.IR.FnBody.inc x_2 n c p x✝
• (Lean.IR.FnBody.dec x_2 n c p b).setBody x✝ = Lean.IR.FnBody.dec x_2 n c p x✝
• (Lean.IR.FnBody.del x_2 b).setBody x✝ = Lean.IR.FnBody.del x_2 x✝
• x✝¹.setBody x✝ = x✝¹

@[inline]

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

Equations

• b.resetBody = b.setBody Lean.IR.FnBody.nil

@[inline]

def Lean.IR.FnBody.split (b : FnBody) : FnBody × FnBody

If b is a non terminal, then return a pair (c, b') s.t. b == c <;> b', and c.body == FnBody.nil

Equations

• b.split = (b.resetBody, b.body)

def Lean.IR.Alt.body : Alt → FnBody

Equations

• (Lean.IR.Alt.ctor info b).body = b
• (Lean.IR.Alt.default b).body = b

def Lean.IR.Alt.setBody : Alt → FnBody → Alt

Equations

• (Lean.IR.Alt.ctor c b).setBody x✝ = Lean.IR.Alt.ctor c x✝
• (Lean.IR.Alt.default b).setBody x✝ = Lean.IR.Alt.default x✝

@[inline]

def Lean.IR.Alt.modifyBody (f : FnBody → FnBody) : Alt → Alt

Equations

• Lean.IR.Alt.modifyBody f (Lean.IR.Alt.ctor info b) = Lean.IR.Alt.ctor info (f b)
• Lean.IR.Alt.modifyBody f (Lean.IR.Alt.default b) = Lean.IR.Alt.default (f b)

@[inline]

def Lean.IR.Alt.modifyBodyM {m : Type → Type} [Monad m] (f : FnBody → m FnBody) : Alt → m Alt

Equations

• Lean.IR.Alt.modifyBodyM f (Lean.IR.Alt.ctor info b) = Lean.IR.Alt.ctor info <$> f b
• Lean.IR.Alt.modifyBodyM f (Lean.IR.Alt.default b) = Lean.IR.Alt.default <$> f b

def Lean.IR.Alt.isDefault : Alt → Bool

Equations

• (Lean.IR.Alt.ctor info b).isDefault = false
• (Lean.IR.Alt.default b).isDefault = true

def Lean.IR.push (bs : Array FnBody) (b : FnBody) : Array FnBody

Equations

• Lean.IR.push bs b = bs.push b.resetBody

partial def Lean.IR.flattenAux (b : FnBody) (r : Array FnBody) : Array FnBody × FnBody

def Lean.IR.FnBody.flatten (b : FnBody) : Array FnBody × FnBody

Equations

• b.flatten = Lean.IR.flattenAux b #[]

partial def Lean.IR.reshapeAux (a : Array FnBody) (i : Nat) (b : FnBody) : FnBody

def Lean.IR.reshape (bs : Array FnBody) (term : FnBody) : FnBody

Equations

• Lean.IR.reshape bs term = Lean.IR.reshapeAux bs bs.size term

@[inline]

def Lean.IR.modifyJPs (bs : Array FnBody) (f : FnBody → FnBody) : Array FnBody

Equations

• Lean.IR.modifyJPs bs f = Array.map (fun (b : Lean.IR.FnBody) => match b with | Lean.IR.FnBody.jdecl j xs v k => Lean.IR.FnBody.jdecl j xs (f v) k | other => other) bs

@[inline]

def Lean.IR.modifyJPsM {m : Type → Type} [Monad m] (bs : Array FnBody) (f : FnBody → m FnBody) : m (Array FnBody)

Equations

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

structure Lean.IR.DeclInfo : Type

Extra information associated with a declaration.

• sorryDep? : Option Name

  If some <blame>, then declaration depends on <blame> which uses a sorry axiom.

inductive Lean.IR.Decl : Type

• fdecl (f : FunId) (xs : Array Param) (type : IRType) (body : FnBody) (info : DeclInfo) : Decl
• extern (f : FunId) (xs : Array Param) (type : IRType) (ext : ExternAttrData) : Decl

instance Lean.IR.instInhabitedDecl : Inhabited Decl

Equations

• Lean.IR.instInhabitedDecl = { default := Lean.IR.Decl.extern default default default default }

def Lean.IR.Decl.name : Decl → FunId

Equations

• (Lean.IR.Decl.fdecl f xs type body info).name = f
• (Lean.IR.Decl.extern f xs type ext).name = f

def Lean.IR.Decl.params : Decl → Array Param

Equations

• (Lean.IR.Decl.fdecl f xs type body info).params = xs
• (Lean.IR.Decl.extern f xs type ext).params = xs

def Lean.IR.Decl.resultType : Decl → IRType

Equations

• (Lean.IR.Decl.fdecl f xs type body info).resultType = type
• (Lean.IR.Decl.extern f xs type ext).resultType = type

def Lean.IR.Decl.isExtern : Decl → Bool

Equations

• (Lean.IR.Decl.extern f xs type ext).isExtern = true
• x✝.isExtern = false

def Lean.IR.Decl.getInfo : Decl → DeclInfo

Equations

• (Lean.IR.Decl.fdecl f xs type body info).getInfo = info
• x✝.getInfo = { }

def Lean.IR.Decl.updateBody! (d : Decl) (bNew : FnBody) : Decl

Equations

• (Lean.IR.Decl.fdecl f xs type body info).updateBody! bNew = Lean.IR.Decl.fdecl f xs type bNew info
• d.updateBody! bNew = panicWithPosWithDecl "Lean.Compiler.IR.Basic" "Lean.IR.Decl.updateBody!" 375 9 "expected definition"

def Lean.IR.mkDummyExternDecl (f : FunId) (xs : Array Param) (ty : IRType) : Decl

Equations

• Lean.IR.mkDummyExternDecl f xs ty = Lean.IR.Decl.fdecl f xs ty Lean.IR.FnBody.unreachable { }

@[reducible, inline]

abbrev Lean.IR.IndexSet : Type

Set of variable and join point names

Equations

• Lean.IR.IndexSet = Std.TreeSet Lean.IR.Index compare

def Lean.IR.mkIndexSet (idx : Index) : IndexSet

Equations

• Lean.IR.mkIndexSet idx = Std.TreeSet.empty.insert idx

inductive Lean.IR.LocalContextEntry : Type

• param : IRType → LocalContextEntry
• localVar : IRType → Expr → LocalContextEntry
• joinPoint : Array Param → FnBody → LocalContextEntry

@[reducible, inline]

abbrev Lean.IR.LocalContext : Type

Equations

• Lean.IR.LocalContext = Std.TreeMap Lean.IR.Index Lean.IR.LocalContextEntry compare

def Lean.IR.LocalContext.addLocal (ctx : LocalContext) (x : VarId) (t : IRType) (v : Expr) : LocalContext

Equations

• ctx.addLocal x t v = Std.TreeMap.insert ctx x.idx (Lean.IR.LocalContextEntry.localVar t v)

def Lean.IR.LocalContext.addJP (ctx : LocalContext) (j : JoinPointId) (xs : Array Param) (b : FnBody) : LocalContext

Equations

• ctx.addJP j xs b = Std.TreeMap.insert ctx j.idx (Lean.IR.LocalContextEntry.joinPoint xs b)

def Lean.IR.LocalContext.addParam (ctx : LocalContext) (p : Param) : LocalContext

Equations

• ctx.addParam p = Std.TreeMap.insert ctx p.x.idx (Lean.IR.LocalContextEntry.param p.ty)

def Lean.IR.LocalContext.addParams (ctx : LocalContext) (ps : Array Param) : LocalContext

Equations

• ctx.addParams ps = Array.foldl Lean.IR.LocalContext.addParam ctx ps

def Lean.IR.LocalContext.isJP (ctx : LocalContext) (idx : Index) : Bool

Equations

• ctx.isJP idx = match Std.TreeMap.get? ctx idx with | some (Lean.IR.LocalContextEntry.joinPoint a a_1) => true | x => false

def Lean.IR.LocalContext.getJPBody (ctx : LocalContext) (j : JoinPointId) : Option FnBody

Equations

• ctx.getJPBody j = match Std.TreeMap.get? ctx j.idx with | some (Lean.IR.LocalContextEntry.joinPoint a b) => some b | x => none

def Lean.IR.LocalContext.getJPParams (ctx : LocalContext) (j : JoinPointId) : Option (Array Param)

Equations

• ctx.getJPParams j = match Std.TreeMap.get? ctx j.idx with | some (Lean.IR.LocalContextEntry.joinPoint ys a) => some ys | x => none

def Lean.IR.LocalContext.isParam (ctx : LocalContext) (idx : Index) : Bool

Equations

• ctx.isParam idx = match Std.TreeMap.get? ctx idx with | some (Lean.IR.LocalContextEntry.param a) => true | x => false

def Lean.IR.LocalContext.isLocalVar (ctx : LocalContext) (idx : Index) : Bool

Equations

• ctx.isLocalVar idx = match Std.TreeMap.get? ctx idx with | some (Lean.IR.LocalContextEntry.localVar a a_1) => true | x => false

def Lean.IR.LocalContext.contains (ctx : LocalContext) (idx : Index) : Bool

Equations

• ctx.contains idx = Std.TreeMap.contains ctx idx

def Lean.IR.LocalContext.eraseJoinPointDecl (ctx : LocalContext) (j : JoinPointId) : LocalContext

Equations

• ctx.eraseJoinPointDecl j = Std.TreeMap.erase ctx j.idx

def Lean.IR.LocalContext.getType (ctx : LocalContext) (x : VarId) : Option IRType

Equations

• ctx.getType x = match Std.TreeMap.get? ctx x.idx with | some (Lean.IR.LocalContextEntry.param t) => some t | some (Lean.IR.LocalContextEntry.localVar t a) => some t | x => none

def Lean.IR.LocalContext.getValue (ctx : LocalContext) (x : VarId) : Option Expr

Equations

• ctx.getValue x = match Std.TreeMap.get? ctx x.idx with | some (Lean.IR.LocalContextEntry.localVar a v) => some v | x => none

@[reducible, inline]

abbrev Lean.IR.IndexRenaming : Type

Equations

• Lean.IR.IndexRenaming = Std.TreeMap Lean.IR.Index Lean.IR.Index compare

class Lean.IR.AlphaEqv (α : Type) : Type

• aeqv : IndexRenaming → α → α → Bool

def Lean.IR.VarId.alphaEqv (ρ : IndexRenaming) (v₁ v₂ : VarId) : Bool

Equations

• Lean.IR.VarId.alphaEqv ρ v₁ v₂ = match Std.TreeMap.get? ρ v₁.idx with | some v => v == v₂.idx | none => v₁ == v₂

instance Lean.IR.instAlphaEqvVarId : AlphaEqv VarId

Equations

• Lean.IR.instAlphaEqvVarId = { aeqv := Lean.IR.VarId.alphaEqv }

def Lean.IR.Arg.alphaEqv (ρ : IndexRenaming) : Arg → Arg → Bool

Equations

• Lean.IR.Arg.alphaEqv ρ (Lean.IR.Arg.var a) (Lean.IR.Arg.var b) = Lean.IR.aeqv ρ a b
• Lean.IR.Arg.alphaEqv ρ Lean.IR.Arg.erased Lean.IR.Arg.erased = true
• Lean.IR.Arg.alphaEqv ρ x✝¹ x✝ = false

instance Lean.IR.instAlphaEqvArg : AlphaEqv Arg

Equations

• Lean.IR.instAlphaEqvArg = { aeqv := Lean.IR.Arg.alphaEqv }

def Lean.IR.args.alphaEqv (ρ : IndexRenaming) (args₁ args₂ : Array Arg) : Bool

Equations

• Lean.IR.args.alphaEqv ρ args₁ args₂ = args₁.isEqv args₂ fun (a b : Lean.IR.Arg) => Lean.IR.aeqv ρ a b

instance Lean.IR.instAlphaEqvArrayArg : AlphaEqv (Array Arg)

Equations

• Lean.IR.instAlphaEqvArrayArg = { aeqv := Lean.IR.args.alphaEqv }

def Lean.IR.Expr.alphaEqv (ρ : IndexRenaming) : Expr → Expr → Bool

Equations

• Lean.IR.Expr.alphaEqv ρ (Lean.IR.Expr.ctor i₁ ys₁) (Lean.IR.Expr.ctor i₂ ys₂) = (i₁ == i₂ && Lean.IR.aeqv ρ ys₁ ys₂)
• Lean.IR.Expr.alphaEqv ρ (Lean.IR.Expr.reset n₁ x₁) (Lean.IR.Expr.reset n₂ x₂) = (n₁ == n₂ && Lean.IR.aeqv ρ x₁ x₂)
• Lean.IR.Expr.alphaEqv ρ (Lean.IR.Expr.reuse x₁ i₁ u₁ ys₁) (Lean.IR.Expr.reuse x₂ i₂ u₂ ys₂) = (Lean.IR.aeqv ρ x₁ x₂ && i₁ == i₂ && u₁ == u₂ && Lean.IR.aeqv ρ ys₁ ys₂)
• Lean.IR.Expr.alphaEqv ρ (Lean.IR.Expr.proj i₁ x₁) (Lean.IR.Expr.proj i₂ x₂) = (i₁ == i₂ && Lean.IR.aeqv ρ x₁ x₂)
• Lean.IR.Expr.alphaEqv ρ (Lean.IR.Expr.uproj i₁ x₁) (Lean.IR.Expr.uproj i₂ x₂) = (i₁ == i₂ && Lean.IR.aeqv ρ x₁ x₂)
• Lean.IR.Expr.alphaEqv ρ (Lean.IR.Expr.sproj n₁ o₁ x₁) (Lean.IR.Expr.sproj n₂ o₂ x₂) = (n₁ == n₂ && o₁ == o₂ && Lean.IR.aeqv ρ x₁ x₂)
• Lean.IR.Expr.alphaEqv ρ (Lean.IR.Expr.fap c₁ ys₁) (Lean.IR.Expr.fap c₂ ys₂) = (c₁ == c₂ && Lean.IR.aeqv ρ ys₁ ys₂)
• Lean.IR.Expr.alphaEqv ρ (Lean.IR.Expr.pap c₁ ys₁) (Lean.IR.Expr.pap c₂ ys₂) = (c₁ == c₂ && Lean.IR.aeqv ρ ys₁ ys₂)
• Lean.IR.Expr.alphaEqv ρ (Lean.IR.Expr.ap x₁ ys₁) (Lean.IR.Expr.ap x₂ ys₂) = (Lean.IR.aeqv ρ x₁ x₂ && Lean.IR.aeqv ρ ys₁ ys₂)
• Lean.IR.Expr.alphaEqv ρ (Lean.IR.Expr.box ty₁ x₁) (Lean.IR.Expr.box ty₂ x₂) = (ty₁ == ty₂ && Lean.IR.aeqv ρ x₁ x₂)
• Lean.IR.Expr.alphaEqv ρ (Lean.IR.Expr.unbox x₁) (Lean.IR.Expr.unbox x₂) = Lean.IR.aeqv ρ x₁ x₂
• Lean.IR.Expr.alphaEqv ρ (Lean.IR.Expr.lit v₁) (Lean.IR.Expr.lit v₂) = (v₁ == v₂)
• Lean.IR.Expr.alphaEqv ρ (Lean.IR.Expr.isShared x₁) (Lean.IR.Expr.isShared x₂) = Lean.IR.aeqv ρ x₁ x₂
• Lean.IR.Expr.alphaEqv ρ x✝¹ x✝ = false

instance Lean.IR.instAlphaEqvExpr : AlphaEqv Expr

Equations

• Lean.IR.instAlphaEqvExpr = { aeqv := Lean.IR.Expr.alphaEqv }

def Lean.IR.addVarRename (ρ : IndexRenaming) (x₁ x₂ : Nat) : IndexRenaming

Equations

• Lean.IR.addVarRename ρ x₁ x₂ = if (x₁ == x₂) = true then ρ else Std.TreeMap.insert ρ x₁ x₂

def Lean.IR.addParamRename (ρ : IndexRenaming) (p₁ p₂ : Param) : Option IndexRenaming

Equations

• Lean.IR.addParamRename ρ p₁ p₂ = if (p₁.ty == p₂.ty && decide (p₁.borrow = p₂.borrow)) = true then some (Lean.IR.addVarRename ρ p₁.x.idx p₂.x.idx) else none

def Lean.IR.addParamsRename (ρ : IndexRenaming) (ps₁ ps₂ : Array Param) : Option IndexRenaming

Equations

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

partial def Lean.IR.FnBody.alphaEqv : IndexRenaming → FnBody → FnBody → Bool

def Lean.IR.FnBody.beq (b₁ b₂ : FnBody) : Bool

Equations

• b₁.beq b₂ = Lean.IR.FnBody.alphaEqv ∅ b₁ b₂

instance Lean.IR.instBEqFnBody : BEq FnBody

Equations

• Lean.IR.instBEqFnBody = { beq := Lean.IR.FnBody.beq }

@[reducible, inline]

abbrev Lean.IR.VarIdSet : Type

Equations

• Lean.IR.VarIdSet = Std.TreeSet Lean.IR.VarId fun (x y : Lean.IR.VarId) => compare x.idx y.idx

def Lean.IR.mkIf (x : VarId) (t e : FnBody) : FnBody

Equations

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

def Lean.IR.getUnboxOpName (t : IRType) : String

Equations

• Lean.IR.getUnboxOpName Lean.IR.IRType.usize = "lean_unbox_usize"
• Lean.IR.getUnboxOpName Lean.IR.IRType.uint32 = "lean_unbox_uint32"
• Lean.IR.getUnboxOpName Lean.IR.IRType.uint64 = "lean_unbox_uint64"
• Lean.IR.getUnboxOpName Lean.IR.IRType.float = "lean_unbox_float"
• Lean.IR.getUnboxOpName Lean.IR.IRType.float32 = "lean_unbox_float32"
• Lean.IR.getUnboxOpName t = "lean_unbox"