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.

@[inline]

abbrev Lean.IR.FunId : Type

Function identifier

Equations

• Lean.IR.FunId = Lean.Name

@[inline]

abbrev Lean.IR.Index : Type

Equations

• Lean.IR.Index = Nat

structure Lean.IR.VarId : Type

• idx : Lean.IR.Index

Variable identifier

instance Lean.IR.instInhabitedVarId : Inhabited Lean.IR.VarId

Equations

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

structure Lean.IR.JoinPointId : Type

• idx : Lean.IR.Index

Join point identifier

instance Lean.IR.instInhabitedJoinPointId : Inhabited Lean.IR.JoinPointId

Equations

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

@[inline]

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

Equations

• Lean.IR.Index.lt a b = decide (a < b)

instance Lean.IR.instBEqVarId : BEq Lean.IR.VarId

Equations

• Lean.IR.instBEqVarId = { beq := fun a b => a.idx == b.idx }

instance Lean.IR.instToStringVarId : ToString Lean.IR.VarId

Equations

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

instance Lean.IR.instToFormatVarId : Lean.ToFormat Lean.IR.VarId

Equations

• Lean.IR.instToFormatVarId = { format := fun a => Std.Format.text (toString a) }

instance Lean.IR.instHashableVarId : Hashable Lean.IR.VarId

Equations

• Lean.IR.instHashableVarId = { hash := fun a => hash a.idx }

instance Lean.IR.instBEqJoinPointId : BEq Lean.IR.JoinPointId

Equations

• Lean.IR.instBEqJoinPointId = { beq := fun a b => a.idx == b.idx }

instance Lean.IR.instToStringJoinPointId : ToString Lean.IR.JoinPointId

Equations

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

instance Lean.IR.instToFormatJoinPointId : Lean.ToFormat Lean.IR.JoinPointId

Equations

• Lean.IR.instToFormatJoinPointId = { format := fun a => Std.Format.text (toString a) }

instance Lean.IR.instHashableJoinPointId : Hashable Lean.IR.JoinPointId

Equations

• Lean.IR.instHashableJoinPointId = { hash := fun a => hash a.idx }

@[inline]

abbrev Lean.IR.MData : Type

Equations

• Lean.IR.MData = Lean.KVMap

@[inline]

abbrev Lean.IR.MData.empty : Lean.IR.MData

Equations

• Lean.IR.MData.empty = { entries := [] }

inductive Lean.IR.IRType : Type

• float: Lean.IR.IRType
• uint8: Lean.IR.IRType
• uint16: Lean.IR.IRType
• uint32: Lean.IR.IRType
• uint64: Lean.IR.IRType
• usize: Lean.IR.IRType
• irrelevant: Lean.IR.IRType
• object: Lean.IR.IRType
• tobject: Lean.IR.IRType
• struct: Option Lean.Name → Array Lean.IR.IRType → Lean.IR.IRType
• union: Lean.Name → Array Lean.IR.IRType → Lean.IR.IRType

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.

• irrelevant for Lean types, propositions and proofs.

• object a pointer to a value in the heap.

• tobject a pointer to a value in the heap or tagged pointer (i.e., the least significant bit is 1) storing a scalar value.

• 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.

instance Lean.IR.instInhabitedIRType : Inhabited Lean.IR.IRType

Equations

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

partial def Lean.IR.IRType.beq : Lean.IR.IRType → Lean.IR.IRType → Bool

instance Lean.IR.IRType.instBEqIRType : BEq Lean.IR.IRType

Equations

• Lean.IR.IRType.instBEqIRType = { beq := Lean.IR.IRType.beq }

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

Equations

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

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

Equations

• Lean.IR.IRType.isObj x = match x with | Lean.IR.IRType.object => true | Lean.IR.IRType.tobject => true | x => false

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

Equations

• Lean.IR.IRType.isIrrelevant x = match x with | Lean.IR.IRType.irrelevant => true | x => false

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

Equations

• Lean.IR.IRType.isStruct x = match x with | Lean.IR.IRType.struct leanTypeName types => true | x => false

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

Equations

• Lean.IR.IRType.isUnion x = match x with | Lean.IR.IRType.union leanTypeName types => true | x => false

inductive Lean.IR.Arg : Type

• var: Lean.IR.VarId → Lean.IR.Arg
• irrelevant: Lean.IR.Arg

Arguments to applications, constructors, etc. We use irrelevant 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 irrelevant arguments. However, f._rarg is only safe to be used in full applications.

