max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: conversions between Float and finite integers (#7083)

Browse source 
This PR adds (value-based, not bitfield-based) conversion functions
between `Float`/`Float32` and `IntX`/`UIntX`.
This commit is contained in:
Markus Himmel 2025-02-17 16:42:10 +01:00 • committed by GitHub
parent 3825c48405
commit 5a8b4459c8
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
7 changed files with 682 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Init/Data/Float.lean
View file

@ -134,7 +134,22 @@ Returns an undefined value if `x` is not finite.
instance : ToString Float where
toString := Float.toString
/-- Obtains the `Float` whose value is the same as the given `UInt8`. -/
@[extern "lean_uint8_to_float"] opaque UInt8.toFloat (n : UInt8) : Float
/-- Obtains the `Float` whose value is the same as the given `UInt16`. -/
@[extern "lean_uint16_to_float"] opaque UInt16.toFloat (n : UInt16) : Float
/-- Obtains the `Float` whose value is the same as the given `UInt32`. -/
@[extern "lean_uint32_to_float"] opaque UInt32.toFloat (n : UInt32) : Float
/-- Obtains a `Float` whose value is near the given `UInt64`. It will be exactly the value of the
given `UInt64` if such a `Float` exists. If no such `Float` exists, the returned value will either
be the smallest `Float` this is larger than the given value, or the largest `Float` this is smaller
than the given value. -/
@[extern "lean_uint64_to_float"] opaque UInt64.toFloat (n : UInt64) : Float
/-- Obtains a `Float` whose value is near the given `USize`. It will be exactly the value of the
given `USize` if such a `Float` exists. If no such `Float` exists, the returned value will either
be the smallest `Float` this is larger than the given value, or the largest `Float` this is smaller
than the given value. -/
@[extern "lean_usize_to_float"] opaque USize.toFloat (n : USize) : Float
instance : Inhabited Float where
default := UInt64.toFloat 0

18
src/Init/Data/Float32.lean
View file

@ -127,7 +127,25 @@ Returns an undefined value if `x` is not finite.
instance : ToString Float32 where
toString := Float32.toString
/-- Obtains the `Float32` whose value is the same as the given `UInt8`. -/
@[extern "lean_uint8_to_float32"] opaque UInt8.toFloat32 (n : UInt8) : Float32
/-- Obtains the `Float32` whose value is the same as the given `UInt16`. -/
@[extern "lean_uint16_to_float32"] opaque UInt16.toFloat32 (n : UInt16) : Float32
/-- Obtains a `Float32` whose value is near the given `UInt32`. It will be exactly the value of the
given `UInt32` if such a `Float32` exists. If no such `Float32` exists, the returned value will either
be the smallest `Float32` this is larger than the given value, or the largest `Float32` this is smaller
than the given value. -/
@[extern "lean_uint32_to_float32"] opaque UInt32.toFloat32 (n : UInt32) : Float32
/-- Obtains a `Float32` whose value is near the given `UInt64`. It will be exactly the value of the
given `UInt64` if such a `Float32` exists. If no such `Float32` exists, the returned value will either
be the smallest `Float32` this is larger than the given value, or the largest `Float32` this is smaller
than the given value. -/
@[extern "lean_uint64_to_float32"] opaque UInt64.toFloat32 (n : UInt64) : Float32
/-- Obtains a `Float32` whose value is near the given `USize`. It will be exactly the value of the
given `USize` if such a `Float32` exists. If no such `Float32` exists, the returned value will either
be the smallest `Float32` this is larger than the given value, or the largest `Float32` this is smaller
than the given value. -/
@[extern "lean_usize_to_float32"] opaque USize.toFloat32 (n : USize) : Float32
instance : Inhabited Float32 where
default := UInt64.toFloat32 0

2
src/Init/Data/SInt.lean
View file

@ -5,6 +5,8 @@ Authors: Henrik Böving
-/
prelude
import Init.Data.SInt.Basic
import Init.Data.SInt.Float
import Init.Data.SInt.Float32
/-!
This module contains the definitions and basic theory about signed fixed width integer types.

71
src/Init/Data/SInt/Float.lean Normal file
View file

@ -0,0 +1,71 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
prelude
import Init.Data.Float
import Init.Data.SInt.Basic
/--
Truncates the value to the nearest integer, rounding towards zero.
If NaN, returns `0`.
If larger than the maximum value for `Int8` (including Inf), returns the maximum value of `Int8`
(i.e. `Int8.maxValue`).
If smaller than the minimum value for `Int8` (including -Inf), returns the minimum value of `Int8`
(i.e. `Int8.minValue`).
-/
@[extern "lean_float_to_int8"] opaque Float.toInt8 : Float → Int8
/--
Truncates the value to the nearest integer, rounding towards zero.
If NaN, returns `0`.
If larger than the maximum value for `Int16` (including Inf), returns the maximum value of `Int16`
(i.e. `Int16.maxValue`).
If smaller than the minimum value for `Int16` (including -Inf), returns the minimum value of `Int16`
(i.e. `Int16.minValue`).
-/
@[extern "lean_float_to_int16"] opaque Float.toInt16 : Float → Int16
/--
Truncates the value to the nearest integer, rounding towards zero.
If NaN, returns `0`.
If larger than the maximum value for `Int32` (including Inf), returns the maximum value of `Int32`
(i.e. `Int32.maxValue`).
If smaller than the minimum value for `Int32` (including -Inf), returns the minimum value of `Int32`
(i.e. `Int32.minValue`).
-/
@[extern "lean_float_to_int32"] opaque Float.toInt32 : Float → Int32
/--
Truncates the value to the nearest integer, rounding towards zero.
If NaN, returns `0`.
If larger than the maximum value for `Int64` (including Inf), returns the maximum value of `Int64`
(i.e. `Int64.maxValue`).
If smaller than the minimum value for `Int64` (including -Inf), returns the minimum value of `Int64`
(i.e. `Int64.minValue`).
-/
@[extern "lean_float_to_int64"] opaque Float.toInt64 : Float → Int64
/--
Truncates the value to the nearest integer, rounding towards zero.
If NaN, returns `0`.
If larger than the maximum value for `ISize` (including Inf), returns the maximum value of `ISize`
(i.e. `ISize.maxValue`).
If smaller than the minimum value for `ISize` (including -Inf), returns the minimum value of `ISize`
(i.e. `ISize.minValue`).
-/
@[extern "lean_float_to_isize"] opaque Float.toISize : Float → ISize
/-- Obtains the `Float` whose value is the same as the given `Int8`. -/
@[extern "lean_int8_to_float"] opaque Int8.toFloat (n : Int8) : Float
/-- Obtains the `Float` whose value is the same as the given `Int16`. -/
@[extern "lean_int16_to_float"] opaque Int16.toFloat (n : Int16) : Float
/-- Obtains the `Float` whose value is the same as the given `Int32`. -/
@[extern "lean_int32_to_float"] opaque Int32.toFloat (n : Int32) : Float
/-- Obtains a `Float` whose value is near the given `Int64`. It will be exactly the value of the
given `Int64` if such a `Float` exists. If no such `Float` exists, the returned value will either
be the smallest `Float` this is larger than the given value, or the largest `Float` this is smaller
than the given value. -/
@[extern "lean_int64_to_float"] opaque Int64.toFloat (n : Int64) : Float
/-- Obtains a `Float` whose value is near the given `ISize`. It will be exactly the value of the
given `ISize` if such a `Float` exists. If no such `Float` exists, the returned value will either
be the smallest `Float` this is larger than the given value, or the largest `Float` this is smaller
than the given value. -/
@[extern "lean_isize_to_float"] opaque ISize.toFloat (n : ISize) : Float

74
src/Init/Data/SInt/Float32.lean Normal file
View file

@ -0,0 +1,74 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
prelude
import Init.Data.Float32
import Init.Data.SInt.Basic
/--
Truncates the value to the nearest integer, rounding towards zero.
If NaN, returns `0`.
If larger than the maximum value for `Int8` (including Inf), returns the maximum value of `Int8`
(i.e. `Int8.maxValue`).
If smaller than the minimum value for `Int8` (including -Inf), returns the minimum value of `Int8`
(i.e. `Int8.minValue`).
-/
@[extern "lean_float32_to_int8"] opaque Float32.toInt8 : Float32 → Int8
/--
Truncates the value to the nearest integer, rounding towards zero.
If NaN, returns `0`.
If larger than the maximum value for `Int16` (including Inf), returns the maximum value of `Int16`
(i.e. `Int16.maxValue`).
If smaller than the minimum value for `Int16` (including -Inf), returns the minimum value of `Int16`
(i.e. `Int16.minValue`).
-/
@[extern "lean_float32_to_int16"] opaque Float32.toInt16 : Float32 → Int16
/--
Truncates the value to the nearest integer, rounding towards zero.
If NaN, returns `0`.
If larger than the maximum value for `Int32` (including Inf), returns the maximum value of `Int32`
(i.e. `Int32.maxValue`).
If smaller than the minimum value for `Int32` (including -Inf), returns the minimum value of `Int32`
(i.e. `Int32.minValue`).
-/
@[extern "lean_float32_to_int32"] opaque Float32.toInt32 : Float32 → Int32
/--
Truncates the value to the nearest integer, rounding towards zero.
If NaN, returns `0`.
If larger than the maximum value for `Int64` (including Inf), returns the maximum value of `Int64`
(i.e. `Int64.maxValue`).
If smaller than the minimum value for `Int64` (including -Inf), returns the minimum value of `Int64`
(i.e. `Int64.minValue`).
-/
@[extern "lean_float32_to_int64"] opaque Float32.toInt64 : Float32 → Int64
/--
Truncates the value to the nearest integer, rounding towards zero.
If NaN, returns `0`.
If larger than the maximum value for `ISize` (including Inf), returns the maximum value of `ISize`
(i.e. `ISize.maxValue`).
If smaller than the minimum value for `ISize` (including -Inf), returns the minimum value of `ISize`
(i.e. `ISize.minValue`).
-/
@[extern "lean_float32_to_isize"] opaque Float32.toISize : Float32 → ISize
/-- Obtains the `Float32` whose value is the same as the given `Int8`. -/
@[extern "lean_int8_to_float32"] opaque Int8.toFloat32 (n : Int8) : Float32
/-- Obtains the `Float32` whose value is the same as the given `Int16`. -/
@[extern "lean_int16_to_float32"] opaque Int16.toFloat32 (n : Int16) : Float32
/-- Obtains a `Float32` whose value is near the given `Int32`. It will be exactly the value of the
given `Int32` if such a `Float32` exists. If no such `Float32` exists, the returned value will either
be the smallest `Float32` this is larger than the given value, or the largest `Float32` this is smaller
than the given value. -/
@[extern "lean_int32_to_float32"] opaque Int32.toFloat32 (n : Int32) : Float32
/-- Obtains a `Float32` whose value is near the given `Int64`. It will be exactly the value of the
given `Int64` if such a `Float32` exists. If no such `Float32` exists, the returned value will either
be the smallest `Float32` this is larger than the given value, or the largest `Float32` this is smaller
than the given value. -/
@[extern "lean_int64_to_float32"] opaque Int64.toFloat32 (n : Int64) : Float32
/-- Obtains a `Float32` whose value is near the given `ISize`. It will be exactly the value of the
given `ISize` if such a `Float32` exists. If no such `Float32` exists, the returned value will either
be the smallest `Float32` this is larger than the given value, or the largest `Float32` this is smaller
than the given value. -/
@[extern "lean_isize_to_float32"] opaque ISize.toFloat32 (n : ISize) : Float32

99
src/include/lean/lean.h
View file

@ -2746,6 +2746,13 @@ static inline uint64_t lean_name_hash(b_lean_obj_arg n) {
}
/* float primitives */
// Here is how casting a float to an integral type works according to the standard:
// * Separate the float into integral parts and fractional parts. The fractional part
// has the same sign as the float, so the integral part is the result of rounding the
// float towards zero.
// * If the integral part fits into the target type, that is the result of the cast.
// * Otherwise, the result is undefined behavior.
static inline uint8_t lean_float_to_uint8(double a) {
return 0. <= a ? (a < 256. ? (uint8_t)a : UINT8_MAX) : 0;
}
@ -2764,6 +2771,43 @@ static inline size_t lean_float_to_usize(double a) {
else
return (size_t) lean_float_to_uint32(a); // NOLINT
}
static inline uint8_t lean_float_to_int8(double a) {
int8_t result;
if (lean_float_isnan(a)) result = 0;
else result = -129. < a ? (a < 128. ? (int8_t)a : INT8_MAX) : INT8_MIN;
return (uint8_t)result;
}
static inline uint16_t lean_float_to_int16(double a) {
int16_t result;
if (lean_float_isnan(a)) result = 0;
else result = -32769. < a ? (a < 32768. ? (int16_t)a : INT16_MAX) : INT16_MIN;
return (uint16_t)result;
}
static inline uint32_t lean_float_to_int32(double a) {
int32_t result;
if (lean_float_isnan(a)) result = 0;
else result = -2147483649. < a ? (a < 2147483648. ? (int32_t)a : INT32_MAX) : INT32_MIN;
return (uint32_t)result;
}
static inline uint64_t lean_float_to_int64(double a) {
int64_t result;
if (lean_float_isnan(a)) result = 0;
else result = -9223372036854775809. < a ? (a < 9223372036854775808. ? (int64_t)a : INT64_MAX) : INT64_MIN;
return (uint64_t)result;
}
static inline size_t lean_float_to_isize(double a) {
if (sizeof(size_t) == sizeof(uint64_t)) {
ptrdiff_t result;
if (lean_float_isnan(a)) result = 0;
else result = -9223372036854775809. < a ? (a < 9223372036854775808. ? (ptrdiff_t)a : INT64_MAX) : INT64_MIN;
return (size_t)result;
} else {
ptrdiff_t result;
if (lean_float_isnan(a)) result = 0;
else result = -2147483649. < a ? (a < 2147483648. ? (ptrdiff_t)a : INT32_MAX) : INT32_MIN;
return (size_t)result;
}
}
LEAN_EXPORT double lean_float_of_bits(uint64_t u);
LEAN_EXPORT uint64_t lean_float_to_bits(double d);
static inline double lean_float_add(double a, double b) { return a + b; }
@ -2774,7 +2818,16 @@ static inline double lean_float_negate(double a) { return -a; }
static inline uint8_t lean_float_beq(double a, double b) { return a == b; }
static inline uint8_t lean_float_decLe(double a, double b) { return a <= b; }
static inline uint8_t lean_float_decLt(double a, double b) { return a < b; }
static inline double lean_uint8_to_float(uint8_t a) { return (double) a; }
static inline double lean_uint16_to_float(uint16_t a) { return (double) a; }
static inline double lean_uint32_to_float(uint32_t a) { return (double) a; }
static inline double lean_uint64_to_float(uint64_t a) { return (double) a; }
static inline double lean_usize_to_float(size_t a) { return (double) a; }
static inline double lean_int8_to_float(uint8_t a) { return (double)(int8_t) a; }
static inline double lean_int16_to_float(uint16_t a) { return (double)(int16_t) a; }
static inline double lean_int32_to_float(uint32_t a) { return (double)(int32_t) a; }
static inline double lean_int64_to_float(uint64_t a) { return (double)(int64_t) a; }
static inline double lean_isize_to_float(size_t a) { return (double)(ptrdiff_t) a; }
/* float32 primitives */
static inline uint8_t lean_float32_to_uint8(float a) {
@ -2795,6 +2848,43 @@ static inline size_t lean_float32_to_usize(float a) {
else
return (size_t) lean_float32_to_uint32(a); // NOLINT
}
static inline uint8_t lean_float32_to_int8(float a) {
int8_t result;
if (lean_float32_isnan(a)) result = 0;
else result = -129. < a ? (a < 128. ? (int8_t)a : INT8_MAX) : INT8_MIN;
return (uint8_t)result;
}
static inline uint16_t lean_float32_to_int16(float a) {
int16_t result;
if (lean_float32_isnan(a)) result = 0;
else result = -32769. < a ? (a < 32768. ? (int16_t)a : INT16_MAX) : INT16_MIN;
return (uint16_t)result;
}
static inline uint32_t lean_float32_to_int32(float a) {
int32_t result;
if (lean_float32_isnan(a)) result = 0;
else result = -2147483649. < a ? (a < 2147483648. ? (int32_t)a : INT32_MAX) : INT32_MIN;
return (uint32_t)result;
}
static inline uint64_t lean_float32_to_int64(float a) {
int64_t result;
if (lean_float32_isnan(a)) result = 0;
else result = -9223372036854775809. < a ? (a < 9223372036854775808. ? (int64_t)a : INT64_MAX) : INT64_MIN;
return (uint64_t)result;
}
static inline size_t lean_float32_to_isize(float a) {
if (sizeof(size_t) == sizeof(uint64_t)) {
ptrdiff_t result;
if (lean_float32_isnan(a)) result = 0;
else result = -9223372036854775809. < a ? (a < 9223372036854775808. ? (ptrdiff_t)a : INT64_MAX) : INT64_MIN;
return (size_t)result;
} else {
ptrdiff_t result;
if (lean_float32_isnan(a)) result = 0;
else result = -2147483649. < a ? (a < 2147483648. ? (ptrdiff_t)a : INT32_MAX) : INT32_MIN;
return (size_t)result;
}
}
LEAN_EXPORT float lean_float32_of_bits(uint32_t u);
LEAN_EXPORT uint32_t lean_float32_to_bits(float d);
static inline float lean_float32_add(float a, float b) { return a + b; }
@ -2805,7 +2895,16 @@ static inline float lean_float32_negate(float a) { return -a; }
static inline uint8_t lean_float32_beq(float a, float b) { return a == b; }
static inline uint8_t lean_float32_decLe(float a, float b) { return a <= b; }
static inline uint8_t lean_float32_decLt(float a, float b) { return a < b; }
static inline float lean_uint8_to_float32(uint8_t a) { return (float) a; }
static inline float lean_uint16_to_float32(uint16_t a) { return (float) a; }
static inline float lean_uint32_to_float32(uint32_t a) { return (float) a; }
static inline float lean_uint64_to_float32(uint64_t a) { return (float) a; }
static inline float lean_usize_to_float32(size_t a) { return (float) a; }
static inline float lean_int8_to_float32(uint8_t a) { return (float)(int8_t) a; }
static inline float lean_int16_to_float32(uint16_t a) { return (float)(int16_t) a; }
static inline float lean_int32_to_float32(uint32_t a) { return (float)(int32_t) a; }
static inline float lean_int64_to_float32(uint64_t a) { return (float)(int64_t) a; }
static inline float lean_isize_to_float32(size_t a) { return (float)(ptrdiff_t) a; }
static inline float lean_float_to_float32(double a) { return (float)a; }
static inline double lean_float32_to_float(float a) { return (double)a; }

403
tests/lean/run/float_conversions.lean Normal file
View file

@ -0,0 +1,403 @@
def check (b : Bool) : IO Unit :=
unless b do
throw $ IO.userError "check failed"
-- Float -> UIntX
def testFloatToUIntX : IO Unit := do
check <| (1/0 : Float).toUInt8 == 255
check <| (0/0 : Float).toUInt8 == 0
check <| (-1/0 : Float).toUInt8 == 0
check <| (-600 : Float).toUInt8 == 0
check <| (-200 : Float).toUInt8 == 0
check <| (200 : Float).toUInt8 == 200
check <| (255 : Float).toUInt8 == 255
check <| (256 : Float).toUInt8 == 255
check <| (600 : Float).toUInt8 == 255
check <| (1/0 : Float).toUInt16 == 65535
check <| (0/0 : Float).toUInt16 == 0
check <| (-1/0 : Float).toUInt16 == 0
check <| (-600000 : Float).toUInt16 == 0
check <| (-60000 : Float).toUInt16 == 0
check <| (60000 : Float).toUInt16 == 60000
check <| (65535 : Float).toUInt16 == 65535
check <| (65536 : Float).toUInt16 == 65535
check <| (600000 : Float).toUInt16 == 65535
check <| (1/0 : Float).toUInt32 == 4294967295
check <| (0/0 : Float).toUInt32 == 0
check <| (-1/0 : Float).toUInt32 == 0
check <| (-4000000000 : Float).toUInt32 == 0
check <| (-40000000000 : Float).toUInt32 == 0
check <| (4000000000 : Float).toUInt32 == 4000000000
check <| (4294967295 : Float).toUInt32 == 4294967295
check <| (4294967296 : Float).toUInt32 == 4294967295
check <| (40000000000 : Float).toUInt32 == 4294967295
check <| (1/0 : Float).toUInt64 == 18446744073709551615
check <| (0/0 : Float).toUInt64 == 0
check <| (-1/0 : Float).toUInt64 == 0
check <| (-4000000000 : Float).toUInt64 == 0
check <| (-40000000000 : Float).toUInt64 == 0
check <| (10000000000000000000 : Float).toUInt64 == 10000000000000000000
check <| (18446744073709551615 : Float).toUInt64 == 18446744073709551615
check <| (18446744073709551616 : Float).toUInt64 == 18446744073709551615
check <| (100000000000000000000 : Float).toUInt64 == 18446744073709551615
check <| (1/0 : Float).toUSize == 4294967295 || (1/0 : Float).toUSize == 18446744073709551615
check <| (0/0 : Float).toUSize == 0
check <| (-1/0 : Float).toUSize == 0
check <| (-4000000000 : Float).toUSize == 0
check <| (-40000000000 : Float).toUSize == 0
check <| (4000000000 : Float).toUSize == 4000000000
check <| (4294967295 : Float).toUSize == 4294967295
check <| (4294967296 : Float).toUSize == 4294967295 || (4294967296 : Float).toUSize == 4294967296
check <| (40000000000 : Float).toUSize == 4294967295 || (40000000000 : Float).toUSize == 40000000000
return ()
#guard_msgs in
#eval testFloatToUIntX
-- Float32 -> UIntX
def testFloat32ToUIntX : IO Unit := do
check <| (1/0 : Float32).toUInt8 == 255
check <| (0/0 : Float32).toUInt8 == 0
check <| (-1/0 : Float32).toUInt8 == 0
check <| (-600 : Float32).toUInt8 == 0
check <| (-200 : Float32).toUInt8 == 0
check <| (200 : Float32).toUInt8 == 200
check <| (255 : Float32).toUInt8 == 255
check <| (256 : Float32).toUInt8 == 255
check <| (600 : Float32).toUInt8 == 255
check <| (1/0 : Float32).toUInt16 == 65535
check <| (0/0 : Float32).toUInt16 == 0
check <| (-1/0 : Float32).toUInt16 == 0
check <| (-600000 : Float32).toUInt16 == 0
check <| (-60000 : Float32).toUInt16 == 0
check <| (60000 : Float32).toUInt16 == 60000
check <| (65535 : Float32).toUInt16 == 65535
check <| (65536 : Float32).toUInt16 == 65535
check <| (600000 : Float32).toUInt16 == 65535
check <| (1/0 : Float32).toUInt32 == 4294967295
check <| (0/0 : Float32).toUInt32 == 0
check <| (-1/0 : Float32).toUInt32 == 0
check <| (-4000000000 : Float32).toUInt32 == 0
check <| (-40000000000 : Float32).toUInt32 == 0
check <| (4000000000 : Float32).toUInt32 == 4000000000
check <| (4294967295 : Float32).toUInt32 == 4294967295
check <| (4294967296 : Float32).toUInt32 == 4294967295
check <| (40000000000 : Float32).toUInt32 == 4294967295
check <| (1/0 : Float32).toUInt64 == 18446744073709551615
check <| (0/0 : Float32).toUInt64 == 0
check <| (-1/0 : Float32).toUInt64 == 0
check <| (-4000000000 : Float32).toUInt64 == 0
check <| (-40000000000 : Float32).toUInt64 == 0
check <| (10000000000000000000 : Float32).toUInt64 == 9999999980506447872 -- imprecision
check <| (18446744073709551615 : Float32).toUInt64 == 18446744073709551615
check <| (18446744073709551616 : Float32).toUInt64 == 18446744073709551615
check <| (100000000000000000000 : Float32).toUInt64 == 18446744073709551615
check <| (1/0 : Float32).toUSize == 4294967295 || (1/0 : Float32).toUSize == 18446744073709551615
check <| (0/0 : Float32).toUSize == 0
check <| (-1/0 : Float32).toUSize == 0
check <| (-4000000000 : Float32).toUSize == 0
check <| (-40000000000 : Float32).toUSize == 0
check <| (4000000000 : Float32).toUSize == 4000000000
check <| (4294967295 : Float32).toUSize == 4294967295 || (4294967295 : Float32).toUSize == 4294967296 -- imprecision
check <| (4294967296 : Float32).toUSize == 4294967295 || (4294967296 : Float32).toUSize == 4294967296
check <| (40000000000 : Float32).toUSize == 4294967295 || (40000000000 : Float32).toUSize == 40000000000
return ()
#guard_msgs in
#eval testFloat32ToUIntX
-- Float -> IntX
def testFloatToIntX : IO Unit := do
check <| (1/0 : Float).toInt8 == 127
check <| (0/0 : Float).toInt8 == 0
check <| (-1/0 : Float).toInt8 == -128
check <| (-600 : Float).toInt8 == -128
check <| (-129 : Float).toInt8 == -128
check <| (-128 : Float).toInt8 == -128
check <| (-127 : Float).toInt8 == -127
check <| (-100 : Float).toInt8 == -100
check <| (100 : Float).toInt8 == 100
check <| (127 : Float).toInt8 == 127
check <| (128 : Float).toInt8 == 127
check <| (600 : Float).toInt8 == 127
check <| (1/0 : Float).toInt16 == 32767
check <| (0/0 : Float).toInt16 == 0
check <| (-1/0 : Float).toInt16 == -32768
check <| (-600000 : Float).toInt16 == -32768
check <| (-32769 : Float).toInt16 == -32768
check <| (-32768 : Float).toInt16 == -32768
check <| (-32767 : Float).toInt16 == -32767
check <| (30000 : Float).toInt16 == 30000
check <| (32767 : Float).toInt16 == 32767
check <| (32768 : Float).toInt16 == 32767
check <| (600000 : Float).toInt16 == 32767
check <| (1/0 : Float).toInt32 == 2147483647
check <| (0/0 : Float).toInt32 == 0
check <| (-1/0 : Float).toInt32 == -2147483648
check <| (-40000000000 : Float).toInt32 == -2147483648
check <| (-2147483649 : Float).toInt32 == -2147483648
check <| (-2147483648 : Float).toInt32 == -2147483648
check <| (-2147483647 : Float).toInt32 == -2147483647
check <| (-2000000000 : Float).toInt32 == -2000000000
check <| (2000000000 : Float).toInt32 == 2000000000
check <| (2147483647 : Float).toInt32 == 2147483647
check <| (2147483648 : Float).toInt32 == 2147483647
check <| (40000000000 : Float).toInt32 == 2147483647
check <| (1/0 : Float).toInt64 == 9223372036854775807
check <| (0/0 : Float).toInt64 == 0
check <| (-1/0 : Float).toInt64 == -9223372036854775808
check <| (-10000000000000000000 : Float).toInt64 == -9223372036854775808
check <| (-9223372036854775808 : Float).toInt64 == -9223372036854775808
check <| (-2000000000 : Float).toInt64 == -2000000000
check <| (2000000000 : Float).toInt64 == 2000000000
check <| (9223372036854775808 : Float).toInt64 == 9223372036854775807
check <| (10000000000000000000 : Float).toInt64 == 9223372036854775807
check <| (1/0 : Float).toISize == 2147483647 || (1/0 : Float).toISize == 9223372036854775807
check <| (0/0 : Float).toISize == 0
check <| (-1/0 : Float).toISize == -2147483648 || (-1/0 : Float).toISize = -9223372036854775808
check <| (-2000000000 : Float).toISize == -2000000000
check <| (4000000000 : Float).toISize == 4000000000
check <| (2147483647 : Float).toISize == 2147483647
check <| (2147483648 : Float).toISize == 2147483647 || (2147483648 : Float).toISize == 2147483648
check <| (20000000000 : Float).toISize == 2147483647 || (20000000000 : Float).toISize == 20000000000
return ()
#guard_msgs in
#eval testFloatToIntX
-- Float32 -> IntX
def testFloat32ToIntX : IO Unit := do
check <| (1/0 : Float32).toInt8 == 127
check <| (0/0 : Float32).toInt8 == 0
check <| (-1/0 : Float32).toInt8 == -128
check <| (-600 : Float32).toInt8 == -128
check <| (-129 : Float32).toInt8 == -128
check <| (-128 : Float32).toInt8 == -128
check <| (-127 : Float32).toInt8 == -127
check <| (-100 : Float32).toInt8 == -100
check <| (100 : Float32).toInt8 == 100
check <| (127 : Float32).toInt8 == 127
check <| (128 : Float32).toInt8 == 127
check <| (600 : Float32).toInt8 == 127
check <| (1/0 : Float32).toInt16 == 32767
check <| (0/0 : Float32).toInt16 == 0
check <| (-1/0 : Float32).toInt16 == -32768
check <| (-600000 : Float32).toInt16 == -32768
check <| (-32769 : Float32).toInt16 == -32768
check <| (-32768 : Float32).toInt16 == -32768
check <| (-32767 : Float32).toInt16 == -32767
check <| (30000 : Float32).toInt16 == 30000
check <| (32767 : Float32).toInt16 == 32767
check <| (32768 : Float32).toInt16 == 32767
check <| (600000 : Float32).toInt16 == 32767
check <| (1/0 : Float32).toInt32 == 2147483647
check <| (0/0 : Float32).toInt32 == 0
check <| (-1/0 : Float32).toInt32 == -2147483648
check <| (-40000000000 : Float32).toInt32 == -2147483648
check <| (-2147483649 : Float32).toInt32 == -2147483648
check <| (-2147483648 : Float32).toInt32 == -2147483648
check <| (-2147483647 : Float32).toInt32 == -2147483648 -- imprecision
check <| (-2000000000 : Float32).toInt32 == -2000000000
check <| (2000000000 : Float32).toInt32 == 2000000000
check <| (2147483647 : Float32).toInt32 == 2147483647
check <| (2147483648 : Float32).toInt32 == 2147483647
check <| (40000000000 : Float32).toInt32 == 2147483647
check <| (1/0 : Float32).toInt64 == 9223372036854775807
check <| (0/0 : Float32).toInt64 == 0
check <| (-1/0 : Float32).toInt64 == -9223372036854775808
check <| (-10000000000000000000 : Float32).toInt64 == -9223372036854775808
check <| (-9223372036854775808 : Float32).toInt64 == -9223372036854775808
check <| (-2000000000 : Float32).toInt64 == -2000000000
check <| (2000000000 : Float32).toInt64 == 2000000000
check <| (9223372036854775808 : Float32).toInt64 == 9223372036854775807
check <| (10000000000000000000 : Float32).toInt64 == 9223372036854775807
check <| (1/0 : Float32).toISize == 2147483647 || (1/0 : Float32).toISize == 9223372036854775807
check <| (0/0 : Float32).toISize == 0
check <| (-1/0 : Float32).toISize == -2147483648 || (-1/0 : Float32).toISize = -9223372036854775808
check <| (-2000000000 : Float32).toISize == -2000000000
check <| (4000000000 : Float32).toISize == 4000000000
check <| (2147483647 : Float32).toISize == 2147483648 -- imprecision
check <| (2147483648 : Float32).toISize == 2147483647 || (2147483648 : Float32).toISize == 2147483648
check <| (20000000000 : Float32).toISize == 2147483647 || (20000000000 : Float32).toISize == 20000000000
return ()
#guard_msgs in
#eval testFloat32ToIntX
-- UIntX -> Float
def testUIntXToFloat : IO Unit := do
check <| (0 : UInt8).toFloat == 0
check <| (1 : UInt8).toFloat == 1
check <| (254 : UInt8).toFloat == 254
check <| (255 : UInt8).toFloat == 255
check <| (0 : UInt16).toFloat == 0
check <| (1 : UInt16).toFloat == 1
check <| (65534 : UInt16).toFloat == 65534
check <| (65535 : UInt16).toFloat == 65535
check <| (0 : UInt32).toFloat == 0
check <| (1 : UInt32).toFloat == 1
check <| (4294967294 : UInt32).toFloat == 4294967294
check <| (4294967295 : UInt32).toFloat == 4294967295
check <| (0 : UInt64).toFloat == 0
check <| (1 : UInt64).toFloat == 1
check <| (18446744073709551614 : UInt64).toFloat == 18446744073709551614
check <| (18446744073709551615 : UInt64).toFloat == 18446744073709551615
check <| (0 : USize).toFloat == 0
check <| (1 : USize).toFloat == 1
check <| (4294967294 : USize).toFloat == 4294967294
check <| (4294967295 : USize).toFloat == 4294967295
return ()
#guard_msgs in
#eval testUIntXToFloat
-- UIntX -> Float32
def testUIntXToFloat32 : IO Unit := do
check <| (0 : UInt8).toFloat32 == 0
check <| (1 : UInt8).toFloat32 == 1
check <| (254 : UInt8).toFloat32 == 254
check <| (255 : UInt8).toFloat32 == 255
check <| (0 : UInt16).toFloat32 == 0
check <| (1 : UInt16).toFloat32 == 1
check <| (65534 : UInt16).toFloat32 == 65534
check <| (65535 : UInt16).toFloat32 == 65535
check <| (0 : UInt32).toFloat32 == 0
check <| (1 : UInt32).toFloat32 == 1
check <| (4294967294 : UInt32).toFloat32 == 4294967294
check <| (4294967295 : UInt32).toFloat32 == 4294967295
check <| (0 : UInt64).toFloat32 == 0
check <| (1 : UInt64).toFloat32 == 1
check <| (18446744073709551614 : UInt64).toFloat32 == 18446744073709551614
check <| (18446744073709551615 : UInt64).toFloat32 == 18446744073709551615
check <| (0 : USize).toFloat32 == 0
check <| (1 : USize).toFloat32 == 1
check <| (4294967294 : USize).toFloat32 == 4294967294
check <| (4294967295 : USize).toFloat32 == 4294967295
return ()
#guard_msgs in
#eval testUIntXToFloat32
-- IntX -> Float
def testIntXToFloat : IO Unit := do
check <| (-128 : Int8).toFloat == -128
check <| (-127 : Int8).toFloat == -127
check <| (-1 : Int8).toFloat == -1
check <| (0 : Int8).toFloat == 0
check <| (1 : Int8).toFloat == 1
check <| (126 : Int8).toFloat == 126
check <| (127 : Int8).toFloat == 127
check <| (-32768 : Int16).toFloat == -32768
check <| (-32767 : Int16).toFloat == -32767
check <| (-1 : Int16).toFloat == -1
check <| (0 : Int16).toFloat == 0
check <| (1 : Int16).toFloat == 1
check <| (32766 : Int16).toFloat == 32766
check <| (32767 : Int16).toFloat == 32767
check <| (-2147483648 : Int32).toFloat == -2147483648
check <| (-2147483647 : Int32).toFloat == -2147483647
check <| (-1 : Int32).toFloat == -1
check <| (0 : Int32).toFloat == 0
check <| (1 : Int32).toFloat == 1
check <| (2147483646 : Int32).toFloat == 2147483646
check <| (2147483647 : Int32).toFloat == 2147483647
check <| (-9223372036854775808 : Int64).toFloat == -9223372036854775808
check <| (-9223372036854775807 : Int64).toFloat == -9223372036854775807
check <| (-1 : Int64).toFloat == -1
check <| (0 : Int64).toFloat == 0
check <| (1 : Int64).toFloat == 1
check <| (9223372036854775806 : Int64).toFloat == 9223372036854775806
check <| (9223372036854775807 : Int64).toFloat == 9223372036854775807
check <| (-2147483648 : ISize).toFloat == -2147483648
check <| (-2147483647 : ISize).toFloat == -2147483647
check <| (-1 : ISize).toFloat == -1
check <| (0 : ISize).toFloat == 0
check <| (1 : ISize).toFloat == 1
check <| (2147483646 : ISize).toFloat == 2147483646
check <| (2147483647 : ISize).toFloat == 2147483647
return ()
#guard_msgs in
#eval testIntXToFloat
-- IntX -> Float32
def testIntXToFloat32 : IO Unit := do
check <| (-128 : Int8).toFloat32 == -128
check <| (-127 : Int8).toFloat32 == -127
check <| (-1 : Int8).toFloat32 == -1
check <| (0 : Int8).toFloat32 == 0
check <| (1 : Int8).toFloat32 == 1
check <| (126 : Int8).toFloat32 == 126
check <| (127 : Int8).toFloat32 == 127
check <| (-32768 : Int16).toFloat32 == -32768
check <| (-32767 : Int16).toFloat32 == -32767
check <| (-1 : Int16).toFloat32 == -1
check <| (0 : Int16).toFloat32 == 0
check <| (1 : Int16).toFloat32 == 1
check <| (32766 : Int16).toFloat32 == 32766
check <| (32767 : Int16).toFloat32 == 32767
check <| (-2147483648 : Int32).toFloat32 == -2147483648
check <| (-2147483647 : Int32).toFloat32 == -2147483647
check <| (-1 : Int32).toFloat32 == -1
check <| (0 : Int32).toFloat32 == 0
check <| (1 : Int32).toFloat32 == 1
check <| (2147483646 : Int32).toFloat32 == 2147483646
check <| (2147483647 : Int32).toFloat32 == 2147483647
check <| (-9223372036854775808 : Int64).toFloat32 == -9223372036854775808
check <| (-9223372036854775807 : Int64).toFloat32 == -9223372036854775807
check <| (-1 : Int64).toFloat32 == -1
check <| (0 : Int64).toFloat32 == 0
check <| (1 : Int64).toFloat32 == 1
check <| (9223372036854775806 : Int64).toFloat32 == 9223372036854775806
check <| (9223372036854775807 : Int64).toFloat32 == 9223372036854775807
check <| (-2147483648 : ISize).toFloat32 == -2147483648
check <| (-2147483647 : ISize).toFloat32 == -2147483647
check <| (-1 : ISize).toFloat32 == -1
check <| (0 : ISize).toFloat32 == 0
check <| (1 : ISize).toFloat32 == 1
check <| (2147483646 : ISize).toFloat32 == 2147483646
check <| (2147483647 : ISize).toFloat32 == 2147483647
return ()
#guard_msgs in
#eval testIntXToFloat32