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, 146 insertions, 6 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 3fd613e905..72585e5014 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -348,6 +348,7 @@ and fterm =
   | FLetIn of Name.t Context.binder_annot * fconstr * fconstr * constr * fconstr subs
   | FEvar of existential * fconstr subs
   | FInt of Uint63.t
+  | FFloat of Float64.t
   | FLIFT of int * fconstr
   | FCLOS of constr * fconstr subs
   | FLOCKED
@@ -428,7 +429,7 @@ let rec stack_args_size = function
 let rec lft_fconstr n ft =
   let r = Mark.relevance ft.mark in
   match ft.term with
-    | (FInd _|FConstruct _|FFlex(ConstKey _|VarKey _)|FInt _) -> ft
+    | (FInd _|FConstruct _|FFlex(ConstKey _|VarKey _)|FInt _|FFloat _) -> ft
     | FRel i -> {mark=mark Norm r;term=FRel(i+n)}
     | FLambda(k,tys,f,e) -> {mark=mark Cstr r; term=FLambda(k,tys,f,subs_shft(n,e))}
     | FFix(fx,e) ->
@@ -499,6 +500,7 @@ let mk_clos e t =
     | Ind kn -> {mark = mark Norm KnownR; term = FInd kn }
     | Construct kn -> {mark = mark Cstr Unknown; term = FConstruct kn }
     | Int i -> {mark = mark Cstr Unknown; term = FInt i}
+    | Float f -> {mark = mark Cstr Unknown; term = FFloat f}
     | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) ->
         {mark = mark Red Unknown; term = FCLOS(t,e)}
 
@@ -616,6 +618,8 @@ let rec to_constr lfts v =
 
     | FInt i ->
        Constr.mkInt i
+    | FFloat f ->
+        Constr.mkFloat f
 
     | FCLOS (t,env) ->
       if is_subs_id env && is_lift_id lfts then t
@@ -926,7 +930,7 @@ let rec knh info m stk =
 
 (* cases where knh stops *)
     | (FFlex _|FLetIn _|FConstruct _|FEvar _|
-       FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _|FInt _) ->
+       FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _|FInt _|FFloat _) ->
         (m, stk)
 
 (* The same for pure terms *)
@@ -940,7 +944,7 @@ and knht info e t stk =
     | Cast(a,_,_) -> knht info e a stk
     | Rel n -> knh info (clos_rel e n) stk
     | Proj (p, c) -> knh info { mark = mark Red Unknown; term = FProj (p, mk_clos e c) } stk
-    | (Ind _|Const _|Construct _|Var _|Meta _ | Sort _ | Int _) -> (mk_clos e t, stk)
+    | (Ind _|Const _|Construct _|Var _|Meta _ | Sort _ | Int _|Float _) -> (mk_clos e t, stk)
     | CoFix cfx -> { mark = mark Cstr Unknown; term = FCoFix (cfx,e) }, stk
     | Lambda _ -> { mark = mark Cstr Unknown; term = mk_lambda e t }, stk
     | Prod (n, t, c) ->
@@ -969,6 +973,11 @@ module FNativeEntries =
       | FInt i -> i
       | _ -> raise Primred.NativeDestKO
 
+    let get_float () e =
+      match [@ocaml.warning "-4"] e.term with
+      | FFloat f -> f
+      | _ -> raise Primred.NativeDestKO
+
     let dummy = {mark = mark Norm KnownR; term = FRel 0}
 
     let current_retro = ref Retroknowledge.empty
@@ -982,6 +991,16 @@ module FNativeEntries =
         fint := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) }
       | None -> defined_int := false
 
+    let defined_float = ref false
+    let ffloat = ref dummy
+
+    let init_float retro =
+      match retro.Retroknowledge.retro_float64 with
+      | Some c ->
+        defined_float := true;
+        ffloat := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) }
+      | None -> defined_float := false
+
     let defined_bool = ref false
     let ftrue = ref dummy
     let ffalse = ref dummy
@@ -1020,6 +1039,7 @@ module FNativeEntries =
     let fEq = ref dummy
     let fLt = ref dummy
     let fGt = ref dummy
+    let fcmp = ref dummy
 
     let init_cmp retro =
       match retro.Retroknowledge.retro_cmp with
@@ -1027,9 +1047,54 @@ module FNativeEntries =
         defined_cmp := true;
         fEq := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cEq) };
         fLt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cLt) };
-        fGt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cGt) }
+        fGt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cGt) };
+        let (icmp, _) = cEq in
+        fcmp := { mark = mark Norm KnownR; term = FInd (Univ.in_punivs icmp) }
       | None -> defined_cmp := false
 
