Lean.Compiler.LCNF.Types

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, and ⊤ the any type.
All type definitions are expanded. If reduction gets stuck, it is replaced with ⊤.

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 -> Any. We convert the return type (tupleN Nat n) to Any, 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 Erased -> Any. Since (Fin n) has dependency on n, we erase the n to get the type (Fin Erased). See that Erased only occurs at argument position to a type constructor.

NOTE: we cannot have separate notions of ErasedProof (which occurs at the value level for erased proofs) and ErasedData (which occurs at the type level for erased dependencies) because of universe polymorphism. Thus, we have a single notion of Erased which unifies the two concepts.

source

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

Lean.MetaM Lean.Expr

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

source

partial def Lean.Compiler.LCNF.toLCNFType.whnfEta (type : Lean.Expr) :

Lean.MetaM Lean.Expr

source

partial def Lean.Compiler.LCNF.toLCNFType.visitForall (e : Lean.Expr) (xs : Array Lean.Expr) :

Lean.MetaM Lean.Expr

source

partial def Lean.Compiler.LCNF.toLCNFType.visitApp (f : Lean.Expr) (args : Array Lean.Expr) :

Lean.MetaM Lean.Expr

source

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

Lean.Expr

source

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

Option Lean.Expr

source

partial def Lean.Compiler.LCNF.isTypeFormerType (type : Lean.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.

source

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

Bool

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

source

partial def Lean.Compiler.LCNF.maybeTypeFormerType (type : Lean.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 lcAny and Nat → lcAny, but this function returns true.

source

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

Lean.CoreM (Option Lean.Name)

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

Equations

One or more equations did not get rendered due to their size.

source

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

Lean.CoreM (Option Lean.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.

source

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

Nat