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/nativevalues.mli | 73 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 73 insertions(+)

(limited to 'kernel/nativevalues.mli')

diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index b54f437e73..d19877c121 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -102,6 +102,9 @@ val mk_int : int -> t
 val mk_uint : Uint63.t -> t
 [@@ocaml.inline always]
 
+val mk_float : Float64.t -> t
+[@@ocaml.inline always]
+
 val napply : t -> t array -> t
 (* Functions over accumulators *)
 
@@ -130,6 +133,7 @@ type kind_of_value =
   | Vfun of (t -> t)
   | Vconst of int
   | Vint64 of int64
+  | Vfloat64 of float
   | Vblock of block
 
 val kind_of_value : t -> kind_of_value
@@ -140,7 +144,9 @@ val str_decode : string -> 'a
 (** Support for machine integers *)
 
 val val_to_int : t -> int
+
 val is_int : t -> bool
+[@@ocaml.inline always]
 
 (* function with check *)
 val head0 : t -> t -> t
@@ -247,3 +253,70 @@ val no_check_le      : t -> t -> t
 [@@ocaml.inline always]
 
 val no_check_compare : t -> t -> t
+
+(** Support for machine floating point values *)
+
+val is_float : t -> bool
+[@@ocaml.inline always]
+
+val fopp : t -> t -> t
+val fabs : t -> t -> t
+val fcompare : t -> t -> t -> t
+val fclassify : t -> t -> t
+val fadd : t -> t -> t -> t
+val fsub : t -> t -> t -> t
+val fmul : t -> t -> t -> t
+val fdiv : t -> t -> t -> t
+val fsqrt : t -> t -> t
+val float_of_int : t -> t -> t
+val normfr_mantissa : t -> t -> t
+val frshiftexp : t -> t -> t
+val ldshiftexp : t -> t -> t -> t
+val next_up : t -> t -> t
+val next_down : t -> t -> t
+
+(* Function without check *)
+val no_check_fopp : t -> t
+[@@ocaml.inline always]
+
+val no_check_fabs : t -> t
+[@@ocaml.inline always]
+
+val no_check_fcompare : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_fclassify : t -> t
+[@@ocaml.inline always]
+
+val no_check_fadd : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_fsub : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_fmul : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_fdiv : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_fsqrt : t -> t
+[@@ocaml.inline always]
+
+val no_check_float_of_int : t -> t
+[@@ocaml.inline always]
+
+val no_check_normfr_mantissa : t -> t
+[@@ocaml.inline always]
+
+val no_check_frshiftexp : t -> t
+[@@ocaml.inline always]
+
+val no_check_ldshiftexp : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_next_up : t -> t
+[@@ocaml.inline always]
+
+val no_check_next_down : t -> t
+[@@ocaml.inline always]
-- 
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 <pierre.roux@onera.fr>
---
 kernel/nativevalues.mli | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'kernel/nativevalues.mli')

diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index d19877c121..815ef3e98e 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -261,6 +261,9 @@ val is_float : t -> bool
 
 val fopp : t -> t -> t
 val fabs : t -> t -> t
+val feq : t -> t -> t -> t
+val flt : t -> t -> t -> t
+val fle : t -> t -> t -> t
 val fcompare : t -> t -> t -> t
 val fclassify : t -> t -> t
 val fadd : t -> t -> t -> t
@@ -282,6 +285,15 @@ val no_check_fopp : t -> t
 val no_check_fabs : t -> t
 [@@ocaml.inline always]
 
+val no_check_feq : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_flt : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_fle : t -> t -> t
+[@@ocaml.inline always]
+
 val no_check_fcompare : t -> t -> t
 [@@ocaml.inline always]
 
-- 
cgit v1.2.3