File-Backed Dataset Sources

Typed NPY and CSV sources for supervised and labeled datasets. This module owns the boundary between external files and TorchLean tensors; importing Data.SampleStream does not pull in these parsers.

def TorchLean.Data.requireFiles (exeName : String) (paths : Array System.FilePath) (hint : String := "") : IO Unit

Require that every path exists, adding hint to a missing-file error when supplied.

def TorchLean.Data.requireFile (exeName label : String) (path : System.FilePath) (hint : String := "") : IO Unit

Require one named data file to exist.

Example:

-- A missing fixture should fail with a sentence the reader can act on.
def checkFixtures : IO Unit :=
  Data.requireFile "cifar10_images" "input tensor" "data/cifar_x.npy"
    (hint := "run: python3 NN/Examples/Data/generate_small_data.py")

def TorchLean.Data.requirePairedFiles (exeName inputLabel : String) (inputPath : System.FilePath) (targetLabel : String) (targetPath : System.FilePath) (hint : String := "") : IO Unit

Require paired supervised input and target files to exist.

def TorchLean.Data.availableNpyRows (path : System.FilePath) (tailShape : Shape) (expectedDesc : String) : IO ℕ

Read an .npy row count from its header while checking all trailing dimensions.

For shape (N, d₁, ..., dₖ), this returns N exactly when the trailing shape is tailShape. The payload is not read; the subsequent full or prefix load checks its required byte range.

def TorchLean.Data.Internal.tensorFromFlat (tag : String) (dims : Shape) (values : Array Float) : Except String (Tensor Float dims)

Validate untrusted flat payload length before crossing into total tensor code.

Tensor.from itself is intentionally total; only external metadata can fail.

inductive TorchLean.Data.Internal.TensorShapeMatch : Type

How a file's physical shape is matched against the requested tensor shape.

• exact : TensorShapeMatch

  Require every physical dimension to equal the requested dimension.

• leadingPrefix : TensorShapeMatch

  Permit a larger first dimension and read its requested prefix.

def TorchLean.Data.Internal.instBEqTensorShapeMatch.beq : TensorShapeMatch → TensorShapeMatch → Bool

@[instance_reducible]

instance TorchLean.Data.Internal.instBEqTensorShapeMatch : BEq TensorShapeMatch

def TorchLean.Data.Internal.instReprTensorShapeMatch.repr : TensorShapeMatch → ℕ → Std.Format

@[instance_reducible]

instance TorchLean.Data.Internal.instReprTensorShapeMatch : Repr TensorShapeMatch

def TorchLean.Data.Internal.readNpyTensor (path : System.FilePath) (dims : Shape) (shapeMatch : TensorShapeMatch := TensorShapeMatch.exact) : IO (Except String (Tensor Float dims))

Load an arbitrary-rank tensor from a .npy file under an explicit shape-matching policy.

With exact, every dimension must match. With leadingPrefix, rank and trailing dimensions must still match, while the file may contain more entries on its first axis. Prefix loading requires a C-order NPY file because the requested values must form one contiguous prefix.

File Sources

The definitions below load tensors by path and expected dimensions, then build supervised or 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.Internal.FileFormat : Type

File encodings inferred from source-path extensions.

• npy : FileFormat

  NumPy .npy, supporting numeric C-order arrays decoded by TorchLean's NPY reader.

• csv : FileFormat

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

@[instance_reducible]

instance TorchLean.Data.Internal.instBEqFileFormat : BEq FileFormat

def TorchLean.Data.Internal.instBEqFileFormat.beq : FileFormat → FileFormat → Bool

@[instance_reducible]

instance TorchLean.Data.Internal.instReprFileFormat : Repr FileFormat

def TorchLean.Data.Internal.instReprFileFormat.repr : FileFormat → ℕ → Std.Format

def TorchLean.Data.Internal.fileFormat (path : System.FilePath) : Except String FileFormat

Infer the supported file encoding from a source path.

