[primitive floats] Add low level hexadecimal printing

2 files changed, 20 insertions, 12 deletions

diff --git a/kernel/float64.ml b/kernel/float64.ml
index 53fc13b04b..76005a3dc6 100644
--- a/kernel/float64.ml
+++ b/kernel/float64.ml
@@ -19,29 +19,27 @@ let is_nan (f : float) = f <> f
 let is_infinity f = f = infinity
 let is_neg_infinity f = f = neg_infinity
 
-(* Printing a binary64 float in 17 decimal places and parsing it again
-   will yield the same float. We assume [to_string_raw] is not given a
-   [nan] or an infinity as input. *)
-let to_string_raw f = Printf.sprintf "%.17g" f
-
 (* OCaml gives a sign to nan values which should not be displayed as
    all NaNs are considered equal here.
    OCaml prints infinities as "inf" (resp. "-inf")
    but we want "infinity" (resp. "neg_infinity"). *)
-let to_string f =
+let to_string_raw fmt f =
   if is_nan f then "nan"
   else if is_infinity f then "infinity"
   else if is_neg_infinity f then "neg_infinity"
-  else to_string_raw f
+  else Printf.sprintf fmt f
+
+let to_hex_string = to_string_raw "%h"
+
+(* Printing a binary64 float in 17 decimal places and parsing it again
+   will yield the same float. *)
+let to_string = to_string_raw "%.17g"
 
 let of_string = float_of_string
 
 (* Compiles a float to OCaml code *)
 let compile f =
-  let s =
-    if is_nan f then "nan" else if is_neg_infinity f then "neg_infinity"
-    else Printf.sprintf "%h" f in
-  Printf.sprintf "Float64.of_float (%s)" s
+  Printf.sprintf "Float64.of_float (%s)" (to_hex_string f)
 
 let of_float f = f
 
diff --git a/kernel/float64.mli b/kernel/float64.mli
index d43ff4553f..0afbfa89da 100644
--- a/kernel/float64.mli
+++ b/kernel/float64.mli
@@ -19,9 +19,19 @@ val is_nan : t -> bool
 val is_infinity : t -> bool
 val is_neg_infinity : t -> bool
 
-val to_string : t -> string
 val of_string : string -> t
 
+(** Print a float exactly as an hexadecimal value (exact decimal
+ * printing would be possible but sometimes requires more than 700
+ * digits). *)
+val to_hex_string : t -> string
+
+(** Print a float as a decimal value. The printing is not exact (the
+ * real value printed is not always the given floating-point value),
+ * however printing is precise enough that forall float [f],
+ * [of_string (to_decimal_string f) = f].  *)
+val to_string : t -> string
+
 val compile : t -> string
 
 val of_float : float -> t