Add primitive float computation in Coq kernel

Beware of 0. = -0. issue for primitive floats

The IEEE 754 declares that 0. and -0. are treated equal but we cannot
say that this is true with Leibniz equality.
Therefore we must patch the equality and the total comparison inside the
kernel to prevent inconsistency.

1 files changed, 6 insertions, 0 deletions

diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index c8f5020d71..fe3c76c960 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -57,6 +57,7 @@ type structured_constant =
   | Const_univ_level of Univ.Level.t
   | Const_val of structured_values
   | Const_uint of Uint63.t
+  | Const_float of Float64.t
 
 type reloc_table = (tag * int) array
 
@@ -105,6 +106,8 @@ let eq_structured_constant c1 c2 = match c1, c2 with
 | Const_val _, _ -> false
 | Const_uint i1, Const_uint i2 -> Uint63.equal i1 i2
 | Const_uint _, _ -> false
+| Const_float f1, Const_float f2 -> Float64.equal f1 f2
+| Const_float _, _ -> false
 
 let hash_structured_constant c =
   let open Hashset.Combine in
@@ -115,6 +118,7 @@ let hash_structured_constant c =
   | Const_univ_level l -> combinesmall 4 (Univ.Level.hash l)
   | Const_val v -> combinesmall 5 (hash_structured_values v)
   | Const_uint i -> combinesmall 6 (Uint63.hash i)
+  | Const_float f -> combinesmall 7 (Float64.hash f)
 
 let eq_annot_switch asw1 asw2 =
   let eq_ci ci1 ci2 =
@@ -149,6 +153,7 @@ let pp_struct_const = function
   | Const_univ_level l -> Univ.Level.pr l
   | Const_val _ -> Pp.str "(value)"
   | Const_uint i -> Pp.str (Uint63.to_string i)
+  | Const_float f -> Pp.str (Float64.to_string f)
 
 (* Abstract data *)
 type vprod
@@ -426,6 +431,7 @@ let obj_of_str_const str =
   | Const_univ_level l -> Obj.repr (Vuniv_level l)
   | Const_val v -> Obj.repr v
   | Const_uint i -> Obj.repr i
+  | Const_float f -> Obj.repr f
 
 let val_of_block tag (args : structured_values array) =
   let nargs = Array.length args in