def TorchLean.Data.Internal.loadCsvTensor (path : System.FilePath) (dims : Shape) (options : CsvOptions := { }) : IO (Except String (Tensor Float 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.Internal.loadFloatTensor (path : System.FilePath) (dims : Shape) (options : CsvOptions := { }) (shapeMatch : TensorShapeMatch := TensorShapeMatch.exact) : IO (Except String (Tensor Float dims))

Load a Float tensor from a path and expected dimensions.

opaque TorchLean.Tensor.load {α : Type} [Storage α] [Runtime.FromFloat α] {shape : Shape} (path : System.FilePath) (csvOptions : Data.CsvOptions := { }) : IO (Tensor α shape)

Load a tensor from NPY or numeric CSV.

The expected result type supplies both the scalar type and shape. File metadata is checked before the tensor is returned.

structure TorchLean.Data.SupervisedSource : Type

Two files representing supervised data:

• inputPath must contain shape (sampleCount, input...),
• targetPath must contain shape (sampleCount, target...).

• sampleCount : ℕ

  Number of samples along the leading batch axis.

• input : Shape

  Shape of one input sample.

• target : Shape

  Shape of one target sample.

• inputPath : System.FilePath

  Path to the batched input tensor.

• targetPath : System.FilePath

  Path to the batched target tensor.

• csvOptions : CsvOptions

  CSV parsing options, ignored for NPY sources.

def TorchLean.Data.SupervisedSource.fromFiles (inputPath targetPath : System.FilePath) (sampleCount : ℕ) (input target : Shape) (csvOptions : CsvOptions := { }) : SupervisedSource

Describe paired input and target tensor files. Encodings are inferred from their extensions.

Example:

-- Shapes are per sample; `sampleCount` says how many leading rows of the files this run uses.
def source : Data.SupervisedSource :=
  Data.SupervisedSource.fromFiles
    (inputPath := "data/inputs.npy") (targetPath := "data/targets.npy")
    (sampleCount := 64) (input := [16]) (target := [1])

opaque TorchLean.Data.SupervisedSource.load {α : Type} [Storage α] [Runtime.FromFloat α] (source : SupervisedSource) : IO (SampleStream (Sample.Supervised α source.input source.target))

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.

structure TorchLean.Data.LabeledSource : Type

Two files representing labeled classification data:

• inputPath must contain shape (sampleCount, input...),
• labelPath must contain shape (sampleCount,) and integer-valued class labels.

• sampleCount : ℕ

  Number of samples along the leading batch axis.

• input : Shape

  Shape of one input sample.

• classCount : ℕ

  Number of classes for one-hot targets.

• inputPath : System.FilePath

  Path to the batched input tensor.

• labelPath : System.FilePath

  Path to the label vector.

• csvOptions : CsvOptions

  CSV parsing options, ignored for NPY sources.

def TorchLean.Data.LabeledSource.fromFiles (inputPath labelPath : System.FilePath) (sampleCount : ℕ) (input : Shape) (classCount : ℕ) (csvOptions : CsvOptions := { }) : LabeledSource

Describe input and class-label tensor files. Encodings are inferred from their extensions.

opaque TorchLean.Data.LabeledSource.load {α : Type} [Storage α] [Context α] [Runtime.FromFloat α] (source : LabeledSource) : IO (SampleStream (Sample.Supervised α source.input [source.classCount]))

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

CSV label vectors may be stored as one column or one row; NPY label vectors have shape [n].

structure TorchLean.Data.TabularSupervisedSource : Type

Single-table supervised CSV source.

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

• path : System.FilePath

  CSV file path.

• inputWidth : ℕ

  Number of input feature columns.

• targetWidth : ℕ

  Number of target columns.

• csvOptions : CsvOptions

  CSV parsing options.

def TorchLean.Data.TabularSupervisedSource.fromCsv (path : System.FilePath) (inputWidth targetWidth : ℕ) (csvOptions : CsvOptions := { }) : TabularSupervisedSource

Describe one CSV table whose rows contain input columns followed by target columns.

opaque TorchLean.Data.TabularSupervisedSource.load {α : Type} [Storage α] [Context α] [Runtime.FromFloat α] (source : TabularSupervisedSource) : IO (SampleStream (Sample.Supervised α [source.inputWidth] [source.targetWidth]))

Load a single-table supervised CSV source.