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.v | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)
 create mode 100644 test-suite/output/FloatSyntax.v

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

diff --git a/test-suite/output/FloatSyntax.v b/test-suite/output/FloatSyntax.v
new file mode 100644
index 0000000000..1caa0bb444
--- /dev/null
+++ b/test-suite/output/FloatSyntax.v
@@ -0,0 +1,34 @@
+Require Import Floats.
+
+Check 2%float.
+Check 2.5%float.
+Check (-2.5)%float.
+Check 2.5e20%float.
+Check (-2.5e-20)%float.
+Check (2 + 2)%float.
+Check (2.5 + 2.5)%float.
+
+Open Scope float_scope.
+
+Check 2.
+Check 2.5.
+Check (-2.5).
+Check 2.5e20.
+Check (-2.5e-20).
+Check (2 + 2).
+Check (2.5 + 2.5).
+
+Open Scope nat_scope.
+
+Check 2.
+Check 2%float.
+
+Delimit Scope float_scope with flt.
+Definition t := 2%float.
+Print t.
+Delimit Scope nat_scope with float.
+Print t.
+Check 2.
+Close Scope nat_scope.
+Check 2.
+Close Scope float_scope.
-- 
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.v | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

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

diff --git a/test-suite/output/FloatSyntax.v b/test-suite/output/FloatSyntax.v
index 1caa0bb444..85f611352c 100644
--- a/test-suite/output/FloatSyntax.v
+++ b/test-suite/output/FloatSyntax.v
@@ -3,8 +3,11 @@ Require Import Floats.
 Check 2%float.
 Check 2.5%float.
 Check (-2.5)%float.
-Check 2.5e20%float.
-Check (-2.5e-20)%float.
+(* Avoid exponents with less than three digits as they are usually
+   displayed with two digits (1e7 is displayed 1e+07) except on
+   Windows where three digits are used (1e+007). *)
+Check 2.5e123%float.
+Check (-2.5e-123)%float.
 Check (2 + 2)%float.
 Check (2.5 + 2.5)%float.
 
@@ -13,8 +16,8 @@ Open Scope float_scope.
 Check 2.
 Check 2.5.
 Check (-2.5).
-Check 2.5e20.
-Check (-2.5e-20).
+Check 2.5e123.
+Check (-2.5e-123).
 Check (2 + 2).
 Check (2.5 + 2.5).
 
-- 
cgit v1.2.3