Element conversion and mixed-type tensor arithmetic

TorchLean tensors remain homogeneous: every individual tensor has one element type and one corresponding physical storage representation. This module provides explicit element conversion and an extensible promotion relation for operations whose inputs have different element types.

The built-in promotion order is

UInt8 < Nat < Int < Rat < Float32 < Float

Moving from exact values to an IEEE type rounds to nearest with ties to even. Rational conversion rounds the exact quotient, avoiding intermediate numerator or denominator overflow. User-defined element types can participate by providing ElementCast and ElementPromotion instances.

class TorchLean.ElementCast (α : Type u) (β : Type v) : Type (max u v)

An explicit element conversion used by Tensor.cast.

Instances need not be lossless. In particular, conversions to Float32 or Float use Lean's ordinary IEEE rounding behavior.

• cast : α → β

  Convert one source element to the target element type.

class TorchLean.ElementPromotion (α β : Type) (γ : outParam Type) : Type

The common element type and two conversions selected for a mixed operation.

The result is an outParam, so typeclass search determines it from the ordered input pair before looking for arithmetic or storage instances. Library instances are symmetric; custom instances should normally provide both operand orders.

• left : α → γ

  Convert the left element to the common type.

• right : β → γ

  Convert the right element to the common type.

@[inline]

def TorchLean.ElementCast.apply {α : Type u} {β : Type v} [conversion : ElementCast α β] (value : α) : β

Apply the registered element conversion.

@[instance_reducible]

def TorchLean.ElementPromotion.ofCasts (α β γ : Type) [leftCast : ElementCast α γ] [rightCast : ElementCast β γ] : ElementPromotion α β γ

Build a promotion from two explicit conversions to one result type.

@[instance_reducible]

instance TorchLean.instElementCast {α : Type u} : ElementCast α α

Every element type converts to itself.

@[instance_reducible]

instance TorchLean.instElementCastUInt8Nat : ElementCast UInt8 ℕ

@[instance_reducible]

instance TorchLean.instElementCastUInt8Int : ElementCast UInt8 ℤ

@[instance_reducible]

instance TorchLean.instElementCastUInt8Rat : ElementCast UInt8 Rat

@[instance_reducible]

instance TorchLean.instElementCastUInt8Float32 : ElementCast UInt8 Float32

@[instance_reducible]

instance TorchLean.instElementCastUInt8Float : ElementCast UInt8 Float

@[instance_reducible]

instance TorchLean.instElementCastNatInt : ElementCast ℕ ℤ

@[instance_reducible]

instance TorchLean.instElementCastNatRat : ElementCast ℕ Rat

@[instance_reducible]

instance TorchLean.instElementCastNatFloat32 : ElementCast ℕ Float32

@[instance_reducible]

instance TorchLean.instElementCastNatFloat : ElementCast ℕ Float

@[instance_reducible]

instance TorchLean.instElementCastIntRat : ElementCast ℤ Rat

@[instance_reducible]

instance TorchLean.instElementCastIntFloat32 : ElementCast ℤ Float32

@[instance_reducible]

instance TorchLean.instElementCastIntFloat : ElementCast ℤ Float

def TorchLean.Rat.roundToFormat (format : Float.Model.Format) (value : Rat) : Float.Model.UnpackedFloat

Round an exact rational through Lean's quotient and residual-bit model.

def TorchLean.Rat.toFloat32 (value : Rat) : Float32

Convert an exact rational to binary32, rounding once to nearest with ties to even.

Small exactly representable integers use native division. Larger values use Lean's float model before packing, so a finite ratio near one does not become ∞ / ∞.

def TorchLean.Rat.toFloat (value : Rat) : Float

Convert an exact rational to binary64, rounding once to nearest with ties to even.

@[instance_reducible]

instance TorchLean.instElementCastRatFloat32 : ElementCast Rat Float32

@[instance_reducible]

