Merge PR #9867: Add primitive floats (binary64 floating-point numbers)

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
Ack-by: proux01
Ack-by: silene
Ack-by: vbgl

1 files changed, 38 insertions, 0 deletions

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).