Skip to content
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

feat: IntX.ofBitVec #7048

Merged
merged 1 commit into from
Feb 12, 2025
Merged

feat: IntX.ofBitVec #7048

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
10 changes: 10 additions & 0 deletions src/Init/Data/SInt/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,6 +85,8 @@ This function has the same behavior as `Int.toNat` for negative numbers.
If you want to obtain the 2's complement representation use `toBitVec`.
-/
@[inline] def Int8.toNat (i : Int8) : Nat := i.toInt.toNat
/-- Obtains the `Int8` whose 2's complement representation is the given `BitVec 8`. -/
@[inline] def Int8.ofBitVec (b : BitVec 8) : Int8 := ⟨⟨b⟩⟩
@[extern "lean_int8_neg"]
def Int8.neg (i : Int8) : Int8 := ⟨⟨-i.toBitVec⟩⟩

Expand Down Expand Up @@ -185,6 +187,8 @@ This function has the same behavior as `Int.toNat` for negative numbers.
If you want to obtain the 2's complement representation use `toBitVec`.
-/
@[inline] def Int16.toNat (i : Int16) : Nat := i.toInt.toNat
/-- Obtains the `Int16` whose 2's complement representation is the given `BitVec 16`. -/
@[inline] def Int16.ofBitVec (b : BitVec 16) : Int16 := ⟨⟨b⟩⟩
@[extern "lean_int16_to_int8"]
def Int16.toInt8 (a : Int16) : Int8 := ⟨⟨a.toBitVec.signExtend 8⟩⟩
@[extern "lean_int8_to_int16"]
Expand Down Expand Up @@ -289,6 +293,8 @@ This function has the same behavior as `Int.toNat` for negative numbers.
If you want to obtain the 2's complement representation use `toBitVec`.
-/
@[inline] def Int32.toNat (i : Int32) : Nat := i.toInt.toNat
/-- Obtains the `Int32` whose 2's complement representation is the given `BitVec 32`. -/
@[inline] def Int32.ofBitVec (b : BitVec 32) : Int32 := ⟨⟨b⟩⟩
@[extern "lean_int32_to_int8"]
def Int32.toInt8 (a : Int32) : Int8 := ⟨⟨a.toBitVec.signExtend 8⟩⟩
@[extern "lean_int32_to_int16"]
Expand Down Expand Up @@ -397,6 +403,8 @@ This function has the same behavior as `Int.toNat` for negative numbers.
If you want to obtain the 2's complement representation use `toBitVec`.
-/
@[inline] def Int64.toNat (i : Int64) : Nat := i.toInt.toNat
/-- Obtains the `Int64` whose 2's complement representation is the given `BitVec 64`. -/
@[inline] def Int64.ofBitVec (b : BitVec 64) : Int64 := ⟨⟨b⟩⟩
@[extern "lean_int64_to_int8"]
def Int64.toInt8 (a : Int64) : Int8 := ⟨⟨a.toBitVec.signExtend 8⟩⟩
@[extern "lean_int64_to_int16"]
Expand Down Expand Up @@ -509,6 +517,8 @@ This function has the same behavior as `Int.toNat` for negative numbers.
If you want to obtain the 2's complement representation use `toBitVec`.
-/
@[inline] def ISize.toNat (i : ISize) : Nat := i.toInt.toNat
/-- Obtains the `ISize` whose 2's complement representation is the given `BitVec`. -/
@[inline] def ISize.ofBitVec (b : BitVec System.Platform.numBits) : ISize := ⟨⟨b⟩⟩
@[extern "lean_isize_to_int32"]
def ISize.toInt32 (a : ISize) : Int32 := ⟨⟨a.toBitVec.signExtend 32⟩⟩
/--
Expand Down
10 changes: 5 additions & 5 deletions tests/lean/sint_basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -98,7 +98,7 @@ def test {α : Type} [BEq α] (w : Nat) (ofBitVec : BitVec w → α) (ofInt : In
return false
return true

#eval test 8 (⟨⟨·⟩⟩) Int8.ofInt Int8.ofNat
#eval test 8 Int8.ofBitVec Int8.ofInt Int8.ofNat

-- runtime representation
set_option trace.compiler.ir.result true in
Expand Down Expand Up @@ -179,7 +179,7 @@ def myId8 (x : Int8) : Int8 := x
#eval min (10 : Int16) (-1) = -1


#eval test 16 (⟨⟨·⟩⟩) Int16.ofInt Int16.ofNat
#eval test 16 Int16.ofBitVec Int16.ofInt Int16.ofNat

-- runtime representation
set_option trace.compiler.ir.result true in
Expand Down Expand Up @@ -261,7 +261,7 @@ def myId16 (x : Int16) : Int16 := x
#eval min (10 : Int32) (-1) = -1


#eval test 32 (⟨⟨·⟩⟩) Int32.ofInt Int32.ofNat
#eval test 32 Int32.ofBitVec Int32.ofInt Int32.ofNat

-- runtime representation
set_option trace.compiler.ir.result true in
Expand Down Expand Up @@ -342,7 +342,7 @@ def myId32 (x : Int32) : Int32 := x
#eval min (10 : Int64) (-1) = -1


#eval test 64 (⟨⟨·⟩⟩) Int64.ofInt Int64.ofNat
#eval test 64 Int64.ofBitVec Int64.ofInt Int64.ofNat

-- runtime representation
set_option trace.compiler.ir.result true in
Expand Down Expand Up @@ -424,7 +424,7 @@ def myId64 (x : Int64) : Int64 := x
#eval min (10 : ISize) (-1) = -1


#eval test System.Platform.numBits (⟨⟨·⟩⟩) ISize.ofInt ISize.ofNat
#eval test System.Platform.numBits ISize.ofBitVec ISize.ofInt ISize.ofNat

-- runtime representation
set_option trace.compiler.ir.result true in
Expand Down
Loading