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.
Instances For
- 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. -
structandunionare 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.
Instances For
- 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.
Instances For
Instances For
- num: Nat → Lean.IR.LitVal
- str: String → Lean.IR.LitVal
Instances For
Constructor information.
nameis the Name of the Constructor in Lean.cidxis the Constructor index (aka tag).sizeis the number of arguments of typeobject/tobject.usizeis the number of arguments of typeusize.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 USize (i.e., size_t)
scalar values, and a sequence of other scalar values.
Instances For
- 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
Extract the
Usizevalue at Positionsizeof(void*)*ifromx. - sproj: Nat → Nat → Lean.IR.VarId → Lean.IR.Expr
Extract the scalar value at Position
sizeof(void*)*n + offsetfromx. - fap: Lean.IR.FunId → Array Lean.IR.Arg → Lean.IR.Expr
Full application.
- 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
Given
x : [t]object, obtain the scalar value. - lit: Lean.IR.LitVal → Lean.IR.Expr
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
- ctor: {FnBody : Type} → Lean.IR.CtorInfo → FnBody → Lean.IR.AltCore FnBody
- default: {FnBody : Type} → FnBody → Lean.IR.AltCore FnBody
Instances For
- 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
j - unreachable: Lean.IR.FnBody
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
If b is a non terminal, then return a pair (c, b') s.t. b == c <;> b',
and c.body == FnBody.nil
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
If
some, then declaration depends onwhich uses asorryaxiom.
Extra information associated with a declaration.
Instances For
- 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
Instances For
Instances For
Instances For
Instances For
Instances For
Set of variable and join point names
Instances For
- 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