diff options
Diffstat (limited to 'test-suite/primitive/float')
| -rw-r--r-- | test-suite/primitive/float/add.v | 63 | ||||
| -rw-r--r-- | test-suite/primitive/float/classify.v | 33 | ||||
| -rw-r--r-- | test-suite/primitive/float/compare.v | 385 | ||||
| -rw-r--r-- | test-suite/primitive/float/coq_env_double_array.v | 13 | ||||
| -rw-r--r-- | test-suite/primitive/float/div.v | 87 | ||||
| -rw-r--r-- | test-suite/primitive/float/double_rounding.v | 38 | ||||
| -rw-r--r-- | test-suite/primitive/float/frexp.v | 28 | ||||
| -rwxr-xr-x | test-suite/primitive/float/gen_compare.sh | 65 | ||||
| -rw-r--r-- | test-suite/primitive/float/ldexp.v | 21 | ||||
| -rw-r--r-- | test-suite/primitive/float/mul.v | 83 | ||||
| -rw-r--r-- | test-suite/primitive/float/next_up_down.v | 122 | ||||
| -rw-r--r-- | test-suite/primitive/float/normfr_mantissa.v | 28 | ||||
| -rw-r--r-- | test-suite/primitive/float/spec_conv.v | 46 | ||||
| -rw-r--r-- | test-suite/primitive/float/sqrt.v | 49 | ||||
| -rw-r--r-- | test-suite/primitive/float/sub.v | 62 | ||||
| -rw-r--r-- | test-suite/primitive/float/syntax.v | 13 | ||||
| -rw-r--r-- | test-suite/primitive/float/valid_binary_conv.v | 46 | ||||
| -rw-r--r-- | test-suite/primitive/float/zero.v | 7 |
18 files changed, 1189 insertions, 0 deletions
diff --git a/test-suite/primitive/float/add.v b/test-suite/primitive/float/add.v new file mode 100644 index 0000000000..f8c5939d0a --- /dev/null +++ b/test-suite/primitive/float/add.v @@ -0,0 +1,63 @@ +Require Import ZArith Int63 Floats. + +Open Scope float_scope. + +Definition two := Eval compute in of_int63 2%int63. +Definition three := Eval compute in of_int63 3%int63. +Definition five := Eval compute in of_int63 5%int63. + +Check (eq_refl : two + three = five). +Check (eq_refl five <: two + three = five). +Check (eq_refl five <<: two + three = five). +Definition compute1 := Eval compute in two + three. +Check (eq_refl compute1 : five = five). + +Definition huge := Eval compute in ldexp one 1023%Z. +Definition tiny := Eval compute in ldexp one (-1023)%Z. + +Check (eq_refl : huge + tiny = huge). +Check (eq_refl huge <: huge + tiny = huge). +Check (eq_refl huge <<: huge + tiny = huge). +Definition compute2 := Eval compute in huge + tiny. +Check (eq_refl compute2 : huge = huge). + +Check (eq_refl : huge + huge = infinity). +Check (eq_refl infinity <: huge + huge = infinity). +Check (eq_refl infinity <<: huge + huge = infinity). +Definition compute3 := Eval compute in huge + huge. +Check (eq_refl compute3 : infinity = infinity). + +Check (eq_refl : one + nan = nan). +Check (eq_refl nan <: one + nan = nan). +Check (eq_refl nan <<: one + nan = nan). +Definition compute4 := Eval compute in one + nan. +Check (eq_refl compute4 : nan = nan). + +Check (eq_refl : infinity + infinity = infinity). +Check (eq_refl infinity <: infinity + infinity = infinity). +Check (eq_refl infinity <<: infinity + infinity = infinity). +Definition compute5 := Eval compute in infinity + infinity. +Check (eq_refl compute5 : infinity = infinity). + +Check (eq_refl : infinity + neg_infinity = nan). +Check (eq_refl nan <: infinity + neg_infinity = nan). +Check (eq_refl nan <<: infinity + neg_infinity = nan). +Definition compute6 := Eval compute in infinity + neg_infinity. +Check (eq_refl compute6 : nan = nan). + +Check (eq_refl : zero + zero = zero). +Check (eq_refl zero <: zero + zero = zero). +Check (eq_refl zero <<: zero + zero = zero). +Check (eq_refl : neg_zero + zero = zero). +Check (eq_refl zero <: neg_zero + zero = zero). +Check (eq_refl zero <<: neg_zero + zero = zero). +Check (eq_refl : neg_zero + neg_zero = neg_zero). +Check (eq_refl neg_zero <: neg_zero + neg_zero = neg_zero). +Check (eq_refl neg_zero <<: neg_zero + neg_zero = neg_zero). +Check (eq_refl : zero + neg_zero = zero). +Check (eq_refl zero <: zero + neg_zero = zero). +Check (eq_refl zero <<: zero + neg_zero = zero). + +Check (eq_refl : huge + neg_infinity = neg_infinity). +Check (eq_refl neg_infinity <: huge + neg_infinity = neg_infinity). +Check (eq_refl neg_infinity <<: huge + neg_infinity = neg_infinity). diff --git a/test-suite/primitive/float/classify.v b/test-suite/primitive/float/classify.v new file mode 100644 index 0000000000..22e3fca844 --- /dev/null +++ b/test-suite/primitive/float/classify.v @@ -0,0 +1,33 @@ +Require Import ZArith Floats. + +Definition epsilon := Eval compute in ldexp one (-1024)%Z. + +Check (eq_refl : classify one = PNormal). +Check (eq_refl : classify (- one)%float = NNormal). +Check (eq_refl : classify epsilon = PSubn). +Check (eq_refl : classify (- epsilon)%float = NSubn). +Check (eq_refl : classify zero = PZero). +Check (eq_refl : classify neg_zero = NZero). +Check (eq_refl : classify infinity = PInf). +Check (eq_refl : classify neg_infinity = NInf). +Check (eq_refl : classify nan = NaN). + +Check (eq_refl PNormal <: classify one = PNormal). +Check (eq_refl NNormal <: classify (- one)%float = NNormal). +Check (eq_refl PSubn <: classify epsilon = PSubn). +Check (eq_refl NSubn <: classify (- epsilon)%float = NSubn). +Check (eq_refl PZero <: classify zero = PZero). +Check (eq_refl NZero <: classify neg_zero = NZero). +Check (eq_refl PInf <: classify infinity = PInf). +Check (eq_refl NInf <: classify neg_infinity = NInf). +Check (eq_refl NaN <: classify nan = NaN). + +Check (eq_refl PNormal <<: classify one = PNormal). +Check (eq_refl NNormal <<: classify (- one)%float = NNormal). +Check (eq_refl PSubn <<: classify epsilon = PSubn). +Check (eq_refl NSubn <<: classify (- epsilon)%float = NSubn). +Check (eq_refl PZero <<: classify zero = PZero). +Check (eq_refl NZero <<: classify neg_zero = NZero). +Check (eq_refl PInf <<: classify infinity = PInf). +Check (eq_refl NInf <<: classify neg_infinity = NInf). +Check (eq_refl NaN <<: classify nan = NaN). diff --git a/test-suite/primitive/float/compare.v b/test-suite/primitive/float/compare.v new file mode 100644 index 0000000000..23d1e5bbae --- /dev/null +++ b/test-suite/primitive/float/compare.v @@ -0,0 +1,385 @@ +(* DO NOT EDIT THIS FILE: automatically generated by ./gen_compare.sh *) +Require Import ZArith Floats. +Local Open Scope float_scope. + +Definition min_denorm := Eval compute in ldexp one (-1074)%Z. + +Definition min_norm := Eval compute in ldexp one (-1024)%Z. + +Check (eq_refl false : nan == nan = false). +Check (eq_refl false : nan == nan = false). +Check (eq_refl false : nan < nan = false). +Check (eq_refl false : nan < nan = false). +Check (eq_refl false : nan <= nan = false). +Check (eq_refl false : nan <= nan = false). +Check (eq_refl FNotComparable : nan ?= nan = FNotComparable). +Check (eq_refl FNotComparable : nan ?= nan = FNotComparable). + +Check (eq_refl false <: nan == nan = false). +Check (eq_refl false <: nan == nan = false). +Check (eq_refl false <: nan < nan = false). +Check (eq_refl false <: nan < nan = false). +Check (eq_refl false <: nan <= nan = false). +Check (eq_refl false <: nan <= nan = false). +Check (eq_refl FNotComparable <: nan ?= nan = FNotComparable). +Check (eq_refl FNotComparable <: nan ?= nan = FNotComparable). + +Check (eq_refl false <<: nan == nan = false). +Check (eq_refl false <<: nan == nan = false). +Check (eq_refl false <<: nan < nan = false). +Check (eq_refl false <<: nan < nan = false). +Check (eq_refl false <<: nan <= nan = false). +Check (eq_refl false <<: nan <= nan = false). +Check (eq_refl FNotComparable <<: nan ?= nan = FNotComparable). +Check (eq_refl FNotComparable <<: nan ?= nan = FNotComparable). + +Check (eq_refl false : nan == - nan = false). +Check (eq_refl false : - nan == nan = false). +Check (eq_refl false : nan < - nan = false). +Check (eq_refl false : - nan < nan = false). +Check (eq_refl false : nan <= - nan = false). +Check (eq_refl false : - nan <= nan = false). +Check (eq_refl FNotComparable : nan ?= - nan = FNotComparable). +Check (eq_refl FNotComparable : - nan ?= nan = FNotComparable). + +Check (eq_refl false <: nan == - nan = false). +Check (eq_refl false <: - nan == nan = false). +Check (eq_refl false <: nan < - nan = false). +Check (eq_refl false <: - nan < nan = false). +Check (eq_refl false <: nan <= - nan = false). +Check (eq_refl false <: - nan <= nan = false). +Check (eq_refl FNotComparable <: nan ?= - nan = FNotComparable). +Check (eq_refl FNotComparable <: - nan ?= nan = FNotComparable). + +Check (eq_refl false <<: nan == - nan = false). +Check (eq_refl false <<: - nan == nan = false). +Check (eq_refl false <<: nan < - nan = false). +Check (eq_refl false <<: - nan < nan = false). +Check (eq_refl false <<: nan <= - nan = false). +Check (eq_refl false <<: - nan <= nan = false). +Check (eq_refl FNotComparable <<: nan ?= - nan = FNotComparable). +Check (eq_refl FNotComparable <<: - nan ?= nan = FNotComparable). + +Check (eq_refl true : one == one = true). +Check (eq_refl true : one == one = true). +Check (eq_refl false : one < one = false). +Check (eq_refl false : one < one = false). +Check (eq_refl true : one <= one = true). +Check (eq_refl true : one <= one = true). +Check (eq_refl FEq : one ?= one = FEq). +Check (eq_refl FEq : one ?= one = FEq). + +Check (eq_refl true <: one == one = true). +Check (eq_refl true <: one == one = true). +Check (eq_refl false <: one < one = false). +Check (eq_refl false <: one < one = false). +Check (eq_refl true <: one <= one = true). +Check (eq_refl true <: one <= one = true). +Check (eq_refl FEq <: one ?= one = FEq). +Check (eq_refl FEq <: one ?= one = FEq). + +Check (eq_refl true <<: one == one = true). +Check (eq_refl true <<: one == one = true). +Check (eq_refl false <<: one < one = false). +Check (eq_refl false <<: one < one = false). +Check (eq_refl true <<: one <= one = true). +Check (eq_refl true <<: one <= one = true). +Check (eq_refl FEq <<: one ?= one = FEq). +Check (eq_refl FEq <<: one ?= one = FEq). + +Check (eq_refl true : zero == zero = true). +Check (eq_refl true : zero == zero = true). +Check (eq_refl false : zero < zero = false). +Check (eq_refl false : zero < zero = false). +Check (eq_refl true : zero <= zero = true). +Check (eq_refl true : zero <= zero = true). +Check (eq_refl FEq : zero ?= zero = FEq). +Check (eq_refl FEq : zero ?= zero = FEq). + +Check (eq_refl true <: zero == zero = true). +Check (eq_refl true <: zero == zero = true). +Check (eq_refl false <: zero < zero = false). +Check (eq_refl false <: zero < zero = false). +Check (eq_refl true <: zero <= zero = true). +Check (eq_refl true <: zero <= zero = true). +Check (eq_refl FEq <: zero ?= zero = FEq). +Check (eq_refl FEq <: zero ?= zero = FEq). + +Check (eq_refl true <<: zero == zero = true). +Check (eq_refl true <<: zero == zero = true). +Check (eq_refl false <<: zero < zero = false). +Check (eq_refl false <<: zero < zero = false). +Check (eq_refl true <<: zero <= zero = true). +Check (eq_refl true <<: zero <= zero = true). +Check (eq_refl FEq <<: zero ?= zero = FEq). +Check (eq_refl FEq <<: zero ?= zero = FEq). + +Check (eq_refl true : zero == - zero = true). +Check (eq_refl true : - zero == zero = true). +Check (eq_refl false : zero < - zero = false). +Check (eq_refl false : - zero < zero = false). +Check (eq_refl true : zero <= - zero = true). +Check (eq_refl true : - zero <= zero = true). +Check (eq_refl FEq : zero ?= - zero = FEq). +Check (eq_refl FEq : - zero ?= zero = FEq). + +Check (eq_refl true <: zero == - zero = true). +Check (eq_refl true <: - zero == zero = true). +Check (eq_refl false <: zero < - zero = false). +Check (eq_refl false <: - zero < zero = false). +Check (eq_refl true <: zero <= - zero = true). +Check (eq_refl true <: - zero <= zero = true). +Check (eq_refl FEq <: zero ?= - zero = FEq). +Check (eq_refl FEq <: - zero ?= zero = FEq). + +Check (eq_refl true <<: zero == - zero = true). +Check (eq_refl true <<: - zero == zero = true). +Check (eq_refl false <<: zero < - zero = false). +Check (eq_refl false <<: - zero < zero = false). +Check (eq_refl true <<: zero <= - zero = true). +Check (eq_refl true <<: - zero <= zero = true). +Check (eq_refl FEq <<: zero ?= - zero = FEq). +Check (eq_refl FEq <<: - zero ?= zero = FEq). + +Check (eq_refl true : - zero == - zero = true). +Check (eq_refl true : - zero == - zero = true). +Check (eq_refl false : - zero < - zero = false). +Check (eq_refl false : - zero < - zero = false). +Check (eq_refl true : - zero <= - zero = true). +Check (eq_refl true : - zero <= - zero = true). +Check (eq_refl FEq : - zero ?= - zero = FEq). +Check (eq_refl FEq : - zero ?= - zero = FEq). + +Check (eq_refl true <: - zero == - zero = true). +Check (eq_refl true <: - zero == - zero = true). +Check (eq_refl false <: - zero < - zero = false). +Check (eq_refl false <: - zero < - zero = false). +Check (eq_refl true <: - zero <= - zero = true). +Check (eq_refl true <: - zero <= - zero = true). +Check (eq_refl FEq <: - zero ?= - zero = FEq). +Check (eq_refl FEq <: - zero ?= - zero = FEq). + +Check (eq_refl true <<: - zero == - zero = true). +Check (eq_refl true <<: - zero == - zero = true). +Check (eq_refl false <<: - zero < - zero = false). +Check (eq_refl false <<: - zero < - zero = false). +Check (eq_refl true <<: - zero <= - zero = true). +Check (eq_refl true <<: - zero <= - zero = true). +Check (eq_refl FEq <<: - zero ?= - zero = FEq). +Check (eq_refl FEq <<: - zero ?= - zero = FEq). + +Check (eq_refl true : infinity == infinity = true). +Check (eq_refl true : infinity == infinity = true). +Check (eq_refl false : infinity < infinity = false). +Check (eq_refl false : infinity < infinity = false). +Check (eq_refl true : infinity <= infinity = true). +Check (eq_refl true : infinity <= infinity = true). +Check (eq_refl FEq : infinity ?= infinity = FEq). +Check (eq_refl FEq : infinity ?= infinity = FEq). + +Check (eq_refl true <: infinity == infinity = true). +Check (eq_refl true <: infinity == infinity = true). +Check (eq_refl false <: infinity < infinity = false). +Check (eq_refl false <: infinity < infinity = false). +Check (eq_refl true <: infinity <= infinity = true). +Check (eq_refl true <: infinity <= infinity = true). +Check (eq_refl FEq <: infinity ?= infinity = FEq). +Check (eq_refl FEq <: infinity ?= infinity = FEq). + +Check (eq_refl true <<: infinity == infinity = true). +Check (eq_refl true <<: infinity == infinity = true). +Check (eq_refl false <<: infinity < infinity = false). +Check (eq_refl false <<: infinity < infinity = false). +Check (eq_refl true <<: infinity <= infinity = true). +Check (eq_refl true <<: infinity <= infinity = true). +Check (eq_refl FEq <<: infinity ?= infinity = FEq). +Check (eq_refl FEq <<: infinity ?= infinity = FEq). + +Check (eq_refl true : - infinity == - infinity = true). +Check (eq_refl true : - infinity == - infinity = true). +Check (eq_refl false : - infinity < - infinity = false). +Check (eq_refl false : - infinity < - infinity = false). +Check (eq_refl true : - infinity <= - infinity = true). +Check (eq_refl true : - infinity <= - infinity = true). +Check (eq_refl FEq : - infinity ?= - infinity = FEq). +Check (eq_refl FEq : - infinity ?= - infinity = FEq). + +Check (eq_refl true <: - infinity == - infinity = true). +Check (eq_refl true <: - infinity == - infinity = true). +Check (eq_refl false <: - infinity < - infinity = false). +Check (eq_refl false <: - infinity < - infinity = false). +Check (eq_refl true <: - infinity <= - infinity = true). +Check (eq_refl true <: - infinity <= - infinity = true). +Check (eq_refl FEq <: - infinity ?= - infinity = FEq). +Check (eq_refl FEq <: - infinity ?= - infinity = FEq). + +Check (eq_refl true <<: - infinity == - infinity = true). +Check (eq_refl true <<: - infinity == - infinity = true). +Check (eq_refl false <<: - infinity < - infinity = false). +Check (eq_refl false <<: - infinity < - infinity = false). +Check (eq_refl true <<: - infinity <= - infinity = true). +Check (eq_refl true <<: - infinity <= - infinity = true). +Check (eq_refl FEq <<: - infinity ?= - infinity = FEq). +Check (eq_refl FEq <<: - infinity ?= - infinity = FEq). + +Check (eq_refl false : min_denorm == min_norm = false). +Check (eq_refl false : min_norm == min_denorm = false). +Check (eq_refl true : min_denorm < min_norm = true). +Check (eq_refl false : min_norm < min_denorm = false). +Check (eq_refl true : min_denorm <= min_norm = true). +Check (eq_refl false : min_norm <= min_denorm = false). +Check (eq_refl FLt : min_denorm ?= min_norm = FLt). +Check (eq_refl FGt : min_norm ?= min_denorm = FGt). + +Check (eq_refl false <: min_denorm == min_norm = false). +Check (eq_refl false <: min_norm == min_denorm = false). +Check (eq_refl true <: min_denorm < min_norm = true). +Check (eq_refl false <: min_norm < min_denorm = false). +Check (eq_refl true <: min_denorm <= min_norm = true). +Check (eq_refl false <: min_norm <= min_denorm = false). +Check (eq_refl FLt <: min_denorm ?= min_norm = FLt). +Check (eq_refl FGt <: min_norm ?= min_denorm = FGt). + +Check (eq_refl false <<: min_denorm == min_norm = false). +Check (eq_refl false <<: min_norm == min_denorm = false). +Check (eq_refl true <<: min_denorm < min_norm = true). +Check (eq_refl false <<: min_norm < min_denorm = false). +Check (eq_refl true <<: min_denorm <= min_norm = true). +Check (eq_refl false <<: min_norm <= min_denorm = false). +Check (eq_refl FLt <<: min_denorm ?= min_norm = FLt). +Check (eq_refl FGt <<: min_norm ?= min_denorm = FGt). + +Check (eq_refl false : min_denorm == one = false). +Check (eq_refl false : one == min_denorm = false). +Check (eq_refl true : min_denorm < one = true). +Check (eq_refl false : one < min_denorm = false). +Check (eq_refl true : min_denorm <= one = true). +Check (eq_refl false : one <= min_denorm = false). +Check (eq_refl FLt : min_denorm ?= one = FLt). +Check (eq_refl FGt : one ?= min_denorm = FGt). + +Check (eq_refl false <: min_denorm == one = false). +Check (eq_refl false <: one == min_denorm = false). +Check (eq_refl true <: min_denorm < one = true). +Check (eq_refl false <: one < min_denorm = false). +Check (eq_refl true <: min_denorm <= one = true). +Check (eq_refl false <: one <= min_denorm = false). +Check (eq_refl FLt <: min_denorm ?= one = FLt). +Check (eq_refl FGt <: one ?= min_denorm = FGt). + +Check (eq_refl false <<: min_denorm == one = false). +Check (eq_refl false <<: one == min_denorm = false). +Check (eq_refl true <<: min_denorm < one = true). +Check (eq_refl false <<: one < min_denorm = false). +Check (eq_refl true <<: min_denorm <= one = true). +Check (eq_refl false <<: one <= min_denorm = false). +Check (eq_refl FLt <<: min_denorm ?= one = FLt). +Check (eq_refl FGt <<: one ?= min_denorm = FGt). + +Check (eq_refl false : min_norm == one = false). +Check (eq_refl false : one == min_norm = false). +Check (eq_refl true : min_norm < one = true). +Check (eq_refl false : one < min_norm = false). +Check (eq_refl true : min_norm <= one = true). +Check (eq_refl false : one <= min_norm = false). +Check (eq_refl FLt : min_norm ?= one = FLt). +Check (eq_refl FGt : one ?= min_norm = FGt). + +Check (eq_refl false <: min_norm == one = false). +Check (eq_refl false <: one == min_norm = false). +Check (eq_refl true <: min_norm < one = true). +Check (eq_refl false <: one < min_norm = false). +Check (eq_refl true <: min_norm <= one = true). +Check (eq_refl false <: one <= min_norm = false). +Check (eq_refl FLt <: min_norm ?= one = FLt). +Check (eq_refl FGt <: one ?= min_norm = FGt). + +Check (eq_refl false <<: min_norm == one = false). +Check (eq_refl false <<: one == min_norm = false). +Check (eq_refl true <<: min_norm < one = true). +Check (eq_refl false <<: one < min_norm = false). +Check (eq_refl true <<: min_norm <= one = true). +Check (eq_refl false <<: one <= min_norm = false). +Check (eq_refl FLt <<: min_norm ?= one = FLt). +Check (eq_refl FGt <<: one ?= min_norm = FGt). + +Check (eq_refl false : one == infinity = false). +Check (eq_refl false : infinity == one = false). +Check (eq_refl true : one < infinity = true). +Check (eq_refl false : infinity < one = false). +Check (eq_refl true : one <= infinity = true). +Check (eq_refl false : infinity <= one = false). +Check (eq_refl FLt : one ?= infinity = FLt). +Check (eq_refl FGt : infinity ?= one = FGt). + +Check (eq_refl false <: one == infinity = false). +Check (eq_refl false <: infinity == one = false). +Check (eq_refl true <: one < infinity = true). +Check (eq_refl false <: infinity < one = false). +Check (eq_refl true <: one <= infinity = true). +Check (eq_refl false <: infinity <= one = false). +Check (eq_refl FLt <: one ?= infinity = FLt). +Check (eq_refl FGt <: infinity ?= one = FGt). + +Check (eq_refl false <<: one == infinity = false). +Check (eq_refl false <<: infinity == one = false). +Check (eq_refl true <<: one < infinity = true). +Check (eq_refl false <<: infinity < one = false). +Check (eq_refl true <<: one <= infinity = true). +Check (eq_refl false <<: infinity <= one = false). +Check (eq_refl FLt <<: one ?= infinity = FLt). +Check (eq_refl FGt <<: infinity ?= one = FGt). + +Check (eq_refl false : - infinity == infinity = false). +Check (eq_refl false : infinity == - infinity = false). +Check (eq_refl true : - infinity < infinity = true). +Check (eq_refl false : infinity < - infinity = false). +Check (eq_refl true : - infinity <= infinity = true). +Check (eq_refl false : infinity <= - infinity = false). +Check (eq_refl FLt : - infinity ?= infinity = FLt). +Check (eq_refl FGt : infinity ?= - infinity = FGt). + +Check (eq_refl false <: - infinity == infinity = false). +Check (eq_refl false <: infinity == - infinity = false). +Check (eq_refl true <: - infinity < infinity = true). +Check (eq_refl false <: infinity < - infinity = false). +Check (eq_refl true <: - infinity <= infinity = true). +Check (eq_refl false <: infinity <= - infinity = false). +Check (eq_refl FLt <: - infinity ?= infinity = FLt). +Check (eq_refl FGt <: infinity ?= - infinity = FGt). + +Check (eq_refl false <<: - infinity == infinity = false). +Check (eq_refl false <<: infinity == - infinity = false). +Check (eq_refl true <<: - infinity < infinity = true). +Check (eq_refl false <<: infinity < - infinity = false). +Check (eq_refl true <<: - infinity <= infinity = true). +Check (eq_refl false <<: infinity <= - infinity = false). +Check (eq_refl FLt <<: - infinity ?= infinity = FLt). +Check (eq_refl FGt <<: infinity ?= - infinity = FGt). + +Check (eq_refl false : - infinity == one = false). +Check (eq_refl false : one == - infinity = false). +Check (eq_refl true : - infinity < one = true). +Check (eq_refl false : one < - infinity = false). +Check (eq_refl true : - infinity <= one = true). +Check (eq_refl false : one <= - infinity = false). +Check (eq_refl FLt : - infinity ?= one = FLt). +Check (eq_refl FGt : one ?= - infinity = FGt). + +Check (eq_refl false <: - infinity == one = false). +Check (eq_refl false <: one == - infinity = false). +Check (eq_refl true <: - infinity < one = true). +Check (eq_refl false <: one < - infinity = false). +Check (eq_refl true <: - infinity <= one = true). +Check (eq_refl false <: one <= - infinity = false). +Check (eq_refl FLt <: - infinity ?= one = FLt). +Check (eq_refl FGt <: one ?= - infinity = FGt). + +Check (eq_refl false <<: - infinity == one = false). +Check (eq_refl false <<: one == - infinity = false). +Check (eq_refl true <<: - infinity < one = true). +Check (eq_refl false <<: one < - infinity = false). +Check (eq_refl true <<: - infinity <= one = true). +Check (eq_refl false <<: one <= - infinity = false). +Check (eq_refl FLt <<: - infinity ?= one = FLt). +Check (eq_refl FGt <<: one ?= - infinity = FGt). diff --git a/test-suite/primitive/float/coq_env_double_array.v b/test-suite/primitive/float/coq_env_double_array.v new file mode 100644 index 0000000000..754ccb69aa --- /dev/null +++ b/test-suite/primitive/float/coq_env_double_array.v @@ -0,0 +1,13 @@ +Require Import Floats. + +Goal True. +pose (f := one). +pose (f' := (-f)%float). + +(* this used to segfault when the coq_env array given to the + coq_interprete C function was an unboxed OCaml Double_array + (created by Array.map in csymtable.ml just before calling + eval_tcode) *) +vm_compute in f'. + +Abort. diff --git a/test-suite/primitive/float/div.v b/test-suite/primitive/float/div.v new file mode 100644 index 0000000000..8e971f575b --- /dev/null +++ b/test-suite/primitive/float/div.v @@ -0,0 +1,87 @@ +Require Import ZArith Int63 Floats. + +Open Scope float_scope. + +Definition two := Eval compute in of_int63 2%int63. +Definition three := Eval compute in of_int63 3%int63. +Definition six := Eval compute in of_int63 6%int63. + +Check (eq_refl : six / three = two). +Check (eq_refl two <: six / three = two). +Check (eq_refl two <<: six / three = two). +Definition compute1 := Eval compute in six / three. +Check (eq_refl compute1 : two = two). + +Definition huge := Eval compute in ldexp one 1023%Z. +Definition tiny := Eval compute in ldexp one (-1023)%Z. + +Check (eq_refl : huge / tiny = infinity). +Check (eq_refl infinity <: huge / tiny = infinity). +Check (eq_refl infinity <<: huge / tiny = infinity). +Definition compute2 := Eval compute in huge / tiny. +Check (eq_refl compute2 : infinity = infinity). + +Check (eq_refl : huge / huge = one). +Check (eq_refl one <: huge / huge = one). +Check (eq_refl one <<: huge / huge = one). +Definition compute3 := Eval compute in huge / huge. +Check (eq_refl compute3 : one = one). + +Check (eq_refl : one / nan = nan). +Check (eq_refl nan <: one / nan = nan). +Check (eq_refl nan <<: one / nan = nan). +Definition compute4 := Eval compute in one / nan. +Check (eq_refl compute4 : nan = nan). + +Check (eq_refl : infinity / infinity = nan). +Check (eq_refl nan <: infinity / infinity = nan). +Check (eq_refl nan <<: infinity / infinity = nan). +Definition compute5 := Eval compute in infinity / infinity. +Check (eq_refl compute5 : nan = nan). + +Check (eq_refl : infinity / neg_infinity = nan). +Check (eq_refl nan <: infinity / neg_infinity = nan). +Check (eq_refl nan <<: infinity / neg_infinity = nan). +Definition compute6 := Eval compute in infinity / neg_infinity. +Check (eq_refl compute6 : nan = nan). + +Check (eq_refl : zero / zero = nan). +Check (eq_refl nan <: zero / zero = nan). +Check (eq_refl nan <<: zero / zero = nan). +Check (eq_refl : neg_zero / zero = nan). +Check (eq_refl nan <: neg_zero / zero = nan). +Check (eq_refl nan <<: neg_zero / zero = nan). + +Check (eq_refl : huge / neg_infinity = neg_zero). +Check (eq_refl neg_zero <: huge / neg_infinity = neg_zero). +Check (eq_refl neg_zero <<: huge / neg_infinity = neg_zero). + +Check (eq_refl : one / tiny = huge). +Check (eq_refl huge <: one / tiny = huge). +Check (eq_refl huge <<: one / tiny = huge). +Check (eq_refl : one / huge = tiny). +Check (eq_refl tiny <: one / huge = tiny). +Check (eq_refl tiny <<: one / huge = tiny). +Check (eq_refl : zero / huge = zero). +Check (eq_refl zero <: zero / huge = zero). +Check (eq_refl zero <<: zero / huge = zero). +Check (eq_refl : zero / (-huge) = neg_zero). +Check (eq_refl neg_zero <: zero / (-huge) = neg_zero). +Check (eq_refl neg_zero <<: zero / (-huge) = neg_zero). + +Check (eq_refl : tiny / one = tiny). +Check (eq_refl tiny <: tiny / one = tiny). +Check (eq_refl tiny <<: tiny / one = tiny). +Check (eq_refl : huge / one = huge). +Check (eq_refl huge <: huge / one = huge). +Check (eq_refl huge <<: huge / one = huge). +Check (eq_refl : infinity / one = infinity). +Check (eq_refl infinity <: infinity / one = infinity). +Check (eq_refl infinity <<: infinity / one = infinity). + +Check (eq_refl : zero / infinity = zero). +Check (eq_refl zero <: zero / infinity = zero). +Check (eq_refl zero <<: zero / infinity = zero). +Check (eq_refl : infinity / zero = infinity). +Check (eq_refl infinity <: infinity / zero = infinity). +Check (eq_refl infinity <<: infinity / zero = infinity). diff --git a/test-suite/primitive/float/double_rounding.v b/test-suite/primitive/float/double_rounding.v new file mode 100644 index 0000000000..e2356cdd7b --- /dev/null +++ b/test-suite/primitive/float/double_rounding.v @@ -0,0 +1,38 @@ +Require Import Floats ZArith. + +(* This test check that there is no double rounding with 80 bits registers inside float computations *) + +Definition big_cbn := Eval cbn in ldexp one (53)%Z. +Definition small_cbn := Eval cbn in (one + ldexp one (-52)%Z)%float. +Definition result_cbn := Eval cbn in (big_cbn + small_cbn)%float. +Definition check_cbn := Eval cbn in (big_cbn + one)%float. + +Check (eq_refl : (result_cbn ?= big_cbn)%float = FGt). +Check (eq_refl : (check_cbn ?= big_cbn)%float = FEq). + + +Definition big_cbv := Eval cbv in ldexp one (53)%Z. +Definition small_cbv := Eval cbv in (one + ldexp one (-52)%Z)%float. +Definition result_cbv := Eval cbv in (big_cbv + small_cbv)%float. +Definition check_cbv := Eval cbv in (big_cbv + one)%float. + +Check (eq_refl : (result_cbv ?= big_cbv)%float = FGt). +Check (eq_refl : (check_cbv ?= big_cbv)%float = FEq). + + +Definition big_vm := Eval vm_compute in ldexp one (53)%Z. +Definition small_vm := Eval vm_compute in (one + ldexp one (-52)%Z)%float. +Definition result_vm := Eval vm_compute in (big_vm + small_vm)%float. +Definition check_vm := Eval vm_compute in (big_vm + one)%float. + +Check (eq_refl : (result_vm ?= big_vm)%float = FGt). +Check (eq_refl : (check_vm ?= big_vm)%float = FEq). + + +Definition big_native := Eval native_compute in ldexp one (53)%Z. +Definition small_native := Eval native_compute in (one + ldexp one (-52)%Z)%float. +Definition result_native := Eval native_compute in (big_native + small_native)%float. +Definition check_native := Eval native_compute in (big_native + one)%float. + +Check (eq_refl : (result_native ?= big_native)%float = FGt). +Check (eq_refl : (check_native ?= big_native)%float = FEq). diff --git a/test-suite/primitive/float/frexp.v b/test-suite/primitive/float/frexp.v new file mode 100644 index 0000000000..2a600429b1 --- /dev/null +++ b/test-suite/primitive/float/frexp.v @@ -0,0 +1,28 @@ +Require Import ZArith Floats. + +Definition denorm := Eval compute in ldexp one (-1074)%Z. +Definition neg_one := Eval compute in (-one)%float. + +Check (eq_refl : let (m,e) := frexp infinity in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF infinity)). +Check (eq_refl (SFfrexp prec emax (Prim2SF infinity)) <: let (m,e) := frexp infinity in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF infinity)). +Check (eq_refl (SFfrexp prec emax (Prim2SF infinity)) <<: let (m,e) := frexp infinity in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF infinity)). + +Check (eq_refl : let (m,e) := frexp nan in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF nan)). +Check (eq_refl (SFfrexp prec emax (Prim2SF nan)) <: let (m,e) := frexp nan in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF nan)). +Check (eq_refl (SFfrexp prec emax (Prim2SF nan)) <<: let (m,e) := frexp nan in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF nan)). + +Check (eq_refl : let (m,e) := frexp zero in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF zero)). +Check (eq_refl (SFfrexp prec emax (Prim2SF zero)) <: let (m,e) := frexp zero in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF zero)). +Check (eq_refl (SFfrexp prec emax (Prim2SF zero)) <<: let (m,e) := frexp zero in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF zero)). + +Check (eq_refl : let (m,e) := frexp one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF one)). +Check (eq_refl (SFfrexp prec emax (Prim2SF one)) <: let (m,e) := frexp one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF one)). +Check (eq_refl (SFfrexp prec emax (Prim2SF one)) <<: let (m,e) := frexp one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF one)). + +Check (eq_refl : let (m,e) := frexp neg_one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF neg_one)). +Check (eq_refl (SFfrexp prec emax (Prim2SF neg_one)) <: let (m,e) := frexp neg_one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF neg_one)). +Check (eq_refl (SFfrexp prec emax (Prim2SF neg_one)) <<: let (m,e) := frexp neg_one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF neg_one)). + +Check (eq_refl : let (m,e) := frexp denorm in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF denorm)). +Check (eq_refl (SFfrexp prec emax (Prim2SF denorm)) <: let (m,e) := frexp denorm in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF denorm)). +Check (eq_refl (SFfrexp prec emax (Prim2SF denorm)) <<: let (m,e) := frexp denorm in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF denorm)). diff --git a/test-suite/primitive/float/gen_compare.sh b/test-suite/primitive/float/gen_compare.sh new file mode 100755 index 0000000000..cd87eb4e5b --- /dev/null +++ b/test-suite/primitive/float/gen_compare.sh @@ -0,0 +1,65 @@ +#!/bin/bash +# -*- compile-command: "mv -f compare.v{,~} && ./gen_compare.sh" -*- +set -e + +exec > compare.v + +cat <<EOF +(* DO NOT EDIT THIS FILE: automatically generated by ./gen_compare.sh *) +Require Import ZArith Floats. +Local Open Scope float_scope. + +Definition min_denorm := Eval compute in ldexp one (-1074)%Z. + +Definition min_norm := Eval compute in ldexp one (-1024)%Z. + +EOF + +genTest() { + if [ $# -ne 10 ]; then + echo >&2 "genTest expects 10 arguments" + fi + TACTICS=(":" "<:" "<<:") + OPS=("==" "<" "<=" "?=") + x="$1" + y="$2" + OPS1=("$3" "$4" "$5" "$6") # for x y + OPS2=("$7" "$8" "$9" "${10}") # for y x + for tac in "${TACTICS[@]}"; do + for i in {0..3}; do + op="${OPS[$i]}" + op1="${OPS1[$i]}" + op2="${OPS2[$i]}" + echo "Check (eq_refl $op1 $tac $x $op $y = $op1)." + echo "Check (eq_refl $op2 $tac $y $op $x = $op2)." + done + echo + done +} + +genTest nan nan \ + false false false FNotComparable \ + false false false FNotComparable +genTest nan "- nan" \ + false false false FNotComparable \ + false false false FNotComparable + +EQ=(true false true FEq \ + true false true FEq) + +genTest one one "${EQ[@]}" +genTest zero zero "${EQ[@]}" +genTest zero "- zero" "${EQ[@]}" +genTest "- zero" "- zero" "${EQ[@]}" +genTest infinity infinity "${EQ[@]}" +genTest "- infinity" "- infinity" "${EQ[@]}" + +LT=(false true true FLt \ + false false false FGt) + +genTest min_denorm min_norm "${LT[@]}" +genTest min_denorm one "${LT[@]}" +genTest min_norm one "${LT[@]}" +genTest one infinity "${LT[@]}" +genTest "- infinity" infinity "${LT[@]}" +genTest "- infinity" one "${LT[@]}" diff --git a/test-suite/primitive/float/ldexp.v b/test-suite/primitive/float/ldexp.v new file mode 100644 index 0000000000..a725deeeca --- /dev/null +++ b/test-suite/primitive/float/ldexp.v @@ -0,0 +1,21 @@ +Require Import ZArith Int63 Floats. + +Check (eq_refl : ldexp one 9223372036854773807%Z = infinity). +Check (eq_refl infinity <: ldexp one 9223372036854773807%Z = infinity). +Check (eq_refl infinity <<: ldexp one 9223372036854773807%Z = infinity). + +Check (eq_refl : ldshiftexp one 9223372036854775807 = infinity). +Check (eq_refl infinity <: ldshiftexp one 9223372036854775807 = infinity). +Check (eq_refl infinity <<: ldshiftexp one 9223372036854775807 = infinity). + +Check (eq_refl : ldexp one (-2102) = 0%float). +Check (eq_refl 0%float <: ldexp one (-2102) = 0%float). +Check (eq_refl 0%float <<: ldexp one (-2102) = 0%float). + +Check (eq_refl : ldexp one (-3) = 0.125%float). +Check (eq_refl 0.125%float <: ldexp one (-3) = 0.125%float). +Check (eq_refl 0.125%float <<: ldexp one (-3) = 0.125%float). + +Check (eq_refl : ldexp one 3 = 8%float). +Check (eq_refl 8%float <: ldexp one 3 = 8%float). +Check (eq_refl 8%float <<: ldexp one 3 = 8%float). diff --git a/test-suite/primitive/float/mul.v b/test-suite/primitive/float/mul.v new file mode 100644 index 0000000000..91fe7e9791 --- /dev/null +++ b/test-suite/primitive/float/mul.v @@ -0,0 +1,83 @@ +Require Import ZArith Int63 Floats. + +Open Scope float_scope. + +Definition two := Eval compute in of_int63 2%int63. +Definition three := Eval compute in of_int63 3%int63. +Definition six := Eval compute in of_int63 6%int63. + +Check (eq_refl : three * two = six). +Check (eq_refl six <: three * two = six). +Check (eq_refl six <<: three * two = six). +Definition compute1 := Eval compute in three * two. +Check (eq_refl compute1 : six = six). + +Definition huge := Eval compute in ldexp one 1023%Z. +Definition tiny := Eval compute in ldexp one (-1023)%Z. + +Check (eq_refl : huge * tiny = one). +Check (eq_refl one <: huge * tiny = one). +Check (eq_refl one <<: huge * tiny = one). +Definition compute2 := Eval compute in huge * tiny. +Check (eq_refl compute2 : one = one). + +Check (eq_refl : huge * huge = infinity). +Check (eq_refl infinity <: huge * huge = infinity). +Check (eq_refl infinity <<: huge * huge = infinity). +Definition compute3 := Eval compute in huge * huge. +Check (eq_refl compute3 : infinity = infinity). + +Check (eq_refl : one * nan = nan). +Check (eq_refl nan <: one * nan = nan). +Check (eq_refl nan <<: one * nan = nan). +Definition compute4 := Eval compute in one * nan. +Check (eq_refl compute4 : nan = nan). + +Check (eq_refl : infinity * infinity = infinity). +Check (eq_refl infinity <: infinity * infinity = infinity). +Check (eq_refl infinity <<: infinity * infinity = infinity). +Definition compute5 := Eval compute in infinity * infinity. +Check (eq_refl compute5 : infinity = infinity). + +Check (eq_refl : infinity * neg_infinity = neg_infinity). +Check (eq_refl neg_infinity <: infinity * neg_infinity = neg_infinity). +Check (eq_refl neg_infinity <<: infinity * neg_infinity = neg_infinity). +Definition compute6 := Eval compute in infinity * neg_infinity. +Check (eq_refl compute6 : neg_infinity = neg_infinity). + +Check (eq_refl : zero * zero = zero). +Check (eq_refl zero <: zero * zero = zero). +Check (eq_refl zero <<: zero * zero = zero). +Check (eq_refl : neg_zero * zero = neg_zero). +Check (eq_refl neg_zero <: neg_zero * zero = neg_zero). +Check (eq_refl neg_zero <<: neg_zero * zero = neg_zero). +Check (eq_refl : neg_zero * neg_zero = zero). +Check (eq_refl zero <: neg_zero * neg_zero = zero). +Check (eq_refl zero <<: neg_zero * neg_zero = zero). +Check (eq_refl : zero * neg_zero = neg_zero). +Check (eq_refl neg_zero <: zero * neg_zero = neg_zero). +Check (eq_refl neg_zero <<: zero * neg_zero = neg_zero). + +Check (eq_refl : huge * neg_infinity = neg_infinity). +Check (eq_refl neg_infinity <: huge * neg_infinity = neg_infinity). +Check (eq_refl neg_infinity <<: huge * neg_infinity = neg_infinity). + +Check (eq_refl : one * tiny = tiny). +Check (eq_refl tiny <: one * tiny = tiny). +Check (eq_refl tiny <<: one * tiny = tiny). +Check (eq_refl : one * huge = huge). +Check (eq_refl huge <: one * huge = huge). +Check (eq_refl huge <<: one * huge = huge). +Check (eq_refl : zero * huge = zero). +Check (eq_refl zero <: zero * huge = zero). +Check (eq_refl zero <<: zero * huge = zero). +Check (eq_refl : zero * (-huge) = neg_zero). +Check (eq_refl neg_zero <: zero * (-huge) = neg_zero). +Check (eq_refl neg_zero <<: zero * (-huge) = neg_zero). + +Check (eq_refl : zero * infinity = nan). +Check (eq_refl nan <: zero * infinity = nan). +Check (eq_refl nan <<: zero * infinity = nan). +Check (eq_refl : neg_infinity * zero = nan). +Check (eq_refl nan <: neg_infinity * zero = nan). +Check (eq_refl nan <<: neg_infinity * zero = nan). diff --git a/test-suite/primitive/float/next_up_down.v b/test-suite/primitive/float/next_up_down.v new file mode 100644 index 0000000000..4f8427dc5b --- /dev/null +++ b/test-suite/primitive/float/next_up_down.v @@ -0,0 +1,122 @@ +Require Import ZArith Int63 Floats. + +Open Scope float_scope. + +Definition f0 := zero. +Definition f1 := neg_zero. +Definition f2 := Eval compute in ldexp one 0. +Definition f3 := Eval compute in -f1. +(* smallest positive float *) +Definition f4 := Eval compute in ldexp one (-1074). +Definition f5 := Eval compute in -f3. +Definition f6 := infinity. +Definition f7 := neg_infinity. +Definition f8 := Eval compute in ldexp one (-1). +Definition f9 := Eval compute in -f8. +Definition f10 := Eval compute in of_int63 42. +Definition f11 := Eval compute in -f10. +(* max float *) +Definition f12 := Eval compute in ldexp (of_int63 9007199254740991) 1024. +Definition f13 := Eval compute in -f12. +(* smallest positive normalized float *) +Definition f14 := Eval compute in ldexp one (-1022). +Definition f15 := Eval compute in -f14. + +Check (eq_refl : Prim2SF (next_up f0) = SF64succ (Prim2SF f0)). +Check (eq_refl : Prim2SF (next_down f0) = SF64pred (Prim2SF f0)). +Check (eq_refl : Prim2SF (next_up f1) = SF64succ (Prim2SF f1)). +Check (eq_refl : Prim2SF (next_down f1) = SF64pred (Prim2SF f1)). +Check (eq_refl : Prim2SF (next_up f2) = SF64succ (Prim2SF f2)). +Check (eq_refl : Prim2SF (next_down f2) = SF64pred (Prim2SF f2)). +Check (eq_refl : Prim2SF (next_up f3) = SF64succ (Prim2SF f3)). +Check (eq_refl : Prim2SF (next_down f3) = SF64pred (Prim2SF f3)). +Check (eq_refl : Prim2SF (next_up f4) = SF64succ (Prim2SF f4)). +Check (eq_refl : Prim2SF (next_down f4) = SF64pred (Prim2SF f4)). +Check (eq_refl : Prim2SF (next_up f5) = SF64succ (Prim2SF f5)). +Check (eq_refl : Prim2SF (next_down f5) = SF64pred (Prim2SF f5)). +Check (eq_refl : Prim2SF (next_up f6) = SF64succ (Prim2SF f6)). +Check (eq_refl : Prim2SF (next_down f6) = SF64pred (Prim2SF f6)). +Check (eq_refl : Prim2SF (next_up f7) = SF64succ (Prim2SF f7)). +Check (eq_refl : Prim2SF (next_down f7) = SF64pred (Prim2SF f7)). +Check (eq_refl : Prim2SF (next_up f8) = SF64succ (Prim2SF f8)). +Check (eq_refl : Prim2SF (next_down f8) = SF64pred (Prim2SF f8)). +Check (eq_refl : Prim2SF (next_up f9) = SF64succ (Prim2SF f9)). +Check (eq_refl : Prim2SF (next_down f9) = SF64pred (Prim2SF f9)). +Check (eq_refl : Prim2SF (next_up f10) = SF64succ (Prim2SF f10)). +Check (eq_refl : Prim2SF (next_down f10) = SF64pred (Prim2SF f10)). +Check (eq_refl : Prim2SF (next_up f11) = SF64succ (Prim2SF f11)). +Check (eq_refl : Prim2SF (next_down f11) = SF64pred (Prim2SF f11)). +Check (eq_refl : Prim2SF (next_up f12) = SF64succ (Prim2SF f12)). +Check (eq_refl : Prim2SF (next_down f12) = SF64pred (Prim2SF f12)). +Check (eq_refl : Prim2SF (next_up f13) = SF64succ (Prim2SF f13)). +Check (eq_refl : Prim2SF (next_down f13) = SF64pred (Prim2SF f13)). +Check (eq_refl : Prim2SF (next_up f14) = SF64succ (Prim2SF f14)). +Check (eq_refl : Prim2SF (next_down f14) = SF64pred (Prim2SF f14)). +Check (eq_refl : Prim2SF (next_up f15) = SF64succ (Prim2SF f15)). +Check (eq_refl : Prim2SF (next_down f15) = SF64pred (Prim2SF f15)). + +Check (eq_refl (SF64succ (Prim2SF f0)) <: Prim2SF (next_up f0) = SF64succ (Prim2SF f0)). +Check (eq_refl (SF64pred (Prim2SF f0)) <: Prim2SF (next_down f0) = SF64pred (Prim2SF f0)). +Check (eq_refl (SF64succ (Prim2SF f1)) <: Prim2SF (next_up f1) = SF64succ (Prim2SF f1)). +Check (eq_refl (SF64pred (Prim2SF f1)) <: Prim2SF (next_down f1) = SF64pred (Prim2SF f1)). +Check (eq_refl (SF64succ (Prim2SF f2)) <: Prim2SF (next_up f2) = SF64succ (Prim2SF f2)). +Check (eq_refl (SF64pred (Prim2SF f2)) <: Prim2SF (next_down f2) = SF64pred (Prim2SF f2)). +Check (eq_refl (SF64succ (Prim2SF f3)) <: Prim2SF (next_up f3) = SF64succ (Prim2SF f3)). +Check (eq_refl (SF64pred (Prim2SF f3)) <: Prim2SF (next_down f3) = SF64pred (Prim2SF f3)). +Check (eq_refl (SF64succ (Prim2SF f4)) <: Prim2SF (next_up f4) = SF64succ (Prim2SF f4)). +Check (eq_refl (SF64pred (Prim2SF f4)) <: Prim2SF (next_down f4) = SF64pred (Prim2SF f4)). +Check (eq_refl (SF64succ (Prim2SF f5)) <: Prim2SF (next_up f5) = SF64succ (Prim2SF f5)). +Check (eq_refl (SF64pred (Prim2SF f5)) <: Prim2SF (next_down f5) = SF64pred (Prim2SF f5)). +Check (eq_refl (SF64succ (Prim2SF f6)) <: Prim2SF (next_up f6) = SF64succ (Prim2SF f6)). +Check (eq_refl (SF64pred (Prim2SF f6)) <: Prim2SF (next_down f6) = SF64pred (Prim2SF f6)). +Check (eq_refl (SF64succ (Prim2SF f7)) <: Prim2SF (next_up f7) = SF64succ (Prim2SF f7)). +Check (eq_refl (SF64pred (Prim2SF f7)) <: Prim2SF (next_down f7) = SF64pred (Prim2SF f7)). +Check (eq_refl (SF64succ (Prim2SF f8)) <: Prim2SF (next_up f8) = SF64succ (Prim2SF f8)). +Check (eq_refl (SF64pred (Prim2SF f8)) <: Prim2SF (next_down f8) = SF64pred (Prim2SF f8)). +Check (eq_refl (SF64succ (Prim2SF f9)) <: Prim2SF (next_up f9) = SF64succ (Prim2SF f9)). +Check (eq_refl (SF64pred (Prim2SF f9)) <: Prim2SF (next_down f9) = SF64pred (Prim2SF f9)). +Check (eq_refl (SF64succ (Prim2SF f10)) <: Prim2SF (next_up f10) = SF64succ (Prim2SF f10)). +Check (eq_refl (SF64pred (Prim2SF f10)) <: Prim2SF (next_down f10) = SF64pred (Prim2SF f10)). +Check (eq_refl (SF64succ (Prim2SF f11)) <: Prim2SF (next_up f11) = SF64succ (Prim2SF f11)). +Check (eq_refl (SF64pred (Prim2SF f11)) <: Prim2SF (next_down f11) = SF64pred (Prim2SF f11)). +Check (eq_refl (SF64succ (Prim2SF f12)) <: Prim2SF (next_up f12) = SF64succ (Prim2SF f12)). +Check (eq_refl (SF64pred (Prim2SF f12)) <: Prim2SF (next_down f12) = SF64pred (Prim2SF f12)). +Check (eq_refl (SF64succ (Prim2SF f13)) <: Prim2SF (next_up f13) = SF64succ (Prim2SF f13)). +Check (eq_refl (SF64pred (Prim2SF f13)) <: Prim2SF (next_down f13) = SF64pred (Prim2SF f13)). +Check (eq_refl (SF64succ (Prim2SF f14)) <: Prim2SF (next_up f14) = SF64succ (Prim2SF f14)). +Check (eq_refl (SF64pred (Prim2SF f14)) <: Prim2SF (next_down f14) = SF64pred (Prim2SF f14)). +Check (eq_refl (SF64succ (Prim2SF f15)) <: Prim2SF (next_up f15) = SF64succ (Prim2SF f15)). +Check (eq_refl (SF64pred (Prim2SF f15)) <: Prim2SF (next_down f15) = SF64pred (Prim2SF f15)). + +Check (eq_refl (SF64succ (Prim2SF f0)) <<: Prim2SF (next_up f0) = SF64succ (Prim2SF f0)). +Check (eq_refl (SF64pred (Prim2SF f0)) <<: Prim2SF (next_down f0) = SF64pred (Prim2SF f0)). +Check (eq_refl (SF64succ (Prim2SF f1)) <<: Prim2SF (next_up f1) = SF64succ (Prim2SF f1)). +Check (eq_refl (SF64pred (Prim2SF f1)) <<: Prim2SF (next_down f1) = SF64pred (Prim2SF f1)). +Check (eq_refl (SF64succ (Prim2SF f2)) <<: Prim2SF (next_up f2) = SF64succ (Prim2SF f2)). +Check (eq_refl (SF64pred (Prim2SF f2)) <<: Prim2SF (next_down f2) = SF64pred (Prim2SF f2)). +Check (eq_refl (SF64succ (Prim2SF f3)) <<: Prim2SF (next_up f3) = SF64succ (Prim2SF f3)). +Check (eq_refl (SF64pred (Prim2SF f3)) <<: Prim2SF (next_down f3) = SF64pred (Prim2SF f3)). +Check (eq_refl (SF64succ (Prim2SF f4)) <<: Prim2SF (next_up f4) = SF64succ (Prim2SF f4)). +Check (eq_refl (SF64pred (Prim2SF f4)) <<: Prim2SF (next_down f4) = SF64pred (Prim2SF f4)). +Check (eq_refl (SF64succ (Prim2SF f5)) <<: Prim2SF (next_up f5) = SF64succ (Prim2SF f5)). +Check (eq_refl (SF64pred (Prim2SF f5)) <<: Prim2SF (next_down f5) = SF64pred (Prim2SF f5)). +Check (eq_refl (SF64succ (Prim2SF f6)) <<: Prim2SF (next_up f6) = SF64succ (Prim2SF f6)). +Check (eq_refl (SF64pred (Prim2SF f6)) <<: Prim2SF (next_down f6) = SF64pred (Prim2SF f6)). +Check (eq_refl (SF64succ (Prim2SF f7)) <<: Prim2SF (next_up f7) = SF64succ (Prim2SF f7)). +Check (eq_refl (SF64pred (Prim2SF f7)) <<: Prim2SF (next_down f7) = SF64pred (Prim2SF f7)). +Check (eq_refl (SF64succ (Prim2SF f8)) <<: Prim2SF (next_up f8) = SF64succ (Prim2SF f8)). +Check (eq_refl (SF64pred (Prim2SF f8)) <<: Prim2SF (next_down f8) = SF64pred (Prim2SF f8)). +Check (eq_refl (SF64succ (Prim2SF f9)) <<: Prim2SF (next_up f9) = SF64succ (Prim2SF f9)). +Check (eq_refl (SF64pred (Prim2SF f9)) <<: Prim2SF (next_down f9) = SF64pred (Prim2SF f9)). +Check (eq_refl (SF64succ (Prim2SF f10)) <<: Prim2SF (next_up f10) = SF64succ (Prim2SF f10)). +Check (eq_refl (SF64pred (Prim2SF f10)) <<: Prim2SF (next_down f10) = SF64pred (Prim2SF f10)). +Check (eq_refl (SF64succ (Prim2SF f11)) <<: Prim2SF (next_up f11) = SF64succ (Prim2SF f11)). +Check (eq_refl (SF64pred (Prim2SF f11)) <<: Prim2SF (next_down f11) = SF64pred (Prim2SF f11)). +Check (eq_refl (SF64succ (Prim2SF f12)) <<: Prim2SF (next_up f12) = SF64succ (Prim2SF f12)). +Check (eq_refl (SF64pred (Prim2SF f12)) <<: Prim2SF (next_down f12) = SF64pred (Prim2SF f12)). +Check (eq_refl (SF64succ (Prim2SF f13)) <<: Prim2SF (next_up f13) = SF64succ (Prim2SF f13)). +Check (eq_refl (SF64pred (Prim2SF f13)) <<: Prim2SF (next_down f13) = SF64pred (Prim2SF f13)). +Check (eq_refl (SF64succ (Prim2SF f14)) <<: Prim2SF (next_up f14) = SF64succ (Prim2SF f14)). +Check (eq_refl (SF64pred (Prim2SF f14)) <<: Prim2SF (next_down f14) = SF64pred (Prim2SF f14)). +Check (eq_refl (SF64succ (Prim2SF f15)) <<: Prim2SF (next_up f15) = SF64succ (Prim2SF f15)). +Check (eq_refl (SF64pred (Prim2SF f15)) <<: Prim2SF (next_down f15) = SF64pred (Prim2SF f15)). diff --git a/test-suite/primitive/float/normfr_mantissa.v b/test-suite/primitive/float/normfr_mantissa.v new file mode 100644 index 0000000000..28bd1c03f5 --- /dev/null +++ b/test-suite/primitive/float/normfr_mantissa.v @@ -0,0 +1,28 @@ +Require Import Int63 ZArith Floats. + +Definition half := ldexp one (-1)%Z. +Definition three_quarters := (half + (ldexp one (-2)%Z))%float. + +Check (eq_refl : normfr_mantissa one = 0%int63). +Check (eq_refl : normfr_mantissa half = (1 << 52)%int63). +Check (eq_refl : normfr_mantissa (-half) = (1 << 52)%int63). +Check (eq_refl : normfr_mantissa (-one) = 0%int63). +Check (eq_refl : normfr_mantissa zero = 0%int63). +Check (eq_refl : normfr_mantissa nan = 0%int63). +Check (eq_refl : normfr_mantissa three_quarters = (3 << 51)%int63). + +Check (eq_refl 0%int63 <: normfr_mantissa one = 0%int63). +Check (eq_refl (1 << 52)%int63 <: normfr_mantissa half = (1 << 52)%int63). +Check (eq_refl (1 << 52)%int63 <: normfr_mantissa (-half) = (1 << 52)%int63). +Check (eq_refl 0%int63 <: normfr_mantissa (-one) = 0%int63). +Check (eq_refl 0%int63 <: normfr_mantissa zero = 0%int63). +Check (eq_refl 0%int63 <: normfr_mantissa nan = 0%int63). +Check (eq_refl (3 << 51)%int63 <: normfr_mantissa three_quarters = (3 << 51)%int63). + +Check (eq_refl 0%int63 <<: normfr_mantissa one = 0%int63). +Check (eq_refl (1 << 52)%int63 <<: normfr_mantissa half = (1 << 52)%int63). +Check (eq_refl (1 << 52)%int63 <<: normfr_mantissa (-half) = (1 << 52)%int63). +Check (eq_refl 0%int63 <<: normfr_mantissa (-one) = 0%int63). +Check (eq_refl 0%int63 <<: normfr_mantissa zero = 0%int63). +Check (eq_refl 0%int63 <<: normfr_mantissa nan = 0%int63). +Check (eq_refl (3 << 51)%int63 <<: normfr_mantissa three_quarters = (3 << 51)%int63). diff --git a/test-suite/primitive/float/spec_conv.v b/test-suite/primitive/float/spec_conv.v new file mode 100644 index 0000000000..a610d39671 --- /dev/null +++ b/test-suite/primitive/float/spec_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 (-1023)%Z. +Definition denorm := Eval compute in ldexp one (-1074)%Z. + +Check (eq_refl : SF2Prim (Prim2SF zero) = zero). +Check (eq_refl : SF2Prim (Prim2SF neg_zero) = neg_zero). +Check (eq_refl : SF2Prim (Prim2SF one) = one). +Check (eq_refl : SF2Prim (Prim2SF (-one)) = (-one)%float). +Check (eq_refl : SF2Prim (Prim2SF infinity) = infinity). +Check (eq_refl : SF2Prim (Prim2SF neg_infinity) = neg_infinity). +Check (eq_refl : SF2Prim (Prim2SF huge) = huge). +Check (eq_refl : SF2Prim (Prim2SF tiny) = tiny). +Check (eq_refl : SF2Prim (Prim2SF denorm) = denorm). +Check (eq_refl : SF2Prim (Prim2SF nan) = nan). +Check (eq_refl : SF2Prim (Prim2SF two) = two). +Check (eq_refl : SF2Prim (Prim2SF half) = half). + +Check (eq_refl zero <: SF2Prim (Prim2SF zero) = zero). +Check (eq_refl neg_zero <: SF2Prim (Prim2SF neg_zero) = neg_zero). +Check (eq_refl one <: SF2Prim (Prim2SF one) = one). +Check (eq_refl (-one)%float <: SF2Prim (Prim2SF (-one)) = (-one)%float). +Check (eq_refl infinity <: SF2Prim (Prim2SF infinity) = infinity). +Check (eq_refl neg_infinity <: SF2Prim (Prim2SF neg_infinity) = neg_infinity). +Check (eq_refl huge <: SF2Prim (Prim2SF huge) = huge). +Check (eq_refl tiny <: SF2Prim (Prim2SF tiny) = tiny). +Check (eq_refl denorm <: SF2Prim (Prim2SF denorm) = denorm). +Check (eq_refl nan <: SF2Prim (Prim2SF nan) = nan). +Check (eq_refl two <: SF2Prim (Prim2SF two) = two). +Check (eq_refl half <: SF2Prim (Prim2SF half) = half). + +Check (eq_refl zero <<: SF2Prim (Prim2SF zero) = zero). +Check (eq_refl neg_zero <<: SF2Prim (Prim2SF neg_zero) = neg_zero). +Check (eq_refl one <<: SF2Prim (Prim2SF one) = one). +Check (eq_refl (-one)%float <<: SF2Prim (Prim2SF (-one)) = (-one)%float). +Check (eq_refl infinity <<: SF2Prim (Prim2SF infinity) = infinity). +Check (eq_refl neg_infinity <<: SF2Prim (Prim2SF neg_infinity) = neg_infinity). +Check (eq_refl huge <<: SF2Prim (Prim2SF huge) = huge). +Check (eq_refl tiny <<: SF2Prim (Prim2SF tiny) = tiny). +Check (eq_refl denorm <<: SF2Prim (Prim2SF denorm) = denorm). +Check (eq_refl nan <<: SF2Prim (Prim2SF nan) = nan). +Check (eq_refl two <<: SF2Prim (Prim2SF two) = two). +Check (eq_refl half <<: SF2Prim (Prim2SF half) = half). diff --git a/test-suite/primitive/float/sqrt.v b/test-suite/primitive/float/sqrt.v new file mode 100644 index 0000000000..04c8ab035d --- /dev/null +++ b/test-suite/primitive/float/sqrt.v @@ -0,0 +1,49 @@ +Require Import ZArith Int63 Floats. + +Open Scope float_scope. + +Definition three := Eval compute in of_int63 3%int63. +Definition nine := Eval compute in of_int63 9%int63. + +Check (eq_refl : sqrt nine = three). +Check (eq_refl three <: sqrt nine = three). +Definition compute1 := Eval compute in sqrt nine. +Check (eq_refl : three = three). + +Definition huge := Eval compute in ldexp one (1023)%Z. +Definition tiny := Eval compute in ldexp one (-1023)%Z. +Definition denorm := Eval compute in ldexp one (-1074)%Z. + +Goal (Prim2SF (sqrt huge) = SF64sqrt (Prim2SF huge)). + now compute. Undo. now vm_compute. +Qed. + +Goal (Prim2SF (sqrt tiny) = SF64sqrt (Prim2SF tiny)). + now compute. Undo. now vm_compute. +Qed. + +Goal (Prim2SF (sqrt denorm) = SF64sqrt (Prim2SF denorm)). + now compute. Undo. now vm_compute. +Qed. + +Check (eq_refl : sqrt neg_zero = neg_zero). +Check (eq_refl neg_zero <: sqrt neg_zero = neg_zero). +Check (eq_refl neg_zero <<: sqrt neg_zero = neg_zero). +Check (eq_refl : sqrt zero = zero). +Check (eq_refl zero <: sqrt zero = zero). +Check (eq_refl zero <<: sqrt zero = zero). +Check (eq_refl : sqrt one = one). +Check (eq_refl one <: sqrt one = one). +Check (eq_refl one <<: sqrt one = one). +Check (eq_refl : sqrt (-one) = nan). +Check (eq_refl nan <: sqrt (-one) = nan). +Check (eq_refl nan <<: sqrt (-one) = nan). +Check (eq_refl : sqrt infinity = infinity). +Check (eq_refl infinity <: sqrt infinity = infinity). +Check (eq_refl infinity <<: sqrt infinity = infinity). +Check (eq_refl : sqrt neg_infinity = nan). +Check (eq_refl nan <: sqrt neg_infinity = nan). +Check (eq_refl nan <<: sqrt neg_infinity = nan). +Check (eq_refl : sqrt infinity = infinity). +Check (eq_refl infinity <: sqrt infinity = infinity). +Check (eq_refl infinity <<: sqrt infinity = infinity). diff --git a/test-suite/primitive/float/sub.v b/test-suite/primitive/float/sub.v new file mode 100644 index 0000000000..fc068cb585 --- /dev/null +++ b/test-suite/primitive/float/sub.v @@ -0,0 +1,62 @@ +Require Import ZArith Int63 Floats. + +Open Scope float_scope. + +Definition two := Eval compute in of_int63 2%int63. +Definition three := Eval compute in of_int63 3%int63. + +Check (eq_refl : three - two = one). +Check (eq_refl one <: three - two = one). +Check (eq_refl one <<: three - two = one). +Definition compute1 := Eval compute in three - two. +Check (eq_refl compute1 : one = one). + +Definition huge := Eval compute in ldexp one 1023%Z. +Definition tiny := Eval compute in ldexp one (-1023)%Z. + +Check (eq_refl : huge - tiny = huge). +Check (eq_refl huge <: huge - tiny = huge). +Check (eq_refl huge <<: huge - tiny = huge). +Definition compute2 := Eval compute in huge - tiny. +Check (eq_refl compute2 : huge = huge). + +Check (eq_refl : huge - huge = zero). +Check (eq_refl zero <: huge - huge = zero). +Check (eq_refl zero <<: huge - huge = zero). +Definition compute3 := Eval compute in huge - huge. +Check (eq_refl compute3 : zero = zero). + +Check (eq_refl : one - nan = nan). +Check (eq_refl nan <: one - nan = nan). +Check (eq_refl nan <<: one - nan = nan). +Definition compute4 := Eval compute in one - nan. +Check (eq_refl compute4 : nan = nan). + +Check (eq_refl : infinity - infinity = nan). +Check (eq_refl nan <: infinity - infinity = nan). +Check (eq_refl nan <<: infinity - infinity = nan). +Definition compute5 := Eval compute in infinity - infinity. +Check (eq_refl compute5 : nan = nan). + +Check (eq_refl : infinity - neg_infinity = infinity). +Check (eq_refl infinity <: infinity - neg_infinity = infinity). +Check (eq_refl infinity <<: infinity - neg_infinity = infinity). +Definition compute6 := Eval compute in infinity - neg_infinity. +Check (eq_refl compute6 : infinity = infinity). + +Check (eq_refl : zero - zero = zero). +Check (eq_refl zero <: zero - zero = zero). +Check (eq_refl zero <<: zero - zero = zero). +Check (eq_refl : neg_zero - zero = neg_zero). +Check (eq_refl neg_zero <: neg_zero - zero = neg_zero). +Check (eq_refl neg_zero <<: neg_zero - zero = neg_zero). +Check (eq_refl : neg_zero - neg_zero = zero). +Check (eq_refl zero <: neg_zero - neg_zero = zero). +Check (eq_refl zero <<: neg_zero - neg_zero = zero). +Check (eq_refl : zero - neg_zero = zero). +Check (eq_refl zero <: zero - neg_zero = zero). +Check (eq_refl zero <<: zero - neg_zero = zero). + +Check (eq_refl : huge - neg_infinity = infinity). +Check (eq_refl infinity <: huge - neg_infinity = infinity). +Check (eq_refl infinity <<: huge - neg_infinity = infinity). diff --git a/test-suite/primitive/float/syntax.v b/test-suite/primitive/float/syntax.v new file mode 100644 index 0000000000..cc0bbcf628 --- /dev/null +++ b/test-suite/primitive/float/syntax.v @@ -0,0 +1,13 @@ +Require Import Floats. + +Open Scope float_scope. + +Definition two := Eval compute in one + one. +Definition half := Eval compute in one / two. + +Check (eq_refl : 1.5 = one + half). +Check (eq_refl : 15e-1 = one + half). +Check (eq_refl : 150e-2 = one + half). +Check (eq_refl : 0.15e+1 = one + half). +Check (eq_refl : 0.15e1 = one + half). +Check (eq_refl : 0.0015e3 = one + half). 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). diff --git a/test-suite/primitive/float/zero.v b/test-suite/primitive/float/zero.v new file mode 100644 index 0000000000..75348d4657 --- /dev/null +++ b/test-suite/primitive/float/zero.v @@ -0,0 +1,7 @@ +Require Import ZArith Int63 Floats. + +Open Scope float_scope. + +Fail Check (eq_refl : zero = neg_zero). +Fail Check (eq_refl <: zero = neg_zero). +Fail Check (eq_refl <<: zero = neg_zero). |