Tensor loaders

These helpers convert simple in-memory Lean containers into typed tensors and datasets.

This is the canonical runtime layer for shape-checked construction from lists/arrays. The public API re-exports these helpers from NN.API.Data; that is not a second implementation, just the user-facing namespace. Keeping the implementation here is useful because the CSV/NPY loaders and training examples can share the same Result error model and the same Dataset type without depending on the higher-level API facade.

Tensor construction from lists

def Runtime.Autograd.Train.vectorOfList {a : Type} [Zero a] (tag : String) (n : ℕ) (xs : List a) : Result (Spec.Tensor a (Spec.Shape.dim n Spec.Shape.scalar))

Build a length-n vector from a list, with a length check.

This is the safe list boundary for dependent tensor shapes: callers bring ordinary runtime data, and the loader either proves the length matches n internally or returns a tagged error.

def Runtime.Autograd.Train.vectorOfArray {a : Type} [Zero a] (tag : String) (n : ℕ) (xs : Array a) : Result (Spec.Tensor a (Spec.Shape.dim n Spec.Shape.scalar))

Build a length-n vector from an Array, using the same checks as vectorOfList.

def Runtime.Autograd.Train.matrixOfLists {a : Type} [Zero a] (tag : String) (m n : ℕ) (rows : List (List a)) : Result (Spec.Tensor a (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar)))

Build an m×n matrix from a list of m rows, each of length n.

Both dimensions are checked before constructing the dependent tensor. If a row has the wrong length, the error reports the first bad row so data issues are easier to diagnose.

def Runtime.Autograd.Train.matrixOfLists.findBad {a : Type} (n : ℕ) : ℕ → List (List a) → Option (ℕ × ℕ)

def Runtime.Autograd.Train.matrixOfArrays {a : Type} [Zero a] (tag : String) (m n : ℕ) (rows : Array (Array a)) : Result (Spec.Tensor a (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar)))

Build an m×n matrix from an Array (Array a), using the same checks as matrixOfLists.

@[simp]

theorem Runtime.Autograd.Train.vectorOfArray_eq_vectorOfList {a : Type} [Zero a] (tag : String) (n : ℕ) (xs : Array a) : vectorOfArray tag n xs = vectorOfList tag n xs.toList

Array-backed vector loading is definitionally list-backed vector loading after toList.

@[simp]

theorem Runtime.Autograd.Train.matrixOfArrays_eq_matrixOfLists {a : Type} [Zero a] (tag : String) (m n : ℕ) (rows : Array (Array a)) : matrixOfArrays tag m n rows = matrixOfLists tag m n (List.map Array.toList rows.toList)

Array-backed matrix loading is definitionally list-backed matrix loading after toList.

Dataset helpers

def Runtime.Autograd.Train.datasetOfPairs {a b : Type} (tag : String) (xs : List a) (ys : List b) : Result (Dataset (a × b))

Zip two lists into a Dataset of pairs, with a length check.

def Runtime.Autograd.Train.datasetOfListVectors {a : Type} [Zero a] (tag : String) (n : ℕ) (rows : List (List a)) : Result (Dataset (Spec.Tensor a (Spec.Shape.dim n Spec.Shape.scalar)))

Convert list-rows into a dataset of length-n vectors.

@[simp]

theorem Runtime.Autograd.Train.datasetOfPairs_eq_ok {a b : Type} (tag : String) (xs : List a) (ys : List b) (h : xs.length = ys.length) : datasetOfPairs tag xs ys = Except.ok (Dataset.ofList (xs.zip ys))

Pair datasets succeed exactly as List.zip when the two sides have the same length.

@[simp]

theorem Runtime.Autograd.Train.datasetOfPairs_eq_error {a b : Type} (tag : String) (xs : List a) (ys : List b) (h : xs.length ≠ ys.length) : datasetOfPairs tag xs ys = Except.error (tagError tag (toString "length mismatch: " ++ toString xs.length ++ toString " vs " ++ toString ys.length))

Pair datasets fail before zipping if the two sides have different lengths.