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
      @[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]
      @[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]
      Instances For
        Equations
        Instances For
          Equations
          • Lean.Compiler.LCNF.instInhabitedFunDeclCore = { default := { fvarId := default, binderName := default, params := default, type := default, value := default } }
          Equations
          • decl.getArity = decl.params.size
          Instances For
            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
                @[irreducible]
                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]
                  Equations
                  Instances For
                    @[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
                      Instances For

                        Return true iff c.size ≤ n

                        Equations
                        Instances For
                          Equations
                          Instances For

                            Declaration being processed by the Lean to Lean compiler passes.

                            • 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 we have 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 auxiliary declarations created during compilation.

                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Equations
                              • decl.size = decl.value.size
                              Instances For
                                Equations
                                • decl.getArity = decl.params.size
                                Instances For
                                  Equations
                                  Instances For
                                    Equations
                                    Instances For
                                      Equations
                                      Instances For
                                        Equations
                                        Instances For

                                          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
                                              • decl.instantiateTypeLevelParams us = decl.type.instantiateLevelParamsNoCache decl.levelParams us
                                              Instances For
                                                Equations
                                                • decl.instantiateParamsLevelParams us = decl.params.mapMono fun (param : Lean.Compiler.LCNF.Param) => param.updateCore (param.type.instantiateLevelParamsNoCache decl.levelParams us)
                                                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