From 3e0db1b645a8653c62b8b5a4978e6d8fbbe9a9cc Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Tue, 26 Mar 2019 21:10:17 +0100
Subject: Pretty-printing primitive float constants

* map special floats to registered CRef's
* kernel/float64.mli: add {is_infinity, is_neg_infinity} functions
* kernel/float64.ml: Replace string_of_float with a safe pretty-printing function

Namely:

  let to_string_raw f = Printf.sprintf "%.17g" f
  let to_string f = if is_nan f then "nan" else to_string_raw f

Summary:

* printing a binary64 float in 17 decimal places and parsing it again
  will yield the same float, e.g.:

  let f1 = 1. +. (0x1p-53 +. 0x1p-105)
  let f2 = float_of_string (to_string f1)
  f1 = f2

* OCaml's string_of_float gives a sign to nan values which shouldn't be
  displayed as all NaNs are considered equal here.
---
 test-suite/output/FloatSyntax.out | 40 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)
 create mode 100644 test-suite/output/FloatSyntax.out

(limited to 'test-suite/output/FloatSyntax.out')

diff --git a/test-suite/output/FloatSyntax.out b/test-suite/output/FloatSyntax.out
new file mode 100644
index 0000000000..f67119020e
--- /dev/null
+++ b/test-suite/output/FloatSyntax.out
@@ -0,0 +1,40 @@
+2%float
+     : float
+2.5%float
+     : float
+(-2.5)%float
+     : float
+2.5e+20%float
+     : float
+(-2.4999999999999999e-20)%float
+     : float
+(2 + 2)%float
+     : float
+(2.5 + 2.5)%float
+     : float
+2
+     : float
+2.5
+     : float
+-2.5
+     : float
+2.5e+20
+     : float
+-2.4999999999999999e-20
+     : float
+2 + 2
+     : float
+2.5 + 2.5
+     : float
+2
+     : nat
+2%float
+     : float
+t = 2%flt
+     : float
+t = 2%flt
+     : float
+2
+     : nat
+2
+     : float
-- 
cgit v1.2.3


From f8fdc27f922694edf74a7b608de1596e0a1ac0e3 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 19 Apr 2019 15:29:53 +0200
Subject: Make primitive float work on Windows

---
 test-suite/output/FloatSyntax.out | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'test-suite/output/FloatSyntax.out')

diff --git a/test-suite/output/FloatSyntax.out b/test-suite/output/FloatSyntax.out
index f67119020e..668a55977d 100644
--- a/test-suite/output/FloatSyntax.out
+++ b/test-suite/output/FloatSyntax.out
@@ -4,9 +4,9 @@
      : float
 (-2.5)%float
      : float
-2.5e+20%float
+2.4999999999999999e+123%float
      : float
-(-2.4999999999999999e-20)%float
+(-2.5000000000000001e-123)%float
      : float
 (2 + 2)%float
      : float
@@ -18,9 +18,9 @@
      : float
 -2.5
      : float
-2.5e+20
+2.4999999999999999e+123
      : float
--2.4999999999999999e-20
+-2.5000000000000001e-123
      : float
 2 + 2
      : float
-- 
cgit v1.2.3