Skip to content

chore: more ByteArray utilities #80

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
Jun 24, 2025
Merged

chore: more ByteArray utilities #80

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
10 changes: 10 additions & 0 deletions TensorLib/ByteArray.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,9 @@ def _root_.ByteArray.toUInt64LE (bs : ByteArray) : Err UInt64 :=
def _root_.ByteArray.toUInt64BE (bs : ByteArray) : Err UInt64 :=
if bs.size != 8 then throw "Expected size 8 byte array" else return bs.toUInt64BE!

def _root_.ByteArray.toInt64LE! (bs : ByteArray) : Int64 := bs.toUInt64LE!.toInt64
def _root_.ByteArray.toInt64BE! (bs : ByteArray) : Int64 := bs.toUInt64BE!.toInt64

/-- Interpret a `ByteArray` of size 4 as a little-endian `UInt32`. Missing from Lean stdlib. -/
def _root_.ByteArray.toUInt32LE (bs : ByteArray) : Err UInt32 :=
if bs.size != 4 then throw "Expected size 4 byte array" else
Expand All @@ -49,6 +52,8 @@ 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

/-- 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 @@ -64,6 +69,8 @@ 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.reverse (arr : ByteArray) : ByteArray := ⟨ arr.data.reverse ⟩

Expand Down Expand Up @@ -107,6 +114,9 @@ def _root_.ByteArray.take (arr : ByteArray) (n : Nat) : ByteArray :=
def _root_.ByteArray.drop (arr : ByteArray) (n : Nat) : ByteArray :=
ByteArray.mk (arr.data.drop n)

def _root_.ByteArray.splitAt (arr : ByteArray) (n : Nat) : ByteArray × ByteArray :=
(arr.take n, arr.drop n)

def _root_.ByteArray.readUInt32 (arr : ByteArray) (offset : Nat) : UInt32 :=
if arr.size < offset + 4 then 0 else
(arr.sub offset 4).toUInt32LE!
Expand Down