Dataset Sources

Typed NPY and CSV sources for supervised and labeled datasets.

def TorchLean.Data.readNpyTensor (path : System.FilePath) (dims : List ℕ) : IO (Except String (Spec.Tensor Float (NN.Tensor.shapeOfDims dims)))

Load an N-D tensor from a .npy file, checking the on-disk shape matches dims.

def TorchLean.Data.readNpyTensorPrefix (path : System.FilePath) (dims : List ℕ) : IO (Except String (Spec.Tensor Float (NN.Tensor.shapeOfDims dims)))

Load an N-D tensor from a .npy file, allowing the file to contain more rows on the leading axis.

This is the dataset-loader analogue of taking tensor[:n] in PyTorch. The rank and trailing dimensions must still match exactly; only the leading dimension may be larger than requested.

We use this for dataset sources rather than the stricter readNpyTensor because an exported dataset usually has a fixed full size, while local runs often request a bounded prefix. For example, a CIFAR file may have shape (50000, 3, 32, 32) while an example command asks for n = 80; the resulting TorchLean tensor has type-level shape (80, 3, 32, 32).

This is still a checked loader, not an implicit reshape:

• rank must agree;
• all trailing dimensions must agree;
• the file must contain at least the requested number of rows;
• only C-order NPY files can be prefix-loaded efficiently by the low-level parser.

def TorchLean.Data.natLabelOfFloat (tag : String) (classes : ℕ) (x : Float) : Except String ℕ

Parse a float-encoded class label as a Nat in [0, classes).

def TorchLean.Data.labeledFromLeadingAxis {α : Type} [Context α] [Runtime.FromFloat α] (tag : String) (classes : ℕ) {n : ℕ} {σ : Spec.Shape} (X : Spec.Tensor Float (Spec.Shape.dim n σ)) (y : Spec.Tensor Float (Spec.Shape.dim n Spec.Shape.scalar)) : Except String (Dataset (TensorPack α [σ, Spec.Shape.dim classes Spec.Shape.scalar]))

Labeled dataset from a batched tensor X : (n, σ) and a label vector y : (n,).

Labels are stored as floats (common when exporting from NumPy); we validate each label is an integer in [0, classes), then one-hot encode it.

def TorchLean.Data.readCsvSupervised {α : Type} [Context α] [Runtime.FromFloat α] (path : System.FilePath) (inDim outDim : ℕ) (opts : CsvOptions := { }) : IO (Except String (Dataset (TensorPack α [Spec.Shape.dim inDim Spec.Shape.scalar, Spec.Shape.dim outDim Spec.Shape.scalar])))

Load a supervised dataset from a CSV with inDim + outDim columns per row:

x1, ..., x_inDim, y1, ..., y_outDim.

File Sources

The definitions below describe tensors by path, format, and expected dimensions:

1. describe each tensor as a TensorSource;
2. load it as a typed TorchLean tensor;
3. build supervised/labeled datasets by slicing the leading batch axis, just like PyTorch TensorDataset.

Policy for external ecosystems:

• NumPy .npy is the canonical interchange format for numeric tensors.
• CSV is supported for small tabular data.
• MATLAB .mat, PyTorch checkpoints, HDF5, Parquet, and image archives should be converted by a small preparation script into .npy tensors plus metadata. The Lean runtime loader intentionally handles a small deterministic interchange format rather than every external binary format.

inductive TorchLean.Data.TensorFormat : Type

File formats supported directly by the Lean side unified data-source loader.

• npy : TensorFormat

  NumPy .npy, supporting the subset decoded by readNpyTensor.

• csv : TensorFormat

  Numeric CSV table. CSV sources are interpreted as 2D tensors [rows, cols].

@[implicit_reducible]

instance TorchLean.Data.instBEqTensorFormat : BEq TensorFormat

def TorchLean.Data.instBEqTensorFormat.beq : TensorFormat → TensorFormat → Bool

def TorchLean.Data.instReprTensorFormat.repr : TensorFormat → ℕ → Std.Format

@[implicit_reducible]

instance TorchLean.Data.instReprTensorFormat : Repr TensorFormat

def TorchLean.Data.TensorFormat.extension : TensorFormat → String

Human-facing extension used by messages and examples.

structure TorchLean.Data.TensorSource : Type

Description of one tensor stored on disk.

dims is the expected tensor shape. NPY can load any rank supported by ofList; CSV is treated as a numeric table and therefore expects dims = [rows, cols].

• path : System.FilePath

  Path to the file.

• dims : List ℕ

  Expected dimensions.

• format : TensorFormat

  Direct Lean side format. External formats should be preconverted to .npy.

• csvOptions : CsvOptions

  CSV parsing options, used only when format = .csv.

def TorchLean.Data.TensorSource.loadCsvTensorND (path : System.FilePath) (dims : List ℕ) (opts : CsvOptions := { }) : IO (Except String (Spec.Tensor Float (NN.Tensor.shapeOfDims dims)))

Load a numeric CSV table as a tensor.

Supported shapes:

• [rows, cols]: ordinary numeric table,
• [n]: either one column with n rows or one row with n columns.

