Datasets

Dataset constructors and file-backed loaders used by TorchLean.Trainer.

def TorchLean.Data.tensorDataset {n : ℕ} {σ τ : Shape} (X : Tensor.T Float (Spec.Shape.dim n σ)) (Y : Tensor.T Float (Spec.Shape.dim n τ)) : Trainer.Dataset σ τ

Runtime-polymorphic supervised dataset for Float tensors.

Use this for most tutorials and file-loader paths: Float data is cast into whichever runtime scalar the command selected with --dtype.

def TorchLean.Data.samples {σ τ : Shape} (mk : {α : Type} → [Context α] → [Runtime.FromFloat α] → List (SupervisedSample α σ τ)) : Trainer.Dataset σ τ

Runtime-polymorphic supervised dataset from an explicit sample builder.

Use this when Lean code generates samples directly rather than loading them from batched tensors, CSV, or NPY files. Sequence windows, synthetic PDE batches, and task-specific examples can keep their own sample logic while still returning a standard Trainer.Dataset.

def TorchLean.Data.singleton {σ τ : Shape} (mk : {α : Type} → [Context α] → [Runtime.FromFloat α] → SupervisedSample α σ τ) : Trainer.Dataset σ τ

Build a singleton dataset from one runtime-polymorphic supervised sample.

Small examples can use the Trainer.Dataset API without fixing the runtime scalar or backend in the dataset definition itself.

def TorchLean.Data.singletonFrom {ρ : Type} {σ τ : Shape} (arg : ρ) (mk : {α : Type} → [Context α] → [Runtime.FromFloat α] → ρ → SupervisedSample α σ τ) : Trainer.Dataset σ τ

Build a singleton dataset by feeding one explicit argument into a runtime-polymorphic sample constructor.

Use this when the sample construction depends on one user-facing payload, such as a prompt string or one file-backed record.

def TorchLean.Data.ioSingletonFloat {σ τ : Shape} (mk : IO (SupervisedSample Float σ τ)) : Trainer.Dataset σ τ

Build a singleton dataset from one Float sample produced inside IO.

Use this when the sample comes from a file-backed or runtime-loaded Float boundary. The public trainer still owns the scalar/backend choice through Trainer.RunConfig and Trainer.TrainOptions.

def TorchLean.Data.floatSamples {σ τ : Shape} (samples : List (SupervisedSample Float σ τ)) : Trainer.Dataset σ τ

Runtime-polymorphic dataset from an in-memory list of Float supervised samples.

Several examples build their training windows in ordinary Float first because the source is text, CSV, NPY, or another external boundary. This constructor keeps those examples on the public trainer API: the samples are still cast to the runtime-selected scalar at training time, so callers do not have to write their own scalar-polymorphic dataset adapter.

def TorchLean.Data.floatSampleArray {σ τ : Shape} (samples : Array (SupervisedSample Float σ τ)) : Trainer.Dataset σ τ

Array form of floatSamples.

def TorchLean.Data.batchDataset {σ τ : Shape} (batch : ℕ) (data : Trainer.Dataset σ τ) (shuffle : Bool := true) (seed : ℕ := 0) (dropLast : Bool := true) : Trainer.Dataset (Spec.Shape.dim batch σ) (Spec.Shape.dim batch τ)

Convert an unbatched supervised dataset into a fixed-size batched dataset.

Public adapter for examples that want to minibatch the dataset before training and let the model own the batch axis. The returned dataset stores samples of shape dim batch σ and dim batch τ, so it can be passed directly to Trainer.new with a batched model.

def TorchLean.Data.randomSplitDataset {σ τ : Shape} (trainSize : ℕ) (data : Trainer.Dataset σ τ) (seed : ℕ := 0) : Trainer.Dataset σ τ × Trainer.Dataset σ τ

Split a public dataset into deterministic train/test views.

Dataset-level analogue of torch.utils.data.random_split: the split happens after the trainer materializes the runtime scalar, but callers stay on ordinary Trainer.Dataset values.

def TorchLean.Data.tabularCsvDataset (path : System.FilePath) (batch inDim outDim : ℕ) (csvOptions : CsvOptions := { }) (shuffle : Bool := true) (seed : ℕ := 0) (dropLast : Bool := true) : Trainer.Dataset (Spec.Shape.dim batch (Spec.Shape.dim inDim Shape.scalar)) (Spec.Shape.dim batch (Spec.Shape.dim outDim Shape.scalar))

Load a numeric CSV table as a dataset of fixed-size tabular regression batches.

Each CSV row is interpreted as inDim feature columns followed by outDim target columns. The returned dataset already has the leading batch dimension expected by a model with input shape .dim batch (.dim inDim .scalar) and output shape .dim batch (.dim outDim .scalar).

def TorchLean.Data.supervisedDataset (src : SupervisedSource) : Trainer.Dataset (Shape.ofDims src.xDims) (Shape.ofDims src.yDims)

Runtime-polymorphic supervised regression dataset from a tensor source.

Public file-data analogue of torch.utils.data.TensorDataset(X, Y) for examples whose targets are tensors rather than class labels. The source records where batched features and targets live; the trainer materializes them at the selected scalar type.

def TorchLean.Data.supervisedNpyDataset (xPath yPath : System.FilePath) (n : ℕ) (xDims yDims : List ℕ) : Trainer.Dataset (Shape.ofDims xDims) (Shape.ofDims yDims)

Runtime-polymorphic supervised dataset backed by paired .npy files.

Common file-backed regression/operator-learning path: xPath stores samples with shape xDims, and yPath stores matching targets with shape yDims.

def TorchLean.Data.labeledDataset (src : LabeledSource) : Trainer.Dataset (Shape.ofDims src.xDims) (Spec.Shape.dim src.classes Shape.scalar)

Runtime-polymorphic one-hot classification dataset from a tensor source.

Public file-data analogue of torch.utils.data.TensorDataset: the source records where features and integer labels live, and the trainer materializes them at the selected scalar type.