Eager Tensor Operations

PyTorch-style tensor operations recorded on the session's tape. Each one runs the CPU or the CUDA kernel of the operation, as the session's device selects, and preserves the typed TensorRef surface.

Linear algebra and concatenation

def Runtime.Autograd.Torch.Internal.EagerSession.matmul {α : Type} [TorchLean.Storage α] [Context α] [TensorTransfer α] (s : EagerSession α) {batchA batchB batch : Spec.Shape} {m n p : ℕ} [broadcastA : batchA.BroadcastTo batch] [broadcastB : batchB.BroadcastTo batch] (a : TensorRef α (batchA.concat [m, n])) (b : TensorRef α (batchB.concat [n, p])) (scale : Option α := none) : IO (TensorRef α (batch.concat [m, p]))

Matrix multiplication with PyTorch-style broadcasting across batch prefixes.

def Runtime.Autograd.Torch.Internal.EagerSession.concat {α : Type} [TorchLean.Storage α] (s : EagerSession α) {n m : ℕ} {sh : Spec.Shape} (a : TensorRef α (Spec.Shape.dim n sh)) (b : TensorRef α (Spec.Shape.dim m sh)) : IO (TensorRef α (Spec.Shape.dim (n + m) sh))

Concatenate along dim 0 for tensors with leading dimension. PyTorch: torch.cat(..., dim=0).

def Runtime.Autograd.Torch.Internal.EagerSession.slice {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Zero α] {n : ℕ} {sh : Spec.Shape} (x : TensorRef α (Spec.Shape.dim n sh)) (start len : ℕ) (h : start + len ≤ n) : IO (TensorRef α (Spec.Shape.dim len sh))

Slice along dim 0: x[start:start+len]. PyTorch: standard slicing.