Flatten (Spec.Tensor → FloatArray)

Row-major order with outermost axis first and innermost axis last.

def Runtime.Autograd.Cuda.Convert.flattenFloatAux {s : Spec.Shape} : Spec.Tensor Float s → FloatArray → FloatArray

Worker for flattenFloat.

The accumulator lets us append in one left-to-right row-major traversal instead of repeatedly concatenating intermediate arrays.

def Runtime.Autograd.Cuda.Convert.flattenFloat {s : Spec.Shape} (t : Spec.Tensor Float s) : FloatArray

Flatten a Spec.Tensor Float s into a row-major FloatArray (CUDA-compatible).

def Runtime.Autograd.Cuda.Convert.flattenBoolMaskAux {s : Spec.Shape} : Spec.Tensor Bool s → FloatArray → FloatArray

Worker for flattenBoolMask; true is encoded as 1.0, false as 0.0.

def Runtime.Autograd.Cuda.Convert.flattenBoolMask {s : Spec.Shape} (mask : Spec.Tensor Bool s) : FloatArray

Flatten a Spec.Tensor Bool s mask to FloatArray as 0.0/1.0 values in row-major order.

Unflatten (FloatArray → Spec.Tensor)

These functions assume row-major order. The ? variants check the expected length and return none on mismatch.

def Runtime.Autograd.Cuda.Convert.unflattenFloatAux {s : Spec.Shape} : FloatArray → (offset : ℕ) → Spec.Tensor Float s

Worker for unflattenFloatUnsafe.

offset is the row-major starting position for the current tensor subtree. The caller is responsible for ensuring the array contains at least offset + Shape.size s elements.

def Runtime.Autograd.Cuda.Convert.unflattenFloatUnsafe {s : Spec.Shape} (a : FloatArray) : Spec.Tensor Float s

Unflatten a row-major FloatArray into a Spec.Tensor Float s (unsafe: assumes correct size).

def Runtime.Autograd.Cuda.Convert.unflattenFloat? {s : Spec.Shape} (a : FloatArray) : Option (Spec.Tensor Float s)

Unflatten a row-major FloatArray into a Spec.Tensor Float s when a.size matches.

def Runtime.Autograd.Cuda.Convert.unflattenBoolMaskAux {s : Spec.Shape} : FloatArray → (offset : ℕ) → Spec.Tensor Bool s

Worker for unflattenBoolMaskUnsafe.

The CUDA mask convention is deliberately simple: zero means false, any nonzero value means true.

def Runtime.Autograd.Cuda.Convert.unflattenBoolMaskUnsafe {s : Spec.Shape} (a : FloatArray) : Spec.Tensor Bool s

Unflatten a FloatArray into a Spec.Tensor Bool s mask (unsafe: nonzero = true).

def Runtime.Autograd.Cuda.Convert.unflattenBoolMask? {s : Spec.Shape} (a : FloatArray) : Option (Spec.Tensor Bool s)

Unflatten a FloatArray into a Spec.Tensor Bool s mask when a.size matches.