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

diff --git a/kernel/primred.ml b/kernel/primred.ml
index d6d0a6143a..1b9badfca9 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -14,6 +14,13 @@ let add_retroknowledge env action =
       | None -> { retro with retro_int63 = Some c }
       | Some c' -> assert (Constant.equal c c'); retro in
     set_retroknowledge env retro
+  | Register_type(PT_float64,c) ->
+    let retro = env.retroknowledge in
+    let retro =
+      match retro.retro_float64 with
+      | None -> { retro with retro_float64 = Some c }
+      | Some c' -> assert (Constant.equal c c'); retro in
+    set_retroknowledge env retro
   | Register_ind(pit,ind) ->
     let retro = env.retroknowledge in
     let retro =
@@ -42,6 +49,12 @@ let add_retroknowledge env action =
           | None -> ((ind,1), (ind,2), (ind,3))
           | Some (((ind',_),_,_) as t) -> assert (eq_ind ind ind'); t in
         { retro with retro_cmp = Some r }
+      | PIT_option ->
+        let r =
+          match retro.retro_option with
+          | None -> ((ind,1), (ind,2))
+          | Some (((ind',_),_) as t) -> assert (eq_ind ind ind'); t in
+        { retro with retro_option = Some r }
     in
     set_retroknowledge env retro
 
@@ -50,6 +63,17 @@ let get_int_type env =
   | Some c -> c
   | None -> anomaly Pp.(str"Reduction of primitive: int63 not registered")
 
+let get_float_type env =
+  match env.retroknowledge.retro_float64 with
+  | Some c -> c
+  | None -> anomaly Pp.(str"Reduction of primitive: float64 not registered")
+
+let get_cmp_type env =
+  match env.retroknowledge.retro_cmp with
+  | Some (((mindcmp,_),_),_,_) ->
+     Constant.make (MutInd.user mindcmp) (MutInd.canonical mindcmp)
+  | None -> anomaly Pp.(str"Reduction of primitive: comparison not registered")
+
 let get_bool_constructors env =
   match env.retroknowledge.retro_bool with
   | Some r -> r
@@ -70,6 +94,11 @@ let get_cmp_constructors env =
   | Some r -> r
   | None -> anomaly Pp.(str"Reduction of primitive: cmp not registered")
 
+let get_option_constructors env =
+  match env.retroknowledge.retro_option with
+  | Some r -> r
+  | None -> anomaly Pp.(str"Reduction of primitive: option not registered")
+
 exception NativeDestKO
 
 module type RedNativeEntries =
@@ -80,14 +109,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 =
@@ -116,6 +149,12 @@ struct
   let get_int3 evd args =
     get_int evd args 0, get_int evd args 1, get_int evd args 2
 
+  let get_float evd args i = E.get_float evd (E.get args i)
+
+  let get_float1 evd args = get_float evd args 0
+
+  let get_float2 evd args = get_float evd args 0, get_float evd args 1
+
   let red_prim_aux env evd op args =
     let open CPrimitives in
     match op with
@@ -193,6 +232,39 @@ struct
         | 0 -> E.mkEq env
         | _ -> E.mkGt env
       end
+    | Float64opp ->
+      let f = get_float1 evd args in E.mkFloat env (Float64.opp f)
+    | Float64abs ->
+      let f = get_float1 evd args in E.mkFloat env (Float64.abs f)
+    | Float64compare ->
+      let f1, f2 = get_float2 evd args in
+      (match Float64.compare f1 f2 with
+      | Float64.Eq -> E.mkSomeCmp env (E.mkEq env)
+      | Float64.Lt -> E.mkSomeCmp env (E.mkLt env)
+      | Float64.Gt -> E.mkSomeCmp env (E.mkGt env)
+      | Float64.NotComparable -> E.mkNoneCmp env)
+    | Float64add ->
+      let f1, f2 = get_float2 evd args in E.mkFloat env (Float64.add f1 f2)
+    | Float64sub ->
+      let f1, f2 = get_float2 evd args in E.mkFloat env (Float64.sub f1 f2)
+    | Float64mul ->
+      let f1, f2 = get_float2 evd args in E.mkFloat env (Float64.mul f1 f2)
+    | Float64div ->
+      let f1, f2 = get_float2 evd args in E.mkFloat env (Float64.div f1 f2)
+    | Float64sqrt ->
+      let f = get_float1 evd args in E.mkFloat env (Float64.sqrt f)
+    | Float64ofInt63 ->
+      let i = get_int1 evd args in E.mkFloat env (Float64.of_int63 i)
+    | Float64normfr_mantissa ->
+      let f = get_float1 evd args in E.mkInt env (Float64.normfr_mantissa f)
+    | Float64frshiftexp ->
+      let f = get_float1 evd args in
+      let (m,e) = Float64.frshiftexp f in
+      E.mkFloatIntPair env (E.mkFloat env m) (E.mkInt env e)
+    | Float64ldshiftexp ->
+      let f = get_float evd args 0 in
+      let e = get_int evd args 1 in
+      E.mkFloat env (Float64.ldshiftexp f e)
 
   let red_prim env evd p args =
     try