def TorchLean.Data.TensorSource.loadFloatAs (format : TensorFormat) (path : System.FilePath) (dims : List ℕ) (opts : CsvOptions := { }) : IO (Except String (Spec.Tensor Float (NN.Tensor.shapeOfDims dims)))

Load a Float tensor from a path/format/dimension tuple.

def TorchLean.Data.TensorSource.loadFloatLeadingPrefixAs (format : TensorFormat) (path : System.FilePath) (dims : List ℕ) (opts : CsvOptions := { }) : IO (Except String (Spec.Tensor Float (NN.Tensor.shapeOfDims dims)))

Load a Float tensor, allowing NPY files to contain more rows than requested on the leading axis.

TensorSource.loadFloatAs is exact: the file shape must equal dims. This prefix variant is for dataset-style sources where dims starts with the number of rows requested by the current run. CSV sources remain exact because CSV has no binary prefix contract; NPY sources use readNpyTensorPrefix.

def TorchLean.Data.TensorSource.loadFloat (src : TensorSource) : IO (Except String (Spec.Tensor Float (NN.Tensor.shapeOfDims src.dims)))

Load a TensorSource as a Float tensor with the statically reflected shapeOfDims src.dims.

structure TorchLean.Data.SupervisedSource : Type

Two tensor sources representing supervised data:

• x must have shape (n, xDims...),
• y must have shape (n, yDims...).

• n : ℕ

  Number of samples along the leading batch axis.

• xDims : List ℕ

  Per-sample input dimensions.

• yDims : List ℕ

  Per-sample target dimensions.

• x : TensorSource

  Source for the batched input tensor.

• y : TensorSource

  Source for the batched target tensor.

def TorchLean.Data.SupervisedSource.ofPaths (format : TensorFormat) (xPath yPath : System.FilePath) (n : ℕ) (xDims yDims : List ℕ) (csvOptions : CsvOptions := { }) : SupervisedSource

Construct a supervised source from paths using the same file format for x and y.

def TorchLean.Data.SupervisedSource.load {α : Type} [Runtime.FromFloat α] (src : SupervisedSource) : IO (Except String (Dataset (TensorPack α [NN.Tensor.shapeOfDims src.xDims, NN.Tensor.shapeOfDims src.yDims])))

Load a supervised dataset by slicing the leading batch axis from the two tensors.

This is the preferred public loader for regression/operator-learning examples, regardless of whether the backing files are .npy or small numeric CSV tables.

def TorchLean.Data.supervisedNpySource (xPath yPath : System.FilePath) (n : ℕ) (xDims yDims : List ℕ) : SupervisedSource

Paired .npy source for supervised regression or operator-learning datasets.

def TorchLean.Data.loadSupervisedNpyFloatSamples (xPath yPath : System.FilePath) (n : ℕ) (xDims yDims : List ℕ) : IO (Except String (Array (Sample.Supervised Float (NN.Tensor.shapeOfDims xDims) (NN.Tensor.shapeOfDims yDims))))

Load paired .npy files as concrete Float supervised samples.

This is useful for reporting, custom evaluation loops, and native kernels that need concrete Float tensors outside the high-level trainer API.

structure TorchLean.Data.LabeledSource : Type

Two tensor sources representing labeled classification data:

• x must have shape (n, xDims...),
• y must have shape (n,) and contain integer-valued labels.

• n : ℕ

  Number of samples along the leading batch axis.

• xDims : List ℕ

  Per-sample input dimensions.

• classes : ℕ

  Number of classes for one-hot targets.

• x : TensorSource

  Source for the batched input tensor.

• y : TensorSource

  Source for the label vector.

def TorchLean.Data.LabeledSource.ofPaths (format : TensorFormat) (xPath yPath : System.FilePath) (n : ℕ) (xDims : List ℕ) (classes : ℕ) (csvOptions : CsvOptions := { }) : LabeledSource

Construct a labeled source from paths using the same file format for x and y.

def TorchLean.Data.LabeledSource.load {α : Type} [Context α] [Runtime.FromFloat α] (src : LabeledSource) : IO (Except String (Dataset (TensorPack α [NN.Tensor.shapeOfDims src.xDims, Spec.Shape.dim src.classes Spec.Shape.scalar])))

Load a labeled classification dataset by slicing the leading batch axis and one-hot encoding labels.

For CSV label vectors, store labels as a single-column table with dims = [n, 1] and use a custom TensorSource if needed; the path constructor above is aimed at .npy label vectors.

structure TorchLean.Data.TabularSupervisedSource : Type

Single-table supervised CSV source.

Use this when one CSV row contains both input and target columns: x1, ..., x_inDim, y1, ..., y_outDim.

• path : System.FilePath

  CSV file path.

• inDim : ℕ

  Number of input feature columns.

• outDim : ℕ

  Number of target columns.

• csvOptions : CsvOptions

  CSV parsing options.

def TorchLean.Data.TabularSupervisedSource.load {α : Type} [Context α] [Runtime.FromFloat α] (src : TabularSupervisedSource) : IO (Except String (Dataset (TensorPack α [Spec.Shape.dim src.inDim Spec.Shape.scalar, Spec.Shape.dim src.outDim Spec.Shape.scalar])))

Load a single-table supervised CSV source.