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
and want to transform this code into
let x := match a with | true => b | false => c; k[x]
let jp := fun x => k[x] match a with | true => jp b | false => jp c
jpis 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
xis 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).
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
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).
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 ...)`.
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,
B[p_1, ..., p_n].
Remark: similar to
Meta.instantiateForall, buf for LCNF types.
type is a LCNF type former type or it is an "any" type.
This function is similar to
isTypeFormerType, but more liberal.
isTypeFormerType returns false for
Nat → ◾, but
this function returns true.