Lean Compiler Normal Form (LCNF) #
It is based on the A-normal form, and the approach described in the paper Compiling without continuations.
This type is used to index the fundamental LCNF IR data structures. Depending on its value different constructors are available for the different semantic phases of LCNF.
Notably in order to save memory we never index the IR types over Purity. Instead the type is
parametrized by the phase and the individual constructors might carry a proof (that will be erased)
that they are only allowed in a certain phase.
- pure : Purity
The code we are acting on is still pure, things like reordering up to value dependencies are acceptable.
- impure : Purity
The code we are acting on is to be considered generally impure, doing reorderings is potentially no longer legal.
Instances For
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
- lit
{pu : Purity}
(value : LitValue)
: LetValue pu
A literal value.
- erased
{pu : Purity}
: LetValue pu
An erased value that is irrelevant for computation.
- proj
{pu : Purity}
(typeName : Name)
(idx : Nat)
(struct : FVarId)
(h : pu = Purity.pure := by purity_tac)
: LetValue pu
A projection from a pure LCNF value.
- const
{pu : Purity}
(declName : Name)
(us : List Level)
(args : Array (Arg pu))
(h : pu = Purity.pure := by purity_tac)
: LetValue pu
A pure application of a constant.
- fvar
{pu : Purity}
(fvarId : FVarId)
(args : Array (Arg pu))
: LetValue pu
An application of a free variable
- ctor
{pu : Purity}
(i : CtorInfo)
(args : Array (Arg pu))
(h : pu = Purity.impure := by purity_tac)
: LetValue pu
Allocating a constructor.
- oproj
{pu : Purity}
(i : Nat)
(var : FVarId)
(h : pu = Purity.impure := by purity_tac)
: LetValue pu
Projecting objects out of a value.
- uproj
{pu : Purity}
(i : Nat)
(var : FVarId)
(h : pu = Purity.impure := by purity_tac)
: LetValue pu
Projecting USize scalars out of a value.
- sproj
{pu : Purity}
(n offset : Nat)
(var : FVarId)
(h : pu = Purity.impure := by purity_tac)
: LetValue pu
Projecting non-USize scalars out of a value
- fap
{pu : Purity}
(fn : Name)
(args : Array (Arg pu))
(h : pu = Purity.impure := by purity_tac)
: LetValue pu
Full, impure, application of a function.
- pap
{pu : Purity}
(fn : Name)
(args : Array (Arg pu))
(h : pu = Purity.impure := by purity_tac)
: LetValue pu
Partial application of a function.
- reset
{pu : Purity}
(n : Nat)
(var : FVarId)
(h : pu = Purity.impure := by purity_tac)
: LetValue pu
The reset instruction from Counting Immutable Beans.
nis the amount of object fields stored in the constructor invar. - reuse
{pu : Purity}
(var : FVarId)
(i : CtorInfo)
(updateHeader : Bool)
(args : Array (Arg pu))
(h : pu = Purity.impure := by purity_tac)
: LetValue pu
reuse x in ctor_i ysinstruction in the paper.updateHeaderis set if the tag in the new ctor differs from the one in the old ctor and thus needs to be updated. - box
{pu : Purity}
(ty : Expr)
(fvarId : FVarId)
(h : pu = Purity.impure := by purity_tac)
: LetValue pu
Given a scalar type
tyand a valuefvarId : ty, this operation returns a value of typetobject. For small scalar values the result is a tagged pointer, and no memory allocation is performed. - unbox
{pu : Purity}
(fvarId : FVarId)
(h : pu = Purity.impure := by purity_tac)
: LetValue pu
Given
fvarId : [t]object, obtain the underlying scalar value.
Instances For
Instances For
- let {pu : Purity} (decl : LetDecl pu) (k : Code pu) : Code pu
- fun {pu : Purity} (decl : FunDecl pu) (k : Code pu) (h : pu = Purity.pure := by purity_tac) : Code pu
- jp {pu : Purity} (decl : FunDecl pu) (k : Code pu) : Code pu
- jmp {pu : Purity} (fvarId : FVarId) (args : Array (Arg pu)) : Code pu
- cases {pu : Purity} (cases : Cases pu) : Code pu
- return {pu : Purity} (fvarId : FVarId) : Code pu
- unreach {pu : Purity} (type : Expr) : Code pu
- uset {pu : Purity} (fvarId : FVarId) (i : Nat) (y : FVarId) (k : Code pu) (h : pu = Purity.impure := by purity_tac) : Code pu
- sset {pu : Purity} (fvarId : FVarId) (i offset : Nat) (y : FVarId) (ty : Expr) (k : Code pu) (h : pu = Purity.impure := by purity_tac) : Code pu
- inc {pu : Purity} (fvarId : FVarId) (n : Nat) (check persistent : Bool) (k : Code pu) (h : pu = Purity.impure := by purity_tac) : Code pu
- dec {pu : Purity} (fvarId : FVarId) (n : Nat) (check persistent : Bool) (k : Code pu) (h : pu = Purity.impure := by purity_tac) : Code pu
Instances For
Instances For
Instances For
Instances For
Return the constructor names that have an explicit (non-default) alternative.
Instances For
- let {pu : Purity} (decl : LetDecl pu) : CodeDecl pu
- fun {pu : Purity} (decl : FunDecl pu) (h : pu = Purity.pure := by purity_tac) : CodeDecl pu
- jp {pu : Purity} (decl : FunDecl pu) : CodeDecl pu
- uset {pu : Purity} (fvarId : FVarId) (i : Nat) (y : FVarId) (h : pu = Purity.impure := by purity_tac) : CodeDecl pu
- sset {pu : Purity} (fvarId : FVarId) (i offset : Nat) (y : FVarId) (ty : Expr) (h : pu = Purity.impure := by purity_tac) : CodeDecl pu
- inc {pu : Purity} (fvarId : FVarId) (n : Nat) (check persistent : Bool) (h : pu = Purity.impure := by purity_tac) : CodeDecl pu
- dec {pu : Purity} (fvarId : FVarId) (n : Nat) (check persistent : Bool) (h : pu = Purity.impure := by purity_tac) : CodeDecl pu
Instances For
Instances For
Low-level update LetDecl function. It does not update the local context.
Consider using LetDecl.update : LetDecl → Expr → Expr → CompilerM LetDecl if you want the local context
to be updated.
Low-level update FunDecl function. It does not update the local context.
Consider using FunDecl.update : LetDecl → Expr → Array Param → Code → CompilerM FunDecl if you want the local context
to be updated.
Instances For
Instances For
The signature of a declaration being processed by the Lean to Lean compiler passes.
- name : Name
The name of the declaration from the
Environmentit came from Universe level parameter names.
- type : Expr
The type of the declaration. Note that this is an erased LCNF type instead of the fully dependent one that might have been the original type of the declaration in the
Environment. Furthermore, once in the impure staged of LCNF this type is only the return type. Parameters.
- safe : Bool
We set this flag to false during LCNF conversion if the Lean function associated with this function was tagged as partial or unsafe. This information affects how static analyzers treat function applications of this kind. See
DefinitionSafety.partialandunsafefunctions may not be terminating, but Lean functions terminate, and some static analyzers exploit this fact. So, we use the following semantics. Suppose we have a (large) natural numberC. We consider a nondeterministic model for computation of Lean expressions as follows: Each call to a partial/unsafe function uses up one "recursion token". Prior to consumingCrecursion tokens all partial functions must be called as normal. Once the model has used upCrecursion tokens, a subsequent call to a partial function has the following nondeterministic options: it can either call the function again, or return any value of the target type (even a noncomputable one). Larger values ofCyield less nondeterminism in the model, but even the intersection of all choices ofCyields nondeterminism wheredef loop : A := loopreturns any value of typeA. The compiler fixes a choice forC. This is a fixed constant greater than 2^2^64, which is allowed to be compiler and architecture dependent, and promises that it will produce an execution consistent with every possible nondeterministic outcome of theC-model. In the event that different nondeterministic executions disagree, the compiler is required to exhaust resources or output a looping computation.
Instances For
Instances For
Declaration being processed by the Lean to Lean compiler passes.
- value : DeclValue pu
The body of the declaration, usually changes as it progresses through compiler passes.
- recursive : Bool
We set this flag to true during LCNF conversion. When we receive a block of functions to be compiled, we set this flag to
trueif there is an application to the function in the block containing it. This is an approximation, but it should be good enough because in the frontend, we invoke the compiler with blocks of strongly connected components only. We use this information to control inlining. - inlineAttr? : Option InlineAttributeKind
We store the inline attribute at LCNF declarations to make sure we can set them for auxiliary declarations created during compilation.
Instances For
Instances For
Instances For
Return true if the given declaration has been annotated with [inline], [inline_if_reduce], [macro_inline], or [always_inline]
Instances For
Return true if the arrow type contains an instance implicit argument.
Instances For
Instances For
Instances For
Traverse the given block of potentially mutually recursive functions
and mark a declaration f as recursive if there is an application
f ... in the block.
This is an overapproximation, and relies on the fact that our frontend
computes strongly connected components.
See comment at recursive field.