Shared Real-Data Helpers for Model Examples

NN/Examples/Models/* should exercise real data paths. This file centralizes the shared parts:

• loading a prepared CIFAR-10 NPY minibatch,
• reading a local text corpus, and
• printing the same "how to prepare data" hint everywhere.

The data files are prepared by scripts/datasets/download_example_data.py; examples report missing inputs explicitly instead of silently falling back to synthetic tensors.

def NN.Examples.Models.RealData.cifarChannels : ℕ

def NN.Examples.Models.RealData.cifarHeight : ℕ

def NN.Examples.Models.RealData.cifarWidth : ℕ

def NN.Examples.Models.RealData.cifarClasses : ℕ

def NN.Examples.Models.RealData.defaultCifarRows : ℕ

def NN.Examples.Models.RealData.imagenet64Channels : ℕ

def NN.Examples.Models.RealData.imagenet64Height : ℕ

def NN.Examples.Models.RealData.imagenet64Width : ℕ

def NN.Examples.Models.RealData.imagenet64Classes : ℕ

def NN.Examples.Models.RealData.defaultImageNet64Rows : ℕ

instance NN.Examples.Models.RealData.instNeZeroNatCifarChannels : NeZero cifarChannels

instance NN.Examples.Models.RealData.instNeZeroNatCifarHeight : NeZero cifarHeight

instance NN.Examples.Models.RealData.instNeZeroNatCifarWidth : NeZero cifarWidth

instance NN.Examples.Models.RealData.instNeZeroNatCifarClasses : NeZero cifarClasses

instance NN.Examples.Models.RealData.instNeZeroNatImagenet64Channels : NeZero imagenet64Channels

instance NN.Examples.Models.RealData.instNeZeroNatImagenet64Height : NeZero imagenet64Height

instance NN.Examples.Models.RealData.instNeZeroNatImagenet64Width : NeZero imagenet64Width

instance NN.Examples.Models.RealData.instNeZeroNatImagenet64Classes : NeZero imagenet64Classes

@[reducible, inline]

abbrev NN.Examples.Models.RealData.CifarImage : Shape

@[reducible, inline]

abbrev NN.Examples.Models.RealData.CifarTarget : Shape

@[reducible, inline]

abbrev NN.Examples.Models.RealData.ImageNet64Image : Shape

ImageNet-style converted image shape used by the higher-resolution diffusion example.

@[reducible, inline]

abbrev NN.Examples.Models.RealData.ImageNet64Target : Shape

One-hot target shape for ImageNet-style folders.

The diffusion example ignores labels, but reusing Data.LabeledSource keeps the data path identical to the supervised examples and lets class-directory conversion catch malformed labels early.

def NN.Examples.Models.RealData.missingCifarHint : String

def NN.Examples.Models.RealData.missingImageNet64Hint : String

def NN.Examples.Models.RealData.missingTextHint : String

def NN.Examples.Models.RealData.parseCifarFlags (args : List String) : Except String (System.FilePath × System.FilePath × ℕ × ℕ × List String)

def NN.Examples.Models.RealData.parseImageNet64Flags (args : List String) : Except String (System.FilePath × System.FilePath × ℕ × ℕ × List String)

Parse the shared flags for an ImageNet-style 64x64 NPY dataset.

The expected input is produced by scripts/datasets/torchlean_data_convert.py image-folder; that converter handles JPEG/PNG decoding, RGB conversion, resizing, class-directory labels, and the final NCHW layout. Lean then reads only the simple .npy tensors.

def NN.Examples.Models.RealData.loadCifarLoader {α : Type} [API.Semantics.Scalar α] [API.Runtime.Scalar α] (exeName : String) (batch nRows seed : ℕ) (xPath yPath : System.FilePath) : IO (API.Data.BatchLoader α batch CifarImage CifarTarget)

def NN.Examples.Models.RealData.loadCifarBatch {α : Type} [API.Semantics.Scalar α] [API.Runtime.Scalar α] (exeName : String) (batch nRows seed : ℕ) (xPath yPath : System.FilePath) : IO (API.sample.Batch α batch CifarImage CifarTarget)

def NN.Examples.Models.RealData.loadImageNet64Loader {α : Type} [API.Semantics.Scalar α] [API.Runtime.Scalar α] (exeName : String) (batch nRows seed : ℕ) (xPath yPath : System.FilePath) : IO (API.Data.BatchLoader α batch ImageNet64Image ImageNet64Target)

Load a user-prepared ImageNet-style 64x64 minibatch.

This is intentionally a .npy reader, not a JPEG reader. The Python converter is the trust boundary for filesystem image decoding and resizing; this Lean path checks the resulting tensor shape and class range before handing the batch to examples.

def NN.Examples.Models.RealData.loadImageNet64Batch {α : Type} [API.Semantics.Scalar α] [API.Runtime.Scalar α] (exeName : String) (batch nRows seed : ℕ) (xPath yPath : System.FilePath) : IO (API.sample.Batch α batch ImageNet64Image ImageNet64Target)

def NN.Examples.Models.RealData.loadCifarVectorBatch (cfg : API.nn.models.VectorGenerativeConfig) (hData : cfg.dataDim ≤ Shape.size CifarImage) (exeName : String) (xPath yPath : System.FilePath) (nRows seed : ℕ) : IO (Spec.Tensor Float (API.nn.models.vectorDataShape cfg))

Load a CIFAR minibatch and expose it as a compact flattened vector batch.

The file paths and download hints remain in NN.Examples, but the flattening logic itself lives in NN.API.Models.Generative so users can reuse it with their own image tensors.

def NN.Examples.Models.RealData.parseTextFlags (args : List String) : Except String (System.FilePath × List String)

def NN.Examples.Models.RealData.readTextCorpus (exeName : String) (path : System.FilePath) : IO String

def NN.Examples.Models.RealData.textCausalSample {α : Type} [API.Semantics.Scalar α] [API.Runtime.Scalar α] (seqLen vocab : ℕ) (input : String) : API.sample.Supervised α (Shape.Mat seqLen vocab) (Shape.Mat seqLen vocab)