max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/elab/float_conversions.lean
Garmelon 08eb78a5b2
chore: switch to new test/bench suite (#12590) 
This PR sets up the new integrated test/bench suite. It then migrates
all benchmarks and some related tests to the new suite. There's also
some documentation and some linting.

For now, a lot of the old tests are left alone so this PR doesn't become
even larger than it already is. Eventually, all tests should be migrated
to the new suite though so there isn't a confusing mix of two systems.
2026-02-25 13:51:53 +00:00

403 lines
16 KiB
Text
Raw Permalink Blame History

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
Reference in a new issue View git blame Copy permalink