From 1b0bd3a9e3a913a4928b68546a134a1a4448f9e8 Mon Sep 17 00:00:00 2001
From: Guillaume Bertholon
Date: Mon, 16 Jul 2018 13:30:37 +0200
Subject: Add tests for primitive floats

Add utility ldexp and frexp functions to prevent dealing with the shift of
ldshiftexp and frshiftexp everywhere.

Also move primitive integer tests to place all primitive tests in the
same directory.
---
 test-suite/primitive/float/add.v               | 45 +++++++++++++++++++++++
 test-suite/primitive/float/div.v               | 51 ++++++++++++++++++++++++++
 test-suite/primitive/float/double_rounding.v   | 20 ++++++++++
 test-suite/primitive/float/frexp.v             | 16 ++++++++
 test-suite/primitive/float/mul.v               | 49 +++++++++++++++++++++++++
 test-suite/primitive/float/normfr_mantissa.v   | 12 ++++++
 test-suite/primitive/float/spec_conv.v         | 20 ++++++++++
 test-suite/primitive/float/sqrt.v              | 33 +++++++++++++++++
 test-suite/primitive/float/sub.v               | 40 ++++++++++++++++++++
 test-suite/primitive/float/valid_binary_conv.v | 20 ++++++++++
 test-suite/primitive/float/zero.v              |  7 ++++
 11 files changed, 313 insertions(+)
 create mode 100644 test-suite/primitive/float/add.v
 create mode 100644 test-suite/primitive/float/div.v
 create mode 100644 test-suite/primitive/float/double_rounding.v
 create mode 100644 test-suite/primitive/float/frexp.v
 create mode 100644 test-suite/primitive/float/mul.v
 create mode 100644 test-suite/primitive/float/normfr_mantissa.v
 create mode 100644 test-suite/primitive/float/spec_conv.v
 create mode 100644 test-suite/primitive/float/sqrt.v
 create mode 100644 test-suite/primitive/float/sub.v
 create mode 100644 test-suite/primitive/float/valid_binary_conv.v
 create mode 100644 test-suite/primitive/float/zero.v

(limited to 'test-suite/primitive/float')

