diff options
Diffstat (limited to 'test-suite/primitive/float/valid_binary_conv.v')
| -rw-r--r-- | test-suite/primitive/float/valid_binary_conv.v | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/test-suite/primitive/float/valid_binary_conv.v b/test-suite/primitive/float/valid_binary_conv.v new file mode 100644 index 0000000000..82e00b8532 --- /dev/null +++ b/test-suite/primitive/float/valid_binary_conv.v @@ -0,0 +1,46 @@ +Require Import ZArith Floats. + +Definition two := Eval compute in (one + one)%float. +Definition half := Eval compute in (one / two)%float. +Definition huge := Eval compute in ldexp one (1023)%Z. +Definition tiny := Eval compute in ldexp one (-1022)%Z. +Definition denorm := Eval compute in ldexp one (-1074)%Z. + +Check (eq_refl : valid_binary (Prim2SF zero) = true). +Check (eq_refl : valid_binary (Prim2SF neg_zero) = true). +Check (eq_refl : valid_binary (Prim2SF one) = true). +Check (eq_refl : valid_binary (Prim2SF (-one)) = true). +Check (eq_refl : valid_binary (Prim2SF infinity) = true). +Check (eq_refl : valid_binary (Prim2SF neg_infinity) = true). +Check (eq_refl : valid_binary (Prim2SF huge) = true). +Check (eq_refl : valid_binary (Prim2SF tiny) = true). +Check (eq_refl : valid_binary (Prim2SF denorm) = true). +Check (eq_refl : valid_binary (Prim2SF nan) = true). +Check (eq_refl : valid_binary (Prim2SF two) = true). +Check (eq_refl : valid_binary (Prim2SF half) = true). + +Check (eq_refl true <: valid_binary (Prim2SF zero) = true). +Check (eq_refl true <: valid_binary (Prim2SF neg_zero) = true). +Check (eq_refl true <: valid_binary (Prim2SF one) = true). +Check (eq_refl true <: valid_binary (Prim2SF (-one)) = true). +Check (eq_refl true <: valid_binary (Prim2SF infinity) = true). +Check (eq_refl true <: valid_binary (Prim2SF neg_infinity) = true). +Check (eq_refl true <: valid_binary (Prim2SF huge) = true). +Check (eq_refl true <: valid_binary (Prim2SF tiny) = true). +Check (eq_refl true <: valid_binary (Prim2SF denorm) = true). +Check (eq_refl true <: valid_binary (Prim2SF nan) = true). +Check (eq_refl true <: valid_binary (Prim2SF two) = true). +Check (eq_refl true <: valid_binary (Prim2SF half) = true). + +Check (eq_refl true <<: valid_binary (Prim2SF zero) = true). +Check (eq_refl true <<: valid_binary (Prim2SF neg_zero) = true). +Check (eq_refl true <<: valid_binary (Prim2SF one) = true). +Check (eq_refl true <<: valid_binary (Prim2SF (-one)) = true). +Check (eq_refl true <<: valid_binary (Prim2SF infinity) = true). +Check (eq_refl true <<: valid_binary (Prim2SF neg_infinity) = true). +Check (eq_refl true <<: valid_binary (Prim2SF huge) = true). +Check (eq_refl true <<: valid_binary (Prim2SF tiny) = true). +Check (eq_refl true <<: valid_binary (Prim2SF denorm) = true). +Check (eq_refl true <<: valid_binary (Prim2SF nan) = true). +Check (eq_refl true <<: valid_binary (Prim2SF two) = true). +Check (eq_refl true <<: valid_binary (Prim2SF half) = true). |