instance TorchLean.instElementCastRatFloat : ElementCast Rat Float

@[instance_reducible]

instance TorchLean.instElementCastFloat32Float : ElementCast Float32 Float

@[instance_reducible]

instance TorchLean.instElementCastFloatFloat32 : ElementCast Float Float32

Explicit binary64-to-binary32 conversion using Lean's IEEE rounding.

@[instance_reducible]

instance TorchLean.instElementPromotion {α : Type} : ElementPromotion α α α

@[instance_reducible]

instance TorchLean.instElementPromotionUInt8Nat : ElementPromotion UInt8 ℕ ℕ

@[instance_reducible]

instance TorchLean.instElementPromotionNatUInt8 : ElementPromotion ℕ UInt8 ℕ

@[instance_reducible]

instance TorchLean.instElementPromotionUInt8Int : ElementPromotion UInt8 ℤ ℤ

@[instance_reducible]

instance TorchLean.instElementPromotionIntUInt8 : ElementPromotion ℤ UInt8 ℤ

@[instance_reducible]

instance TorchLean.instElementPromotionUInt8Rat : ElementPromotion UInt8 Rat Rat

@[instance_reducible]

instance TorchLean.instElementPromotionRatUInt8 : ElementPromotion Rat UInt8 Rat

@[instance_reducible]

instance TorchLean.instElementPromotionUInt8Float32 : ElementPromotion UInt8 Float32 Float32

@[instance_reducible]

instance TorchLean.instElementPromotionFloat32UInt8 : ElementPromotion Float32 UInt8 Float32

@[instance_reducible]

instance TorchLean.instElementPromotionUInt8Float : ElementPromotion UInt8 Float Float

@[instance_reducible]

instance TorchLean.instElementPromotionFloatUInt8 : ElementPromotion Float UInt8 Float

@[instance_reducible]

instance TorchLean.instElementPromotionNatInt : ElementPromotion ℕ ℤ ℤ

@[instance_reducible]

instance TorchLean.instElementPromotionIntNat : ElementPromotion ℤ ℕ ℤ

@[instance_reducible]

instance TorchLean.instElementPromotionNatRat : ElementPromotion ℕ Rat Rat

@[instance_reducible]

instance TorchLean.instElementPromotionRatNat : ElementPromotion Rat ℕ Rat

@[instance_reducible]

instance TorchLean.instElementPromotionNatFloat32 : ElementPromotion ℕ Float32 Float32

@[instance_reducible]

instance TorchLean.instElementPromotionFloat32Nat : ElementPromotion Float32 ℕ Float32

@[instance_reducible]

instance TorchLean.instElementPromotionNatFloat : ElementPromotion ℕ Float Float

@[instance_reducible]

instance TorchLean.instElementPromotionFloatNat : ElementPromotion Float ℕ Float

@[instance_reducible]

instance TorchLean.instElementPromotionIntRat : ElementPromotion ℤ Rat Rat

@[instance_reducible]

instance TorchLean.instElementPromotionRatInt : ElementPromotion Rat ℤ Rat

@[instance_reducible]

instance TorchLean.instElementPromotionIntFloat32 : ElementPromotion ℤ Float32 Float32

@[instance_reducible]

instance TorchLean.instElementPromotionFloat32Int : ElementPromotion Float32 ℤ Float32

@[instance_reducible]

instance TorchLean.instElementPromotionIntFloat : ElementPromotion ℤ Float Float

@[instance_reducible]

instance TorchLean.instElementPromotionFloatInt : ElementPromotion Float ℤ Float

@[instance_reducible]

instance TorchLean.instElementPromotionRatFloat32 : ElementPromotion Rat Float32 Float32

@[instance_reducible]

instance TorchLean.instElementPromotionFloat32Rat : ElementPromotion Float32 Rat Float32

@[instance_reducible]

instance TorchLean.instElementPromotionRatFloat : ElementPromotion Rat Float Float

