NN.API.Common

Small, practical helpers used across TorchLean workflows and entrypoints: typed tensor constructors, casting between scalar backends, and Except/IO glue.

Common Helpers For Workflows And Small Programs

We keep this module small and practical: it contains helper functions that show up repeatedly in executable workflows and tutorials.

What belongs here:

• casting Spec.Tensor Float into an arbitrary scalar backend α (given Float → α)
• building typed tensors from raw lists (tensorF, vecF, matF)
• bridging Except String into IO (orThrow)
• running small examples under a chosen scalar backend via --dtype (see NN.API.DType)

What does not belong here:

• core semantics/proofs (those live under NN / NN.Proofs)
• serious CLI parsing (these helpers are for small runnable binaries)

PyTorch Mapping Notes

If you're coming from PyTorch, this module plays the role of the small shared utility layer often written around:

• torch.tensor([...], dtype=..., device=...)
• choosing a dtype/backend based on CLI flags
• try/except wrappers for dataset loading and runnable workflow code

The main difference is that TorchLean tracks shapes in types, so tensor constructors here return Except String ... rather than silently reshaping.

def NN.API.Common.castTensor {α : Type} (cast : Float → α) {s : Spec.Shape} (t : Spec.Tensor Float s) : Spec.Tensor α s

Cast a tensor elementwise while preserving its type-level shape.

def NN.API.Common.orThrow {α : Type} (tag : String := "Example") : Except String α → IO α

Convert an Except String α into an IO α, raising a tagged userError on failure.

This is handy in main functions where we want the process to exit with a readable message.

def NN.API.Common.check (tag msg : String) (b : Bool) : IO Unit

Fail with a tagged userError if a boolean condition is false.

This is a small convenience for examples that want short, readable checks: Common.check exeName "loss finite" (loss == loss).

