Documentation

Lean.Compiler.IR.Boxing

Add explicit boxing and unboxing instructions. Recall that the Lean to λ_pure compiler produces code without these instructions.

Assumptions:

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

            Infer scrutinee type using case alternatives. This can be done whenever alts does not contain an Alt.default _ value.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              • nextIdx : Lean.IR.Index
              • auxDecls : Array Lean.IR.Decl

                We create auxiliary declarations when boxing constant and literals. The idea is to avoid code such as

                let x1 := Uint64.inhabited;
                let x2 := box x1;
                ...
                

                We currently do not cache these declarations in an environment extension, but we use auxDeclCache to avoid creating equivalent auxiliary declarations more than once when processing the same IR declaration.

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

                            Auxiliary function used by castVarIfNeeded. It is used when the expected type does not match xType. If xType is scalar, then we need to "box" it. Otherwise, we need to "unbox" it.

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