Typed Program Arguments

Arguments α shapes is the public container for an ordered set of tensors supplied to a multi-input program. Each tensor retains its own statically known shape while the tensor-pack representation remains behind Arguments.Internal.

structure TorchLean.Arguments (α : Type) [Storage α] (shapes : List Shape) : Type

Ordered tensor arguments for a program whose input shapes are known statically.

• tensors : TorchLean.TensorPack α shapes

def TorchLean.Arguments.Internal.fromTensorPack {α : Type} [Storage α] {shapes : List Shape} (tensors : TensorPack α shapes) : Arguments α shapes

Wrap the tensor-pack representation at an implementation boundary.

def TorchLean.Arguments.Internal.toTensorPack {α : Type} [Storage α] {shapes : List Shape} (arguments : Arguments α shapes) : TensorPack α shapes

Reveal the tensor-pack representation at an implementation boundary.

@[simp]

theorem TorchLean.Arguments.Internal.toTensorPack_fromTensorPack {α : Type} [Storage α] {shapes : List Shape} (tensors : TensorPack α shapes) : toTensorPack (fromTensorPack tensors) = tensors

Revealing a freshly wrapped tensor pack returns the original pack.

@[simp]

theorem TorchLean.Arguments.Internal.fromTensorPack_toTensorPack {α : Type} [Storage α] {shapes : List Shape} (arguments : Arguments α shapes) : fromTensorPack (toTensorPack arguments) = arguments

Wrapping the representation of arguments reconstructs those arguments.

theorem TorchLean.Arguments.ext {α : Type} [Storage α] {shapes : List Shape} {left right : Arguments α shapes} (h : Internal.toTensorPack left = Internal.toTensorPack right) : left = right

Two argument sequences are equal when their tensor-pack representations are equal.

theorem TorchLean.Arguments.ext_iff {α : Type} [Storage α] {shapes : List Shape} {left right : Arguments α shapes} : left = right ↔ Internal.toTensorPack left = Internal.toTensorPack right

def TorchLean.Arguments.empty {α : Type} [Storage α] : Arguments α []

No program arguments.

def TorchLean.Arguments.push {α : Type} [Storage α] {shapes : List Shape} {shape : Shape} (arguments : Arguments α shapes) (tensor : Tensor α shape) : Arguments α (shapes ++ [shape])

Add one tensor at the end of an argument sequence.

def TorchLean.Arguments.get {α : Type} [Storage α] {shapes : List Shape} (arguments : Arguments α shapes) (index : Fin shapes.length) : Tensor α (shapes.get index)

Read one argument; its result shape is determined by the index.

def TorchLean.Arguments.map {α β : Type} [Storage α] [Storage β] {shapes : List Shape} (arguments : Arguments α shapes) (f : {shape : Shape} → Tensor α shape → Tensor β shape) : Arguments β shapes

Apply a shape-preserving conversion to every argument.

def TorchLean.Arguments.zipWith {α β γ : Type} [Storage α] [Storage β] [Storage γ] {shapes : List Shape} (first : Arguments α shapes) (second : Arguments β shapes) (f : {shape : Shape} → Tensor α shape → Tensor β shape → Tensor γ shape) : Arguments γ shapes

Combine corresponding arguments with a shape-preserving operation.

def TorchLean.Arguments.append {α : Type} [Storage α] {leftShapes rightShapes : List Shape} (first : Arguments α leftShapes) (second : Arguments α rightShapes) : Arguments α (leftShapes ++ rightShapes)

Concatenate two ordered argument sequences.

@[instance_reducible]

instance TorchLean.Arguments.instRepr {α : Type} [Storage α] {shapes : List Shape} [Repr α] : Repr (Arguments α shapes)

structure TorchLean.Arguments.Partition (α : Type) [Storage α] (leftShapes rightShapes : List Shape) : Type

Named result of splitting arguments at a statically known shape-list boundary.

• left : Arguments α leftShapes

  Arguments before the split boundary.

• right : Arguments α rightShapes

  Arguments after the split boundary.

@[instance_reducible]

instance TorchLean.Arguments.instReprPartition {α✝ : Type} {inst✝ : Storage α✝} {leftShapes✝ rightShapes✝ : List Shape} [Repr α✝] : Repr (Partition α✝ leftShapes✝ rightShapes✝)

def TorchLean.Arguments.instReprPartition.repr {α✝ : Type} {inst✝ : Storage α✝} {leftShapes✝ rightShapes✝ : List Shape} [Repr α✝] : Partition α✝ leftShapes✝ rightShapes✝ → ℕ → Std.Format

def TorchLean.Arguments.split {α : Type} [Storage α] {leftShapes rightShapes : List Shape} (arguments : Arguments α (leftShapes ++ rightShapes)) : Partition α leftShapes rightShapes

Split arguments at a statically known shape-list boundary.