From 136454f306c8d4de83b8f37201307205a7c57786 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 1 Oct 2020 20:34:40 +0200
Subject: Inline the functions from coq_float64.h.

Since the code is compiled in -fPIC mode, the compiler cannot inline the
functions, due to the ABI mandating the ability to interpose visible
symbols. Hiding the symbols of coq_float64.h would work, except that they
float64.ml needs to reference them. (See #13124 for more details.)

This commit improves performances by 7% on the following code.

    From Coq Require Import Int63 BinPos PrimFloat.
    Definition foo n :=
      let two := of_int63 2 in
      Pos.iter (fun x => sub (mul x two) two) two n.
    Time Eval vm_compute in foo 100000000.

If we consider only the floating-point operations (by ignoring the cost of
the loop), the speedup is actually 30%.
---
 kernel/byterun/coq_interp.c | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

(limited to 'kernel')

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 672ee60c6d..e94af96b72 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1577,21 +1577,21 @@ value coq_interprete
       Instruct (CHECKEQFLOAT) {
         print_instr("CHECKEQFLOAT");
         CheckFloat2();
-        accu = coq_feq(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false;
+        accu = Double_val(accu) == Double_val(*sp++) ? coq_true : coq_false;
         Next;
       }
 
       Instruct (CHECKLTFLOAT) {
         print_instr("CHECKLTFLOAT");
         CheckFloat2();
-        accu = coq_flt(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false;
+        accu = Double_val(accu) < Double_val(*sp++) ? coq_true : coq_false;
         Next;
       }
 
       Instruct (CHECKLEFLOAT) {
         print_instr("CHECKLEFLOAT");
         CheckFloat2();
-        accu = coq_fle(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false;
+        accu = Double_val(accu) <= Double_val(*sp++) ? coq_true : coq_false;
         Next;
       }
 
@@ -1644,35 +1644,35 @@ value coq_interprete
       Instruct (CHECKADDFLOAT) {
         print_instr("CHECKADDFLOAT");
         CheckFloat2();
-        Coq_copy_double(coq_fadd(Double_val(accu), Double_val(*sp++)));
+        Coq_copy_double(Double_val(accu) + Double_val(*sp++));
         Next;
       }
 
       Instruct (CHECKSUBFLOAT) {
         print_instr("CHECKSUBFLOAT");
         CheckFloat2();
-        Coq_copy_double(coq_fsub(Double_val(accu), Double_val(*sp++)));
+        Coq_copy_double(Double_val(accu) - Double_val(*sp++));
         Next;
       }
 
       Instruct (CHECKMULFLOAT) {
         print_instr("CHECKMULFLOAT");
         CheckFloat2();
-        Coq_copy_double(coq_fmul(Double_val(accu), Double_val(*sp++)));
+        Coq_copy_double(Double_val(accu) * Double_val(*sp++));
         Next;
       }
 
       Instruct (CHECKDIVFLOAT) {
         print_instr("CHECKDIVFLOAT");
         CheckFloat2();
-        Coq_copy_double(coq_fdiv(Double_val(accu), Double_val(*sp++)));
+        Coq_copy_double(Double_val(accu) / Double_val(*sp++));
         Next;
       }
 
       Instruct (CHECKSQRTFLOAT) {
         print_instr("CHECKSQRTFLOAT");
         CheckFloat1();
-        Coq_copy_double(coq_fsqrt(Double_val(accu)));
+        Coq_copy_double(sqrt(Double_val(accu)));
         Next;
       }
 
@@ -1743,14 +1743,14 @@ value coq_interprete
       Instruct (CHECKNEXTUPFLOAT) {
         print_instr("CHECKNEXTUPFLOAT");
         CheckFloat1();
-        Coq_copy_double(coq_next_up(Double_val(accu)));
+        Coq_copy_double(nextafter(Double_val(accu), INFINITY));
         Next;
       }
 
       Instruct (CHECKNEXTDOWNFLOAT) {
         print_instr("CHECKNEXTDOWNFLOAT");
         CheckFloat1();
-        Coq_copy_double(coq_next_down(Double_val(accu)));
+        Coq_copy_double(nextafter(Double_val(accu), -INFINITY));
         Next;
       }
 
-- 
cgit v1.2.3