def NN.API.Common.writeBeforeAfterLossLog (path : System.FilePath) (title : String) (steps : ℕ) (loss0 loss1 : Float) (notes : Array String := #[]) : IO Unit

Write a standard JSON training artifact for routines that record an initial and final loss.

This is a convenience wrapper around Runtime.Training.TrainLog.beforeAfterLoss and the stable TrainLog JSON format. It is intentionally independent of any particular model, dataset, or runtime backend.

def NN.API.Common.writeBeforeAfterLossLogTo (dest : Runtime.Training.LogDestination) (title : String) (steps : ℕ) (loss0 loss1 : Float) (notes : Array String := #[]) : IO Unit

Write a before/after loss log to an explicit logging destination.

LogDestination.disabled is a no-op, mirroring wandb disabled for quick smoke tests.

def NN.API.Common.writeCurveLog (path : System.FilePath) (title : String) (curve : Runtime.Training.Curve) (seriesName : String := "loss") (notes : Array String := #[]) : IO Unit

Write a one-series scalar curve as a standard TrainLog JSON artifact.

def NN.API.Common.writeCurveLogTo (dest : Runtime.Training.LogDestination) (title : String) (curve : Runtime.Training.Curve) (seriesName : String := "loss") (notes : Array String := #[]) : IO Unit

Write a one-series scalar curve to an explicit logging destination.

structure NN.API.Common.LoggedTrainFlags : Type

Common CLI result for training commands that accept --steps/--epochs and --log.

• steps : ℕ

  Number of optimizer updates.

• log : Runtime.Training.LogDestination

  Logging destination. Use --log false / off / none to disable.

• logPath : System.FilePath

  Path where the JSON TrainLog should be written.

def NN.API.Common.instReprLoggedTrainFlags.repr : LoggedTrainFlags → ℕ → Std.Format

@[implicit_reducible]

instance NN.API.Common.instReprLoggedTrainFlags : Repr LoggedTrainFlags

def NN.API.Common.parseLoggedTrainFlags (exeName : String) (args : List String) (defaultLogPath : System.FilePath) (defaultSteps : ℕ := 1) (allowZeroSteps : Bool := false) : Except String (LoggedTrainFlags × List String)

Parse common training flags: positive --steps/--epochs plus optional --log.

--log <path> writes the standard local JSON artifact. --log false, --log off, or --log none disables artifact writing while preserving the parsed step count.

structure NN.API.Common.ModelTrainFlags : Type

Training flags shared by the runnable model examples.

Most model commands should not each define their own parser for the same knobs. They can parse model-specific data flags first, then call parseModelTrainFlags for the common optimizer loop:

• --steps / --epochs: how many optimizer passes the example should run;
• --log: where to write a TrainLog JSON artifact;
• --lr: Adam learning rate.

Special examples can still extend this record with extra fields, but the default path stays one shared parser rather than one local TrainOptions clone per model.

• train : LoggedTrainFlags

  Shared step/epoch count and logging destination.

• lr : Float

  Learning rate for the default Adam optimizer used by examples.

def NN.API.Common.instReprModelTrainFlags.repr : ModelTrainFlags → ℕ → Std.Format

@[implicit_reducible]

instance NN.API.Common.instReprModelTrainFlags : Repr ModelTrainFlags

def NN.API.Common.parseModelTrainFlags (exeName : String) (args : List String) (defaultLogPath : System.FilePath) (defaultSteps : ℕ := 1) (defaultLr : Float := 1e-3) (allowZeroSteps : Bool := false) : Except String (ModelTrainFlags × List String)

Parse the standard model-training flags: --steps/--epochs, --log, and --lr.

def NN.API.Common.adamOptimizer {α : Type} [Semantics.Scalar α] [Runtime.Scalar α] (cast : Float → α) (ps : List Shape) (lr : Float) : Runtime.Autograd.TorchLean.Optimizer α ps

Default Adam optimizer constructor used by supervised and vision examples.

The reusable part is the optimizer convention, not the model. Individual examples still own their architecture and loss, while this helper keeps the Adam hyperparameter spelling identical across MLP, CNN, ResNet, ViT, and similar small demos.

def NN.API.Common.runAnyOrFloat (exeName : String) (args : List String) (preferFloat : List String → Bool) (banner : Runtime.Autograd.Torch.Options → String) (anyK : {α : Type} → [Semantics.Scalar α] → [DecidableEq Spec.Shape] → [ToString α] → [Runtime.Scalar α] → (Float → α) → Runtime.Autograd.Torch.Options → List String → IO Unit) (floatK : Runtime.Autograd.Torch.Options → List String → IO Unit) (printOk : Bool := true) : IO UInt32

Run an executable with the standard TorchLean runtime parser, using the polymorphic scalar path by default and switching to the Float path when requested.

This is the common shape for public examples that support all executable scalar backends, but need the Float path for CUDA bridges, decoded probes, or JSON artifacts whose metrics are stored as Float.

def NN.API.Common.listGen {α : Type} (n : ℕ) (f : ℕ → α) : List α

List generator: [0, 1, ..., n-1] mapped through f.

def NN.API.Common.tensorF {α : Type} [Context α] (cast : Float → α) (dims : List ℕ) (xs : List Float) : Except String (Spec.Tensor α (Tensor.shapeOfDims dims))

Build an N-D tensor from a raw list of floats and cast it into the chosen scalar backend.

Fails if xs.length ≠ numel(dims).

def NN.API.Common.tensorFGen {α : Type} [Context α] (cast : Float → α) (dims : List ℕ) (f : ℕ → Float) : Except String (Spec.Tensor α (Tensor.shapeOfDims dims))

Generate an N-D tensor by calling f for each element index, then cast into the chosen backend.

The function f is indexed by the flat element index 0..numel-1.

def NN.API.Common.tensorFGen! {α : Type} [Context α] (cast : Float → α) (dims : List ℕ) (f : ℕ → Float) : Spec.Tensor α (Tensor.shapeOfDims dims)

Generate an N-D tensor by calling f for each flat element index, with no failure case.

This is the “total” sibling of tensorFGen: since we generate exactly numel(dims) values, the reshape cannot fail, so we avoid an Except. When you want to build a deterministic constant tensor for an example, this is usually the right tool.

def NN.API.Common.tensorFGenShape! {α : Type} [Context α] (cast : Float → α) (s : Spec.Shape) (f : ℕ → Float) : Spec.Tensor α s

Generate a tensor of a known shape s by calling f for each flat element index, then cast into the chosen backend.

This is a convenience wrapper used in examples to avoid the common boilerplate:

let xDyn : Tensor α (shapeOfDims s.toList) := ...
let x : Tensor α s := by simpa using xDyn

def NN.API.Common.vecF {α : Type} [Context α] (cast : Float → α) (n : ℕ) (xs : List Float) : Except String (Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar))

1D vector tensor constructor specialized to shape Vec n.

Fails if xs.length ≠ n.

def NN.API.Common.vecFGen {α : Type} [Context α] (cast : Float → α) (n : ℕ) (f : ℕ → Float) : Except String (Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar))

Generator variant of vecF.

def NN.API.Common.matF {α : Type} [Context α] (cast : Float → α) (rows cols : ℕ) (xs : List Float) : Except String (Spec.Tensor α (Spec.Shape.dim rows (Spec.Shape.dim cols Spec.Shape.scalar)))

2D matrix tensor constructor specialized to shape Mat rows cols.

Fails if xs.length ≠ rows * cols.

def NN.API.Common.matFGen {α : Type} [Context α] (cast : Float → α) (rows cols : ℕ) (f : ℕ → Float) : Except String (Spec.Tensor α (Spec.Shape.dim rows (Spec.Shape.dim cols Spec.Shape.scalar)))

Generator variant of matF.

def NN.API.Common.runWithDType (title : String) (args : List String) (k : {α : Type} → [Semantics.Scalar α] → [DecidableEq Spec.Shape] → [ToString α] → (Float → α) → IO Unit) : IO Unit

Run a workflow once under a dtype selected from args (via --dtype / --float32-mode).

This logs the chosen dtype and then calls k with a cast function Float → α for the selected scalar backend.

In particular:

• --dtype=float selects Lean's builtin Float (trusted semantics, executable),
• --dtype=float32 selects TorchLean's verified IEEE32 executable semantics,
• --dtype=complex selects TorchLean's parametric complex scalar over Float32,
• --dtype=real selects ℝ (proof-only; errors at runtime).

def NN.API.Common.runWithRuntimeDType (title : String) (args : List String) (k : {α : Type} → [Semantics.Scalar α] → [DecidableEq Spec.Shape] → [ToString α] → [Runtime.Scalar α] → IO Unit) : IO Unit

Like runWithDType, but also provides an API.Runtime.Scalar α instance.

Use this when your workflow uses numeric literals (1.0, -3.5, etc.) at runtime.

@[reducible, inline]

abbrev NN.API.Common.mainWithRuntimeDType (title : String) (args : List String) (k : {α : Type} → [Semantics.Scalar α] → [DecidableEq Spec.Shape] → [ToString α] → [Runtime.Scalar α] → IO Unit) : IO Unit

Convenience wrapper for runnable binaries that need runtime float-literal injection.