@[instance_reducible]

instance TorchLean.instElementPromotionFloatRat : ElementPromotion Float Rat Float

@[instance_reducible]

instance TorchLean.instElementPromotionFloat32Float : ElementPromotion Float32 Float Float

@[instance_reducible]

instance TorchLean.instElementPromotionFloatFloat32 : ElementPromotion Float Float32 Float

class TorchLean.Tensor.Internal.PointwiseAdd (α β : Type) (γ : outParam Type) [Storage α] [Storage β] [Storage γ] : Type

Execution strategy for pointwise tensor addition.

The low-priority instance preserves the fully generic mixed-type operation. Packed element types can provide a higher-priority implementation while proving the same coordinate semantics.

• scalar : α → β → γ

  Scalar operation implemented by this tensor kernel.

• apply {shape : Shape} : Rep α shape → Rep β shape → Rep γ shape

  Build the pointwise sum.

• apply_at {shape : Shape} (left : Rep α shape) (right : Rep β shape) (coordinate : Coord shape) : (apply left right).get coordinate = scalar (left.get coordinate) (right.get coordinate)

  The tensor implementation agrees with its scalar operation.

@[inline]

def TorchLean.Tensor.Internal.PointwiseAdd.run {α β γ : Type} [Storage α] [Storage β] [Storage γ] [operation : PointwiseAdd α β γ] {shape : Shape} (left : Rep α shape) (right : Rep β shape) : Rep γ shape

Use the selected pointwise addition strategy.

class TorchLean.Tensor.Internal.PointwiseSub (α β : Type) (γ : outParam Type) [Storage α] [Storage β] [Storage γ] : Type

Execution strategy for pointwise tensor subtraction.

• scalar : α → β → γ

  Scalar operation implemented by this tensor kernel.

• apply {shape : Shape} : Rep α shape → Rep β shape → Rep γ shape

  Build the pointwise difference.

• apply_at {shape : Shape} (left : Rep α shape) (right : Rep β shape) (coordinate : Coord shape) : (apply left right).get coordinate = scalar (left.get coordinate) (right.get coordinate)

  The tensor implementation agrees with its scalar operation.

@[inline]

def TorchLean.Tensor.Internal.PointwiseSub.run {α β γ : Type} [Storage α] [Storage β] [Storage γ] [operation : PointwiseSub α β γ] {shape : Shape} (left : Rep α shape) (right : Rep β shape) : Rep γ shape

Use the selected pointwise subtraction strategy.

class TorchLean.Tensor.Internal.PointwiseMul (α β : Type) (γ : outParam Type) [Storage α] [Storage β] [Storage γ] : Type

Execution strategy for pointwise tensor multiplication.

• scalar : α → β → γ

  Scalar operation implemented by this tensor kernel.

• apply {shape : Shape} : Rep α shape → Rep β shape → Rep γ shape

  Build the pointwise product.

• apply_at {shape : Shape} (left : Rep α shape) (right : Rep β shape) (coordinate : Coord shape) : (apply left right).get coordinate = scalar (left.get coordinate) (right.get coordinate)

  The tensor implementation agrees with its scalar operation.

@[inline]

def TorchLean.Tensor.Internal.PointwiseMul.run {α β γ : Type} [Storage α] [Storage β] [Storage γ] [operation : PointwiseMul α β γ] {shape : Shape} (left : Rep α shape) (right : Rep β shape) : Rep γ shape

Use the selected pointwise multiplication strategy.

class TorchLean.Tensor.Internal.PointwiseDiv (α β : Type) (γ : outParam Type) [Storage α] [Storage β] [Storage γ] : Type

Execution strategy for pointwise tensor division.

• scalar : α → β → γ

  Scalar operation implemented by this tensor kernel.

• apply {shape : Shape} : Rep α shape → Rep β shape → Rep γ shape

  Build the pointwise quotient.

