Documentation

Lean.Compiler.LCNF.Types

Equations
  • e.isErased = e.isAppOf `lcErased
Instances For

    Return true iff type is Prop or As → Prop.

    Equations
    Instances For

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

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

        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:

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

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

        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.

        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
        Instances For
          @[irreducible]
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

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

            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.

            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

              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.

              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