From 5b2d1c010aa0deb8b5ac89a9c9cdaa263e3b9d64 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 1 Oct 2020 20:42:43 +0200
Subject: Turn coq_float64.h into a .c file as it is no longer needed by
 coq_interp.c.

---
 kernel/byterun/coq_float64.c | 58 ++++++++++++++++++++++++++++++++++++++++++++
 kernel/byterun/coq_float64.h | 58 --------------------------------------------
 kernel/byterun/coq_interp.c  |  1 -
 kernel/byterun/dune          |  2 +-
 4 files changed, 59 insertions(+), 60 deletions(-)
 create mode 100644 kernel/byterun/coq_float64.c
 delete mode 100644 kernel/byterun/coq_float64.h

(limited to 'kernel')

diff --git a/kernel/byterun/coq_float64.c b/kernel/byterun/coq_float64.c
new file mode 100644
index 0000000000..5ddddbf650
--- /dev/null
+++ b/kernel/byterun/coq_float64.c
@@ -0,0 +1,58 @@
+/************************************************************************/
+/*         *   The Coq Proof Assistant / The Coq Development Team       */
+/*  v      *         Copyright INRIA, CNRS and contributors             */
+/* <O___,, * (see version control and CREDITS file for authors & dates) */
+/*   \VV/  **************************************************************/
+/*    //   *    This file is distributed under the terms of the         */
+/*         *     GNU Lesser General Public License Version 2.1          */
+/*         *     (see LICENSE file for the text of the license)         */
+/************************************************************************/
+
+#include <math.h>
+
+#define CAML_INTERNALS
+#include <caml/alloc.h>
+
+#include "coq_values.h"
+
+#define DECLARE_FREL(name, e)                                           \
+  int coq_##name(double x, double y) {                                  \
+    return e;                                                           \
+  }                                                                     \
+                                                                        \
+  value coq_##name##_byte(value x, value y) {                           \
+    return coq_##name(Double_val(x), Double_val(y));                    \
+  }
+
+#define DECLARE_FBINOP(name, e)                                         \
+  double coq_##name(double x, double y) {                               \
+    return e;                                                           \
+  }                                                                     \
+                                                                        \
+  value coq_##name##_byte(value x, value y) {                           \
+    return caml_copy_double(coq_##name(Double_val(x), Double_val(y)));  \
+  }
+
+#define DECLARE_FUNOP(name, e)                                          \
+  double coq_##name(double x) {                                         \
+    return e;                                                           \
+  }                                                                     \
+                                                                        \
+  value coq_##name##_byte(value x) {                                    \
+    return caml_copy_double(coq_##name(Double_val(x)));                 \
+  }
+
+DECLARE_FREL(feq, x == y)
+DECLARE_FREL(flt, x < y)
+DECLARE_FREL(fle, x <= y)
+DECLARE_FBINOP(fmul, x * y)
+DECLARE_FBINOP(fadd, x + y)
+DECLARE_FBINOP(fsub, x - y)
+DECLARE_FBINOP(fdiv, x / y)
+DECLARE_FUNOP(fsqrt, sqrt(x))
+DECLARE_FUNOP(next_up, nextafter(x, INFINITY))
+DECLARE_FUNOP(next_down, nextafter(x, -INFINITY))
+
+value coq_is_double(value x) {
+  return Val_long(Is_double(x));
+}
diff --git a/kernel/byterun/coq_float64.h b/kernel/byterun/coq_float64.h
deleted file mode 100644
index 84a3edf1c7..0000000000
--- a/kernel/byterun/coq_float64.h
+++ /dev/null
@@ -1,58 +0,0 @@
-/************************************************************************/
-/*         *   The Coq Proof Assistant / The Coq Development Team       */
-/*  v      *         Copyright INRIA, CNRS and contributors             */
-/* <O___,, * (see version control and CREDITS file for authors & dates) */
-/*   \VV/  **************************************************************/
-/*    //   *    This file is distributed under the terms of the         */
-/*         *     GNU Lesser General Public License Version 2.1          */
-/*         *     (see LICENSE file for the text of the license)         */
-/************************************************************************/
-
-#ifndef _COQ_FLOAT64_
-#define _COQ_FLOAT64_
-
-#include <math.h>
-
-#define DECLARE_FREL(name, e)                                           \
-  int coq_##name(double x, double y) {                                  \
-    return e;                                                           \
-  }                                                                     \
-                                                                        \
-  value coq_##name##_byte(value x, value y) {                           \
-    return coq_##name(Double_val(x), Double_val(y));                    \
-  }
-
-#define DECLARE_FBINOP(name, e)                                         \
-  double coq_##name(double x, double y) {                               \
-    return e;                                                           \
-  }                                                                     \
-                                                                        \
-  value coq_##name##_byte(value x, value y) {                           \
-    return caml_copy_double(coq_##name(Double_val(x), Double_val(y)));  \
-  }
-
-#define DECLARE_FUNOP(name, e)                                          \
-  double coq_##name(double x) {                                         \
-    return e;                                                           \
-  }                                                                     \
-                                                                        \
-  value coq_##name##_byte(value x) {                                    \
-    return caml_copy_double(coq_##name(Double_val(x)));                 \
-  }
-
-DECLARE_FREL(feq, x == y)
-DECLARE_FREL(flt, x < y)
-DECLARE_FREL(fle, x <= y)
-DECLARE_FBINOP(fmul, x * y)
-DECLARE_FBINOP(fadd, x + y)
-DECLARE_FBINOP(fsub, x - y)
-DECLARE_FBINOP(fdiv, x / y)
-DECLARE_FUNOP(fsqrt, sqrt(x))
-DECLARE_FUNOP(next_up, nextafter(x, INFINITY))
-DECLARE_FUNOP(next_down, nextafter(x, -INFINITY))
-
-value coq_is_double(value x) {
-  return Val_long(Is_double(x));
-}
-
-#endif /* _COQ_FLOAT64_ */
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index e94af96b72..0f7713a6bb 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -28,7 +28,6 @@
 #include "coq_fix_code.h"
 #include "coq_memory.h"
 #include "coq_values.h"
-#include "coq_float64.h"
 
 #if OCAML_VERSION < 41000
 extern void caml_minor_collection(void);
diff --git a/kernel/byterun/dune b/kernel/byterun/dune
index 2998178be2..d3e2a2fa7f 100644
--- a/kernel/byterun/dune
+++ b/kernel/byterun/dune
@@ -4,7 +4,7 @@
  (public_name coq.vm)
  (foreign_stubs
   (language c)
-  (names coq_fix_code coq_memory coq_values coq_interp)
+  (names coq_fix_code coq_float64 coq_memory coq_values coq_interp)
   (flags (:include %{project_root}/config/dune.c_flags))))
 
 (rule
-- 
cgit v1.2.3