Merge PR #13147: Use OCaml floating-point operations on 64 bits arch

Reviewed-by: erikmd
Reviewed-by: silene

1 files changed, 35 insertions, 0 deletions

diff --git a/kernel/float64_63.ml b/kernel/float64_63.ml
new file mode 100644
index 0000000000..0025531cb1
--- /dev/null
+++ b/kernel/float64_63.ml
@@ -0,0 +1,35 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+include Float64_common
+
+let mul (x : float) (y : float) : float = x *. y
+[@@ocaml.inline always]
+
+let add (x : float) (y : float) : float = x +. y
+[@@ocaml.inline always]
+
+let sub (x : float) (y : float) : float = x -. y
+[@@ocaml.inline always]
+
+let div (x : float) (y : float) : float = x /. y
+[@@ocaml.inline always]
+
+let sqrt (x : float) : float = sqrt x
+[@@ocaml.inline always]
+
+(*** Test at runtime that no harmful double rounding seems to
+   be performed with an intermediate 80 bits representation (x87). *)
+let () =
+  let b = ldexp 1. 53 in
+  let s = add 1. (ldexp 1. (-52)) in
+  if add b s <= b || add b 1. <> b || ldexp 1. (-1074) <= 0. then
+    failwith "Detected non IEEE-754 compliant architecture (or wrong \
+              rounding mode). Use of Float is thus unsafe."