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, 178 insertions, 0 deletions

diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index f788832d5b..e4a8344eaf 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -225,6 +225,9 @@ let mk_bool (b : bool) = (Obj.magic (not b) : t)
 let mk_uint (x : Uint63.t) = (Obj.magic x : t)
 [@@ocaml.inline always]
 
+let mk_float (x : Float64.t) = (Obj.magic x : t)
+[@@ocaml.inline always]
+
 type block
 
 let block_size (b:block) =
@@ -240,16 +243,19 @@ type kind_of_value =
   | Vfun of (t -> t)
   | Vconst of int
   | Vint64 of int64
+  | Vfloat64 of float
   | Vblock of block
 
 let kind_of_value (v:t) =
   let o = Obj.repr v in
   if Obj.is_int o then Vconst (Obj.magic v)
+  else if Obj.tag o == Obj.double_tag then Vfloat64 (Obj.magic v)
   else
     let tag = Obj.tag o in
     if Int.equal tag accumulate_tag then
       Vaccu (Obj.magic v)
     else if Int.equal tag Obj.custom_tag then Vint64 (Obj.magic v)
+    else if Int.equal tag Obj.double_tag then Vfloat64 (Obj.magic v)
     else if (tag < Obj.lazy_tag) then Vblock (Obj.magic v)
       else
         (* assert (tag = Obj.closure_tag || tag = Obj.infix_tag); 
@@ -261,6 +267,7 @@ let kind_of_value (v:t) =
 let is_int (x:t) =
   let o = Obj.repr x in
   Obj.is_int o || Int.equal (Obj.tag o) Obj.custom_tag
+[@@ocaml.inline always]
 
 let val_to_int (x:t) = (Obj.magic x : int)
 [@@ocaml.inline always]
@@ -508,6 +515,177 @@ let print x =
   flush stderr;
   x
 
+(** Support for machine floating point values *)
+
+external is_float : t -> bool = "coq_is_double"
+[@@noalloc]
+
+let to_float (x:t) = (Obj.magic x : Float64.t)
+[@@ocaml.inline always]
+
+let no_check_fopp x =
+  mk_float (Float64.opp (to_float x))
+[@@ocaml.inline always]
+
+let fopp accu x =
+  if is_float x then no_check_fopp x
+  else accu x
+
+let no_check_fabs x =
+  mk_float (Float64.abs (to_float x))
+[@@ocaml.inline always]
+
+let fabs accu x =
+  if is_float x then no_check_fabs x
+  else accu x
+
+let no_check_feq x y =
+  mk_bool (Float64.eq (to_float x) (to_float y))
+
+let feq accu x y =
+  if is_float x && is_float y then no_check_feq x y
+  else accu x y
+
+let no_check_flt x y =
+  mk_bool (Float64.lt (to_float x) (to_float y))
+
+let flt accu x y =
+  if is_float x && is_float y then no_check_flt x y
+  else accu x y
+
+let no_check_fle x y =
+  mk_bool (Float64.le (to_float x) (to_float y))
+
+let fle accu x y =
+  if is_float x && is_float y then no_check_fle x y
+  else accu x y
+
+type coq_fcmp =
+  | CFcmpAccu of t
+  | CFcmpEq
+  | CFcmpLt
+  | CFcmpGt
+  | CFcmpNotComparable
+
+let no_check_fcompare x y =
+  let c = Float64.compare (to_float x) (to_float y) in
+  (Obj.magic c:t)
+[@@ocaml.inline always]
+
+let fcompare accu x y =
+  if is_float x && is_float y then no_check_fcompare x y
+  else accu x y
+
+type coq_fclass =
+  | CFclassAccu of t
+  | CFclassPNormal
+  | CFclassNNormal
+  | CFclassPSubn
+  | CFclassNSubn
+  | CFclassPZero
+  | CFclassNZero
+  | CFclassPInf
+  | CFclassNInf
+  | CFclassNaN
+
+let no_check_fclassify x =
+  let c = Float64.classify (to_float x) in
+  (Obj.magic c:t)
+[@@ocaml.inline always]
+
+let fclassify accu x =
+  if is_float x then no_check_fclassify x
+  else accu x
+
+let no_check_fadd x y =
+  mk_float (Float64.add (to_float x) (to_float y))
+[@@ocaml.inline always]
+
+let fadd accu x y =
+  if is_float x && is_float y then no_check_fadd x y
+  else accu x y
+
+let no_check_fsub x y =
+  mk_float (Float64.sub (to_float x) (to_float y))
+[@@ocaml.inline always]
+
+let fsub accu x y =
+  if is_float x && is_float y then no_check_fsub x y
+  else accu x y
+
+let no_check_fmul x y =
+  mk_float (Float64.mul (to_float x) (to_float y))
+[@@ocaml.inline always]
+
+let fmul accu x y =
+  if is_float x && is_float y then no_check_fmul x y
+  else accu x y
+
+let no_check_fdiv x y =
+  mk_float (Float64.div (to_float x) (to_float y))
+[@@ocaml.inline always]
+
+let fdiv accu x y =
+  if is_float x && is_float y then no_check_fdiv x y
+  else accu x y
+
+let no_check_fsqrt x =
+  mk_float (Float64.sqrt (to_float x))
+[@@ocaml.inline always]
+
+let fsqrt accu x =
+  if is_float x then no_check_fsqrt x
+  else accu x
+
+let no_check_float_of_int x =
+  mk_float (Float64.of_int63 (to_uint x))
+[@@ocaml.inline always]
+
+let float_of_int accu x =
+  if is_int x then no_check_float_of_int x
+  else accu x
+
+let no_check_normfr_mantissa x =
+  mk_uint (Float64.normfr_mantissa (to_float x))
+[@@ocaml.inline always]
+
+let normfr_mantissa accu x =
+  if is_float x then no_check_normfr_mantissa x
+  else accu x
+
+let no_check_frshiftexp x =
+  let f, e = Float64.frshiftexp (to_float x) in
+  (Obj.magic (PPair(mk_float f, mk_uint e)):t)
+[@@ocaml.inline always]
+
+let frshiftexp accu x =
+  if is_float x then no_check_frshiftexp x
+  else accu x
+
+let no_check_ldshiftexp x e =
+  mk_float (Float64.ldshiftexp (to_float x) (to_uint e))
+[@@ocaml.inline always]
+
+let ldshiftexp accu x e =
+  if is_float x && is_int e then no_check_ldshiftexp x e
+  else accu x e
+
+let no_check_next_up x =
+  mk_float (Float64.next_up (to_float x))
+[@@ocaml.inline always]
+
+let next_up accu x =
+  if is_float x then no_check_next_up x
+  else accu x
+
+let no_check_next_down x =
+  mk_float (Float64.next_down (to_float x))
+[@@ocaml.inline always]
+
+let next_down accu x =
+  if is_float x then no_check_next_down x
+  else accu x
+
 let hobcnv = Array.init 256 (fun i -> Printf.sprintf "%02x" i)
 let bohcnv = Array.init 256 (fun i -> i -
                                       (if 0x30 <= i then 0x30 else 0) -