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.
Function identifier
Equations
Instances For
Equations
- Lean.IR.instInhabitedVarId = { default := { idx := default } }
Equations
- Lean.IR.instReprVarId = { reprPrec := Lean.IR.reprVarId✝ }
Equations
- Lean.IR.instInhabitedJoinPointId = { default := { idx := default } }
Equations
- Lean.IR.instReprJoinPointId = { reprPrec := Lean.IR.reprJoinPointId✝ }
Instances For
Equations
- Lean.IR.instBEqVarId = { beq := fun (a b : Lean.IR.VarId) => a.idx == b.idx }
Equations
- Lean.IR.instBEqJoinPointId = { beq := fun (a b : Lean.IR.JoinPointId) => a.idx == b.idx }
Equations
- Lean.IR.instToStringJoinPointId = { toString := fun (a : Lean.IR.JoinPointId) => "block_" ++ toString a.idx }
Equations
- Lean.IR.instToFormatJoinPointId = { format := fun (a : Lean.IR.JoinPointId) => Std.Format.text (toString a) }
Equations
- Lean.IR.instHashableJoinPointId = { hash := fun (a : Lean.IR.JoinPointId) => hash a.idx }
Equations
Instances For
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
andunion
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: 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
Instances For
Equations
- Lean.IR.instInhabitedIRType = { default := Lean.IR.IRType.float }
Equations
- Lean.IR.IRType.float.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
Instances For
Equations
- (Lean.IR.IRType.struct leanTypeName types).isStruct = true
- x.isStruct = false
Instances For
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.
- var: Lean.IR.VarId → Lean.IR.Arg
- irrelevant: Lean.IR.Arg
Instances For
Equations
- Lean.IR.instInhabitedArg = { default := Lean.IR.Arg.var default }
- num: Nat → Lean.IR.LitVal
- str: String → Lean.IR.LitVal
Instances For
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 typeobject/tobject
.usize
is the number of arguments of typeusize
.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
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
Usize
value at Positionsizeof(void*)*i
fromx
. - sproj: Nat → Nat → Lean.IR.VarId → Lean.IR.Expr
Extract the scalar value at Position
sizeof(void*)*n + offset
fromx
. - 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
pap
value (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
Equations
- Lean.IR.mkFAppExpr c ys = Lean.IR.Expr.fap c ys
Instances For
Equations
- Lean.IR.mkPAppExpr c ys = Lean.IR.Expr.pap c ys
Instances For
Instances For
Equations
- Lean.IR.instInhabitedParam = { default := { x := default, borrow := default, ty := default } }
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: 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
- 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
Equations
- Lean.IR.mkCase tid x cs = Lean.IR.FnBody.case tid x Lean.IR.IRType.object cs
Instances For
Equations
Instances For
Instances For
Equations
Instances For
Equations
Instances For
Instances For
Equations
- Lean.IR.Alt.default = Lean.IR.AltCore.default
Instances For
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
Instances For
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
- (Lean.IR.FnBody.mdata d b).body = b
- x.body = x
Instances For
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
- (Lean.IR.FnBody.mdata d b).setBody x = Lean.IR.FnBody.mdata d x
- x✝.setBody x = x✝
Instances For
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)
Instances For
Equations
Instances For
Equations
- Lean.IR.push bs b = bs.push b.resetBody
Instances For
Instances For
Equations
- Lean.IR.reshape bs term = Lean.IR.reshapeAux bs bs.size term
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Extra information associated with a declaration.
If
some <blame>
, then declaration depends on<blame>
which uses asorry
axiom.
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
Equations
- Lean.IR.instInhabitedDecl = { default := Lean.IR.Decl.extern default default default default }
Equations
- (Lean.IR.Decl.fdecl f xs type body info).name = f
- (Lean.IR.Decl.extern f xs type ext).name = f
Instances For
Equations
- (Lean.IR.Decl.fdecl f xs type body info).getInfo = info
- x.getInfo = { sorryDep? := none }
Instances For
Instances For
Equations
- Lean.IR.mkDecl f xs ty b = Lean.IR.Decl.fdecl f xs ty b { sorryDep? := none }
Instances For
Equations
- Lean.IR.mkExternDecl f xs ty e = Lean.IR.Decl.extern f xs ty e
Instances For
Equations
- Lean.IR.mkDummyExternDecl f xs ty = Lean.IR.Decl.fdecl f xs ty Lean.IR.FnBody.unreachable { sorryDep? := none }
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
Instances For
Equations
Instances For
Instances For
Equations
- ctx.addJP j xs b = Lean.RBMap.insert ctx j.idx (Lean.IR.LocalContextEntry.joinPoint xs b)
Instances For
Instances For
Equations
- ctx.addParams ps = Array.foldl Lean.IR.LocalContext.addParam ctx ps
Instances For
Equations
- ctx.isJP idx = match Lean.RBMap.find? ctx idx with | some (Lean.IR.LocalContextEntry.joinPoint a a_1) => true | x => false
Instances For
Equations
- ctx.getJPBody j = match Lean.RBMap.find? ctx j.idx with | some (Lean.IR.LocalContextEntry.joinPoint a b) => some b | x => none
Instances For
Instances For
Instances For
Instances For
Instances For
Equations
- ctx.eraseJoinPointDecl j = Lean.RBMap.erase ctx j.idx
Instances For
Instances For
Equations
- ctx.getValue x = match Lean.RBMap.find? ctx x.idx with | some (Lean.IR.LocalContextEntry.localVar a v) => some v | x => none
Instances For
Equations
- Lean.IR.VarId.alphaEqv ρ v₁ v₂ = match Lean.RBMap.find? ρ v₁.idx with | some v => v == v₂.idx | none => v₁ == v₂
Instances For
Instances For
Instances For
Instances For
Equations
- Lean.IR.instAlphaEqvExpr = { aeqv := Lean.IR.Expr.alphaEqv }
Instances For
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
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- b₁.beq b₂ = Lean.IR.FnBody.alphaEqv ∅ b₁ b₂
Instances For
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 t = "lean_unbox"