• apply_at {shape : Shape} (left : Rep α shape) (right : Rep β shape) (coordinate : Coord shape) : (apply left right).get coordinate = scalar (left.get coordinate) (right.get coordinate)

  The tensor implementation agrees with its scalar operation.

@[inline]

def TorchLean.Tensor.Internal.PointwiseDiv.run {α β γ : Type} [Storage α] [Storage β] [Storage γ] [operation : PointwiseDiv α β γ] {shape : Shape} (left : Rep α shape) (right : Rep β shape) : Rep γ shape

Use the selected pointwise division strategy.

@[instance_reducible, instance 100]

instance TorchLean.Tensor.Internal.Rep.instPointwiseAddOfElementPromotionOfAdd {α β γ : Type} [Storage α] [Storage β] [promotion : ElementPromotion α β γ] [Storage γ] [Add γ] : PointwiseAdd α β γ

Generic one-pass fallback for every supported scalar promotion.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Rep.instPointwiseAddFloat : PointwiseAdd Float Float Float

Packed Float addition uses one exact-size native output loop.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Rep.instPointwiseAddUInt8Float : PointwiseAdd UInt8 Float Float

Packed byte-to-float promotion is fused with packed Float addition.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Rep.instPointwiseAddFloatUInt8 : PointwiseAdd Float UInt8 Float

Packed Float addition is fused with packed byte-to-float promotion.

@[instance_reducible, instance 100]

instance TorchLean.Tensor.Internal.Rep.instPointwiseSubOfElementPromotionOfSub {α β γ : Type} [Storage α] [Storage β] [promotion : ElementPromotion α β γ] [Storage γ] [Sub γ] : PointwiseSub α β γ

Generic one-pass fallback for every supported subtraction promotion.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Rep.instPointwiseSubFloat : PointwiseSub Float Float Float

Packed Float subtraction uses one exact-size native output loop.

@[instance_reducible, instance 100]

instance TorchLean.Tensor.Internal.Rep.instPointwiseMulOfElementPromotionOfMul {α β γ : Type} [Storage α] [Storage β] [promotion : ElementPromotion α β γ] [Storage γ] [Mul γ] : PointwiseMul α β γ

Generic one-pass fallback for every supported multiplication promotion.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Rep.instPointwiseMulFloat : PointwiseMul Float Float Float

Packed Float multiplication uses one exact-size native output loop.

@[instance_reducible, instance 100]

instance TorchLean.Tensor.Internal.Rep.instPointwiseDivOfElementPromotionOfDiv {α β γ : Type} [Storage α] [Storage β] [promotion : ElementPromotion α β γ] [Storage γ] [Div γ] : PointwiseDiv α β γ

Generic one-pass fallback for every supported division promotion.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Rep.instPointwiseDivFloat : PointwiseDiv Float Float Float

Packed Float division uses one exact-size native output loop.

def TorchLean.Tensor.Internal.Rep.cast {α : Type u} [Storage α] {shape : Shape} (tensor : Rep α shape) (target : Type v) [Storage target] [ElementCast α target] : Rep target shape

Convert every element while preserving the tensor's static shape.

The target Storage instance selects the target physical buffer, so a cast to Float writes a FloatArray and a cast to UInt8 writes a ByteArray.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.cast_apply {α : Type u} [Storage α] {shape : Shape} (tensor : Rep α shape) (target : Type v) [Storage target] [ElementCast α target] (coordinate : Coord shape) : (tensor.cast target).get coordinate = ElementCast.apply (tensor.get coordinate)

Reading a cast tensor converts the element at the same coordinate.

def TorchLean.Tensor.Internal.Rep.add {α β γ : Type} [Storage α] [Storage β] [Storage γ] [PointwiseAdd α β γ] {shape : Shape} (left : Rep α shape) (right : Rep β shape) : Rep γ shape

Add two tensors pointwise, promoting their element types when necessary.

