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.
---
 interp/constrextern.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 217381d854..589df6af07 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -972,6 +972,9 @@ let rec extern inctx scopes vars r =
        (Numeral (SPlus, NumTok.int (Uint63.to_string i)))
        "int63" "int63_scope" (snd scopes)
 
+  | GFloat f ->
+     CPrim(String (Float64.to_string f))
+
   in insert_coercion coercion (CAst.make ?loc c)
 
 and extern_typ (subentry,(_,scopes)) =
@@ -1314,6 +1317,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
   | PSort Sorts.InSet -> GSort (UNamed [GSet,0])
   | PSort Sorts.InType -> GSort (UAnonymous {rigid=true})
   | PInt i -> GInt i
+  | PFloat f -> GFloat f
 
 let extern_constr_pattern env sigma pat =
   extern true (InConstrEntrySomeLevel,(None,[])) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat)
-- 
cgit v1.2.3


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.
---
 interp/constrextern.ml | 27 +++++++++++++++++++++++++--
 1 file changed, 25 insertions(+), 2 deletions(-)

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 589df6af07..0a1371413a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -751,6 +751,30 @@ let extended_glob_local_binder_of_decl loc = function
 
 let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_local_binder_of_decl loc u)
 
+(**********************************************************************)
+(* mapping special floats                                             *)
+
+(* this helper function is copied from notation.ml as it's not exported *)
+let qualid_of_ref n =
+  n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty
+
+let q_infinity () = qualid_of_ref "num.float.infinity"
+let q_neg_infinity () = qualid_of_ref "num.float.neg_infinity"
+let q_nan () = qualid_of_ref "num.float.nan"
+
+let extern_float f scopes =
+  if Float64.is_nan f then CRef(q_nan (), None)
+  else if Float64.is_infinity f then CRef(q_infinity (), None)
+  else if Float64.is_neg_infinity f then CRef(q_neg_infinity (), None)
+  else
+    let sign = if Float64.sign f then SMinus else SPlus in
+    let s = Float64.(to_string (abs f)) in
+    match NumTok.of_string s with
+    | None -> assert false
+    | Some n ->
+       extern_prim_token_delimiter_if_required (Numeral (sign, n))
+       "float" "float_scope" scopes
+
 (**********************************************************************)
 (* mapping glob_constr to constr_expr                                    *)
 
@@ -972,8 +996,7 @@ let rec extern inctx scopes vars r =
        (Numeral (SPlus, NumTok.int (Uint63.to_string i)))
        "int63" "int63_scope" (snd scopes)
 
-  | GFloat f ->
-     CPrim(String (Float64.to_string f))
+  | GFloat f -> extern_float f (snd scopes)
 
   in insert_coercion coercion (CAst.make ?loc c)
 
-- 
cgit v1.2.3