From e4bd2c34a51c87d86e3b33a33fdcdbca55d5362b Mon Sep 17 00:00:00 2001 From: Sean McLaughlin Date: Mon, 7 Jul 2025 19:14:20 -0700 Subject: [PATCH] chore: add more byte conversions, fix namespaces --- TensorLib/ByteArray.lean | 14 ++++++++++---- TensorLib/Float.lean | 16 ++++++++-------- 2 files changed, 18 insertions(+), 12 deletions(-) diff --git a/TensorLib/ByteArray.lean b/TensorLib/ByteArray.lean index f483190..4e86fe7 100644 --- a/TensorLib/ByteArray.lean +++ b/TensorLib/ByteArray.lean @@ -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 := @@ -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 ⟩ diff --git a/TensorLib/Float.lean b/TensorLib/Float.lean index 8b74a2a..b599488 100644 --- a/TensorLib/Float.lean +++ b/TensorLib/Float.lean @@ -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