Upgrade embedded version of Flocq to 3.1.

Main changes to CompCert outside of Flocq are as follows:

- Minimal supported version of Coq is now 8.7, due to Flocq requirements.

- Most modifications are due to Z2R being dropped in favor of IZR and to
  the way Flocq now handles NaNs.

- CompCert now correctly handles NaNs for the Risc-V architecture
  (hopefully).

1 files changed, 16 insertions, 14 deletions

diff --git a/riscV/Archi.v b/riscV/Archi.v
index a1664262..3758d686 100644
--- a/riscV/Archi.v
+++ b/riscV/Archi.v
@@ -17,8 +17,8 @@
 (** Architecture-dependent parameters for RISC-V *)
 
 Require Import ZArith.
-Require Import Fappli_IEEE.
-Require Import Fappli_IEEE_bits.
+(*From Flocq*)
+Require Import Binary Bits.
 
 Parameter ptr64 : bool.
 
@@ -38,26 +38,28 @@ Qed.
    floating-point operation is NaN, it is the canonical NaN. The
    canonical NaN has a positive sign and all significand bits clear
    except the MSB, a.k.a. the quiet bit."
-   We need to extend the [choose_binop_pl] functions to account for
-   this case. *)
+   Exceptions are operations manipulating signs. *)
 
-Program Definition default_pl_64 : bool * nan_pl 53 :=
-  (false, iter_nat 51 _ xO xH).
+Definition default_nan_64 : { x : binary64 | is_nan _ _ x = true } :=
+  exist _ (B754_nan 53 1024 false (iter_nat 51 _ xO xH) (eq_refl true)) (eq_refl true).
 
-Definition choose_binop_pl_64 (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) :=
-  false.                        (**r always choose first NaN *)
+Definition choose_binop_pl_64 (pl1 pl2 : positive) :=
+  false.                        (**r irrelevant *)
 
-Program Definition default_pl_32 : bool * nan_pl 24 :=
-  (false, iter_nat 22 _ xO xH).
+Definition default_nan_32 : { x : binary32 | is_nan _ _ x = true } :=
+  exist _ (B754_nan 24 128 false (iter_nat 22 _ xO xH) (eq_refl true)) (eq_refl true).
 
-Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_pl 24) :=
-  false.                        (**r always choose first NaN *)
+Definition choose_binop_pl_32 (pl1 pl2 : positive) :=
+  false.                        (**r irrelevant *)
+
+Definition fpu_returns_default_qNaN := true.
 
 Definition float_of_single_preserves_sNaN := false.
 
 Global Opaque ptr64 big_endian splitlong
-              default_pl_64 choose_binop_pl_64
-              default_pl_32 choose_binop_pl_32
+              default_nan_64 choose_binop_pl_64
+              default_nan_32 choose_binop_pl_32
+              fpu_returns_default_qNaN
               float_of_single_preserves_sNaN.
 
 (** Whether to generate position-independent code or not *)