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

diff --git a/kernel/primred.mli b/kernel/primred.mli
index f5998982d7..b2c9ebc6ea 100644
--- a/kernel/primred.mli
+++ b/kernel/primred.mli
@@ -5,10 +5,13 @@ open Environ
 val add_retroknowledge : env -> Retroknowledge.action -> env
 
 val get_int_type : env -> Constant.t
+val get_float_type : env -> Constant.t
+val get_cmp_type : env -> Constant.t
 val get_bool_constructors : env -> constructor * constructor
 val get_carry_constructors : env -> constructor * constructor
 val get_pair_constructor : env -> constructor
 val get_cmp_constructors : env -> constructor * constructor * constructor
+val get_option_constructors : env -> constructor * constructor
 
 exception NativeDestKO (* Should be raised by get_* functions on failure *)
 
@@ -20,13 +23,18 @@ module type RedNativeEntries =
 
     val get : args -> int -> elem
     val get_int : evd -> elem -> Uint63.t
+    val get_float : evd -> elem -> Float64.t
     val mkInt : env -> Uint63.t -> elem
+    val mkFloat : env -> Float64.t -> elem
     val mkBool : env -> bool -> elem
     val mkCarry : env -> bool -> elem -> elem (* true if carry *)
     val mkIntPair : env -> elem -> elem -> elem
+    val mkFloatIntPair : env -> elem -> elem -> elem
     val mkLt : env -> elem
     val mkEq : env -> elem
     val mkGt : env -> elem
+    val mkSomeCmp : env -> elem -> elem
+    val mkNoneCmp : env -> elem
   end
 
 module type RedNative =