Both conversions and the addition occur in one output-building pass.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.add_apply {α β γ : Type} [Storage α] [Storage β] [Storage γ] [operation : PointwiseAdd α β γ] {shape : Shape} (left : Rep α shape) (right : Rep β shape) (coordinate : Coord shape) : (left.add right).get coordinate = PointwiseAdd.scalar (left.get coordinate) (right.get coordinate)

Coordinate semantics of pointwise tensor addition.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Rep.instHAddOfPointwiseAdd {α β γ : Type} [Storage α] [Storage β] [Storage γ] [PointwiseAdd α β γ] {shape : Shape} : HAdd (Rep α shape) (Rep β shape) (Rep γ shape)

Tensor addition automatically selects the common element type.

def TorchLean.Tensor.Internal.Rep.sub {α β γ : Type} [Storage α] [Storage β] [Storage γ] [PointwiseSub α β γ] {shape : Shape} (left : Rep α shape) (right : Rep β shape) : Rep γ shape

Subtract two tensors pointwise, promoting their element types when necessary.

Both conversions and the subtraction occur in one output-building pass.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.sub_apply {α β γ : Type} [Storage α] [Storage β] [Storage γ] [operation : PointwiseSub α β γ] {shape : Shape} (left : Rep α shape) (right : Rep β shape) (coordinate : Coord shape) : (left.sub right).get coordinate = PointwiseSub.scalar (left.get coordinate) (right.get coordinate)

Coordinate semantics of pointwise tensor subtraction.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Rep.instHSubOfPointwiseSub {α β γ : Type} [Storage α] [Storage β] [Storage γ] [PointwiseSub α β γ] {shape : Shape} : HSub (Rep α shape) (Rep β shape) (Rep γ shape)

Tensor subtraction automatically selects the common element type.

def TorchLean.Tensor.Internal.Rep.mul {α β γ : Type} [Storage α] [Storage β] [Storage γ] [PointwiseMul α β γ] {shape : Shape} (left : Rep α shape) (right : Rep β shape) : Rep γ shape

Multiply two tensors pointwise, promoting their element types when necessary.

Both conversions and the multiplication occur in one output-building pass.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.mul_apply {α β γ : Type} [Storage α] [Storage β] [Storage γ] [operation : PointwiseMul α β γ] {shape : Shape} (left : Rep α shape) (right : Rep β shape) (coordinate : Coord shape) : (left.mul right).get coordinate = PointwiseMul.scalar (left.get coordinate) (right.get coordinate)

Coordinate semantics of pointwise tensor multiplication.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Rep.instHMulOfPointwiseMul {α β γ : Type} [Storage α] [Storage β] [Storage γ] [PointwiseMul α β γ] {shape : Shape} : HMul (Rep α shape) (Rep β shape) (Rep γ shape)

Tensor multiplication automatically selects the common element type.

def TorchLean.Tensor.Internal.Rep.div {α β γ : Type} [Storage α] [Storage β] [Storage γ] [PointwiseDiv α β γ] {shape : Shape} (left : Rep α shape) (right : Rep β shape) : Rep γ shape

Divide two tensors pointwise, promoting their element types when necessary.

Both conversions and the division occur in one output-building pass.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.div_apply {α β γ : Type} [Storage α] [Storage β] [Storage γ] [operation : PointwiseDiv α β γ] {shape : Shape} (left : Rep α shape) (right : Rep β shape) (coordinate : Coord shape) : (left.div right).get coordinate = PointwiseDiv.scalar (left.get coordinate) (right.get coordinate)

Coordinate semantics of pointwise tensor division.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Rep.instHDivOfPointwiseDiv {α β γ : Type} [Storage α] [Storage β] [Storage γ] [PointwiseDiv α β γ] {shape : Shape} : HDiv (Rep α shape) (Rep β shape) (Rep γ shape)

Tensor division automatically selects the common element type.