instance Lean.IR.instInhabitedArg : Inhabited Lean.IR.Arg

Equations

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

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

Equations

• Lean.IR.Arg.beq x x = match x, x with | Lean.IR.Arg.var x, Lean.IR.Arg.var y => x == y | Lean.IR.Arg.irrelevant, Lean.IR.Arg.irrelevant => true | x, x_1 => false

instance Lean.IR.instBEqArg : BEq Lean.IR.Arg

Equations

• Lean.IR.instBEqArg = { beq := Lean.IR.Arg.beq }

@[export lean_ir_mk_var_arg]

def Lean.IR.mkVarArg (id : Lean.IR.VarId) : Lean.IR.Arg

Equations

• Lean.IR.mkVarArg id = Lean.IR.Arg.var id

inductive Lean.IR.LitVal : Type

• num: Nat → Lean.IR.LitVal
• str: String → Lean.IR.LitVal

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

Equations

• Lean.IR.LitVal.beq x x = match x, x with | Lean.IR.LitVal.num v₁, Lean.IR.LitVal.num v₂ => v₁ == v₂ | Lean.IR.LitVal.str v₁, Lean.IR.LitVal.str v₂ => v₁ == v₂ | x, x_1 => false

instance Lean.IR.instBEqLitVal : BEq Lean.IR.LitVal

Equations

• Lean.IR.instBEqLitVal = { beq := Lean.IR.LitVal.beq }

structure Lean.IR.CtorInfo : Type

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

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.

instance Lean.IR.instReprCtorInfo : Repr Lean.IR.CtorInfo

Equations

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

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

Equations

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

instance Lean.IR.instBEqCtorInfo : BEq Lean.IR.CtorInfo

Equations

• Lean.IR.instBEqCtorInfo = { beq := Lean.IR.CtorInfo.beq }

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

Equations

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

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

Equations

• Lean.IR.CtorInfo.isScalar info = !Lean.IR.CtorInfo.isRef info

inductive Lean.IR.Expr : Type

• 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.

  ctor: Lean.IR.CtorInfo → Array Lean.IR.Arg → Lean.IR.Expr
• reset: Nat → Lean.IR.VarId → Lean.IR.Expr

• reuse x in ctor_i ys instruction in the paper.

  reuse: Lean.IR.VarId → Lean.IR.CtorInfo → Bool → Array Lean.IR.Arg → Lean.IR.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.

  proj: Nat → Lean.IR.VarId → Lean.IR.Expr

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

  uproj: Nat → Lean.IR.VarId → Lean.IR.Expr

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

  sproj: Nat → Nat → Lean.IR.VarId → Lean.IR.Expr

• Full application.

  fap: Lean.IR.FunId → Array Lean.IR.Arg → Lean.IR.Expr

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

  pap: Lean.IR.FunId → Array Lean.IR.Arg → Lean.IR.Expr

• Application. x must be a pap value.

  ap: Lean.IR.VarId → Array Lean.IR.Arg → Lean.IR.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.

  box: Lean.IR.IRType → Lean.IR.VarId → Lean.IR.Expr

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

  unbox: Lean.IR.VarId → Lean.IR.Expr
• lit: Lean.IR.LitVal → Lean.IR.Expr

• Return 1 : uint8 Iff RC(x) > 1

  isShared: Lean.IR.VarId → Lean.IR.Expr

• Return 1 : uint8 Iff x : tobject is a tagged pointer (storing a scalar value).

  isTaggedPtr: Lean.IR.VarId → Lean.IR.Expr

@[export lean_ir_mk_ctor_expr]

def Lean.IR.mkCtorExpr (n : Lean.Name) (cidx : Nat) (size : Nat) (usize : Nat) (ssize : Nat) (ys : Array Lean.IR.Arg) : Lean.IR.Expr

Equations

• Lean.IR.mkCtorExpr n cidx size usize ssize ys = Lean.IR.Expr.ctor { name := n, cidx := cidx, size := size, usize := usize, ssize := ssize } ys

@[export lean_ir_mk_proj_expr]

def Lean.IR.mkProjExpr (i : Nat) (x : Lean.IR.VarId) : Lean.IR.Expr

Equations

• Lean.IR.mkProjExpr i x = Lean.IR.Expr.proj i x

@[export lean_ir_mk_uproj_expr]

def Lean.IR.mkUProjExpr (i : Nat) (x : Lean.IR.VarId) : Lean.IR.Expr

