def Lean.Compiler.«term◾» : ParserDescr

def Lean.Compiler.LCNF.erasedExpr : Expr

def Lean.Compiler.LCNF.anyExpr : Expr

def Lean.Expr.isVoid (e : Expr) : Bool

def Lean.Expr.isErased (e : Expr) : Bool

def Lean.Expr.isAny (e : Expr) : Bool

def Lean.Compiler.LCNF.isPropFormerTypeQuick : Expr → Bool

def Lean.Compiler.LCNF.isPropFormerType (type : Expr) : MetaM Bool

Return true iff type is Prop or As → Prop.

def Lean.Compiler.LCNF.isPropFormer (e : Expr) : MetaM Bool

Return true iff e : Prop or e : As → Prop.

The code generator uses a format based on A-normal form. This normal form uses many let-expressions and it is very convenient for applying compiler transformations. However, it creates a few issues in a dependently typed programming language.

• Many casts are needed.
• It is too expensive to ensure we are not losing typeability when creating join points and simplifying let-values
• It may not be possible to create a join point because the resulting expression is not type correct. For example, suppose we are trying to create a join point for making the following match terminal.

  let x := match a with | true => b | false => c;
  k[x]
  

  and want to transform this code into

  let jp := fun x => k[x]
  match a with
  | true => jp b
  | false => jp c
  

  where jp is a new join point (i.e., a local function that is always fully applied and tail recursive). In many examples in the Lean code-base, we have to skip this transformation because it produces a type-incorrect term. Recall that types/propositions in k[x] may rely on the fact that x is definitionally equal to match a with ... before the creation of the join point.

Thus, in the first code generator pass, we convert types into a LCNFType (Lean Compiler Normal Form Type). The method toLCNFType produces a type with the following properties:

• All constants occurring in the result type are inductive datatypes.
• The arguments of type formers are type formers, or ◾. We use ◾ to denote erased information.
• All type definitions are expanded. If reduction gets stuck, it is replaced with ◾.

Remark: you can view ◾ occurring in a type position as the "any type". Remark: in our runtime, ◾ is represented as box(0).

The goal is to preserve as much information as possible and avoid the problems described above. Then, we don't have let x := v; ... in LCNF code when x is a type former. If the user provides a let x := v; ... where x is a type former, we can always expand it when converting into LCNF. Thus, given a let x := v, ... in occurring in LCNF, we know x cannot occur in any type since it is not a type former.

We try to preserve type information because they unlock new optimizations, and we can type check the result produced by each code generator step.

