From 5a8b4459c88cdbb18796498ee640d911a3d74c19 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Mon, 17 Feb 2025 16:42:10 +0100 Subject: [PATCH] feat: conversions between `Float` and finite integers (#7083) This PR adds (value-based, not bitfield-based) conversion functions between `Float`/`Float32` and `IntX`/`UIntX`. --- src/Init/Data/Float.lean | 15 + src/Init/Data/Float32.lean | 18 ++ src/Init/Data/SInt.lean | 2 + src/Init/Data/SInt/Float.lean | 71 +++++ src/Init/Data/SInt/Float32.lean | 74 +++++ src/include/lean/lean.h | 99 +++++++ tests/lean/run/float_conversions.lean | 403 ++++++++++++++++++++++++++ 7 files changed, 682 insertions(+) create mode 100644 src/Init/Data/SInt/Float.lean create mode 100644 src/Init/Data/SInt/Float32.lean create mode 100644 tests/lean/run/float_conversions.lean diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean index 65ee6eb7d5..859bd8334d 100644 --- a/src/Init/Data/Float.lean +++ b/src/Init/Data/Float.lean @@ -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 diff --git a/src/Init/Data/Float32.lean b/src/Init/Data/Float32.lean index 8fe74e527a..cb6fc924a2 100644 --- a/src/Init/Data/Float32.lean +++ b/src/Init/Data/Float32.lean @@ -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 diff --git a/src/Init/Data/SInt.lean b/src/Init/Data/SInt.lean index efbeb970b5..f9e16fb925 100644 --- a/src/Init/Data/SInt.lean +++ b/src/Init/Data/SInt.lean @@ -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. diff --git a/src/Init/Data/SInt/Float.lean b/src/Init/Data/SInt/Float.lean new file mode 100644 index 0000000000..ceaf19069e --- /dev/null +++ b/src/Init/Data/SInt/Float.lean @@ -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 diff --git a/src/Init/Data/SInt/Float32.lean b/src/Init/Data/SInt/Float32.lean new file mode 100644 index 0000000000..692115a44b --- /dev/null +++ b/src/Init/Data/SInt/Float32.lean @@ -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 diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index 472c0de61d..a9df85a259 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -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; } diff --git a/tests/lean/run/float_conversions.lean b/tests/lean/run/float_conversions.lean new file mode 100644 index 0000000000..528ec5db83 --- /dev/null +++ b/tests/lean/run/float_conversions.lean @@ -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