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. --- kernel/float64.mli | 52 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 52 insertions(+) create mode 100644 kernel/float64.mli (limited to 'kernel/float64.mli') diff --git a/kernel/float64.mli b/kernel/float64.mli new file mode 100644 index 0000000000..fd84f9e61d --- /dev/null +++ b/kernel/float64.mli @@ -0,0 +1,52 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* bool + +val to_string : t -> string +val of_string : string -> t + +val opp : t -> t +val abs : t -> t + +type float_comparison = Eq | Lt | Gt | NotComparable + +(** The IEEE 754 float comparison. + * NotComparable is returned if there is a NaN in the arguments *) +val compare : t -> t -> float_comparison + +val mul : t -> t -> t +val add : t -> t -> t +val sub : t -> t -> t +val div : t -> t -> t +val sqrt : t -> t + +(** Link with integers *) +val of_int63 : Uint63.t -> t +val normfr_mantissa : t -> Uint63.t + +(** Shifted exponent extraction *) +val frshiftexp : t -> t * Uint63.t (* float remainder, shifted exponent *) +val ldshiftexp : t -> Uint63.t -> t + +(** Return true if two floats are equal. + * All NaN values are considered equal. *) +val equal : t -> t -> bool + +val hash : t -> int + +(** Total order relation over float values. Behaves like [Pervasives.compare].*) +val total_compare : t -> t -> int -- cgit v1.2.3 From cc7dfa82705b64d1cf43408244ef6c7dd930a6e9 Mon Sep 17 00:00:00 2001 From: Guillaume Bertholon Date: Thu, 19 Jul 2018 13:33:17 +0200 Subject: Add primitive floats to 'vm_compute' * This commit add float instructions to the VM, their encoding in bytecode and the interpretation of primitive float values after the reduction. * The flag '-std=c99' could be added to the C compiler flags to ensure that float computation strictly follows the norm (ie. i387 80-bits format is not used as an optimization). Actually, we use '-fexcess-precision=standard' instead of '-std=c99' because the latter would disable GNU asm used in the VM. --- kernel/float64.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'kernel/float64.mli') diff --git a/kernel/float64.mli b/kernel/float64.mli index fd84f9e61d..7ced535dc0 100644 --- a/kernel/float64.mli +++ b/kernel/float64.mli @@ -19,6 +19,8 @@ val is_nan : t -> bool val to_string : t -> string val of_string : string -> t +val of_float : float -> t + val opp : t -> t val abs : t -> t -- cgit v1.2.3 From 79605dabb10e889ae998bf72c8483f095277e693 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 28 Aug 2018 14:31:37 +0200 Subject: Change return type of primitive float comparison Replace `option comparison` with `float_comparison` (:= `FEq | FLt | FGt | FNotComparable`) as suggested by Guillaume Melquiond to avoid boxing and an extra match when using primitive float comparison. --- kernel/float64.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/float64.mli') diff --git a/kernel/float64.mli b/kernel/float64.mli index 7ced535dc0..c82f1d84da 100644 --- a/kernel/float64.mli +++ b/kernel/float64.mli @@ -24,7 +24,7 @@ val of_float : float -> t val opp : t -> t val abs : t -> t -type float_comparison = Eq | Lt | Gt | NotComparable +type float_comparison = FEq | FLt | FGt | FNotComparable (** The IEEE 754 float comparison. * NotComparable is returned if there is a NaN in the arguments *) -- cgit v1.2.3 From d18b928154a48ff8d90aaff69eca7d6eb3dfa0ab Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 28 Aug 2018 18:56:07 +0200 Subject: Implement classify on primitive float --- kernel/float64.mli | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'kernel/float64.mli') diff --git a/kernel/float64.mli b/kernel/float64.mli index c82f1d84da..1ad980a691 100644 --- a/kernel/float64.mli +++ b/kernel/float64.mli @@ -30,6 +30,11 @@ type float_comparison = FEq | FLt | FGt | FNotComparable * NotComparable is returned if there is a NaN in the arguments *) val compare : t -> t -> float_comparison +type float_class = + | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN + +val classify : t -> float_class + val mul : t -> t -> t val add : t -> t -> t val sub : t -> t -> t -- cgit v1.2.3 From 5f1270242f71a0a1da7c868967e1071d28ed83fb Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 28 Aug 2018 23:37:49 +0200 Subject: Add next_{up,down} primitive float functions --- kernel/float64.mli | 3 +++ 1 file changed, 3 insertions(+) (limited to 'kernel/float64.mli') diff --git a/kernel/float64.mli b/kernel/float64.mli index 1ad980a691..580004126d 100644 --- a/kernel/float64.mli +++ b/kernel/float64.mli @@ -49,6 +49,9 @@ val normfr_mantissa : t -> Uint63.t val frshiftexp : t -> t * Uint63.t (* float remainder, shifted exponent *) val ldshiftexp : t -> Uint63.t -> t +val next_up : t -> t +val next_down : t -> t + (** Return true if two floats are equal. * All NaN values are considered equal. *) val equal : t -> t -> bool -- cgit v1.2.3 From 73580b9c5f206e2d3a7107123d207515f2330978 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 23 Oct 2018 17:52:39 +0200 Subject: Add primitive floats to 'native_compute' * Float added to is_value/get_value to avoid stack overflows (cf. #7646) * beware of the use of Array.map with floats (cf. comment in the makeblock function) NB: From here one, the configure option "-native-compiler no" is no longer needed. --- kernel/float64.mli | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) (limited to 'kernel/float64.mli') diff --git a/kernel/float64.mli b/kernel/float64.mli index 580004126d..1e6ea8bb96 100644 --- a/kernel/float64.mli +++ b/kernel/float64.mli @@ -15,10 +15,14 @@ indistinguishable from Coq's perspective. *) type t 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 +val compile : t -> string + val of_float : float -> t val opp : t -> t @@ -29,32 +33,55 @@ type float_comparison = FEq | FLt | FGt | FNotComparable (** The IEEE 754 float comparison. * NotComparable is returned if there is a NaN in the arguments *) val compare : t -> t -> float_comparison +[@@ocaml.inline always] type float_class = | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN val classify : t -> float_class +[@@ocaml.inline always] val mul : t -> t -> t +[@@ocaml.inline always] + val add : t -> t -> t +[@@ocaml.inline always] + val sub : t -> t -> t +[@@ocaml.inline always] + val div : t -> t -> t +[@@ocaml.inline always] + val sqrt : t -> t +[@@ocaml.inline always] (** Link with integers *) val of_int63 : Uint63.t -> t +[@@ocaml.inline always] + val normfr_mantissa : t -> Uint63.t +[@@ocaml.inline always] (** Shifted exponent extraction *) +val eshift : int + val frshiftexp : t -> t * Uint63.t (* float remainder, shifted exponent *) +[@@ocaml.inline always] + val ldshiftexp : t -> Uint63.t -> t +[@@ocaml.inline always] val next_up : t -> t +[@@ocaml.inline always] + val next_down : t -> t +[@@ocaml.inline always] (** Return true if two floats are equal. * All NaN values are considered equal. *) val equal : t -> t -> bool +[@@ocaml.inline always] val hash : t -> int -- cgit v1.2.3 From 6133877fc097412233a60740fdf94374abb79559 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 20 Feb 2019 18:00:04 +0100 Subject: Add primitive floats to checker --- kernel/float64.mli | 3 +++ 1 file changed, 3 insertions(+) (limited to 'kernel/float64.mli') diff --git a/kernel/float64.mli b/kernel/float64.mli index 1e6ea8bb96..927594115e 100644 --- a/kernel/float64.mli +++ b/kernel/float64.mli @@ -87,3 +87,6 @@ val hash : t -> int (** Total order relation over float values. Behaves like [Pervasives.compare].*) val total_compare : t -> t -> int + +val is_float64 : Obj.t -> bool +[@@ocaml.inline always] -- 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. --- kernel/float64.mli | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'kernel/float64.mli') 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 -- cgit v1.2.3 From dca0135a263717b3a1a1d7c4f054f039dc08109e Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 4 Apr 2019 00:14:47 +0200 Subject: Make primitive float work on x86_32 Flag -fexcess-precision=standard is not enough on x86_32 where -msse2 -mfpmath=sse is required (-msse is not enough) to avoid double rounding issues in the VM. Most floating-point operation are now implemented in C because OCaml is suffering double rounding issues on x86_32 with 80 bits extended precision registers used for floating-point values, causing double rounding making floating-point arithmetic incorrect with respect to its specification. Add a runtime test for double roundings. --- kernel/float64.mli | 7 ------- 1 file changed, 7 deletions(-) (limited to 'kernel/float64.mli') diff --git a/kernel/float64.mli b/kernel/float64.mli index acc3a556ab..78dc1a7bd7 100644 --- a/kernel/float64.mli +++ b/kernel/float64.mli @@ -46,19 +46,14 @@ val classify : t -> float_class [@@ocaml.inline always] val mul : t -> t -> t -[@@ocaml.inline always] val add : t -> t -> t -[@@ocaml.inline always] val sub : t -> t -> t -[@@ocaml.inline always] val div : t -> t -> t -[@@ocaml.inline always] val sqrt : t -> t -[@@ocaml.inline always] (** Link with integers *) val of_int63 : Uint63.t -> t @@ -77,10 +72,8 @@ val ldshiftexp : t -> Uint63.t -> t [@@ocaml.inline always] val next_up : t -> t -[@@ocaml.inline always] val next_down : t -> t -[@@ocaml.inline always] (** Return true if two floats are equal. * All NaN values are considered equal. *) -- cgit v1.2.3 From f155ba664a782f000e278d97ee5666e2e7d2adea Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Wed, 3 Jul 2019 15:08:44 +0200 Subject: Add "==", "<", "<=" in PrimFloat.v * Add a related test-suite in compare.v (generated by a bash script) Co-authored-by: Pierre Roux --- kernel/float64.mli | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'kernel/float64.mli') diff --git a/kernel/float64.mli b/kernel/float64.mli index 78dc1a7bd7..2aa9796526 100644 --- a/kernel/float64.mli +++ b/kernel/float64.mli @@ -34,6 +34,12 @@ val abs : t -> t type float_comparison = FEq | FLt | FGt | FNotComparable +val eq : t -> t -> bool + +val lt : t -> t -> bool + +val le : t -> t -> bool + (** The IEEE 754 float comparison. * NotComparable is returned if there is a NaN in the arguments *) val compare : t -> t -> float_comparison -- cgit v1.2.3