From e30eab16b2669cfcd63a718fa10a7bc7f6020b8a Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 30 Jan 2020 14:45:49 +0100
Subject: 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.
---
 kernel/float64.ml | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

(limited to 'kernel/float64.ml')

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
   (
-- 
cgit v1.2.3