Tensor Shape-Erasure Boundary

Conversions between statically shape-indexed TensorPack values and arrays of existentially packaged Spec.SomeTensor values. Runtime tapes and heterogeneous external data use the erased representation; typed computation should recover a TensorPack immediately after crossing that boundary.

def TorchLean.TensorPack.toShapeErasedArray {α : Type} [Storage α] {ss : List Spec.Shape} : TensorPack α ss → Array (Spec.SomeTensor α)

Erase the individual tensor shapes in a typed pack into a runtime array.

def TorchLean.TensorPack.toIndexedShapeErasedArray {α : Type} [Storage α] {ss : List Spec.Shape} : TensorPack α ss → ℕ → Array (ℕ × Spec.SomeTensor α)

Tag each shape-erased tensor with its runtime index, beginning at start.

def TorchLean.TensorPack.toShapeErasedArrayAux {α : Type} [Storage α] {ss : List Spec.Shape} : TensorPack α ss → Array (Spec.SomeTensor α) → Array (Spec.SomeTensor α)

Push the shape-erased tensors of a pack onto acc, from the head of the pack onward.

theorem TorchLean.TensorPack.toShapeErasedArrayAux_eq {α : Type} [Storage α] {ss : List Spec.Shape} (tensors : TensorPack α ss) (acc : Array (Spec.SomeTensor α)) : tensors.toShapeErasedArrayAux acc = acc ++ tensors.toShapeErasedArray

Pushing onto acc appends the ordinary shape erasure to it.

def TorchLean.TensorPack.toShapeErasedArrayFast {α : Type} [Storage α] {ss : List Spec.Shape} (tensors : TensorPack α ss) : Array (Spec.SomeTensor α)

toShapeErasedArray in one pass of pushes, which replaces it in compiled code.

@[csimp]

theorem TorchLean.TensorPack.toShapeErasedArray_eq_toShapeErasedArrayFast : @toShapeErasedArray = @toShapeErasedArrayFast

Compiled code runs toShapeErasedArrayFast in place of toShapeErasedArray.

def TorchLean.TensorPack.toIndexedShapeErasedArrayAux {α : Type} [Storage α] {ss : List Spec.Shape} : TensorPack α ss → ℕ → Array (ℕ × Spec.SomeTensor α) → Array (ℕ × Spec.SomeTensor α)

Push the indexed shape-erased tensors of a pack onto acc, numbering from index.

theorem TorchLean.TensorPack.toIndexedShapeErasedArrayAux_eq {α : Type} [Storage α] {ss : List Spec.Shape} (tensors : TensorPack α ss) (index : ℕ) (acc : Array (ℕ × Spec.SomeTensor α)) : tensors.toIndexedShapeErasedArrayAux index acc = acc ++ tensors.toIndexedShapeErasedArray index

Pushing onto acc appends the ordinary indexed shape erasure to it.

def TorchLean.TensorPack.toIndexedShapeErasedArrayFast {α : Type} [Storage α] {ss : List Spec.Shape} (tensors : TensorPack α ss) (index : ℕ) : Array (ℕ × Spec.SomeTensor α)

toIndexedShapeErasedArray in one pass of pushes, which replaces it in compiled code.

@[csimp]

theorem TorchLean.TensorPack.toIndexedShapeErasedArray_eq_toIndexedShapeErasedArrayFast : @toIndexedShapeErasedArray = @toIndexedShapeErasedArrayFast

Compiled code runs toIndexedShapeErasedArrayFast in place of the indexed erasure.

def TorchLean.TensorPack.ofShapeErasedArray {α : Type} [Storage α] (values : Array (Spec.SomeTensor α)) (start : ℕ := 0) {shapes : List Spec.Shape} : Except String (TensorPack α shapes)

Recover a statically shape-indexed pack from a prefix of a shape-erased runtime array.

start selects the first array entry to consume. The conversion checks every stored shape and fails if the array is too short or an entry has the wrong shape. Entries after the requested pack are intentionally ignored, which supports recovering a typed prefix of a larger runtime context.