Tensor Type Definitions

Core types for tensor operations in Hesper. Supports multi-dimensional tensors with shape information.

structure Hesper.Tensor.Shape : Type

Tensor shape represented as a list of dimensions

• dims : List Nat

instance Hesper.Tensor.instInhabitedShape : Inhabited Shape

Equations

• Hesper.Tensor.instInhabitedShape = { default := Hesper.Tensor.instInhabitedShape.default }

def Hesper.Tensor.instInhabitedShape.default : Shape

Equations

• Hesper.Tensor.instInhabitedShape.default = { dims := default }

instance Hesper.Tensor.instReprShape : Repr Shape

Equations

• Hesper.Tensor.instReprShape = { reprPrec := Hesper.Tensor.instReprShape.repr }

def Hesper.Tensor.instReprShape.repr : Shape → Nat → Std.Format

Equations

• Hesper.Tensor.instReprShape.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "dims" ++ Std.Format.text " := " ++ (Std.Format.nest 8 (repr x✝.dims)).group) " }"

def Hesper.Tensor.Shape.scalar : Shape

Equations

• Hesper.Tensor.Shape.scalar = { dims := [] }

def Hesper.Tensor.Shape.vector (n : Nat) : Shape

Equations

• Hesper.Tensor.Shape.vector n = { dims := [n] }

def Hesper.Tensor.Shape.matrix (rows cols : Nat) : Shape

Equations

• Hesper.Tensor.Shape.matrix rows cols = { dims := [rows, cols] }

def Hesper.Tensor.Shape.tensor3D (d1 d2 d3 : Nat) : Shape

Equations

• Hesper.Tensor.Shape.tensor3D d1 d2 d3 = { dims := [d1, d2, d3] }

def Hesper.Tensor.Shape.tensor4D (d1 d2 d3 d4 : Nat) : Shape

Equations

• Hesper.Tensor.Shape.tensor4D d1 d2 d3 d4 = { dims := [d1, d2, d3, d4] }

def Hesper.Tensor.Shape.size (s : Shape) : Nat

Total number of elements in the tensor

Equations

• s.size = List.foldl (fun (x1 x2 : Nat) => x1 * x2) 1 s.dims

def Hesper.Tensor.Shape.rank (s : Shape) : Nat

Rank (number of dimensions)

Equations

• s.rank = s.dims.length

inductive Hesper.Tensor.DType : Type

Tensor data type (scalar type of elements)

• f32 : DType
• f16 : DType
• i32 : DType
• u32 : DType

def Hesper.Tensor.instInhabitedDType.default : DType

Equations

• Hesper.Tensor.instInhabitedDType.default = Hesper.Tensor.DType.f32

instance Hesper.Tensor.instInhabitedDType : Inhabited DType

Equations

• Hesper.Tensor.instInhabitedDType = { default := Hesper.Tensor.instInhabitedDType.default }

def Hesper.Tensor.instReprDType.repr : DType → Nat → Std.Format

Equations

• Hesper.Tensor.instReprDType.repr Hesper.Tensor.DType.f32 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.Tensor.DType.f32")).group prec✝
• Hesper.Tensor.instReprDType.repr Hesper.Tensor.DType.f16 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.Tensor.DType.f16")).group prec✝
• Hesper.Tensor.instReprDType.repr Hesper.Tensor.DType.i32 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.Tensor.DType.i32")).group prec✝
• Hesper.Tensor.instReprDType.repr Hesper.Tensor.DType.u32 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.Tensor.DType.u32")).group prec✝

instance Hesper.Tensor.instReprDType : Repr DType

Equations

• Hesper.Tensor.instReprDType = { reprPrec := Hesper.Tensor.instReprDType.repr }

instance Hesper.Tensor.instBEqDType : BEq DType

Equations

• Hesper.Tensor.instBEqDType = { beq := Hesper.Tensor.instBEqDType.beq }

def Hesper.Tensor.instBEqDType.beq : DType → DType → Bool

Equations

• Hesper.Tensor.instBEqDType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Hesper.Tensor.DType.toWGSL : DType → WGSL.ScalarType

Equations

• Hesper.Tensor.DType.f32.toWGSL = Hesper.WGSL.ScalarType.f32
• Hesper.Tensor.DType.f16.toWGSL = Hesper.WGSL.ScalarType.f16
• Hesper.Tensor.DType.i32.toWGSL = Hesper.WGSL.ScalarType.i32
• Hesper.Tensor.DType.u32.toWGSL = Hesper.WGSL.ScalarType.u32