Equations

• Lean.IR.mkUProjExpr i x = Lean.IR.Expr.uproj i x

@[export lean_ir_mk_sproj_expr]

def Lean.IR.mkSProjExpr (n : Nat) (offset : Nat) (x : Lean.IR.VarId) : Lean.IR.Expr

Equations

• Lean.IR.mkSProjExpr n offset x = Lean.IR.Expr.sproj n offset x

@[export lean_ir_mk_fapp_expr]

def Lean.IR.mkFAppExpr (c : Lean.IR.FunId) (ys : Array Lean.IR.Arg) : Lean.IR.Expr

Equations

• Lean.IR.mkFAppExpr c ys = Lean.IR.Expr.fap c ys

@[export lean_ir_mk_papp_expr]

def Lean.IR.mkPAppExpr (c : Lean.IR.FunId) (ys : Array Lean.IR.Arg) : Lean.IR.Expr

Equations

• Lean.IR.mkPAppExpr c ys = Lean.IR.Expr.pap c ys

@[export lean_ir_mk_app_expr]

def Lean.IR.mkAppExpr (x : Lean.IR.VarId) (ys : Array Lean.IR.Arg) : Lean.IR.Expr

Equations

• Lean.IR.mkAppExpr x ys = Lean.IR.Expr.ap x ys

@[export lean_ir_mk_num_expr]

def Lean.IR.mkNumExpr (v : Nat) : Lean.IR.Expr

Equations

• Lean.IR.mkNumExpr v = Lean.IR.Expr.lit (Lean.IR.LitVal.num v)

@[export lean_ir_mk_str_expr]

def Lean.IR.mkStrExpr (v : String) : Lean.IR.Expr

Equations

• Lean.IR.mkStrExpr v = Lean.IR.Expr.lit (Lean.IR.LitVal.str v)

structure Lean.IR.Param : Type

• x : Lean.IR.VarId
• borrow : Bool
• ty : Lean.IR.IRType

instance Lean.IR.instInhabitedParam : Inhabited Lean.IR.Param

Equations

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

@[export lean_ir_mk_param]

def Lean.IR.mkParam (x : Lean.IR.VarId) (borrow : Bool) (ty : Lean.IR.IRType) : Lean.IR.Param

Equations

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

inductive Lean.IR.AltCore (FnBody : Type) : Type

• ctor: {FnBody : Type} → Lean.IR.CtorInfo → FnBody → Lean.IR.AltCore FnBody
• default: {FnBody : Type} → FnBody → Lean.IR.AltCore FnBody

inductive Lean.IR.FnBody : Type

• let x : ty := e; b

  vdecl: Lean.IR.VarId → Lean.IR.IRType → Lean.IR.Expr → Lean.IR.FnBody → Lean.IR.FnBody

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

  jdecl: Lean.IR.JoinPointId → Array Lean.IR.Param → Lean.IR.FnBody → Lean.IR.FnBody → Lean.IR.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.

  set: Lean.IR.VarId → Nat → Lean.IR.Arg → Lean.IR.FnBody → Lean.IR.FnBody
• setTag: Lean.IR.VarId → Nat → Lean.IR.FnBody → Lean.IR.FnBody

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

  uset: Lean.IR.VarId → Nat → Lean.IR.VarId → Lean.IR.FnBody → Lean.IR.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, irrelevant nor Usize.

  sset: Lean.IR.VarId → Nat → Nat → Lean.IR.VarId → Lean.IR.IRType → Lean.IR.FnBody → Lean.IR.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.

  inc: Lean.IR.VarId → Nat → Bool → Bool → Lean.IR.FnBody → Lean.IR.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.

  dec: Lean.IR.VarId → Nat → Bool → Bool → Lean.IR.FnBody → Lean.IR.FnBody
• del: Lean.IR.VarId → Lean.IR.FnBody → Lean.IR.FnBody
• mdata: Lean.IR.MData → Lean.IR.FnBody → Lean.IR.FnBody
• case: Lean.Name → Lean.IR.VarId → Lean.IR.IRType → Array (Lean.IR.AltCore Lean.IR.FnBody) → Lean.IR.FnBody
• ret: Lean.IR.Arg → Lean.IR.FnBody

• Jump to join point j

  jmp: Lean.IR.JoinPointId → Array Lean.IR.Arg → Lean.IR.FnBody
• unreachable: Lean.IR.FnBody

instance Lean.IR.instInhabitedFnBody : Inhabited Lean.IR.FnBody

