Merge PR #11986: [primitive floats] Add low level printing

Ack-by: SkySkimmer
Reviewed-by: ppedrot

3 files changed, 33 insertions, 14 deletions

diff --git a/test-suite/output/FloatExtraction.out b/test-suite/output/FloatExtraction.out
index dd8189c56f..539ec9b2bf 100644
--- a/test-suite/output/FloatExtraction.out
+++ b/test-suite/output/FloatExtraction.out
@@ -1,16 +1,18 @@
 File "stdin", line 25, characters 8-12:
 Warning: The constant 0.01 is not a binary64 floating-point value. A closest
-value will be used and unambiguously printed 0.01. [inexact-float,parsing]
+value 0x1.47ae147ae147bp-7 will be used and unambiguously printed 0.01.
+[inexact-float,parsing]
 File "stdin", line 25, characters 20-25:
 Warning: The constant -0.01 is not a binary64 floating-point value. A closest
-value will be used and unambiguously printed -0.01. [inexact-float,parsing]
+value -0x1.47ae147ae147bp-7 will be used and unambiguously printed -0.01.
+[inexact-float,parsing]
 File "stdin", line 25, characters 27-35:
 Warning: The constant 1.7e+308 is not a binary64 floating-point value. A
-closest value will be used and unambiguously printed 1.6999999999999999e+308.
-[inexact-float,parsing]
+closest value 0x1.e42d130773b76p+1023 will be used and unambiguously printed
+1.6999999999999999e+308. [inexact-float,parsing]
 File "stdin", line 25, characters 37-46:
 Warning: The constant -1.7e-308 is not a binary64 floating-point value. A
-closest value will be used and unambiguously printed
+closest value -0x0.c396c98f8d899p-1022 will be used and unambiguously printed
 -1.7000000000000002e-308. [inexact-float,parsing]
 
 (** val infinity : Float64.t **)
diff --git a/test-suite/output/FloatSyntax.out b/test-suite/output/FloatSyntax.out
index 4a5a700879..0b18e9a3d2 100644
--- a/test-suite/output/FloatSyntax.out
+++ b/test-suite/output/FloatSyntax.out
@@ -6,13 +6,13 @@
      : float
 File "stdin", line 9, characters 6-13:
 Warning: The constant 2.5e123 is not a binary64 floating-point value. A
-closest value will be used and unambiguously printed 2.4999999999999999e+123.
-[inexact-float,parsing]
+closest value 0x1.e412f0f768fadp+409 will be used and unambiguously printed
+2.4999999999999999e+123. [inexact-float,parsing]
 2.4999999999999999e+123%float
      : float
 File "stdin", line 10, characters 7-16:
 Warning: The constant -2.5e-123 is not a binary64 floating-point value. A
-closest value will be used and unambiguously printed
+closest value -0x1.a71368f0f3047p-408 will be used and unambiguously printed
 -2.5000000000000001e-123. [inexact-float,parsing]
 (-2.5000000000000001e-123)%float
      : float
@@ -28,13 +28,13 @@ closest value will be used and unambiguously printed
      : float
 File "stdin", line 19, characters 6-13:
 Warning: The constant 2.5e123 is not a binary64 floating-point value. A
-closest value will be used and unambiguously printed 2.4999999999999999e+123.
-[inexact-float,parsing]
+closest value 0x1.e412f0f768fadp+409 will be used and unambiguously printed
+2.4999999999999999e+123. [inexact-float,parsing]
 2.4999999999999999e+123
      : float
 File "stdin", line 20, characters 7-16:
 Warning: The constant -2.5e-123 is not a binary64 floating-point value. A
-closest value will be used and unambiguously printed
+closest value -0x1.a71368f0f3047p-408 will be used and unambiguously printed
 -2.5000000000000001e-123. [inexact-float,parsing]
 -2.5000000000000001e-123
      : float
@@ -56,16 +56,24 @@ closest value will be used and unambiguously printed
      : float
 File "stdin", line 30, characters 6-11:
 Warning: The constant 1e309 is not a binary64 floating-point value. A closest
-value will be used and unambiguously printed infinity.
+value infinity will be used and unambiguously printed infinity.
 [inexact-float,parsing]
 infinity
      : float
 File "stdin", line 31, characters 6-12:
 Warning: The constant -1e309 is not a binary64 floating-point value. A
-closest value will be used and unambiguously printed neg_infinity.
-[inexact-float,parsing]
+closest value neg_infinity will be used and unambiguously printed
+neg_infinity. [inexact-float,parsing]
 neg_infinity
      : float
+0x1p-1
+     : float
+0.5
+     : float
+0x1p-1
+     : float
+0.5
+     : float
 2
      : nat
 2%float
diff --git a/test-suite/output/FloatSyntax.v b/test-suite/output/FloatSyntax.v
index 36ffc27239..d3eb6d2e4c 100644
--- a/test-suite/output/FloatSyntax.v
+++ b/test-suite/output/FloatSyntax.v
@@ -30,6 +30,15 @@ Check -0xb.2cp-2.
 Check 1e309.
 Check -1e309.
 
+Set Printing All.
+Check 0.5.
+Unset Printing All.
+Check 0.5.
+Unset Printing Float.
+Check 0.5.
+Set Printing Float.
+Check 0.5.
+
 Open Scope nat_scope.
 
 Check 2.