Packed Tensors

The public result type shared by pack and unpack. Component shapes live in the type, so ordinary unpacking does not expose an anonymous metadata tuple.

structure TorchLean.Tensor.Packed (α : Type) (shape : Spec.Shape) (componentShapes : List Spec.Shape) [Storage α] : Type

A tensor produced by pack, indexed by the star shape of every source tensor.

Use unpack packed pattern to recover the source tensors. The packed tensor is available as packed.tensor, and packed.shapes exposes the recorded component shapes.

The pack elaborator computes this metadata, and unpack checks it against the pattern and packed shape. The public constructor itself carries no proof that arbitrary componentShapes describe a valid partition of shape.

• tensor : Tensor α shape

  Row-major tensor containing every packed component. Scalar storage is chosen by Storage α.

def TorchLean.Tensor.Packed.shapes {α : Type} {shape : Spec.Shape} {componentShapes : List Spec.Shape} [Storage α] : Packed α shape componentShapes → List Spec.Shape

Return the star shapes recorded in the component-shape index.