diff --git a/test-suite/primitive/float/add.v b/test-suite/primitive/float/add.v
new file mode 100644
index 0000000000..cd157ede83
--- /dev/null
+++ b/test-suite/primitive/float/add.v
@@ -0,0 +1,45 @@
+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 5 <<: 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).
+Definition compute3 := Eval compute in huge + huge.
+Check (eq_refl compute3 : infinity = infinity).
+
+Check (eq_refl : one + nan = nan).
+Definition compute4 := Eval compute in one + nan.
+Check (eq_refl compute4 : nan = nan).
+
+Check (eq_refl : infinity + infinity = infinity).
+Definition compute5 := Eval compute in infinity + infinity.
+Check (eq_refl compute5 : infinity = infinity).
+
+Check (eq_refl : 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 : neg_zero + zero = zero).
+Check (eq_refl : neg_zero + neg_zero = neg_zero).
+Check (eq_refl : zero + neg_zero = zero).
+
+Check (eq_refl : huge + neg_infinity = neg_infinity).
diff --git a/test-suite/primitive/float/div.v b/test-suite/primitive/float/div.v
new file mode 100644
index 0000000000..b2e9278e71
--- /dev/null
+++ b/test-suite/primitive/float/div.v
@@ -0,0 +1,51 @@
+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).
+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).
+Definition compute2 := Eval compute in huge / tiny.
+Check (eq_refl compute2 : infinity = infinity).
+
+Check (eq_refl : huge / huge = one).
+Definition compute3 := Eval compute in huge / huge.
+Check (eq_refl compute3 : one = one).
+
+Check (eq_refl : one / nan = nan).
+Definition compute4 := Eval compute in one / nan.
+Check (eq_refl compute4 : nan = nan).
+
+Check (eq_refl : infinity / infinity = nan).
+Definition compute5 := Eval compute in infinity / infinity.
+Check (eq_refl compute5 : nan = nan).
+
+Check (eq_refl : 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 : neg_zero / zero = nan).
+
+Check (eq_refl : huge / neg_infinity = neg_zero).
+
+Check (eq_refl : one / tiny = huge).
+Check (eq_refl : one / huge = tiny).
+Check (eq_refl : zero / huge = zero).
+Check (eq_refl : zero / (-huge) = neg_zero).
+
+Check (eq_refl : tiny / one = tiny).
+Check (eq_refl : huge / one = huge).
+Check (eq_refl : infinity / one = infinity).
+
+Check (eq_refl : zero / infinity = zero).
+Check (eq_refl : 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..92322ea473
--- /dev/null
+++ b/test-suite/primitive/float/double_rounding.v
@@ -0,0 +1,20 @@
+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 = Some Gt).
+Check (eq_refl : (check_cbn ?= big_cbn)%float = Some Eq).
+
+
+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 = Some Gt).
+Check (eq_refl : (check_cbv ?= big_cbv)%float = Some Eq).
diff --git a/test-suite/primitive/float/frexp.v b/test-suite/primitive/float/frexp.v
new file mode 100644
index 0000000000..254dfa7028
--- /dev/null
+++ b/test-suite/primitive/float/frexp.v
@@ -0,0 +1,16 @@
+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 : 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 : 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 : let (m,e) := frexp denorm in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF denorm)).
diff --git a/test-suite/primitive/float/mul.v b/test-suite/primitive/float/mul.v
new file mode 100644
index 0000000000..99b431896f
--- /dev/null
+++ b/test-suite/primitive/float/mul.v
@@ -0,0 +1,49 @@
+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).
+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).
+Definition compute2 := Eval compute in huge * tiny.
+Check (eq_refl compute2 : one = one).
+
+Check (eq_refl : huge * huge = infinity).
+Definition compute3 := Eval compute in huge * huge.
+Check (eq_refl compute3 : infinity = infinity).
+
+Check (eq_refl : one * nan = nan).
+Definition compute4 := Eval compute in one * nan.
+Check (eq_refl compute4 : nan = nan).
+
+Check (eq_refl : infinity * infinity = infinity).
+Definition compute5 := Eval compute in infinity * infinity.
+Check (eq_refl compute5 : infinity = infinity).
+
+Check (eq_refl : 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 : neg_zero * zero = neg_zero).
+Check (eq_refl : neg_zero * neg_zero = zero).
+Check (eq_refl : zero * neg_zero = neg_zero).
+
+Check (eq_refl : huge * neg_infinity = neg_infinity).
+
+Check (eq_refl : one * tiny = tiny).
+Check (eq_refl : one * huge = huge).
+Check (eq_refl : zero * huge = zero).
+Check (eq_refl : zero * (-huge) = neg_zero).
+
+Check (eq_refl : zero * infinity = nan).
+Check (eq_refl : neg_infinity * zero = nan).
diff --git a/test-suite/primitive/float/normfr_mantissa.v b/test-suite/primitive/float/normfr_mantissa.v
new file mode 100644
index 0000000000..6cc9f5ef92
--- /dev/null
+++ b/test-suite/primitive/float/normfr_mantissa.v
@@ -0,0 +1,12 @@
+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).
diff --git a/test-suite/primitive/float/spec_conv.v b/test-suite/primitive/float/spec_conv.v
new file mode 100644
index 0000000000..12a5fe4dca
--- /dev/null
+++ b/test-suite/primitive/float/spec_conv.v
@@ -0,0 +1,20 @@
+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).
diff --git a/test-suite/primitive/float/sqrt.v b/test-suite/primitive/float/sqrt.v
new file mode 100644
index 0000000000..0bacda9686
--- /dev/null
+++ b/test-suite/primitive/float/sqrt.v
@@ -0,0 +1,33 @@
+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).
+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.
+Qed.
+
+Goal (Prim2SF (sqrt tiny) = SF64sqrt (Prim2SF tiny)).
+  now compute.
+Qed.
+
+Goal (Prim2SF (sqrt denorm) = SF64sqrt (Prim2SF denorm)).
+  now compute.
+Qed.
+
+Check (eq_refl : sqrt neg_zero = neg_zero).
+Check (eq_refl : sqrt zero = zero).
+Check (eq_refl : sqrt one = one).
+Check (eq_refl : sqrt (-one) = nan).
+Check (eq_refl : sqrt infinity = infinity).
+Check (eq_refl : sqrt neg_infinity = nan).
diff --git a/test-suite/primitive/float/sub.v b/test-suite/primitive/float/sub.v
new file mode 100644
index 0000000000..0796ff51ff
--- /dev/null
+++ b/test-suite/primitive/float/sub.v
@@ -0,0 +1,40 @@
+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).
+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).
+Definition compute2 := Eval compute in huge - tiny.
+Check (eq_refl compute2 : huge = huge).
+
+Check (eq_refl : huge - huge = zero).
+Definition compute3 := Eval compute in huge - huge.
+Check (eq_refl compute3 : zero = zero).
+
+Check (eq_refl : one - nan = nan).
+Definition compute4 := Eval compute in one - nan.
+Check (eq_refl compute4 : nan = nan).
+
+Check (eq_refl : infinity - infinity = nan).
+Definition compute5 := Eval compute in infinity - infinity.
+Check (eq_refl compute5 : nan = nan).
+
+Check (eq_refl : 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 : neg_zero - zero = neg_zero).
+Check (eq_refl : neg_zero - neg_zero = zero).
+Check (eq_refl : zero - neg_zero = zero).
+
+Check (eq_refl : huge - neg_infinity = infinity).
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..ad81e55667
--- /dev/null
+++ b/test-suite/primitive/float/valid_binary_conv.v
@@ -0,0 +1,20 @@
+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).
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).
-- 
cgit v1.2.3


