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.ml | 82 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 82 insertions(+) create mode 100644 kernel/float64.ml (limited to 'kernel/float64.ml') diff --git a/kernel/float64.ml b/kernel/float64.ml new file mode 100644 index 0000000000..e74fd2e9f1 --- /dev/null +++ b/kernel/float64.ml @@ -0,0 +1,82 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* f + +(* 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 +let of_string = float_of_string + +let opp = ( ~-. ) +let abs = abs_float + +type float_comparison = Eq | Lt | Gt | NotComparable + +let compare x y = + if x < y then Lt + else + ( + if x > y then Gt + else + ( + if x = y then Eq + else NotComparable (* NaN case *) + ) + ) + +let mul = ( *. ) +let add = ( +. ) +let sub = ( -. ) +let div = ( /. ) +let sqrt = sqrt + +let of_int63 = Uint63.to_float +let prec = 53 +let normfr_mantissa f = + let f = abs f in + if f >= 0.5 && f < 1. then Uint63.of_float (ldexp f prec) + else Uint63.zero + +let eshift = 1022 + 52 (* minimum negative exponent + binary precision *) + +(* When calling frexp on a nan or an infinity, the returned value inside + the exponent is undefined. + Therefore we must always set it to a fixed value (here 0). *) +let frshiftexp f = + match classify_float f with + | FP_zero | FP_infinite | FP_nan -> (f, Uint63.zero) + | FP_normal | FP_subnormal -> + let (m, e) = frexp f in + m, Uint63.of_int (e + eshift) + +let ldshiftexp f e = ldexp f (snd (Uint63.to_int2 e) - eshift) + +let equal f1 f2 = + match classify_float f1 with + | FP_normal | FP_subnormal | FP_infinite -> (f1 = f2) + | FP_nan -> is_nan f2 + | FP_zero -> f1 = f2 && 1. /. f1 = 1. /. f2 (* OCaml consider 0. = -0. *) + +let hash = + (* Hashtbl.hash already considers all NaNs as equal, + cf. https://github.com/ocaml/ocaml/commit/aea227fdebe0b5361fd3e1d0aaa42cf929052269 + and http://caml.inria.fr/pub/docs/manual-ocaml/libref/Hashtbl.html *) + Hashtbl.hash + +let total_compare f1 f2 = + (* pervasives_compare considers all NaNs as equal, which is fine here, + but also considers -0. and +0. as equal *) + if f1 = 0. && f2 = 0. then Util.pervasives_compare (1. /. f1) (1. /. f2) + else Util.pervasives_compare f1 f2 -- 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.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'kernel/float64.ml') diff --git a/kernel/float64.ml b/kernel/float64.ml index e74fd2e9f1..0b22e07e82 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -19,6 +19,8 @@ let is_nan f = f <> f let to_string f = if is_nan f then "nan" else string_of_float f let of_string = float_of_string +let of_float f = f + let opp = ( ~-. ) let abs = abs_float -- cgit v1.2.3 From dda50a88aab0fa0cfb74c8973b5a4353fe5c8447 Mon Sep 17 00:00:00 2001 From: Guillaume Bertholon Date: Fri, 3 Aug 2018 17:38:48 +0200 Subject: Put axioms on ldshiftexp and frshiftexp Axioms on ldexp and frexp are replaced by proofs inside FloatLemmas. The shift value has been increased to 2 * emax + prec because in ldexp we want to be able to transform the smallest denormalized to the biggest float value in one call. --- kernel/float64.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/float64.ml') diff --git a/kernel/float64.ml b/kernel/float64.ml index 0b22e07e82..a625c0f551 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -51,7 +51,7 @@ let normfr_mantissa f = if f >= 0.5 && f < 1. then Uint63.of_float (ldexp f prec) else Uint63.zero -let eshift = 1022 + 52 (* minimum negative exponent + binary precision *) +let eshift = 2101 (* 2*emax + prec *) (* When calling frexp on a nan or an infinity, the returned value inside the exponent is undefined. -- 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.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'kernel/float64.ml') diff --git a/kernel/float64.ml b/kernel/float64.ml index a625c0f551..eebc8f35ef 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -24,17 +24,17 @@ let of_float f = f let opp = ( ~-. ) let abs = abs_float -type float_comparison = Eq | Lt | Gt | NotComparable +type float_comparison = FEq | FLt | FGt | FNotComparable let compare x y = - if x < y then Lt + if x < y then FLt else ( - if x > y then Gt + if x > y then FGt else ( - if x = y then Eq - else NotComparable (* NaN case *) + if x = y then FEq + else FNotComparable (* NaN case *) ) ) -- 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.ml | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'kernel/float64.ml') diff --git a/kernel/float64.ml b/kernel/float64.ml index eebc8f35ef..7b54fd0c4b 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -38,6 +38,17 @@ let compare x y = ) ) +type float_class = + | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN + +let classify x = + match classify_float x with + | FP_normal -> if 0. < x then PNormal else NNormal + | FP_subnormal -> if 0. < x then PSubn else NSubn + | FP_zero -> if 0. < 1. /. x then PZero else NZero + | FP_infinite -> if 0. < x then PInf else NInf + | FP_nan -> NaN + let mul = ( *. ) let add = ( +. ) let sub = ( -. ) -- 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.ml | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'kernel/float64.ml') diff --git a/kernel/float64.ml b/kernel/float64.ml index 7b54fd0c4b..351661f44d 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -76,6 +76,24 @@ let frshiftexp f = let ldshiftexp f e = ldexp f (snd (Uint63.to_int2 e) - eshift) +let eta_float = ldexp 1. (-1074) (* smallest positive float (subnormal) *) + +let next_up f = + match classify_float f with + | FP_nan -> f + | FP_infinite -> if 0. < f then f else -.max_float + | FP_zero | FP_subnormal -> + let f = f +. eta_float in + if f = 0. then -0. else f (* or next_down may return -0. *) + | FP_normal -> + let f, e = frexp f in + if 0. < f || f <> -0.5 || e = -1021 then + ldexp (f +. epsilon_float /. 2.) e + else + ldexp (-0.5 +. epsilon_float /. 4.) e + +let next_down f = -.(next_up (-.f)) + let equal f1 f2 = match classify_float f1 with | FP_normal | FP_subnormal | FP_infinite -> (f1 = f2) -- 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.ml | 40 ++++++++++++++++++++++++++++++++++------ 1 file changed, 34 insertions(+), 6 deletions(-) (limited to 'kernel/float64.ml') diff --git a/kernel/float64.ml b/kernel/float64.ml index 351661f44d..c0611f37a0 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -13,12 +13,21 @@ type t = float 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 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 + let of_float f = f let opp = ( ~-. ) @@ -37,6 +46,7 @@ let compare x y = else FNotComparable (* NaN case *) ) ) +[@@ocaml.inline always] type float_class = | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN @@ -48,19 +58,32 @@ let classify x = | FP_zero -> if 0. < 1. /. x then PZero else NZero | FP_infinite -> if 0. < x then PInf else NInf | FP_nan -> NaN +[@@ocaml.inline always] + +let mul x y = x *. y +[@@ocaml.inline always] + +let add x y = x +. y +[@@ocaml.inline always] + +let sub x y = x -. y +[@@ocaml.inline always] + +let div x y = x /. y +[@@ocaml.inline always] + +let sqrt x = sqrt x +[@@ocaml.inline always] -let mul = ( *. ) -let add = ( +. ) -let sub = ( -. ) -let div = ( /. ) -let sqrt = sqrt +let of_int63 x = Uint63.to_float x +[@@ocaml.inline always] -let of_int63 = Uint63.to_float let prec = 53 let normfr_mantissa f = let f = abs f in if f >= 0.5 && f < 1. then Uint63.of_float (ldexp f prec) else Uint63.zero +[@@ocaml.inline always] let eshift = 2101 (* 2*emax + prec *) @@ -73,8 +96,10 @@ let frshiftexp f = | FP_normal | FP_subnormal -> let (m, e) = frexp f in m, Uint63.of_int (e + eshift) +[@@ocaml.inline always] let ldshiftexp f e = ldexp f (snd (Uint63.to_int2 e) - eshift) +[@@ocaml.inline always] let eta_float = ldexp 1. (-1074) (* smallest positive float (subnormal) *) @@ -91,14 +116,17 @@ let next_up f = ldexp (f +. epsilon_float /. 2.) e else ldexp (-0.5 +. epsilon_float /. 4.) e +[@@ocaml.inline always] let next_down f = -.(next_up (-.f)) +[@@ocaml.inline always] let equal f1 f2 = match classify_float f1 with | FP_normal | FP_subnormal | FP_infinite -> (f1 = f2) | FP_nan -> is_nan f2 | FP_zero -> f1 = f2 && 1. /. f1 = 1. /. f2 (* OCaml consider 0. = -0. *) +[@@ocaml.inline always] let hash = (* Hashtbl.hash already considers all NaNs as equal, -- 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.ml | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) (limited to 'kernel/float64.ml') diff --git a/kernel/float64.ml b/kernel/float64.ml index c0611f37a0..72f0d83359 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -35,6 +35,9 @@ let abs = abs_float type float_comparison = FEq | FLt | FGt | FNotComparable +(* inspired by lib/util.ml; see also #10471 *) +let pervasives_compare = compare + let compare x y = if x < y then FLt else @@ -137,5 +140,9 @@ let hash = let total_compare f1 f2 = (* pervasives_compare considers all NaNs as equal, which is fine here, but also considers -0. and +0. as equal *) - if f1 = 0. && f2 = 0. then Util.pervasives_compare (1. /. f1) (1. /. f2) - else Util.pervasives_compare f1 f2 + if f1 = 0. && f2 = 0. then pervasives_compare (1. /. f1) (1. /. f2) + else pervasives_compare f1 f2 + +let is_float64 t = + Obj.tag t = Obj.double_tag +[@@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.ml | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) (limited to 'kernel/float64.ml') 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 -- 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.ml | 52 ++++++++++++++++++++++++---------------------------- 1 file changed, 24 insertions(+), 28 deletions(-) (limited to 'kernel/float64.ml') diff --git a/kernel/float64.ml b/kernel/float64.ml index 5160d32892..55ad472ea9 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -70,20 +70,20 @@ let classify x = | FP_nan -> NaN [@@ocaml.inline always] -let mul x y = x *. y -[@@ocaml.inline always] +external mul : float -> float -> float = "coq_fmul_byte" "coq_fmul" +[@@unboxed] [@@noalloc] -let add x y = x +. y -[@@ocaml.inline always] +external add : float -> float -> float = "coq_fadd_byte" "coq_fadd" +[@@unboxed] [@@noalloc] -let sub x y = x -. y -[@@ocaml.inline always] +external sub : float -> float -> float = "coq_fsub_byte" "coq_fsub" +[@@unboxed] [@@noalloc] -let div x y = x /. y -[@@ocaml.inline always] +external div : float -> float -> float = "coq_fdiv_byte" "coq_fdiv" +[@@unboxed] [@@noalloc] -let sqrt x = sqrt x -[@@ocaml.inline always] +external sqrt : float -> float = "coq_fsqrt_byte" "coq_fsqrt" +[@@unboxed] [@@noalloc] let of_int63 x = Uint63.to_float x [@@ocaml.inline always] @@ -111,25 +111,11 @@ let frshiftexp f = let ldshiftexp f e = ldexp f (snd (Uint63.to_int2 e) - eshift) [@@ocaml.inline always] -let eta_float = ldexp 1. (-1074) (* smallest positive float (subnormal) *) +external next_up : float -> float = "coq_next_up_byte" "coq_next_up" +[@@unboxed] [@@noalloc] -let next_up f = - match classify_float f with - | FP_nan -> f - | FP_infinite -> if 0. < f then f else -.max_float - | FP_zero | FP_subnormal -> - let f = f +. eta_float in - if f = 0. then -0. else f (* or next_down may return -0. *) - | FP_normal -> - let f, e = frexp f in - if 0. < f || f <> -0.5 || e = -1021 then - ldexp (f +. epsilon_float /. 2.) e - else - ldexp (-0.5 +. epsilon_float /. 4.) e -[@@ocaml.inline always] - -let next_down f = -.(next_up (-.f)) -[@@ocaml.inline always] +external next_down : float -> float = "coq_next_down_byte" "coq_next_down" +[@@unboxed] [@@noalloc] let equal f1 f2 = match classify_float f1 with @@ -153,3 +139,13 @@ let total_compare f1 f2 = let is_float64 t = Obj.tag t = Obj.double_tag [@@ocaml.inline always] + +(*** Test at runtime that no harmful double rounding seems to + be performed with an intermediate 80 bits representation (x87). *) +let () = + let b = ldexp 1. 53 in + let s = add 1. (ldexp 1. (-52)) in + if add b s <= b || add b 1. <> b then + failwith "Detected double rounding due to the use of intermediate \ + 80 bits floating-point representation. Use of Float is \ + thus unsafe." -- 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.ml | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'kernel/float64.ml') diff --git a/kernel/float64.ml b/kernel/float64.ml index 55ad472ea9..86b14c5cd2 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -42,6 +42,15 @@ let abs = abs_float type float_comparison = FEq | FLt | FGt | FNotComparable +let eq x y = x = y +[@@ocaml.inline always] + +let lt x y = x < y +[@@ocaml.inline always] + +let le x y = x <= y +[@@ocaml.inline always] + (* inspired by lib/util.ml; see also #10471 *) let pervasives_compare = compare -- cgit v1.2.3 From d39fab9a7c39d8da868c4481b96cf1086c21b1a4 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 10 Oct 2019 20:11:02 +0200 Subject: Fix ldshiftexp * Fix the implementations and add tests * Change shift from int63 to Z (was always used as a Z) * Update FloatLemmas.v accordingly Co-authored-by: Erik Martin-Dorel --- kernel/float64.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/float64.ml') diff --git a/kernel/float64.ml b/kernel/float64.ml index 86b14c5cd2..07fb25734b 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -117,7 +117,7 @@ let frshiftexp f = m, Uint63.of_int (e + eshift) [@@ocaml.inline always] -let ldshiftexp f e = ldexp f (snd (Uint63.to_int2 e) - eshift) +let ldshiftexp f e = ldexp f (Uint63.to_int_min e (2 * eshift) - eshift) [@@ocaml.inline always] external next_up : float -> float = "coq_next_up_byte" "coq_next_up" -- cgit v1.2.3 From 7088b2d4981496d5a2acf24566f486219237ef99 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Thu, 17 Oct 2019 18:08:36 +0200 Subject: feat: Use SSE2_MATH if available & Die if missing on x87 Co-authored-by: Pierre Roux --- kernel/float64.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/float64.ml') diff --git a/kernel/float64.ml b/kernel/float64.ml index 07fb25734b..c08069f3e3 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -155,6 +155,6 @@ let () = let b = ldexp 1. 53 in let s = add 1. (ldexp 1. (-52)) in if add b s <= b || add b 1. <> b then - failwith "Detected double rounding due to the use of intermediate \ - 80 bits floating-point representation. Use of Float is \ + failwith "Detected double-rounding due to the use of intermediate \ + 80-bit floating-point representation. Use of Float is \ thus unsafe." -- cgit v1.2.3 From 0caf27d014853693836ef06b1706502070b032f6 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 18 Oct 2019 12:12:12 +0200 Subject: Add a check for gradual underflows --- kernel/float64.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'kernel/float64.ml') diff --git a/kernel/float64.ml b/kernel/float64.ml index c08069f3e3..3e36373b77 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -154,7 +154,6 @@ let is_float64 t = let () = let b = ldexp 1. 53 in let s = add 1. (ldexp 1. (-52)) in - if add b s <= b || add b 1. <> b then - failwith "Detected double-rounding due to the use of intermediate \ - 80-bit floating-point representation. Use of Float is \ - thus unsafe." + if add b s <= b || add b 1. <> b || ldexp 1. (-1074) <= 0. then + failwith "Detected non IEEE-754 compliant architecture (or wrong \ + rounding mode). Use of Float is thus unsafe." -- cgit v1.2.3