Below, we provide some example programs and their erased variants: -- 1. Source type: f: (n: Nat) -> (tupleN Nat n). LCNF type: f: Nat -> ◾. We convert the return type (tupleN Nat n) to ◾, since we cannot reduce (tupleN Nat n)to a term of the form(InductiveTy ...)`.

-- 2. Source type: f: (n: Nat) (fin: Fin n) -> (tupleN Nat fin). LCNF type: f: Nat -> Fin ◾ -> ◾. Since (Fin n) has dependency on n, we erase the n to get the type (Fin ◾).

def Lean.Compiler.LCNF.toLCNFType (type : Expr) : MetaM Expr

Convert a Lean type into a LCNF type used by the code generator.

partial def Lean.Compiler.LCNF.joinTypes (a b : Expr) : Expr

partial def Lean.Compiler.LCNF.joinTypes? (a b : Expr) : Option Expr

partial def Lean.Compiler.LCNF.isTypeFormerType (type : Expr) : Bool

Return true if type is a LCNF type former type.

Remark: This is faster than Lean.Meta.isTypeFormer, as this assumes that the input type is an LCNF type.

def Lean.Compiler.LCNF.instantiateForall (type : Expr) (ps : Array Expr) : CoreM Expr

Given a LCNF type of the form forall (a_1 : A_1) ... (a_n : A_n), B[a_1, ..., a_n] and p_1 : A_1, ... p_n : A_n, return B[p_1, ..., p_n].

Remark: similar to Meta.instantiateForall, buf for LCNF types.

partial def Lean.Compiler.LCNF.isPredicateType (type : Expr) : Bool

Return true if type is a predicate. Examples: Nat → Prop, Prop, Int → Bool → Prop.

partial def Lean.Compiler.LCNF.maybeTypeFormerType (type : Expr) : Bool

Return true if type is a LCNF type former type or it is an "any" type. This function is similar to isTypeFormerType, but more liberal. For example, isTypeFormerType returns false for ◾ and Nat → ◾, but this function returns true.

def Lean.Compiler.LCNF.isClass? (type : Expr) : CoreM (Option Name)

isClass? type return some ClsName if the LCNF type is an instance of the class ClsName.

partial def Lean.Compiler.LCNF.isArrowClass? (type : Expr) : CoreM (Option Name)

isArrowClass? type return some ClsName if the LCNF type is an instance of the class ClsName, or if it is arrow producing an instance of the class ClsName.

partial def Lean.Compiler.LCNF.getArrowArity (e : Expr) : Nat

def Lean.Compiler.LCNF.isInductiveWithNoCtors (type : Expr) : CoreM Bool

Return true if type is an inductive datatype with 0 constructors.

def Lean.Compiler.LCNF.mkBoxedName (n : Name) : Name

def Lean.Compiler.LCNF.isBoxedName (name : Name) : Bool

This section defines the low level IR types used in the impure phase of LCNF.

@[match_pattern, inline]

def Lean.Compiler.LCNF.ImpureType.float : Expr

float is a 64-bit floating point number.

@[match_pattern, inline]

def Lean.Compiler.LCNF.ImpureType.float32 : Expr

float32 is a 32-bit floating point number.

@[match_pattern, inline]

def Lean.Compiler.LCNF.ImpureType.uint8 : Expr

uint8 is an 8-bit unsigned integer.

@[match_pattern, inline]

def Lean.Compiler.LCNF.ImpureType.uint16 : Expr

uint16 is a 16-bit unsigned integer.

@[match_pattern, inline]

def Lean.Compiler.LCNF.ImpureType.uint32 : Expr

uint32 is a 32-bit unsigned integer.

@[match_pattern, inline]

def Lean.Compiler.LCNF.ImpureType.uint64 : Expr

uint64 is a 64-bit unsigned integer.

@[match_pattern, inline]

def Lean.Compiler.LCNF.ImpureType.usize : Expr

usize represents the C size_t type. It has a separate representation because depending on the target architecture it has a different width and we try to generate platform independent C code.

We generally assume that sizeof(size_t) == sizeof(void).

@[match_pattern, inline]

def Lean.Compiler.LCNF.ImpureType.erased : Expr

erased represents type arguments, propositions and proofs which are no longer relevant at this point in time.

@[match_pattern, inline]

def Lean.Compiler.LCNF.ImpureType.object : Expr

@[match_pattern, inline]

def Lean.Compiler.LCNF.ImpureType.tobject : Expr

tobject is either an object or a tagged pointer.

Crucially the RC the RC operations for tobject are slightly more expensive because we first need to test whether the tobject is really a pointer or not.

@[match_pattern, inline]

def Lean.Compiler.LCNF.ImpureType.tagged : Expr

tagged` is a tagged pointer (i.e., the least significant bit is 1) storing a scalar value.

@[match_pattern, inline]

def Lean.Compiler.LCNF.ImpureType.void : Expr

void is used to identify uses of the state token from BaseIO which do no longer need to be passed around etc. at this point in the pipeline.

def Lean.Compiler.LCNF.ImpureType.Lean.Expr.isScalar : Expr → Bool

Whether the type is a scalar as opposed to a pointer (or a value disguised as a pointer).

def Lean.Compiler.LCNF.ImpureType.Lean.Expr.isObj : Expr → Bool

Whether the type is an object which is to say a pointer or a value disguised as a pointer.

def Lean.Compiler.LCNF.ImpureType.Lean.Expr.isPossibleRef : Expr → Bool

Whether the type might be an actual pointer (crucially this excludes tagged).

def Lean.Compiler.LCNF.ImpureType.Lean.Expr.isDefiniteRef : Expr → Bool

Whether the type is a pointer for sure.

def Lean.Compiler.LCNF.ImpureType.Lean.Expr.boxed : Expr → Expr

The boxed version of types.