From 55d32c9f3a91058f69f34c17c17701d0dc81874d Mon Sep 17 00:00:00 2001
From: Guillaume Bertholon
Date: Thu, 19 Jul 2018 13:33:17 +0200
Subject: Add tests for primitive floats with 'vm_compute'

Tests are updated to include VM computations and check for double
rounding.
---
 test-suite/primitive/float/add.v                  | 17 +++++++++++++----
 test-suite/primitive/float/coq_env_double_array.v | 13 +++++++++++++
 test-suite/primitive/float/div.v                  | 18 ++++++++++++++++++
 test-suite/primitive/float/double_rounding.v      |  9 +++++++++
 test-suite/primitive/float/frexp.v                |  6 ++++++
 test-suite/primitive/float/mul.v                  | 17 +++++++++++++++++
 test-suite/primitive/float/normfr_mantissa.v      |  8 ++++++++
 test-suite/primitive/float/spec_conv.v            | 13 +++++++++++++
 test-suite/primitive/float/sqrt.v                 | 15 ++++++++++++---
 test-suite/primitive/float/sub.v                  | 11 +++++++++++
 test-suite/primitive/float/valid_binary_conv.v    | 13 +++++++++++++
 11 files changed, 133 insertions(+), 7 deletions(-)
 create mode 100644 test-suite/primitive/float/coq_env_double_array.v

(limited to 'test-suite/primitive/float')

diff --git a/test-suite/primitive/float/add.v b/test-suite/primitive/float/add.v
index cd157ede83..5b15eb2fa7 100644
--- a/test-suite/primitive/float/add.v
+++ b/test-suite/primitive/float/add.v
@@ -7,8 +7,8 @@ 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 5 <<: 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).
 
@@ -16,30 +16,39 @@ 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).*)
+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).
 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).
 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).
 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).
 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 : 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 : 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).
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
index b2e9278e71..5c231192fd 100644
--- a/test-suite/primitive/float/div.v
+++ b/test-suite/primitive/float/div.v
@@ -7,6 +7,7 @@ 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).
 Definition compute1 := Eval compute in six / three.
 Check (eq_refl compute1 : two = two).
 
@@ -14,38 +15,55 @@ 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).
 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).
 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).
 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).
 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).
 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 : 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 : 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 : 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 : 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 : 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 : 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
index 92322ea473..04c91cd56a 100644
--- a/test-suite/primitive/float/double_rounding.v
+++ b/test-suite/primitive/float/double_rounding.v
@@ -18,3 +18,12 @@ Definition check_cbv := Eval cbv in (big_cbv + one)%float.
 
 Check (eq_refl : (result_cbv ?= big_cbv)%float = Some Gt).
 Check (eq_refl : (check_cbv ?= big_cbv)%float = Some Eq).
+
+
+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 = Some Gt).
+Check (eq_refl : (check_vm ?= big_vm)%float = Some Eq).
diff --git a/test-suite/primitive/float/frexp.v b/test-suite/primitive/float/frexp.v
index 254dfa7028..3a3cbed4e2 100644
--- a/test-suite/primitive/float/frexp.v
+++ b/test-suite/primitive/float/frexp.v
@@ -4,13 +4,19 @@ 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 : 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 : 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 : 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/mul.v b/test-suite/primitive/float/mul.v
index 99b431896f..a335889c05 100644
--- a/test-suite/primitive/float/mul.v
+++ b/test-suite/primitive/float/mul.v
@@ -7,6 +7,7 @@ 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).
 Definition compute1 := Eval compute in three * two.
 Check (eq_refl compute1 : six = six).
 