Equations

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

@[inline]

abbrev Lean.IR.FnBody.nil : Lean.IR.FnBody

Equations

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

@[export lean_ir_mk_vdecl]

def Lean.IR.mkVDecl (x : Lean.IR.VarId) (ty : Lean.IR.IRType) (e : Lean.IR.Expr) (b : Lean.IR.FnBody) : Lean.IR.FnBody

Equations

• Lean.IR.mkVDecl x ty e b = Lean.IR.FnBody.vdecl x ty e b

@[export lean_ir_mk_jdecl]

def Lean.IR.mkJDecl (j : Lean.IR.JoinPointId) (xs : Array Lean.IR.Param) (v : Lean.IR.FnBody) (b : Lean.IR.FnBody) : Lean.IR.FnBody

Equations

• Lean.IR.mkJDecl j xs v b = Lean.IR.FnBody.jdecl j xs v b

@[export lean_ir_mk_uset]

def Lean.IR.mkUSet (x : Lean.IR.VarId) (i : Nat) (y : Lean.IR.VarId) (b : Lean.IR.FnBody) : Lean.IR.FnBody

Equations

• Lean.IR.mkUSet x i y b = Lean.IR.FnBody.uset x i y b

@[export lean_ir_mk_sset]

def Lean.IR.mkSSet (x : Lean.IR.VarId) (i : Nat) (offset : Nat) (y : Lean.IR.VarId) (ty : Lean.IR.IRType) (b : Lean.IR.FnBody) : Lean.IR.FnBody

Equations

• Lean.IR.mkSSet x i offset y ty b = Lean.IR.FnBody.sset x i offset y ty b

@[export lean_ir_mk_case]

def Lean.IR.mkCase (tid : Lean.Name) (x : Lean.IR.VarId) (cs : Array (Lean.IR.AltCore Lean.IR.FnBody)) : Lean.IR.FnBody

Equations

• Lean.IR.mkCase tid x cs = Lean.IR.FnBody.case tid x Lean.IR.IRType.object cs

@[export lean_ir_mk_ret]

def Lean.IR.mkRet (x : Lean.IR.Arg) : Lean.IR.FnBody

Equations

• Lean.IR.mkRet x = Lean.IR.FnBody.ret x

@[export lean_ir_mk_jmp]

def Lean.IR.mkJmp (j : Lean.IR.JoinPointId) (ys : Array Lean.IR.Arg) : Lean.IR.FnBody

Equations

• Lean.IR.mkJmp j ys = Lean.IR.FnBody.jmp j ys

@[export lean_ir_mk_unreachable]

def Lean.IR.mkUnreachable : Unit → Lean.IR.FnBody

Equations

• Lean.IR.mkUnreachable x = Lean.IR.FnBody.unreachable

@[inline]

abbrev Lean.IR.Alt : Type

Equations

• Lean.IR.Alt = Lean.IR.AltCore Lean.IR.FnBody

@[match_pattern, inline]

abbrev Lean.IR.Alt.ctor (info : Lean.IR.CtorInfo) (b : Lean.IR.FnBody) : Lean.IR.AltCore Lean.IR.FnBody

Equations

• Lean.IR.Alt.ctor = Lean.IR.AltCore.ctor

@[match_pattern, inline]

abbrev Lean.IR.Alt.default (b : Lean.IR.FnBody) : Lean.IR.AltCore Lean.IR.FnBody

Equations

• Lean.IR.Alt.default = Lean.IR.AltCore.default

instance Lean.IR.instInhabitedAlt : Inhabited Lean.IR.Alt

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

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

Equations

• Lean.IR.FnBody.split b = let b' := Lean.IR.FnBody.body b; let c := Lean.IR.FnBody.resetBody b; (c, b')

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

Equations

• Lean.IR.AltCore.body x = match x with | Lean.IR.AltCore.ctor info b => b | Lean.IR.AltCore.default b => b

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

Equations

• Lean.IR.AltCore.setBody x x = match x, x with | Lean.IR.AltCore.ctor c b, b_1 => Lean.IR.Alt.ctor c b_1 | Lean.IR.AltCore.default b, b_1 => Lean.IR.Alt.default b_1

@[inline]

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

Equations

• Lean.IR.AltCore.modifyBody f x = match x with | Lean.IR.AltCore.ctor c b => Lean.IR.Alt.ctor c (f b) | Lean.IR.AltCore.default b => Lean.IR.Alt.default (f b)

