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

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

                              Equations
                                Instances For
                                  Equations
                                    Instances For
                                      Instances For
                                        • nextIdx : Index
                                        • auxDecls : Array 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.

                                        • auxDeclCache : AssocList FnBody Expr
                                        • nextAuxId : Nat
                                        Instances For
                                          @[reducible, inline]
                                          Equations
                                            Instances For
                                              Equations
                                                Instances For
                                                  Equations
                                                    Instances For
                                                      @[inline]
                                                      def Lean.IR.ExplicitBoxing.withParams {α : Type} (xs : Array Param) (k : M α) :
                                                      M α
                                                      Equations
                                                        Instances For
                                                          @[inline]
                                                          def Lean.IR.ExplicitBoxing.withVDecl {α : Type} (x : VarId) (ty : IRType) (v : Expr) (k : M α) :
                                                          M α
                                                          Equations
                                                            Instances For
                                                              @[inline]
                                                              def Lean.IR.ExplicitBoxing.withJDecl {α : Type} (j : JoinPointId) (xs : Array Param) (v : FnBody) (k : M α) :
                                                              M α
                                                              Equations
                                                                Instances For
                                                                  def Lean.IR.ExplicitBoxing.mkCast (x : VarId) (xType expectedType : IRType) :

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