@@ -14,36 +15,52 @@ 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).
 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).
 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).
 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).
 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).
 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 : 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).
+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 : 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 : 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 : 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).
diff --git a/test-suite/primitive/float/normfr_mantissa.v b/test-suite/primitive/float/normfr_mantissa.v
index 6cc9f5ef92..e1a465a9e1 100644
--- a/test-suite/primitive/float/normfr_mantissa.v
+++ b/test-suite/primitive/float/normfr_mantissa.v
@@ -10,3 +10,11 @@ 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).
diff --git a/test-suite/primitive/float/spec_conv.v b/test-suite/primitive/float/spec_conv.v
index 12a5fe4dca..d7e87275a9 100644
--- a/test-suite/primitive/float/spec_conv.v
+++ b/test-suite/primitive/float/spec_conv.v
@@ -18,3 +18,16 @@ 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).
diff --git a/test-suite/primitive/float/sqrt.v b/test-suite/primitive/float/sqrt.v
index 0bacda9686..89d76ab870 100644
--- a/test-suite/primitive/float/sqrt.v
+++ b/test-suite/primitive/float/sqrt.v
@@ -6,6 +6,7 @@ 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).
 
@@ -14,20 +15,28 @@ 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.
+  now compute. Undo. now vm_compute.
 Qed.
 
 Goal (Prim2SF (sqrt tiny) = SF64sqrt (Prim2SF tiny)).
-  now compute.
+  now compute. Undo. now vm_compute.
 Qed.
 
 Goal (Prim2SF (sqrt denorm) = SF64sqrt (Prim2SF denorm)).
-  now compute.
+  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 : 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 : 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 : 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).
diff --git a/test-suite/primitive/float/sub.v b/test-suite/primitive/float/sub.v
index 0796ff51ff..af21d2c656 100644
--- a/test-suite/primitive/float/sub.v
+++ b/test-suite/primitive/float/sub.v
@@ -6,6 +6,7 @@ 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).
 Definition compute1 := Eval compute in three - two.
 Check (eq_refl compute1 : one = one).
 
@@ -13,28 +14,38 @@ 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).
 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).
 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).
 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).
 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).
 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 : 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 = zero).
+Check (eq_refl zero <: zero - neg_zero = zero).
 
 Check (eq_refl : huge - neg_infinity = infinity).
+Check (eq_refl infinity <: huge - neg_infinity = infinity).
diff --git a/test-suite/primitive/float/valid_binary_conv.v b/test-suite/primitive/float/valid_binary_conv.v
index ad81e55667..53fad1a74c 100644
--- a/test-suite/primitive/float/valid_binary_conv.v
+++ b/test-suite/primitive/float/valid_binary_conv.v
@@ -18,3 +18,16 @@ 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).
-- 
cgit v1.2.3


From 79605dabb10e889ae998bf72c8483f095277e693 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 28 Aug 2018 14:31:37 +0200
Subject: Change return type of primitive float comparison

Replace `option comparison` with `float_comparison` (:= `FEq | FLt |
FGt | FNotComparable`) as suggested by Guillaume Melquiond to avoid
boxing and an extra match when using primitive float comparison.
---
 test-suite/primitive/float/double_rounding.v | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'test-suite/primitive/float')

diff --git a/test-suite/primitive/float/double_rounding.v b/test-suite/primitive/float/double_rounding.v
index 04c91cd56a..8aa9b4ca45 100644
--- a/test-suite/primitive/float/double_rounding.v
+++ b/test-suite/primitive/float/double_rounding.v
@@ -7,8 +7,8 @@ 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 = Some Gt).
-Check (eq_refl : (check_cbn ?= big_cbn)%float = Some Eq).
+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.
@@ -16,8 +16,8 @@ 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 = Some Gt).
-Check (eq_refl : (check_cbv ?= big_cbv)%float = Some Eq).
+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.
@@ -25,5 +25,5 @@ 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 = Some Gt).
-Check (eq_refl : (check_vm ?= big_vm)%float = Some Eq).
+Check (eq_refl : (result_vm ?= big_vm)%float = FGt).
+Check (eq_refl : (check_vm ?= big_vm)%float = FEq).
-- 
cgit v1.2.3


From d18b928154a48ff8d90aaff69eca7d6eb3dfa0ab Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 28 Aug 2018 18:56:07 +0200
Subject: Implement classify on primitive float

---
 test-suite/primitive/float/classify.v | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)
 create mode 100644 test-suite/primitive/float/classify.v

(limited to 'test-suite/primitive/float')

