TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Tensor.Conversion

Tensor Conversion #

Total in-memory conversion belongs here. Sources carry their intrinsic shape: ordinary arrays and lists become vectors, while future structured sources may provide richer shapes through Tensor.From.

Changing only the interpretation of a flat row-major buffer is Tensor.reshape and requires a proof that the scalar count is unchanged. Validation of external files and untrusted runtime metadata belongs in the corresponding loader.

source
class TorchLean.Tensor.SourceShape (source : Type) :
Type

Intrinsic tensor shape described by an in-memory source value.

  • shape : source → Spec.Shape

    Shape intrinsically described by the source value.

Instances
    source
    class TorchLean.Tensor.From (source : Type) (α : outParam Type) [Storage α] [SourceShape source] :
    Type

    Extensible, total materialization of a shaped in-memory source.

    Instances
      source
      def TorchLean.Tensor.from {source α : Type} [Storage α] [SourceShape source] [conversion : From source α] (value : source) :
      Tensor α (SourceShape.shape value)

      Convert an in-memory value into a tensor with its intrinsic shape.

      Instances For
        source
        @[instance_reducible]
        instance TorchLean.Tensor.arraySourceShape {α : Type} :
        SourceShape (Array α)

        An Array describes one dimension, its length.

        The shape is computed from the value rather than declared by the caller, which is what lets Tensor.from be written without a shape annotation.

        source
        @[simp]
        theorem TorchLean.Tensor.sourceShape_array {α : Type} (values : Array α) :
        SourceShape.shape values = [values.size]

        The shape an Array describes is its length.

        source
        @[instance_reducible]
        instance TorchLean.Tensor.arrayFrom {α : Type} [Storage α] :
        From (Array α) α

        Materialize an Array as a rank-one tensor; the buffer is already row-major.

        source
        @[instance_reducible]
        instance TorchLean.Tensor.listSourceShape {α : Type} :
        SourceShape (List α)

        A List behaves like an Array: one dimension, its length.

        source
        @[simp]
        theorem TorchLean.Tensor.sourceShape_list {α : Type} (values : List α) :
        SourceShape.shape values = [values.length]

        The shape a List describes is its length.

        source
        @[instance_reducible]
        instance TorchLean.Tensor.listFrom {α : Type} [Storage α] :
        From (List α) α

        Materialize a List as a rank-one tensor, copying once through List.toArray.

        source
        @[instance_reducible]
        instance TorchLean.Tensor.vectorSourceShape {α : Type} {n : ℕ} :
        SourceShape (Vector α n)

        A Vector α n carries its length in its type, so the shape is known without inspecting the value at all.

        source
        @[simp]
        theorem TorchLean.Tensor.sourceShape_vector {α : Type} {n : ℕ} (values : Vector α n) :
        SourceShape.shape values = [n]

        The shape a Vector α n describes is [n], independently of the value.

        source
        @[instance_reducible]
        instance TorchLean.Tensor.vectorFrom {α : Type} [Storage α] {n : ℕ} :
        From (Vector α n) α

        Materialize a Vector α n as a Tensor α [n]; no length check is needed.

        source
        @[instance_reducible]
        instance TorchLean.Tensor.floatArraySourceShape :
        SourceShape FloatArray

        A FloatArray describes one dimension, the length reported by its Storage instance.

        source
        @[instance_reducible]
        instance TorchLean.Tensor.floatArrayFrom :
        From FloatArray Float

        A FloatArray is already the unboxed Float storage, so materialization is a rewrap.

        source
        @[instance_reducible]
        instance TorchLean.Tensor.byteArraySourceShape :
        SourceShape ByteArray

        A ByteArray describes one dimension, the length reported by its Storage instance.

        source
        @[instance_reducible]
        instance TorchLean.Tensor.byteArrayFrom :
        From ByteArray UInt8

        A ByteArray is already the unboxed UInt8 storage, so materialization is a rewrap.

        source
        def TorchLean.Tensor.reshape {α : Type} [Storage α] {source : Spec.Shape} (tensor : Tensor α source) (target : Spec.Shape) (hSize : source.size = target.size := by decide) :
        Tensor α target

        Reinterpret the same row-major buffer at an equal-size shape.

        The equality is the complete safety condition: reshape neither pads, truncates, nor moves scalar data.

        Example:

        -- Same buffer, new shape. The size equality is the entire safety condition, and it is checked