+    let defined_f_cmp = ref false
+    let fFEq = ref dummy
+    let fFLt = ref dummy
+    let fFGt = ref dummy
+    let fFNotComparable = ref dummy
+
+    let init_f_cmp retro =
+      match retro.Retroknowledge.retro_f_cmp with
+      | Some (cFEq, cFLt, cFGt, cFNotComparable) ->
+        defined_f_cmp := true;
+        fFEq := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cFEq) };
+        fFLt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cFLt) };
+        fFGt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cFGt) };
+        fFNotComparable :=
+          { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cFNotComparable) };
+      | None -> defined_f_cmp := false
+
+    let defined_f_class = ref false
+    let fPNormal = ref dummy
+    let fNNormal = ref dummy
+    let fPSubn = ref dummy
+    let fNSubn = ref dummy
+    let fPZero = ref dummy
+    let fNZero = ref dummy
+    let fPInf = ref dummy
+    let fNInf = ref dummy
+    let fNaN = ref dummy
+
+    let init_f_class retro =
+      match retro.Retroknowledge.retro_f_class with
+      | Some (cPNormal, cNNormal, cPSubn, cNSubn, cPZero, cNZero,
+              cPInf, cNInf, cNaN) ->
+        defined_f_class := true;
+        fPNormal := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cPNormal) };
+        fNNormal := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNNormal) };
+        fPSubn := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cPSubn) };
+        fNSubn := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNSubn) };
+        fPZero := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cPZero) };
+        fNZero := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNZero) };
+        fPInf := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cPInf) };
+        fNInf := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNInf) };
+        fNaN := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNaN) };
+      | None -> defined_f_class := false
     let defined_refl = ref false
 
     let frefl = ref dummy
@@ -1044,10 +1109,13 @@ module FNativeEntries =
     let init env =
       current_retro := env.retroknowledge;
       init_int !current_retro;
+      init_float !current_retro;
       init_bool !current_retro;
       init_carry !current_retro;
       init_pair !current_retro;
       init_cmp !current_retro;
+      init_f_cmp !current_retro;
+      init_f_class !current_retro;
       init_refl !current_retro
 
     let check_env env =
@@ -1057,6 +1125,10 @@ module FNativeEntries =
       check_env env;
       assert (!defined_int)
 
+    let check_float env =
+      check_env env;
+      assert (!defined_float)
+
     let check_bool env =
       check_env env;
       assert (!defined_bool)
@@ -1073,10 +1145,22 @@ module FNativeEntries =
       check_env env;
       assert (!defined_cmp)
 
+    let check_f_cmp env =
+      check_env env;
+      assert (!defined_f_cmp)
+
+    let check_f_class env =
+      check_env env;
+      assert (!defined_f_class)
+
     let mkInt env i =
       check_int env;
       { mark = mark Cstr KnownR; term = FInt i }
 
+    let mkFloat env f =
+      check_float env;
+      { mark = mark Norm KnownR; term = FFloat f }
+
     let mkBool env b =
       check_bool env;
       if b then !ftrue else !ffalse
@@ -1090,6 +1174,11 @@ module FNativeEntries =
       check_pair env;
       { mark = mark Cstr KnownR; term = FApp(!fPair, [|!fint;!fint;e1;e2|]) }
 
+    let mkFloatIntPair env f i =
+      check_pair env;
+      check_float env;
+      { mark = mark Cstr KnownR; term = FApp(!fPair, [|!ffloat;!fint;f;i|]) }
+
     let mkLt env =
       check_cmp env;
       !fLt
@@ -1102,6 +1191,57 @@ module FNativeEntries =
       check_cmp env;
       !fGt
 
+    let mkFLt env =
+      check_f_cmp env;
+      !fFLt
+
+    let mkFEq env =
+      check_f_cmp env;
+      !fFEq
+
+    let mkFGt env =
+      check_f_cmp env;
+      !fFGt
+
+    let mkFNotComparable env =
+      check_f_cmp env;
+      !fFNotComparable
+
+    let mkPNormal env =
+      check_f_class env;
+      !fPNormal
+
+    let mkNNormal env =
+      check_f_class env;
+      !fNNormal
+
+    let mkPSubn env =
+      check_f_class env;
+      !fPSubn
+
+    let mkNSubn env =
+      check_f_class env;
+      !fNSubn
+
+    let mkPZero env =
+      check_f_class env;
+      !fPZero
+
+    let mkNZero env =
+      check_f_class env;
+      !fNZero
+
+    let mkPInf env =
+      check_f_class env;
+      !fPInf
+
+    let mkNInf env =
+      check_f_class env;
+      !fNInf
+
+    let mkNaN env =
+      check_f_class env;
+      !fNaN
   end
 
 module FredNative = RedNative(FNativeEntries)
@@ -1164,7 +1304,7 @@ let rec knr info tab m stk =
       (match info.i_cache.i_sigma ev with
           Some c -> knit info tab env c stk
         | None -> (m,stk))
-  | FInt _ ->
+  | FInt _ | FFloat _ ->
     (match [@ocaml.warning "-4"] strip_update_shift_app m stk with
      | (_, _, Zprimitive(op,c,rargs,nargs)::s) ->
        let (rargs, nargs) = skip_native_args (m::rargs) nargs in
@@ -1270,7 +1410,7 @@ and norm_head info tab m =
       | FProj (p,c) ->
           mkProj (p, kl info tab c)
       | FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FConstruct _
-        | FApp _ | FCaseT _ | FLIFT _ | FCLOS _ | FInt _ -> term_of_fconstr m
+        | FApp _ | FCaseT _ | FLIFT _ | FCLOS _ | FInt _ | FFloat _ -> term_of_fconstr m
 
 (* Initialization and then normalization *)