Documentation

Lean.Compiler.LCNF.Basic

Lean Compiler Normal Form (LCNF) #

It is based on the A-normal form, and the approach described in the paper Compiling without continuations.

Instances For
    Equations
    Instances For
      Equations
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.Arg.updateTypeImp]
          @[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.Arg.updateFVarImp]
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateProjImp]
            @[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateConstImp]
            @[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateFVarImp]
            @[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateArgsImp]
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Instances For
                Equations
                Instances For
                  Equations
                  • Lean.Compiler.LCNF.instInhabitedFunDeclCore = { default := { fvarId := default, binderName := default, params := default, type := default, value := default } }
                  Instances For
                    Equations
                    • Lean.Compiler.LCNF.instInhabitedCasesCore = { default := { typeName := default, resultType := default, discr := default, alts := default } }

                    Return the constructor names that have an explicit (non-default) alternative.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.eqImp]
                          @[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.eqFunDecl]
                          @[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateAltCodeImp]
                          @[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateAltImp]
                          @[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateAltsImp]
                          @[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateCasesImp]
                          @[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateLetImp]
                          @[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateContImp]
                          @[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateFunImp]
                          @[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateReturnImp]
                          @[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateJmpImp]
                          @[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateUnreachImp]
                          @[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateParamCoreImp]

                          Low-level update Param function. It does not update the local context. Consider using Param.update : Param → Expr → CompilerM Param if you want the local context to be updated.

                          @[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateLetDeclCoreImp]

                          Low-level update LetDecl function. It does not update the local context. Consider using LetDecl.update : LetDecl → Expr → Expr → CompilerM LetDecl if you want the local context to be updated.

                          @[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateFunDeclCoreImp]

                          Low-level update FunDecl function. It does not update the local context. Consider using FunDecl.update : LetDecl → Expr → Array ParamCode → CompilerM FunDecl if you want the local context to be updated.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              Equations
                              Instances For
                                Equations
                                Instances For
                                  • name : Lake.Name

                                    The name of the declaration from the Environment it came from

                                  • levelParams : List Lake.Name

                                    Universe level parameter names.

                                  • type : Lean.Expr

                                    The type of the declaration. Note that this is an erased LCNF type instead of the fully dependent one that might have been the original type of the declaration in the Environment.

                                  • Parameters.

                                  • The body of the declaration, usually changes as it progresses through compiler passes.

                                  • recursive : Bool

                                    We set this flag to true during LCNF conversion. When we receive a block of functions to be compiled, we set this flag to true if there is an application to the function in the block containing it. This is an approximation, but it should be good enough because in the frontend, we invoke the compiler with blocks of strongly connected components only. We use this information to control inlining.

                                  • safe : Bool

                                    We set this flag to false during LCNF conversion if the Lean function associated with this function was tagged as partial or unsafe. This information affects how static analyzers treat function applications of this kind. See DefinitionSafety. partial and unsafe functions may not be terminating, but Lean functions terminate, and some static analyzers exploit this fact. So, we use the following semantics. Suppose whe hav a (large) natural number C. We consider a nondeterministic model for computation of Lean expressions as follows: Each call to a partial/unsafe function uses up one "recursion token". Prior to consuming C recursion tokens all partial functions must be called as normal. Once the model has used up C recursion tokens, a subsequent call to a partial function has the following nondeterministic options: it can either call the function again, or return any value of the target type (even a noncomputable one). Larger values of C yield less nondeterminism in the model, but even the intersection of all choices of C yields nondeterminism where def loop : A := loop returns any value of type A. The compiler fixes a choice for C. This is a fixed constant greater than 2^2^64, which is allowed to be compiler and architecture dependent, and promises that it will produce an execution consistent with every possible nondeterministic outcome of the C-model. In the event that different nondeterministic executions disagree, the compiler is required to exhaust resources or output a looping computation.

                                  • We store the inline attribute at LCNF declarations to make sure we can set them for auxliary declarations created during compilation.

                                  Declaration being processed by the Lean to Lean compiler passes.

                                  Instances For
                                    Equations
                                    • One or more equations did not get rendered due to their size.

                                    Return true if the given declaration has been annotated with [inline], [inline_if_reduce], [macro_inline], or [always_inline]

                                    Equations
                                    Instances For

                                      Return some i if decl is of the form

                                      def f (a_0 ... a_i ...) :=
                                        ...
                                        cases a_i
                                        | ...
                                        | ...
                                      

                                      That is, f is a sequence of declarations followed by a cases on the parameter i. We use this function to decide whether we should inline a declaration tagged with [inline_if_reduce] or not.

                                      Equations
                                      Instances For
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For

                                                  Return true if the arrow type contains an instance implicit argument.

                                                  Equations
                                                  Instances For

                                                    Return true if decl is supposed to be inlined/specialized.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For

                                                      Traverse the given block of potentially mutually recursive functions and mark a declaration f as recursive if there is an application f ... in the block. This is an overapproximation, and relies on the fact that our frontend computes strongly connected components. See comment at recursive field.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For