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, 12 insertions, 1 deletions

diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml
index b8eccd19fb..e38389ca13 100644
--- a/kernel/uint63_31.ml
+++ b/kernel/uint63_31.ml
@@ -26,6 +26,13 @@ let mask63 i = Int64.logand i maxuint63
 let of_int i = Int64.of_int i
 let to_int2 i = (Int64.to_int (Int64.shift_right_logical i 31), Int64.to_int i)
 let of_int64 i = i
+
+let to_int_min n m =
+  if Int64.(compare n (of_int m)) < 0 then Int64.to_int n else m
+
+let of_float f = mask63 (Int64.of_float f)
+let to_float = Int64.to_float
+
 let hash i =
   let (h,l) = to_int2 i in
   (*Hashset.combine h l*)
@@ -213,4 +220,8 @@ let () =
   Callback.register "uint63 one" one;
   Callback.register "uint63 sub" sub;
   Callback.register "uint63 subcarry" subcarry;
-  Callback.register "uint63 tail0" tail0
+  Callback.register "uint63 tail0" tail0;
+  Callback.register "uint63 of_float" of_float;
+  Callback.register "uint63 to_float" to_float;
+  Callback.register "uint63 of_int" of_int;
+  Callback.register "uint63 to_int_min" to_int_min