Skip to content

chore: add more byte conversions, fix namespaces #82

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
seanmcl merged 1 commit into from
Jul 8, 2025
Merged

chore: add more byte conversions, fix namespaces #82

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 10 additions & 4 deletions TensorLib/ByteArray.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,8 +52,11 @@ def _root_.ByteArray.toUInt32BE (bs : ByteArray) : Err UInt32 :=

def _root_.ByteArray.toUInt32LE! (bs : ByteArray) : UInt32 := get! bs.toUInt32LE
def _root_.ByteArray.toUInt32BE! (bs : ByteArray) : UInt32 := get! bs.toUInt32BE
def _root_.ByteArray.toInt32LE! (bs : ByteArray) : Int32 := bs.toUInt32LE!.toInt32
def _root_.ByteArray.toInt32BE! (bs : ByteArray) : Int32 := bs.toUInt32BE!.toInt32

def _root_.ByteArray.toInt32LE (bs : ByteArray) : Err Int32 := bs.toUInt32LE.map UInt32.toInt32
def _root_.ByteArray.toInt32BE (bs : ByteArray) : Err Int32 := bs.toUInt32BE.map UInt32.toInt32
def _root_.ByteArray.toInt32LE! (bs : ByteArray) : Int32 := get! bs.toInt32LE
def _root_.ByteArray.toInt32BE! (bs : ByteArray) : Int32 := get! bs.toInt32BE

/-- Interpret a `ByteArray` of size 2 as a little-endian `UInt16`. Missing from Lean stdlib. -/
def _root_.ByteArray.toUInt16LE (bs : ByteArray) : Err UInt16 :=
Expand All @@ -69,8 +72,11 @@ def _root_.ByteArray.toUInt16BE (bs : ByteArray) : Err UInt16 :=

def _root_.ByteArray.toUInt16LE! (bs : ByteArray) : UInt16 := get! bs.toUInt16LE
def _root_.ByteArray.toUInt16BE! (bs : ByteArray) : UInt16 := get! bs.toUInt16BE
def _root_.ByteArray.toInt16LE! (bs : ByteArray) : Int16 := bs.toUInt16LE!.toInt16
def _root_.ByteArray.toInt16BE! (bs : ByteArray) : Int16 := bs.toUInt16BE!.toInt16

def _root_.ByteArray.toInt16LE (bs : ByteArray) : Err Int16 := bs.toUInt16LE.map UInt16.toInt16
def _root_.ByteArray.toInt16BE (bs : ByteArray) : Err Int16 := bs.toUInt16BE.map UInt16.toInt16
def _root_.ByteArray.toInt16LE! (bs : ByteArray) : Int16 := get! bs.toInt16LE
def _root_.ByteArray.toInt16BE! (bs : ByteArray) : Int16 := get! bs.toInt16BE

def _root_.ByteArray.reverse (arr : ByteArray) : ByteArray := ⟨ arr.data.reverse ⟩

Expand Down
16 changes: 8 additions & 8 deletions TensorLib/Float.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,23 +41,23 @@ instance : ToLEByteArray Float where
instance : ToBEByteArray Float where
toBEByteArray f := toBEByteArray f.toBits

def Float32.ofLEByteArray (arr : ByteArray) : Err Float32 := do
def _root_.Float32.ofLEByteArray (arr : ByteArray) : Err Float32 := do
return Float32.ofBits (<- arr.toUInt32LE)

def Float32.ofBEByteArray (arr : ByteArray) : Err Float32 := do
def _root_.Float32.ofBEByteArray (arr : ByteArray) : Err Float32 := do
return Float32.ofBits (<- arr.toUInt32BE)

def Float32.ofLEByteArray! (arr : ByteArray) : Float32 := get! $ Float32.ofLEByteArray arr
def Float32.ofBEByteArray! (arr : ByteArray) : Float32 := get! $ Float32.ofBEByteArray arr
def _root_.Float32.ofLEByteArray! (arr : ByteArray) : Float32 := get! $ Float32.ofLEByteArray arr
def _root_.Float32.ofBEByteArray! (arr : ByteArray) : Float32 := get! $ Float32.ofBEByteArray arr

def Float.ofLEByteArray (arr : ByteArray) : Err Float := do
def _root_.Float.ofLEByteArray (arr : ByteArray) : Err Float := do
return Float.ofBits (<- arr.toUInt64LE)

def Float.ofBEByteArray (arr : ByteArray) : Err Float := do
def _root_.Float.ofBEByteArray (arr : ByteArray) : Err Float := do
return Float.ofBits (<- arr.toUInt64BE)

def Float.ofLEByteArray! (arr : ByteArray) : Float := get! $ Float.ofLEByteArray arr
def Float.ofBEByteArray! (arr : ByteArray) : Float := get! $ Float.ofBEByteArray arr
def _root_.Float.ofLEByteArray! (arr : ByteArray) : Float := get! $ Float.ofLEByteArray arr
def _root_.Float.ofBEByteArray! (arr : ByteArray) : Float := get! $ Float.ofBEByteArray arr

def _root_.Float32.toNat (f : Float32) : Nat := f.toUInt64.toNat

Expand Down