Finite Sample Streams

This module provides the lower-level data source used by the trainer API. A SampleStream α records a finite number of samples and computes a sample only when its index is requested. Array- backed data is wrapped without copying, while generated data and tensor slices remain lazy.

Application code normally constructs TorchLean.Trainer.Dataset; this module is useful for manual training loops and data-source implementations that already know their runtime scalar type.

structure TorchLean.Data.SampleStream (α : Type) : Type

A finite, lazily indexed source of samples.

• size : Nat

  Number of samples available from the stream.

• get : Fin self.size → α

  Compute the sample at an in-bounds index.

structure TorchLean.Data.SampleStream.SplitResult (α : Type) : Type

Named halves of a stream split.

• selected : SampleStream α

  Samples before the split point.

• remaining : SampleStream α

  Samples at and after the split point.

structure TorchLean.Data.SampleStream.ShuffleResult (α : Type) : Type

State and stream produced by deterministic shuffling.

• nextSeed : Nat

  Seed to use for the next deterministic shuffle.

• stream : SampleStream α

  Stream in shuffled index order.

structure TorchLean.Data.SampleStream.RandomSplitResult (α : Type) : Type

State and named partitions produced by a shuffled split.

• nextSeed : Nat

  Seed to use for the next deterministic shuffle.

• selected : SampleStream α

  Samples selected before the split point.

• remaining : SampleStream α

  Samples selected at and after the split point.

def TorchLean.Data.SampleStream.fromFunction {α : Type} (size : Nat) (get : Fin size → α) : SampleStream α

Construct a finite stream from an index function.

def TorchLean.Data.SampleStream.fromArray {α : Type} (xs : Array α) : SampleStream α

Wrap an array as a finite stream without copying it.

def TorchLean.Data.SampleStream.toArray {α : Type} (stream : SampleStream α) : Array α

Materialize the samples in index order.

@[simp]

theorem TorchLean.Data.SampleStream.size_fromArray {α : Type} (xs : Array α) : (fromArray xs).size = xs.size

A stream built from an array reports that array's length.

def TorchLean.Data.SampleStream.isEmpty {α : Type} (stream : SampleStream α) : Bool

Return true exactly when the stream contains no samples.

def TorchLean.Data.SampleStream.get? {α : Type} (stream : SampleStream α) (i : Nat) : Option α

Safely request a sample by a natural-number index.

def TorchLean.Data.SampleStream.map {α β : Type} (f : α → β) (stream : SampleStream α) : SampleStream β

Transform samples when they are requested.

def TorchLean.Data.SampleStream.append {α : Type} (xs ys : SampleStream α) : SampleStream α

Append two finite streams in index order.

def TorchLean.Data.SampleStream.splitAt {α : Type} (n : Nat) (stream : SampleStream α) : SplitResult α

Split a stream into its first n samples and the remaining suffix.

def TorchLean.Data.SampleStream.shuffle {α : Type} (seed : Nat) (stream : SampleStream α) : ShuffleResult α

Shuffle the indices deterministically, returning the next seed and a stream with the new order.

Only the index permutation is stored; requesting a shuffled sample still evaluates the original stream at that index.

def TorchLean.Data.SampleStream.shuffled {α : Type} (seed : Nat) (stream : SampleStream α) : SampleStream α

Deterministically shuffle a stream and discard the next pseudo-random seed.

def TorchLean.Data.SampleStream.randomSplitAt {α : Type} (seed n : Nat) (stream : SampleStream α) : RandomSplitResult α

Shuffle a stream once and split the result at n.

def TorchLean.Data.SampleStream.batches {α : Type} (name : String) (batchSize : Nat) (stream : SampleStream α) : Except String (Array (Array α))

Split a nonempty stream into consecutive nonempty batches of size at most batchSize.

def TorchLean.Data.SampleStream.cycle {α : Type} (stream : SampleStream α) (h : 0 < stream.size) (i : Nat) : α

Cycle through a nonempty stream indefinitely.

def TorchLean.Data.SampleStream.cycleOrError {α : Type} (stream : SampleStream α) (error : String := "empty sample stream") : Except String (Nat → α)

Build a cycling sample function, rejecting an empty stream once at construction time.

structure TorchLean.Data.EpochLoader (α : Type) : Type

Configuration and deterministic shuffle state for epoch traversal.

• samples : SampleStream α

  Samples traversed by each epoch.

• batchSize : Nat

  Maximum number of samples in each batch.

• shuffle : Bool

  Whether to shuffle before each epoch.

• seed : Nat

  Seed threaded through deterministic shuffles.

• dropLast : Bool

  Whether to discard a final batch shorter than batchSize.

structure TorchLean.Data.Epoch (Loader Batch : Type) : Type

Batches produced for one epoch together with the loader state for the next epoch.

• nextLoader : Loader

  Loader state to use for the next epoch.

• batches : Array Batch

  Batches produced by this epoch.

def TorchLean.Data.EpochLoader.fromStream {α : Type} (samples : SampleStream α) (batchSize : Nat) (shuffle : Bool := false) (seed : Nat := 0) (dropLast : Bool := false) : EpochLoader α

Construct an epoch loader for a finite stream.

def TorchLean.Data.EpochLoader.nextEpoch {α : Type} (name : String) (loader : EpochLoader α) : Except String (Epoch (EpochLoader α) (Array α))

Produce one epoch of batches and the loader state for the next epoch. Each shuffle applies the next seed to the original source. Keeping that source avoids retaining an additional permutation closure for every completed epoch.

def TorchLean.Data.EpochLoader.mapNextEpoch {α β : Type} (name : String) (loader : EpochLoader α) (collate : Array α → Except String β) : Except String (Epoch (EpochLoader α) β)

Produce one epoch and map each raw batch through collate.