diff options
| author | Pierre Roux | 2020-01-30 14:45:49 +0100 |
|---|---|---|
| committer | Pierre Roux | 2020-01-30 14:45:49 +0100 |
| commit | e30eab16b2669cfcd63a718fa10a7bc7f6020b8a (patch) | |
| tree | b9610b2105a0c9f2bce6780b3b0951fd246a7e4f | |
| parent | 92a294ca53752b61b0270a719826ffc759a25e8d (diff) | |
Fix 11483
Performance bug of PrimFLoat.compare with native_compute
When adapting Coq.Interval with @erikmd and @silene, we noticed that
PrimFLoat.compare is taking a lot of time with native_compute (much
more than with vm_compute).
This comes from the implementation using the OCaml polymorphic
comparison instead of the float comparison.
| -rw-r--r-- | kernel/float64.ml | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/kernel/float64.ml b/kernel/float64.ml index 3e36373b77..cc661aeba3 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -12,7 +12,10 @@ format *) type t = float -let is_nan f = f <> f +(* The [f : float] type annotation enable the compiler to compile f <> f + as comparison on floats rather than the polymorphic OCaml comparison + which is much slower. *) +let is_nan (f : float) = f <> f let is_infinity f = f = infinity let is_neg_infinity f = f = neg_infinity @@ -42,19 +45,20 @@ let abs = abs_float type float_comparison = FEq | FLt | FGt | FNotComparable -let eq x y = x = y +(* See above comment on [is_nan] for the [float] type annotations. *) +let eq (x : float) (y : float) = x = y [@@ocaml.inline always] -let lt x y = x < y +let lt (x : float) (y : float) = x < y [@@ocaml.inline always] -let le x y = x <= y +let le (x : float) (y : float) = x <= y [@@ocaml.inline always] (* inspired by lib/util.ml; see also #10471 *) -let pervasives_compare = compare +let pervasives_compare (x : float) (y : float) = compare x y -let compare x y = +let compare (x : float) (y : float) = if x < y then FLt else ( |