Shape-Indexed Tensors

Tensor construction, shape operations, runtime conversion, and executable tensor operators.

Low-level executable ops 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.ofDims : List ℕ → NN.Tensor.Shape

Construct a shape from its outermost-to-innermost dimensions.

def TorchLean.Tensor.flattenBatchPrefix {α : Type} [Inhabited α] (batch takeDim : ℕ) {source : Shape} (hTake : takeDim ≤ source.size) (x : Spec.Tensor α (Spec.Shape.dim batch source)) : Spec.Tensor α (Spec.Shape.dim batch (Spec.Shape.dim takeDim Shape.scalar))

Flatten each sample in a batch and retain its first takeDim entries.

The proof hTake rules out truncation beyond the flattened source shape, so the result has the statically known shape batch × takeDim.

def TorchLean.Tensor.vectorFromArray {α : Type} (n : ℕ) (xs : Array α) (fallback : α) : Spec.Tensor α (Spec.Shape.dim n Shape.scalar)

Construct a fixed-length vector from an array.

Entries beyond the array use fallback; entries beyond length n are ignored. This constructor is useful at runtime data boundaries where the tensor length is fixed by a model type while the source array is checked or padded by the caller.

@[reducible, inline]

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

Public shorthand for TorchLean's shape-indexed tensor family.

@[reducible, inline]

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

Apply a scalar function pointwise while preserving the tensor shape.

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

Convert a Float tensor pointwise with an explicitly supplied scalar cast.

def TorchLean.Tensor.fromFloatList {α : Type} [Context α] (cast : Float → α) (dims : List ℕ) (xs : List Float) : Except String (T α (Shape.ofDims dims))

Construct a tensor from a flat list of Float values and convert each entry to the selected scalar type. The list length must equal the product of dims.

def TorchLean.Tensor.generateFromFloat {α : Type} [Context α] (cast : Float → α) (dims : List ℕ) (f : ℕ → Float) : T α (Shape.ofDims dims)

Generate a tensor from its flat element index and convert each generated Float to the selected scalar type.

def TorchLean.Tensor.generateFromFloatShape {α : Type} [Context α] (cast : Float → α) (shape : Shape) (f : ℕ → Float) : T α shape

Generate a tensor of a statically known shape from its flat element index.

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} [Context α] [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.

Trainer prediction handles use this so examples can train under executable IEEE32 or another scalar backend, then inspect ordinary Float tensors afterward.

Related Namespaces

Model construction, training, runtime selection, and verification live in their corresponding TorchLean namespaces.