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
    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]
      @[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
        Instances For
          Instances For
            @[inline, reducible]
            Instances For
              @[inline, reducible]
              Instances For
                @[inline, reducible]
                Instances For

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

                  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.

                      Return true iff c.size ≤ n

                      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

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

                          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.

                            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.

                                Instances For
                                  @[inline, reducible]
                                  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.

                                    Instances For