structure Sparkle.Core.Vector.HWVector (α : Type) (n : Nat) : Type

Hardware vector with compile-time known size.

This is a wrapper around an array that carries its size in the type, making it suitable for hardware synthesis.

• data : Array α
• size_eq : self.data.size = n

def Sparkle.Core.Vector.HWVector.ofArray {α : Type} {n : Nat} (arr : Array α) (h : arr.size = n := by rfl) : HWVector α n

Create a vector from an array (checks size at runtime)

Equations

• Sparkle.Core.Vector.HWVector.ofArray arr h = { data := arr, size_eq := h }

def Sparkle.Core.Vector.HWVector.get {α : Type} {n : Nat} (v : HWVector α n) (i : Fin n) : α

Get element at index i

Equations

• v.get i = v.data[↑i]

def Sparkle.Core.Vector.HWVector.set {α : Type} {n : Nat} (v : HWVector α n) (i : Fin n) (val : α) : HWVector α n

Set element at index i

Equations

• v.set i val = { data := v.data.set (↑⟨↑i, ⋯⟩) val ⋯, size_eq := ⋯ }

def Sparkle.Core.Vector.HWVector.replicate {α : Type} (n : Nat) (val : α) : HWVector α n

Create a vector by replicating a value

Equations

• Sparkle.Core.Vector.HWVector.replicate n val = { data := { toList := List.replicate n val }, size_eq := ⋯ }

def Sparkle.Core.Vector.HWVector.map {α β : Type} {n : Nat} (f : α → β) (v : HWVector α n) : HWVector β n

Map a function over all elements

Equations

• Sparkle.Core.Vector.HWVector.map f v = { data := Array.map f v.data, size_eq := ⋯ }

def Sparkle.Core.Vector.HWVector.ofList {α : Type} (l : List α) : HWVector α l.length

Create vector from list (checks size)

Equations

• Sparkle.Core.Vector.HWVector.ofList l = { data := { toList := l }, size_eq := ⋯ }

def Sparkle.Core.Vector.HWVector.toList {α : Type} {n : Nat} (v : HWVector α n) : List α

Convert vector to list

Equations

• v.toList = v.data.toList

instance Sparkle.Core.Vector.HWVector.instRepr {α : Type} {n : Nat} [Repr α] : Repr (HWVector α n)

Equations

• Sparkle.Core.Vector.HWVector.instRepr = { reprPrec := fun (v : Sparkle.Core.Vector.HWVector α n) (x : Nat) => repr v.toList }