Mathematical modules

Spec.Module α σ τ packages a pure tensor map from shape σ to shape τ. The input and output shapes occur in the type, so ill-shaped compositions are rejected by Lean.

Spec.Module.Chain composes these maps. The kind and pythonExpr fields are descriptive metadata; forward alone gives the module its mathematical meaning.

structure Spec.Module (α : Type) [TorchLean.Storage α] (inShape outShape : Shape) : Type

A pure, shape-indexed tensor map with descriptive code-generation metadata.

• forward : TorchLean.Tensor α inShape → TorchLean.Tensor α outShape

  The mathematical meaning of the module.

• kind : String

  A stable operation name used in reports and exported graphs.

• pythonExpr : String

  A Python expression used by the source exporter. This field is not part of the semantics.

inductive Spec.Module.Chain (α : Type) [TorchLean.Storage α] : Shape → Shape → Type

Dependent composition of modules whose adjacent shapes agree definitionally.

• single {α : Type} [TorchLean.Storage α] {s t : Shape} (m : Module α s t) : Chain α s t
• comp {α : Type} [TorchLean.Storage α] {s t u : Shape} (a : Chain α s t) (b : Chain α t u) : Chain α s u

def Spec.Module.Chain.forward {α : Type} [TorchLean.Storage α] {s t : Shape} (c : Chain α s t) : TorchLean.Tensor α s → TorchLean.Tensor α t

Evaluate a chain from left to right.

def Spec.Module.Chain.append {α : Type} [TorchLean.Storage α] {s t u : Shape} (a : Chain α s t) (b : Module α t u) : Chain α s u

Append one module to the output of a chain.

def Spec.Module.Chain.kinds {α : Type} [TorchLean.Storage α] {s t : Shape} : Chain α s t → Array String

Return operation names in evaluation order.

def Spec.Module.Chain.layerInfo {α : Type} [TorchLean.Storage α] {s t : Shape} : Chain α s t → Array (String × String)

Return operation names and Python expressions in evaluation order.

def Spec.Module.liftLeading {α : Type} [TorchLean.Storage α] [Context α] {n : ℕ} {elemIn elemOut : Shape} (m : Module α elemIn elemOut) : Module α (Shape.dim n elemIn) (Shape.dim n elemOut)

Lift a module to operate independently over one new leading dimension.

def Spec.Module.select {α : Type} [TorchLean.Storage α] {shape : Shape} (axis : ℕ) [Shape.AxisInBounds axis shape] (i : Fin (shape.axisSize axis)) : Module α shape (shape.eraseAxis axis)

Select one coordinate along any valid axis.