-- here rather than trusted.
def matrix (flat : Tensor Float [12]) : Tensor Float [3, 4] :=
  Tensor.reshape flat [3, 4]
        Instances For
          source
          class TorchLean.Tensor.To (α : Type) [Storage α] (shape : Spec.Shape) (target : Type) :
          Type

          Extensible conversion from a tensor to a requested in-memory target type.

          • convert : Tensor α shape → target

            Materialize or expose the requested target representation.

          Instances
            source
            @[reducible, inline]
            abbrev TorchLean.Tensor.to {α : Type} [Storage α] {shape : Spec.Shape} (tensor : Tensor α shape) (target : Type) [conversion : To α shape target] :
            target

            Convert a tensor to the requested target type.

            Instances For
              source
              @[instance_reducible]
              instance TorchLean.Tensor.arrayTo {α : Type} [Storage α] {shape : Spec.Shape} :
              To α shape (Array α)

              Read a tensor out as its row-major array.

              source
              @[instance_reducible]
              instance TorchLean.Tensor.listTo {α : Type} [Storage α] {shape : Spec.Shape} :
              To α shape (List α)

              Read a tensor out as its row-major list.

              source
              @[instance_reducible]
              instance TorchLean.Tensor.vectorTo {α : Type} [Storage α] {shape : Spec.Shape} :
              To α shape (Vector α shape.size)

              Read a tensor out as a length-indexed vector.

              source
              @[instance_reducible]
              instance TorchLean.Tensor.floatArrayTo {shape : Spec.Shape} :
              To Float shape FloatArray

              Expose the native buffer of a Float tensor.

              source
              @[instance_reducible]
              instance TorchLean.Tensor.byteArrayTo {shape : Spec.Shape} :
              To UInt8 shape ByteArray

              Expose the native buffer of a byte tensor.

              source
              @[simp]
              theorem TorchLean.Tensor.to_array_eq_data {α : Type} [Storage α] {shape : Spec.Shape} (tensor : Tensor α shape) :
              tensor.to (Array α) = Internal.Rep.data tensor

              Converting to Array exposes the row-major observation, boxing packed storage if needed.

              source
              @[simp]
              theorem TorchLean.Tensor.to_list_eq_data {α : Type} [Storage α] {shape : Spec.Shape} (tensor : Tensor α shape) :
              tensor.to (List α) = (Internal.Rep.data tensor).toList

              Converting to List is the array conversion followed by Array.toList.

              source
              @[simp]
              theorem TorchLean.Tensor.to_array_from_array {α : Type} [Storage α] (values : Array α) :
              («from» values).to (Array α) = values

              Array in, array out: Tensor.from then Tensor.to is the identity.

              Importing and exporting preserves the entries and their order. The list round trips below reuse this array result.

              source
              @[simp]
              theorem TorchLean.Tensor.to_list_from_array {α : Type} [Storage α] (values : Array α) :
              («from» values).to (List α) = values.toList

              Array in, list out.

              source
              @[simp]
              theorem TorchLean.Tensor.to_list_from_list {α : Type} [Storage α] (values : List α) :
              («from» values).to (List α) = values

              List in, list out.

              source
              @[simp]
              theorem TorchLean.Tensor.to_array_castShape {α : Type} [Storage α] {source target : Spec.Shape} (tensor : Tensor α source) (hShape : source = target) :
              (tensor.castShape hShape).to (Array α) = tensor.to (Array α)

              A shape cast does not touch the data, so exporting before or after it gives the same array.

              This is the statement that makes castShape free: it is a retyping, not a copy.

              source
              @[simp]
              theorem TorchLean.Tensor.to_list_castShape {α : Type} [Storage α] {source target : Spec.Shape} (tensor : Tensor α source) (hShape : source = target) :
              (tensor.castShape hShape).to (List α) = tensor.to (List α)

              The list version of to_array_castShape.

              source
              @[simp]
              theorem TorchLean.Tensor.to_array_reshape {α : Type} [Storage α] {source target : Spec.Shape} (tensor : Tensor α source) (hSize : source.size = target.size) :
              (tensor.reshape target hSize).to (Array α) = tensor.to (Array α)

              Reshaping is likewise data-preserving: only the interpretation of the flat buffer changes.

              Together with to_array_castShape this pins down the row-major convention. A reshape that permuted elements would break this lemma, so it doubles as a regression test on the layout.

              source
              @[simp]
              theorem TorchLean.Tensor.to_list_full {α : Type} [Storage α] (shape : Spec.Shape) (value : α) :
              (full shape value).to (List α) = List.replicate shape.size value

              Converting a filled tensor to a list produces one value per scalar position.

              source
              @[simp]
              theorem TorchLean.Tensor.to_shape_full (rank value : ℕ) :
              (full [rank] value).to Spec.Shape = Spec.Shape.ofList (List.replicate rank value)

              A filled natural-number vector describes the corresponding uniform shape.

              source
              theorem TorchLean.Tensor.prod_eq_to_list_prod {α : Type} [Storage α] [Monoid α] {n : ℕ} (tensor : Tensor α [n]) :
              tensor.prod = (tensor.to (List α)).prod

              Native vector multiplication agrees with the product of its list conversion.

              source
              @[simp]
              theorem TorchLean.Tensor.size_to_shape {rank : ℕ} (tensor : Tensor ℕ [rank]) :
              (tensor.to Spec.Shape).size = tensor.prod

              Converting a natural-number vector to a shape preserves its product as the shape size.