From dda50a88aab0fa0cfb74c8973b5a4353fe5c8447 Mon Sep 17 00:00:00 2001
From: Guillaume Bertholon
Date: Fri, 3 Aug 2018 17:38:48 +0200
Subject: Put axioms on ldshiftexp and frshiftexp

Axioms on ldexp and frexp are replaced by proofs inside FloatLemmas.

The shift value has been increased to 2 * emax + prec because in ldexp
we want to be able to transform the smallest denormalized to the biggest
float value in one call.
---
 kernel/byterun/coq_values.h | 2 +-
 kernel/float64.ml           | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index 14f3f152bf..fa51b2d31f 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -45,6 +45,6 @@
 #define coq_tag_Some 1
 #define coq_None Val_int(0)
 
-#define FLOAT_EXP_SHIFT (1022 + 52)
+#define FLOAT_EXP_SHIFT (2101) /* 2*emax + prec */
 
 #endif /* _COQ_VALUES_ */
diff --git a/kernel/float64.ml b/kernel/float64.ml
index 0b22e07e82..a625c0f551 100644
--- a/kernel/float64.ml
+++ b/kernel/float64.ml
@@ -51,7 +51,7 @@ let normfr_mantissa f =
   if f >= 0.5 && f < 1. then Uint63.of_float (ldexp f prec)
   else Uint63.zero
 
-let eshift = 1022 + 52 (* minimum negative exponent + binary precision *)
+let eshift = 2101 (* 2*emax + prec *)
 
 (* When calling frexp on a nan or an infinity, the returned value inside
    the exponent is undefined.
-- 
cgit v1.2.3