diff --git a/test-suite/primitive/float/classify.v b/test-suite/primitive/float/classify.v
new file mode 100644
index 0000000000..e4373415cb
--- /dev/null
+++ b/test-suite/primitive/float/classify.v
@@ -0,0 +1,23 @@
+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).
-- 
cgit v1.2.3


From 5f1270242f71a0a1da7c868967e1071d28ed83fb Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 28 Aug 2018 23:37:49 +0200
Subject: Add next_{up,down} primitive float functions

---
 test-suite/primitive/float/next_up_down.v | 89 +++++++++++++++++++++++++++++++
 1 file changed, 89 insertions(+)
 create mode 100644 test-suite/primitive/float/next_up_down.v

(limited to 'test-suite/primitive/float')

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..95f5248bf7
--- /dev/null
+++ b/test-suite/primitive/float/next_up_down.v
@@ -0,0 +1,89 @@
+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)).
-- 
cgit v1.2.3


From f0bf1511e59e528e090a87cfcc220f93c2431ecd Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Sun, 9 Jun 2019 10:41:10 +0200
Subject: Add tests for primitive floats with 'native_compute'

Tests are updated to include native computations.
---
 test-suite/primitive/float/add.v               | 13 ++++++++--
 test-suite/primitive/float/classify.v          | 10 ++++++++
 test-suite/primitive/float/div.v               | 18 ++++++++++++++
 test-suite/primitive/float/double_rounding.v   |  9 +++++++
 test-suite/primitive/float/frexp.v             |  6 +++++
 test-suite/primitive/float/mul.v               | 17 +++++++++++++
 test-suite/primitive/float/next_up_down.v      | 33 ++++++++++++++++++++++++++
 test-suite/primitive/float/normfr_mantissa.v   |  8 +++++++
 test-suite/primitive/float/spec_conv.v         | 13 ++++++++++
 test-suite/primitive/float/sqrt.v              |  7 ++++++
 test-suite/primitive/float/sub.v               | 11 +++++++++
 test-suite/primitive/float/valid_binary_conv.v | 13 ++++++++++
 12 files changed, 156 insertions(+), 2 deletions(-)

(limited to 'test-suite/primitive/float')

diff --git a/test-suite/primitive/float/add.v b/test-suite/primitive/float/add.v
index 5b15eb2fa7..f8c5939d0a 100644
--- a/test-suite/primitive/float/add.v
+++ b/test-suite/primitive/float/add.v
@@ -8,7 +8,7 @@ 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).*)
+Check (eq_refl five <<: two + three = five).
 Definition compute1 := Eval compute in two + three.
 Check (eq_refl compute1 : five = five).
 
@@ -17,38 +17,47 @@ 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).*)
+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
index e4373415cb..22e3fca844 100644
--- a/test-suite/primitive/float/classify.v
+++ b/test-suite/primitive/float/classify.v
@@ -21,3 +21,13 @@ 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/div.v b/test-suite/primitive/float/div.v
index 5c231192fd..8e971f575b 100644
--- a/test-suite/primitive/float/div.v
+++ b/test-suite/primitive/float/div.v
@@ -8,6 +8,7 @@ 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).
 
@@ -16,54 +17,71 @@ 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
index 8aa9b4ca45..e2356cdd7b 100644
--- a/test-suite/primitive/float/double_rounding.v
+++ b/test-suite/primitive/float/double_rounding.v
@@ -27,3 +27,12 @@ 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
index 3a3cbed4e2..2a600429b1 100644
--- a/test-suite/primitive/float/frexp.v
+++ b/test-suite/primitive/float/frexp.v
@@ -5,18 +5,24 @@ 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/mul.v b/test-suite/primitive/float/mul.v
index a335889c05..91fe7e9791 100644
--- a/test-suite/primitive/float/mul.v
+++ b/test-suite/primitive/float/mul.v
@@ -8,6 +8,7 @@ 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).
 
