# Documentation

Lean.Compiler.IR.Basic

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]

Function identifier

Equations
@[inline]
Equations
structure Lean.IR.VarId :

Variable identifier

Instances For
Equations

Join point identifier

Instances For
Equations
@[inline]
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
@[inline]
Equations
@[inline]
Equations
inductive 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.

Instances For
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• = match x with | Lean.IR.IRType.object => true | Lean.IR.IRType.tobject => true | x => false
Equations
• = match x with | Lean.IR.IRType.irrelevant => true | x => false
Equations
Equations
inductive 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
Equations
Equations
@[export lean_ir_mk_var_arg]
Equations
inductive Lean.IR.LitVal :
• num:
• str:
Instances For
Equations
• = match x, x with | , => v₁ == v₂ | , => v₁ == v₂ | x, x_1 => false

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.

Instances For
Equations
• One or more equations did not get rendered due to their size.
Equations
inductive Lean.IR.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.

ctor:
• reset:
• reuse x in ctor_i ys instruction in the paper.

reuse:
• 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:
• Extract the Usize value at Position sizeof(void*)*i from x.

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

sproj:
• Full application.

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

pap:
• Application. x must be a pap value.

ap:
• 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:
• Given x : [t]object, obtain the scalar value.

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

isShared:
Instances For
@[export lean_ir_mk_ctor_expr]
def Lean.IR.mkCtorExpr (n : Lean.Name) (cidx : Nat) (size : Nat) (usize : Nat) (ssize : Nat) (ys : ) :
Equations
@[export lean_ir_mk_proj_expr]
Equations
@[export lean_ir_mk_uproj_expr]
Equations
@[export lean_ir_mk_sproj_expr]
Equations
@[export lean_ir_mk_fapp_expr]
Equations
@[export lean_ir_mk_papp_expr]
Equations
@[export lean_ir_mk_app_expr]
Equations
@[export lean_ir_mk_num_expr]
Equations
@[export lean_ir_mk_str_expr]
Equations
structure Lean.IR.Param :
Instances For
Equations
@[export lean_ir_mk_param]
Equations
inductive Lean.IR.AltCore (FnBody : Type) :
Instances For
inductive Lean.IR.FnBody :
• let x : ty := e; b

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

jdecl:
• 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:
• setTag:
• Store y : Usize at Position sizeof(void*)*i in x. x must be a Constructor object and RC(x) must be 1.

uset:
• 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:
• 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.VarIdNat
• 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.VarIdNat
• del:
• mdata:
• case:
• ret:
• Jump to join point j

jmp:
• unreachable: Lean.IR.FnBody
Instances For
@[inline]
Equations
@[export lean_ir_mk_vdecl]
Equations
@[export lean_ir_mk_jdecl]
Equations
@[export lean_ir_mk_uset]
Equations
@[export lean_ir_mk_sset]
Equations
@[export lean_ir_mk_case]
Equations
@[export lean_ir_mk_ret]
Equations
@[export lean_ir_mk_jmp]
Equations
@[export lean_ir_mk_unreachable]
Equations
@[inline]
Equations
@[match_pattern, inline]
Equations
@[match_pattern, inline]
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
@[inline]
Equations
@[inline]

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

Equations
• = let b' := ; let c := ; (c, b')
Equations
Equations
@[inline]
Equations
@[inline]
def Lean.IR.AltCore.mmodifyBody {m : } [inst : ] (f : ) :
Equations
• = match x with | => <\$> f b | =>
Equations
def Lean.IR.push (bs : ) (b : Lean.IR.FnBody) :
Equations
partial def Lean.IR.flattenAux (b : Lean.IR.FnBody) (r : ) :
Equations
@[inline]
def Lean.IR.modifyJPs (bs : ) (f : ) :
Equations
@[inline]
def Lean.IR.mmodifyJPs {m : } [inst : ] (bs : ) (f : ) :
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) :
Equations
• If some , then declaration depends on which uses a sorry axiom.

sorryDep? :

Extra information associated with a declaration.

Instances For
inductive Lean.IR.Decl :
• fdecl:
• extern:
Instances For
Equations
Equations
Equations
Equations
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
@[export lean_ir_mk_decl]
Equations
@[export lean_ir_mk_extern_decl]
Equations
@[export lean_ir_mk_dummy_extern_decl]
Equations
@[inline]

Set of variable and join point names

Equations
Equations
Equations
• param:
• localVar:
• joinPoint:
Instances For
@[inline]
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
@[inline]
Equations
class Lean.IR.AlphaEqv (α : Type) :
Instances
Equations
Equations
def Lean.IR.args.alphaEqv (args₁ : ) (args₂ : ) :
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
def Lean.IR.addParamsRename (ps₁ : ) (ps₂ : ) :
Equations
• One or more equations did not get rendered due to their size.
@[inline]
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.