Shape/axis helpers

def Runtime.Autograd.Model.F.swapAdjacentAtDepth {α : Type} [TorchLean.Storage α] [Context α] {m : Type → Type} [Monad m] [Ops m α] {s : Spec.Shape} (depth : ℕ) (x : RefTy m α s) : m (RefTy m α (s.swapAdjacentAtDepth depth))

Swap two adjacent axes at a given nesting depth.

This is the primitive used to implement general permutations via a sequence of adjacent swaps. It corresponds to the backend op Torch.swapAdjacentAtDepth.

Core tensor semantics (PyTorch-style)

def Runtime.Autograd.Model.F.hasDupNat (xs : Array ℕ) : Bool

Detect duplicate axes in a runtime axis array.

def Runtime.Autograd.Model.F.hasDupNat.go (seen : List ℕ) : List ℕ → Bool

def Runtime.Autograd.Model.F.insertDesc (x : ℕ) : List ℕ → List ℕ

Insert x into a list kept in descending order.

def Runtime.Autograd.Model.F.sortDesc (xs : Array ℕ) : Array ℕ

Sort a runtime axis array in descending order.

def Runtime.Autograd.Model.F.permute? {α : Type} [TorchLean.Storage α] [Context α] {m : Type → Type} [Monad m] [Ops m α] {s : Spec.Shape} (axes : Array ℕ) (x : RefTy m α s) : m (Option ((s' : Spec.Shape) × RefTy m α s'))

Dynamic permutation: like permute, but returns an existential output shape.

PyTorch analogue: torch.permute / Tensor.permute (with runtime checks).

def Runtime.Autograd.Model.F.permute {α : Type} [TorchLean.Storage α] [Context α] {m : Type → Type} [Monad m] [Ops m α] {s sOut : Spec.Shape} (axes : Array ℕ) (x : RefTy m α s) : m (Option (RefTy m α sOut))

Permutation with an expected output shape.

This calls permute? and checks that the computed shape equals sOut.

def Runtime.Autograd.Model.F.transpose {α : Type} [TorchLean.Storage α] [Context α] {m : Type → Type} [Monad m] [Ops m α] {s sOut : Spec.Shape} (axis₁ axis₂ : ℕ) (x : RefTy m α s) : m (Option (RefTy m α sOut))

Exchange two arbitrary axes and check the statically expected output shape.

The result is none when either axis is invalid or the transposed shape is not sOut.

def Runtime.Autograd.Model.F.Internal.reduceAlongLastSum {α : Type} [TorchLean.Storage α] [Context α] {m : Type → Type} [Monad m] [Ops m α] (x : (s : Spec.Shape) × RefTy m α s) : m (Option ((s' : Spec.Shape) × RefTy m α s'))

Reduce along the last axis with sum, returning the new (existential) shape.

This is the primitive step used by reduceAxesCore after it has permuted the requested axis to the last position.

def Runtime.Autograd.Model.F.Internal.reduceAlongLastMean {α : Type} [TorchLean.Storage α] [Context α] {m : Type → Type} [Monad m] [Ops m α] (x : (s : Spec.Shape) × RefTy m α s) : m (Option ((s' : Spec.Shape) × RefTy m α s'))

Like reduceAlongLastSum, but using mean.

def Runtime.Autograd.Model.F.Internal.reduceAxesCore {α : Type} [TorchLean.Storage α] [Context α] {m : Type → Type} [Monad m] [Ops m α] (reduceLast : (s : Spec.Shape) × RefTy m α s → m (Option ((s' : Spec.Shape) × RefTy m α s'))) {s : Spec.Shape} (axes : Array ℕ) (keepdim : Bool) (x : RefTy m α s) : m (Option ((s' : Spec.Shape) × RefTy m α s'))

Core implementation for reductions over a runtime array of axes.

This lowers “reduce along axis k” to:

1. permute axis k to the last position,
2. call reduceLast, and
3. optionally re-insert a singleton dimension when keepdim = true.

reduceSumDims? and reduceMeanDims? specialize this operation.

def Runtime.Autograd.Model.F.reduceSumDims? {α : Type} [TorchLean.Storage α] [Context α] {m : Type → Type} [Monad m] [Ops m α] {s : Spec.Shape} (axes : Array ℕ) (x : RefTy m α s) (keepdim : Bool := false) : m (Option ((s' : Spec.Shape) × RefTy m α s'))

Dynamic multi-axis sum reduction (like torch.sum(x, dim=axes, keepdim=...)).

def Runtime.Autograd.Model.F.reduceMeanDims? {α : Type} [TorchLean.Storage α] [Context α] {m : Type → Type} [Monad m] [Ops m α] {s : Spec.Shape} (axes : Array ℕ) (x : RefTy m α s) (keepdim : Bool := false) : m (Option ((s' : Spec.Shape) × RefTy m α s'))

Dynamic multi-axis mean reduction (like torch.mean(x, dim=axes, keepdim=...)).

def Runtime.Autograd.Model.F.softmax {α : Type} [TorchLean.Storage α] [Context α] {m : Type → Type} [Monad m] [Ops m α] {s : Spec.Shape} (axis : ℕ) [Spec.Shape.AxisInBounds axis s] (x : RefTy m α s) : m (RefTy m α s)

Softmax along any valid tensor dimension.

The selected dimension is moved to the end for the backend's row-softmax primitive and then moved back. The reverse-swap theorem makes the result shape exactly s; no runtime shape check is needed.

def Runtime.Autograd.Model.F.logSoftmax {α : Type} [TorchLean.Storage α] [Context α] {m : Type → Type} [Monad m] [Ops m α] {s : Spec.Shape} (axis : ℕ) [Spec.Shape.AxisInBounds axis s] (x : RefTy m α s) : m (RefTy m α s)

Log-softmax along any valid tensor dimension.