From b0b3cc67e01b165272588b2d8bc178840ba83945 Mon Sep 17 00:00:00 2001
From: Guillaume Bertholon
Date: Fri, 13 Jul 2018 16:22:35 +0200
Subject: Add primitive float computation in Coq kernel

Beware of 0. = -0. issue for primitive floats

The IEEE 754 declares that 0. and -0. are treated equal but we cannot
say that this is true with Leibniz equality.
Therefore we must patch the equality and the total comparison inside the
kernel to prevent inconsistency.
---
 kernel/uint63_63.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/uint63_63.ml')

diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml
index 5c4028e1c8..4c9377b628 100644
--- a/kernel/uint63_63.ml
+++ b/kernel/uint63_63.ml
@@ -27,6 +27,9 @@ let to_int2 i = (0,i)
 
 let of_int64 _i = assert false
 
+let of_float = int_of_float
+let to_float i = Int64.to_float (to_uint64 i)
+
 let hash i = i
 [@@ocaml.inline always]
 
-- 
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.
---
 kernel/uint63_63.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'kernel/uint63_63.ml')

diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml
index 4c9377b628..1776f904d6 100644
--- a/kernel/uint63_63.ml
+++ b/kernel/uint63_63.ml
@@ -27,8 +27,13 @@ let to_int2 i = (0,i)
 
 let of_int64 _i = assert false
 
+let to_int_saturate i = i
+
 let of_float = int_of_float
-let to_float i = Int64.to_float (to_uint64 i)
+
+external to_float : int -> (float [@unboxed])
+  = "coq_uint63_to_float_byte" "coq_uint63_to_float"
+[@@noalloc]
 
 let hash i = i
 [@@ocaml.inline always]
-- 
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>
---
 kernel/uint63_63.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'kernel/uint63_63.ml')

diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml
index 1776f904d6..85b44528a7 100644
--- a/kernel/uint63_63.ml
+++ b/kernel/uint63_63.ml
@@ -27,8 +27,6 @@ let to_int2 i = (0,i)
 
 let of_int64 _i = assert false
 
-let to_int_saturate i = i
-
 let of_float = int_of_float
 
 external to_float : int -> (float [@unboxed])
@@ -104,6 +102,10 @@ let le (x : int) (y : int) =
   (x lxor 0x4000000000000000) <= (y lxor 0x4000000000000000)
 [@@ocaml.inline always]
 
+let to_int_min n m =
+  if lt n m then n else m
+[@@ocaml.inline always]
+
     (* division of two numbers by one *)
 (* precondition: xh < y *)
 (* outputs: q, r s.t. x = q * y + r, r < y *)
-- 
cgit v1.2.3