def Hesper.Tensor.DType.sizeBytes : DType → Nat

Equations

• Hesper.Tensor.DType.f32.sizeBytes = 4
• Hesper.Tensor.DType.f16.sizeBytes = 2
• Hesper.Tensor.DType.i32.sizeBytes = 4
• Hesper.Tensor.DType.u32.sizeBytes = 4

structure Hesper.Tensor.TensorDesc : Type

Tensor descriptor with shape and data type

• shape : Shape
• dtype : DType

instance Hesper.Tensor.instInhabitedTensorDesc : Inhabited TensorDesc

Equations

• Hesper.Tensor.instInhabitedTensorDesc = { default := Hesper.Tensor.instInhabitedTensorDesc.default }

def Hesper.Tensor.instInhabitedTensorDesc.default : TensorDesc

Equations

• Hesper.Tensor.instInhabitedTensorDesc.default = { shape := default, dtype := default }

def Hesper.Tensor.instReprTensorDesc.repr : TensorDesc → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Hesper.Tensor.instReprTensorDesc : Repr TensorDesc

Equations

• Hesper.Tensor.instReprTensorDesc = { reprPrec := Hesper.Tensor.instReprTensorDesc.repr }

def Hesper.Tensor.TensorDesc.sizeBytes (desc : TensorDesc) : Nat

Total size in bytes

Equations

• desc.sizeBytes = desc.shape.size * desc.dtype.sizeBytes

def Hesper.Tensor.TensorDesc.matrix (rows cols : Nat) (dtype : DType := DType.f32) : TensorDesc

Create a matrix descriptor

Equations

• Hesper.Tensor.TensorDesc.matrix rows cols dtype = { shape := Hesper.Tensor.Shape.matrix rows cols, dtype := dtype }

def Hesper.Tensor.TensorDesc.vector (n : Nat) (dtype : DType := DType.f32) : TensorDesc

Create a vector descriptor

Equations

• Hesper.Tensor.TensorDesc.vector n dtype = { shape := Hesper.Tensor.Shape.vector n, dtype := dtype }

structure Hesper.Tensor.MatMulConfig : Type

Matrix multiplication configuration

• M : Nat

  Matrix A dimensions: M × K

• K : Nat
• N : Nat

  Matrix B dimensions: K × N

• tileSize : Nat

  Workgroup tile size

• dtype : DType

  Data type

def Hesper.Tensor.instInhabitedMatMulConfig.default : MatMulConfig

Equations

• Hesper.Tensor.instInhabitedMatMulConfig.default = { M := default, K := default, N := default, tileSize := default, dtype := default }

instance Hesper.Tensor.instInhabitedMatMulConfig : Inhabited MatMulConfig

Equations

• Hesper.Tensor.instInhabitedMatMulConfig = { default := Hesper.Tensor.instInhabitedMatMulConfig.default }

instance Hesper.Tensor.instReprMatMulConfig : Repr MatMulConfig

Equations

• Hesper.Tensor.instReprMatMulConfig = { reprPrec := Hesper.Tensor.instReprMatMulConfig.repr }

def Hesper.Tensor.instReprMatMulConfig.repr : MatMulConfig → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Hesper.Tensor.MatMulConfig.shapeA (c : MatMulConfig) : Shape

Shape of matrix A

Equations

• c.shapeA = Hesper.Tensor.Shape.matrix c.M c.K

def Hesper.Tensor.MatMulConfig.shapeB (c : MatMulConfig) : Shape

Shape of matrix B

Equations

• c.shapeB = Hesper.Tensor.Shape.matrix c.K c.N

def Hesper.Tensor.MatMulConfig.shapeC (c : MatMulConfig) : Shape

Shape of result matrix C

Equations

• c.shapeC = Hesper.Tensor.Shape.matrix c.M c.N

def Hesper.Tensor.MatMulConfig.workgroupSize (c : MatMulConfig) : Nat × Nat × Nat

Workgroup size for compute shader

Equations

• c.workgroupSize = (c.tileSize, c.tileSize, 1)

def Hesper.Tensor.MatMulConfig.numWorkgroups (c : MatMulConfig) : Nat × Nat × Nat

Number of workgroups needed

Equations

• c.numWorkgroups = ((c.N + c.tileSize - 1) / c.tileSize, (c.M + c.tileSize - 1) / c.tileSize, 1)