source
def Lean.Compiler.«term◾» :
ParserDescr
Equations

- Lean.Compiler.«term◾» = Lean.ParserDescr.node `Lean.Compiler.«term◾» 1024 (Lean.ParserDescr.symbol "◾")

Instances For

source
def Lean.Compiler.LCNF.erasedExpr :
Expr
Equations

- Lean.Compiler.LCNF.erasedExpr = Lean.mkConst `lcErased

Instances For

source
def Lean.Compiler.LCNF.anyExpr :
Expr
Equations

- Lean.Compiler.LCNF.anyExpr = Lean.mkConst `lcAny

Instances For

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

- e.isErased = e.isAppOf `lcErased

Instances For

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

- e.isAny = e.isAppOf `lcAny

Instances For

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

- Lean.Compiler.LCNF.isPropFormerTypeQuick (Lean.Expr.forallE binderName binderType b binderInfo) = Lean.Compiler.LCNF.isPropFormerTypeQuick b
- Lean.Compiler.LCNF.isPropFormerTypeQuick (Lean.Expr.sort Lean.Level.zero) = true
- Lean.Compiler.LCNF.isPropFormerTypeQuick x✝ = false

Instances For

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

Return true iff `type` is `Prop` or `As → Prop`.

Equations

- Lean.Compiler.LCNF.isPropFormerType type = match Lean.Compiler.LCNF.isPropFormerTypeQuick type with | true => pure true | false => Lean.Compiler.LCNF.isPropFormerType.go✝ type #[]

Instances For

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

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

Equations

- Lean.Compiler.LCNF.isPropFormer e = do let __do_lift ← Lean.Meta.inferType e Lean.Compiler.LCNF.isPropFormerType __do_lift

Instances For

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 ◾)`.

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

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

Equations

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

Instances For

source
partial def Lean.Compiler.LCNF.joinTypes (a b : Expr) :
Expr
source
partial def Lean.Compiler.LCNF.joinTypes? (a b : Expr) :
Option Expr
source
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.

source
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.

Equations

- Lean.Compiler.LCNF.instantiateForall type ps = Lean.Compiler.LCNF.instantiateForall.go✝ ps 0 type

Instances For

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

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

source
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.

source
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`.

Equations

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

Instances For

source
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`.

source
partial def Lean.Compiler.LCNF.getArrowArity (e : Expr) :
Nat
source
def Lean.Compiler.LCNF.isInductiveWithNoCtors (type : Expr) :
CoreM Bool

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

Equations

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

Instances For