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.

1 files changed, 27 insertions, 0 deletions

diff --git a/kernel/float64.mli b/kernel/float64.mli
index 580004126d..1e6ea8bb96 100644
--- a/kernel/float64.mli
+++ b/kernel/float64.mli
@@ -15,10 +15,14 @@ indistinguishable from Coq's perspective. *)
 type t
 
 val is_nan : t -> bool
+val is_infinity : t -> bool
+val is_neg_infinity : t -> bool
 
 val to_string : t -> string
 val of_string : string -> t
 
+val compile : t -> string
+
 val of_float : float -> t
 
 val opp : t -> t
@@ -29,32 +33,55 @@ type float_comparison = FEq | FLt | FGt | FNotComparable
 (** The IEEE 754 float comparison.
  * NotComparable is returned if there is a NaN in the arguments *)
 val compare : t -> t -> float_comparison
+[@@ocaml.inline always]
 
 type float_class =
   | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN
 
 val classify : t -> float_class
+[@@ocaml.inline always]
 
 val mul : t -> t -> t
+[@@ocaml.inline always]
+
 val add : t -> t -> t
+[@@ocaml.inline always]
+
 val sub : t -> t -> t
+[@@ocaml.inline always]
+
 val div : t -> t -> t
+[@@ocaml.inline always]
+
 val sqrt : t -> t
+[@@ocaml.inline always]
 
 (** Link with integers *)
 val of_int63 : Uint63.t -> t
+[@@ocaml.inline always]
+
 val normfr_mantissa : t -> Uint63.t
+[@@ocaml.inline always]
 
 (** Shifted exponent extraction *)
+val eshift : int
+
 val frshiftexp : t -> t * Uint63.t (* float remainder, shifted exponent *)
+[@@ocaml.inline always]
+
 val ldshiftexp : t -> Uint63.t -> t
+[@@ocaml.inline always]
 
 val next_up : t -> t
+[@@ocaml.inline always]
+
 val next_down : t -> t
+[@@ocaml.inline always]
 
 (** Return true if two floats are equal.
  * All NaN values are considered equal. *)
 val equal : t -> t -> bool
+[@@ocaml.inline always]
 
 val hash : t -> int