@[inline]

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

Equations

• Lean.IR.AltCore.mmodifyBody f x = match x with | Lean.IR.AltCore.ctor c b => Lean.IR.Alt.ctor c <$> f b | Lean.IR.AltCore.default b => Lean.IR.Alt.default <$> f b

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

Equations

• Lean.IR.Alt.isDefault x = match x with | Lean.IR.AltCore.ctor info b => false | Lean.IR.AltCore.default b => true

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

Equations

• Lean.IR.push bs b = let b := Lean.IR.FnBody.resetBody b; Array.push bs b

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

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

Equations

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

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

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

Equations

• Lean.IR.reshape bs term = Lean.IR.reshapeAux bs (Array.size bs) term

@[inline]

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

Equations

• Lean.IR.modifyJPs bs f = Array.map (fun b => 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.mmodifyJPs {m : Type → Type} [inst : Monad m] (bs : Array Lean.IR.FnBody) (f : Lean.IR.FnBody → m Lean.IR.FnBody) : m (Array Lean.IR.FnBody)

Equations

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

@[export lean_ir_mk_alt]

def Lean.IR.mkAlt (n : Lean.Name) (cidx : Nat) (size : Nat) (usize : Nat) (ssize : Nat) (b : Lean.IR.FnBody) : Lean.IR.Alt

Equations

• Lean.IR.mkAlt n cidx size usize ssize b = Lean.IR.Alt.ctor { name := n, cidx := cidx, size := size, usize := usize, ssize := ssize } b

structure Lean.IR.DeclInfo : Type

• If some , then declaration depends on which uses a sorry axiom.

  sorryDep? : Option Lean.Name

Extra information associated with a declaration.

inductive Lean.IR.Decl : Type

• fdecl: Lean.IR.FunId → Array Lean.IR.Param → Lean.IR.IRType → Lean.IR.FnBody → Lean.IR.DeclInfo → Lean.IR.Decl
• extern: Lean.IR.FunId → Array Lean.IR.Param → Lean.IR.IRType → Lean.ExternAttrData → Lean.IR.Decl

instance Lean.IR.instInhabitedDecl : Inhabited Lean.IR.Decl

Equations

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

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

Equations

• Lean.IR.Decl.name x = match x with | Lean.IR.Decl.fdecl f xs type body info => f | Lean.IR.Decl.extern f xs type ext => f

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

Equations

• Lean.IR.Decl.params x = match x with | Lean.IR.Decl.fdecl f xs type body info => xs | Lean.IR.Decl.extern f xs type ext => xs

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

Equations

• Lean.IR.Decl.resultType x = match x with | Lean.IR.Decl.fdecl f xs t body info => t | Lean.IR.Decl.extern f xs t ext => t

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

Equations

• Lean.IR.Decl.isExtern x = match x with | Lean.IR.Decl.extern f xs type ext => true | x => false

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

Equations

• Lean.IR.Decl.getInfo x = match x with | Lean.IR.Decl.fdecl f xs type body info => info | x => { sorryDep? := none }

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

Equations

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

@[export lean_ir_mk_decl]

def Lean.IR.mkDecl (f : Lean.IR.FunId) (xs : Array Lean.IR.Param) (ty : Lean.IR.IRType) (b : Lean.IR.FnBody) : Lean.IR.Decl

Equations

• Lean.IR.mkDecl f xs ty b = Lean.IR.Decl.fdecl f xs ty b { sorryDep? := none }

@[export lean_ir_mk_extern_decl]

def Lean.IR.mkExternDecl (f : Lean.IR.FunId) (xs : Array Lean.IR.Param) (ty : Lean.IR.IRType) (e : Lean.ExternAttrData) : Lean.IR.Decl

Equations

• Lean.IR.mkExternDecl f xs ty e = Lean.IR.Decl.extern f xs ty e

@[export lean_ir_mk_dummy_extern_decl]

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

Equations

• Lean.IR.mkDummyExternDecl f xs ty = Lean.IR.Decl.fdecl f xs ty Lean.IR.FnBody.unreachable { sorryDep? := none }

@[inline]

abbrev Lean.IR.IndexSet : Type

Set of variable and join point names

Equations

• Lean.IR.IndexSet = Lean.RBTree Lean.IR.Index compare

instance Lean.IR.instInhabitedIndexSet : Inhabited Lean.IR.IndexSet

Equations

• Lean.IR.instInhabitedIndexSet = { default := ∅ }

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

Equations

• Lean.IR.mkIndexSet idx = Lean.RBTree.insert Lean.RBTree.empty idx

inductive Lean.IR.LocalContextEntry : Type

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

@[inline]

abbrev Lean.IR.LocalContext : Type

Equations

• Lean.IR.LocalContext = Lean.RBMap Lean.IR.Index Lean.IR.LocalContextEntry compare

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.IR.LocalContext.addParams ctx ps = Array.foldl Lean.IR.LocalContext.addParam ctx ps 0 (Array.size ps)

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

Equations

• Lean.IR.LocalContext.isJP ctx idx = match Lean.RBMap.find? ctx idx with | some (Lean.IR.LocalContextEntry.joinPoint a a_1) => true | x => false

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

Equations

• Lean.IR.LocalContext.getJPBody ctx j = match Lean.RBMap.find? ctx j.idx with | some (Lean.IR.LocalContextEntry.joinPoint a b) => some b | x => none

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

Equations

• Lean.IR.LocalContext.getJPParams ctx j = match Lean.RBMap.find? ctx j.idx with | some (Lean.IR.LocalContextEntry.joinPoint ys a) => some ys | x => none

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

Equations

• Lean.IR.LocalContext.isParam ctx idx = match Lean.RBMap.find? ctx idx with | some (Lean.IR.LocalContextEntry.param a) => true | x => false

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

Equations

• Lean.IR.LocalContext.isLocalVar ctx idx = match Lean.RBMap.find? ctx idx with | some (Lean.IR.LocalContextEntry.localVar a a_1) => true | x => false

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

Equations

• Lean.IR.LocalContext.contains ctx idx = Lean.RBMap.contains ctx idx

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

Equations

• Lean.IR.LocalContext.eraseJoinPointDecl ctx j = Lean.RBMap.erase ctx j.idx

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

Equations

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

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

Equations

• Lean.IR.LocalContext.getValue ctx x = match Lean.RBMap.find? ctx x.idx with | some (Lean.IR.LocalContextEntry.localVar a v) => some v | x => none

@[inline]

abbrev Lean.IR.IndexRenaming : Type

Equations

• Lean.IR.IndexRenaming = Lean.RBMap Lean.IR.Index Lean.IR.Index compare

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

• aeqv : Lean.IR.IndexRenaming → α → α → Bool

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

Equations

• Lean.IR.VarId.alphaEqv ρ v₁ v₂ = match Lean.RBMap.find? ρ v₁.idx with | some v => v == v₂.idx | none => v₁ == v₂

instance Lean.IR.instAlphaEqvVarId : Lean.IR.AlphaEqv Lean.IR.VarId

Equations

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

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

Equations

• Lean.IR.Arg.alphaEqv ρ x x = match x, x with | Lean.IR.Arg.var v₁, Lean.IR.Arg.var v₂ => Lean.IR.aeqv ρ v₁ v₂ | Lean.IR.Arg.irrelevant, Lean.IR.Arg.irrelevant => true | x, x_1 => false

instance Lean.IR.instAlphaEqvArg : Lean.IR.AlphaEqv Lean.IR.Arg

Equations

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

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

Equations

• Lean.IR.args.alphaEqv ρ args₁ args₂ = Array.isEqv args₁ args₂ fun a b => Lean.IR.aeqv ρ a b

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

Equations

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

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

Equations

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

instance Lean.IR.instAlphaEqvExpr : Lean.IR.AlphaEqv Lean.IR.Expr

Equations

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

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

Equations

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

def Lean.IR.addParamRename (ρ : Lean.IR.IndexRenaming) (p₁ : Lean.IR.Param) (p₂ : Lean.IR.Param) : Option Lean.IR.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 (ρ : Lean.IR.IndexRenaming) (ps₁ : Array Lean.IR.Param) (ps₂ : Array Lean.IR.Param) : Option Lean.IR.IndexRenaming

Equations

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

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

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

Equations

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

instance Lean.IR.instBEqFnBody : BEq Lean.IR.FnBody

Equations

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

@[inline]

abbrev Lean.IR.VarIdSet : Type

Equations

• Lean.IR.VarIdSet = Lean.RBTree Lean.IR.VarId fun x y => compare x.idx y.idx

instance Lean.IR.instInhabitedVarIdSet : Inhabited Lean.IR.VarIdSet

Equations

• Lean.IR.instInhabitedVarIdSet = { default := ∅ }

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

Equations

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

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

Equations

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