Merge PR #9867: Add primitive floats (binary64 floating-point numbers)

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
Ack-by: proux01
Ack-by: silene
Ack-by: vbgl

1 files changed, 10 insertions, 0 deletions

diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml
index 5c4028e1c8..85b44528a7 100644
--- a/kernel/uint63_63.ml
+++ b/kernel/uint63_63.ml
@@ -27,6 +27,12 @@ let to_int2 i = (0,i)
 
 let of_int64 _i = assert false
 
+let of_float = int_of_float
+
+external to_float : int -> (float [@unboxed])
+  = "coq_uint63_to_float_byte" "coq_uint63_to_float"
+[@@noalloc]
+
 let hash i = i
 [@@ocaml.inline always]
 
@@ -96,6 +102,10 @@ let le (x : int) (y : int) =
   (x lxor 0x4000000000000000) <= (y lxor 0x4000000000000000)
 [@@ocaml.inline always]
 
+let to_int_min n m =
+  if lt n m then n else m
+[@@ocaml.inline always]
+
     (* division of two numbers by one *)
 (* precondition: xh < y *)
 (* outputs: q, r s.t. x = q * y + r, r < y *)