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.
- 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 Lake.Name → Array Lean.IR.IRType → Lean.IR.IRType
- union: Lake.Name → Array Lean.IR.IRType → Lean.IR.IRType
Low Level IR types. Most are self explanatory.
usizerepresents the C++
size_tType. 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.
irrelevantfor Lean types, propositions and proofs.
objecta pointer to a value in the heap.
tobjecta pointer to a value in the heap or tagged pointer (i.e., the least significant bit is 1) storing a scalar value.
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
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.
x occurs only at a single
ret x instruction. That is, it is being consumed by being returned.
x occurs only at a single
ctor. That is, it is being "consumed" by being stored into another
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.
Arguments to applications, constructors, etc.
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.
nameis the Name of the Constructor in Lean.
cidxis the Constructor index (aka tag).
sizeis the number of arguments of type
usizeis the number of arguments of type
ssizeis 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
scalar values, and a sequence of other scalar values.
- ctor: Lean.IR.CtorInfo → Array Lean.IR.Arg → Lean.IR.Expr
- reset: Nat → Lean.IR.VarId → Lean.IR.Expr
- reuse: Lean.IR.VarId → Lean.IR.CtorInfo → Bool → Array Lean.IR.Arg → Lean.IR.Expr
- proj: Nat → Lean.IR.VarId → Lean.IR.Expr
- uproj: Nat → Lean.IR.VarId → Lean.IR.Expr
Usizevalue at Position
- sproj: Nat → Nat → Lean.IR.VarId → Lean.IR.Expr
Extract the scalar value at Position
sizeof(void*)*n + offsetfrom
- fap: Lean.IR.FunId → Array Lean.IR.Arg → Lean.IR.Expr
- pap: Lean.IR.FunId → Array Lean.IR.Arg → Lean.IR.Expr
Partial application that creates a
papvalue (aka closure in our nonstandard terminology).
- ap: Lean.IR.VarId → Array Lean.IR.Arg → Lean.IR.Expr
- box: Lean.IR.IRType → Lean.IR.VarId → Lean.IR.Expr
- unbox: Lean.IR.VarId → Lean.IR.Expr
x : [t]object, obtain the scalar value.
- lit: Lean.IR.LitVal → Lean.IR.Expr
- vdecl: Lean.IR.VarId → Lean.IR.IRType → Lean.IR.Expr → Lean.IR.FnBody → Lean.IR.FnBody
- jdecl: Lean.IR.JoinPointId → Array Lean.IR.Param → Lean.IR.FnBody → Lean.IR.FnBody → Lean.IR.FnBody
Join point Declaration
block_j (xs) := e; b
- 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
- uset: Lean.IR.VarId → Nat → Lean.IR.VarId → Lean.IR.FnBody → Lean.IR.FnBody
- sset: Lean.IR.VarId → Nat → Nat → Lean.IR.VarId → Lean.IR.IRType → Lean.IR.FnBody → Lean.IR.FnBody
- inc: Lean.IR.VarId → Nat → Bool → Bool → Lean.IR.FnBody → Lean.IR.FnBody
- 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: Lake.Name → Lean.IR.VarId → Lean.IR.IRType → Array (Lean.IR.AltCore Lean.IR.FnBody) → Lean.IR.FnBody
- ret: Lean.IR.Arg → Lean.IR.FnBody
- jmp: Lean.IR.JoinPointId → Array Lean.IR.Arg → Lean.IR.FnBody
Jump to join point
- unreachable: Lean.IR.FnBody