Add tests for primitive floats with 'vm_compute'

Tests are updated to include VM computations and check for double
rounding.

11 files changed, 133 insertions, 7 deletions

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