Shape-Tagged Tensors

A small existential package for storing tensors whose shapes are known only at runtime. The package and its shape-changing adjacent-swap operation are shared by executable tensor interpreters.

@[reducible, inline]

abbrev Spec.PackedTensor (alpha : Type) [Context alpha] : Type

A tensor paired with the shape that indexes its type.

def Spec.PackedTensor.shape {alpha : Type} [Context alpha] (value : PackedTensor alpha) : Shape

The runtime shape carried by a packed tensor.

def Spec.PackedTensor.tensor {alpha : Type} [Context alpha] (value : PackedTensor alpha) : Tensor alpha value.shape

The tensor stored in a packed tensor, indexed by its recovered shape.

def Spec.PackedTensor.mk {alpha : Type} [Context alpha] (shape : Shape) (tensor : Tensor alpha shape) : PackedTensor alpha

Package a statically shaped tensor for shape-erased storage.

def Spec.PackedTensor.swapAdjacentAtDepth {alpha : Type} [Context alpha] (value : PackedTensor alpha) (depth : ℕ) : PackedTensor alpha

Swap two adjacent axes at depth, retaining the resulting shape in the package.