diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/float64.ml | 13 | ||||
| -rw-r--r-- | kernel/float64.mli | 4 |
2 files changed, 14 insertions, 3 deletions
diff --git a/kernel/float64.ml b/kernel/float64.ml index 72f0d83359..5160d32892 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -16,9 +16,14 @@ let is_nan f = f <> f let is_infinity f = f = infinity let is_neg_infinity f = f = neg_infinity -(* OCaml give a sign to nan values which should not be displayed as all nan are - * considered equal *) -let to_string f = if is_nan f then "nan" else string_of_float f +(* 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] 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 *) +let to_string f = if is_nan f then "nan" else to_string_raw f let of_string = float_of_string (* Compiles a float to OCaml code *) @@ -30,6 +35,8 @@ let compile f = let of_float f = f +let sign f = copysign 1. f < 0. + let opp = ( ~-. ) let abs = abs_float diff --git a/kernel/float64.mli b/kernel/float64.mli index 927594115e..acc3a556ab 100644 --- a/kernel/float64.mli +++ b/kernel/float64.mli @@ -14,6 +14,7 @@ Beware: NaNs have a sign and a payload, while they should be indistinguishable from Coq's perspective. *) type t +(** Test functions for special values to avoid calling [classify] *) val is_nan : t -> bool val is_infinity : t -> bool val is_neg_infinity : t -> bool @@ -25,6 +26,9 @@ val compile : t -> string val of_float : float -> t +(** Return [true] for "-", [false] for "+". *) +val sign : t -> bool + val opp : t -> t val abs : t -> t |