TorchLean Tensor Facade

Ops, random, shape, tensor, and semantic names exposed by the NN umbrella.

Executable program operations for verification and compiler-facing examples.

Most model code should use nn.* and Trainer.*. Use Ops.* when writing an explicit TorchLean executable program directly, for example before compiling a hand-built fragment to NN.IR.Graph.

@[reducible, inline]

abbrev TorchLean.Shape.scalar : Spec.Shape

@[reducible, inline]

abbrev TorchLean.Shape.size : Spec.Shape → ℕ

Total number of scalar elements (a.k.a. “numel”).

@[reducible, inline]

abbrev TorchLean.Shape.batch : ℕ → Spec.Shape → Spec.Shape

@[reducible, inline]

abbrev TorchLean.Shape.vec (n : ℕ) : Spec.Shape

Vector shape n.

@[reducible, inline]

abbrev TorchLean.Shape.mat (rows cols : ℕ) : Spec.Shape

Matrix shape rows × cols.

@[reducible, inline]

abbrev TorchLean.Shape.image (c h w : ℕ) : Spec.Shape

Image shape C × H × W (channel-first).

@[reducible, inline]

abbrev TorchLean.Shape.images (n c h w : ℕ) : Spec.Shape

Batched image shape N × C × H × W (PyTorch default for images).

@[reducible, inline]

abbrev TorchLean.Shape.nchw (n c h w : ℕ) : Spec.Shape

Batched image shape N × C × H × W (PyTorch default for images).

@[reducible, inline]

abbrev TorchLean.Shape.imageSize (channels height width : ℕ) : ℕ

Number of scalar features in a CHW image shape.

@[reducible, inline]

abbrev TorchLean.Shape.ofDims : List ℕ → NN.Tensor.Shape

Convert a runtime list of dimensions like [2, 3, 4] into a nested Shape.

Why this exists:

• In the spec layer we usually carry the shape in the type (great for safety).
• In “API land” we often start from lists (CLI args, JSON, compact examples, …).

shapeOfDims is the bridge between those representations.

@[reducible, inline]

abbrev TorchLean.Shape.toList : Spec.Shape → List ℕ

Convert to a list of dimensions (outermost first).

@[reducible, inline]

abbrev TorchLean.Tensor.T (α : Type) : Spec.Shape → Type

Shape-indexed tensor datatype for the spec layer.

This is a functional representation:

• a scalar tensor is just an α,
• an n-dimensional tensor is a function Fin n → Tensor α s.

The spec layer does not commit to a concrete memory layout.

@[reducible, inline]

abbrev TorchLean.Tensor.vector (α : Type := Float) (xs : List α) : T α (Spec.Shape.dim xs.length Spec.Shape.scalar)

Create a 1-D tensor from a Lean List.

Notes:

• The shape is computed from xs.length, so the type remembers the length.
• This is total and does not perform any runtime checks.

PyTorch analogy: torch.tensor(xs) producing a 1D tensor.

@[reducible, inline]

abbrev TorchLean.Tensor.fromList1d {α : Type} (xs : List α) : T α (Spec.Shape.dim xs.length Spec.Shape.scalar)

Build a vector tensor from a list.

PyTorch analogy: torch.tensor(xs) producing a 1D tensor.

@[reducible, inline]

abbrev TorchLean.Tensor.fromList2d {α : Type} [Inhabited α] (xss : List (List α)) : Option (T α (Spec.Shape.dim xss.length (Spec.Shape.dim (if xss.isEmpty = true then 0 else xss.head!.length) Spec.Shape.scalar)))

Build a matrix tensor from a list of rows (strict validation).

This is the "safe by default" constructor used by the user-facing API layer. It refuses empty input and refuses ragged rows, because that usually indicates a bug at the call site (e.g. an accidental missing column in imported weights).

PyTorch analogy: torch.tensor(xss) will also error if xss is ragged.

@[reducible, inline]

abbrev TorchLean.Tensor.ofList {α : Type} (dims : List ℕ) (xs : List α) : Except String (T α (Shape.ofDims dims))

N-D tensor from a runtime dims list and a flat xs, with a runtime length check.

This is the “dynamic / user-friendly” version: it fails with a descriptive message if the number of provided scalars doesn’t match the implied numel.

@[reducible, inline]

abbrev TorchLean.Tensor.float32Vector (xs : List Float) : T Floats.IEEE754.IEEE32Exec (Spec.Shape.dim xs.length Spec.Shape.scalar)

1-D tensor from Float literals, cast into the executable IEEE-754 FP32 backend.

@[reducible, inline]

abbrev TorchLean.Tensor.fill {α : Type} (value : α) (s : Shape) : T α s

Fill a tensor of shape s with a constant value.

PyTorch analogy: torch.full(shape, value).

@[reducible, inline]

abbrev TorchLean.Tensor.map {α β : Type} {s : Shape} (f : α → β) (x : T α s) : T β s

Map a scalar function across a tensor, changing the element type.

PyTorch analogy: torch.Tensor.to(dtype=...) is implemented as a scalar cast map under the hood. We keep this explicit at the spec layer because it is a common building block.

@[reducible, inline]

abbrev TorchLean.Tensor.vecGet {α : Type} {n : ℕ} (x : T α (Spec.Shape.dim n Spec.Shape.scalar)) (i : Fin n) : α

Extract the i-th entry from a vector tensor.

@[reducible, inline]

abbrev TorchLean.Tensor.print {α : Type} [NN.Tensor.DTypeName α] [NN.Tensor.TensorPrintable α] {s : Shape} (t : T α s) : IO Unit

Print a tensor with a dtype tag, or throw an IO.userError if the dtype refuses to print.

@[reducible, inline]

abbrev TorchLean.Tensor.pretty {α : Type} [ToString α] {s : Shape} (t : T α s) : String

Pretty‑print a tensor using ToString on scalars.

@[reducible, inline]

abbrev TorchLean.Tensor.toScalar {α : Type} (t : T α Spec.Shape.scalar) : α

Extract the scalar value from a scalar tensor.

@[reducible, inline]

abbrev TorchLean.Tensor.castFloat {α : Type} (cast : Float → α) {s : Shape} (t : T Float s) : T α s

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

def TorchLean.Tensor.repeatBatch {α : Type} {s : Shape} (batch : ℕ) (x : T α s) : T α (Spec.Shape.dim batch s)

Repeat one tensor across a fixed batch axis.

Use this for classifier demos whose checked model consumes a whole batch, while the example wants to inspect one ordinary input.

def TorchLean.Tensor.toFloatIO {α : Type} [Runtime.TensorScalar α] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] {s : Shape} : T α s → IO (T Float s)

Convert a runtime tensor back to a Float tensor inside IO.

This is the public bridge used by trainer prediction handles: examples can train under executable IEEE32 or other runtime scalar backends, but still receive ordinary Float tensors for inspection, printing, and follow-up scripting.

@[reducible, inline]

abbrev TorchLean.Semantics.relu {α : Type} [Zero α] [Max α] (x : α) : α

Host-side scalar ReLU for task definitions and synthetic targets.

Public Namespaces

These namespaces are the user-facing spelling for model construction, tensor utilities, training, runtime selection, and verification-adjacent examples. The definitions below forward to the checked implementation; the semantics are not copied or forked.