@@ -16,51 +17,67 @@ 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
index 95f5248bf7..4f8427dc5b 100644
--- a/test-suite/primitive/float/next_up_down.v
+++ b/test-suite/primitive/float/next_up_down.v
@@ -87,3 +87,36 @@ Check (eq_refl (SF64succ (Prim2SF f14)) <: Prim2SF (next_up f14) = SF64succ (Pri
 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
index e1a465a9e1..28bd1c03f5 100644
--- a/test-suite/primitive/float/normfr_mantissa.v
+++ b/test-suite/primitive/float/normfr_mantissa.v
@@ -18,3 +18,11 @@ 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
index d7e87275a9..a610d39671 100644
--- a/test-suite/primitive/float/spec_conv.v
+++ b/test-suite/primitive/float/spec_conv.v
@@ -31,3 +31,16 @@ 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
index 89d76ab870..04c8ab035d 100644
--- a/test-suite/primitive/float/sqrt.v
+++ b/test-suite/primitive/float/sqrt.v
@@ -28,15 +28,22 @@ 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
index af21d2c656..fc068cb585 100644
--- a/test-suite/primitive/float/sub.v
+++ b/test-suite/primitive/float/sub.v
@@ -7,6 +7,7 @@ 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).
 
@@ -15,37 +16,47 @@ 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/valid_binary_conv.v b/test-suite/primitive/float/valid_binary_conv.v
index 53fad1a74c..82e00b8532 100644
--- a/test-suite/primitive/float/valid_binary_conv.v
+++ b/test-suite/primitive/float/valid_binary_conv.v
@@ -31,3 +31,16 @@ 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).
-- 
cgit v1.2.3


From fdfcadc111fb5618a8e4a769c50607dc920b7dec Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Sat, 20 Oct 2018 23:43:07 +0200
Subject: Parsing primitive float constants

---
 test-suite/primitive/float/syntax.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 test-suite/primitive/float/syntax.v

(limited to 'test-suite/primitive/float')

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).
-- 
cgit v1.2.3


From dca0135a263717b3a1a1d7c4f054f039dc08109e Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 4 Apr 2019 00:14:47 +0200
Subject: Make primitive float work on x86_32

Flag -fexcess-precision=standard is not enough on x86_32
where -msse2 -mfpmath=sse is required (-msse is not enough)
to avoid double rounding issues in the VM.

Most floating-point operation are now implemented in C because OCaml
is suffering double rounding issues on x86_32 with 80 bits extended
precision registers used for floating-point values, causing double
rounding making floating-point arithmetic incorrect with respect to
its specification.

Add a runtime test for double roundings.
---
 test-suite/primitive/float/frexp.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'test-suite/primitive/float')

diff --git a/test-suite/primitive/float/frexp.v b/test-suite/primitive/float/frexp.v
index 2a600429b1..f13d5cebf6 100644
--- a/test-suite/primitive/float/frexp.v
+++ b/test-suite/primitive/float/frexp.v
@@ -1,3 +1,5 @@
+(* TODO add tests for ldexp (particularly with overflow with 31 and 63 bits integers) *)
+
 Require Import ZArith Floats.
 
 Definition denorm := Eval compute in ldexp one (-1074)%Z.
-- 
cgit v1.2.3


From f155ba664a782f000e278d97ee5666e2e7d2adea Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 3 Jul 2019 15:08:44 +0200
Subject: Add "==", "<", "<=" in PrimFloat.v

* Add a related test-suite in compare.v (generated by a bash script)

Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
---
 test-suite/primitive/float/compare.v      | 385 ++++++++++++++++++++++++++++++
 test-suite/primitive/float/gen_compare.sh |  65 +++++
 2 files changed, 450 insertions(+)
 create mode 100644 test-suite/primitive/float/compare.v
 create mode 100755 test-suite/primitive/float/gen_compare.sh

(limited to 'test-suite/primitive/float')

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/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[@]}"
-- 
cgit v1.2.3


From d39fab9a7c39d8da868c4481b96cf1086c21b1a4 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 10 Oct 2019 20:11:02 +0200
Subject: Fix ldshiftexp

* Fix the implementations and add tests
* Change shift from int63 to Z (was always used as a Z)
* Update FloatLemmas.v accordingly

Co-authored-by: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
---
 test-suite/primitive/float/frexp.v |  2 --
 test-suite/primitive/float/ldexp.v | 21 +++++++++++++++++++++
 2 files changed, 21 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/primitive/float/ldexp.v

(limited to 'test-suite/primitive/float')

diff --git a/test-suite/primitive/float/frexp.v b/test-suite/primitive/float/frexp.v
index f13d5cebf6..2a600429b1 100644
--- a/test-suite/primitive/float/frexp.v
+++ b/test-suite/primitive/float/frexp.v
@@ -1,5 +1,3 @@
-(* TODO add tests for ldexp (particularly with overflow with 31 and 63 bits integers) *)
-
 Require Import ZArith Floats.
 
 Definition denorm := Eval compute in ldexp one (-1074)%Z.
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).
-- 
cgit v1.2.3