Implement classify on primitive float

26 files changed, 369 insertions, 15 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index bca2cc3bd9..fb39ca8358 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -65,6 +65,7 @@ void init_arity () {
     arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]=
     arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]=
     arity[CHECKOPPFLOAT]=arity[CHECKABSFLOAT]=arity[CHECKCOMPAREFLOAT]=
+    arity[CHECKCLASSIFYFLOAT]=
     arity[CHECKADDFLOAT]=arity[CHECKSUBFLOAT]=arity[CHECKMULFLOAT]=
     arity[CHECKDIVFLOAT]=arity[CHECKSQRTFLOAT]=
     arity[CHECKFLOATOFINT63]=arity[CHECKFLOATNORMFRMANTISSA]=
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 74edd79872..b862480fda 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1565,6 +1565,31 @@ value coq_interprete
         Next;
       }
 
+      Instruct (CHECKCLASSIFYFLOAT) {
+        double x;
+        print_instr("CHECKCLASSIFYFLOAT");
+        CheckFloat1();
+        x = Double_val(accu);
+        switch (fpclassify(x)) {
+        case FP_NORMAL:
+          accu = signbit(x) ? coq_NNormal : coq_PNormal;
+          break;
+        case FP_SUBNORMAL:
+          accu = signbit(x) ? coq_NSubn : coq_PSubn;
+          break;
+        case FP_ZERO:
+          accu = signbit(x) ? coq_NZero : coq_PZero;
+          break;
+        case FP_INFINITE:
+          accu = signbit(x) ? coq_NInf : coq_PInf;
+          break;
+        default:  /* FP_NAN */
+          accu = coq_NaN;
+          break;
+        }
+        Next;
+      }
+
       Instruct (CHECKADDFLOAT) {
         print_instr("CHECKADDFLOAT");
         CheckFloat2();
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index c79a8f1b4f..b027673ac7 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -46,6 +46,15 @@
 #define coq_FLt Val_int(1)
 #define coq_FGt Val_int(2)
 #define coq_FNotComparable Val_int(3)
+#define coq_PNormal Val_int(0)
+#define coq_NNormal Val_int(1)
+#define coq_PSubn Val_int(2)
+#define coq_NSubn Val_int(3)
+#define coq_PZero Val_int(4)
+#define coq_NZero Val_int(5)
+#define coq_PInf Val_int(6)
+#define coq_NInf Val_int(7)
+#define coq_NaN Val_int(8)
 
 #define FLOAT_EXP_SHIFT (2101) /* 2*emax + prec */
 
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 77352595f1..72585e5014 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -1069,6 +1069,32 @@ module FNativeEntries =
           { 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
@@ -1089,6 +1115,7 @@ module FNativeEntries =
       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 =
@@ -1122,6 +1149,10 @@ module FNativeEntries =
       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 }
@@ -1175,6 +1206,42 @@ module FNativeEntries =
     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)
diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index d5ed2c1a06..02a5351ccf 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -36,6 +36,7 @@ type t =
   | Float64opp
   | Float64abs
   | Float64compare
+  | Float64classify
   | Float64add
   | Float64sub
   | Float64mul
@@ -77,15 +78,16 @@ let hash = function
   | Float64opp -> 25
   | Float64abs -> 26
   | Float64compare -> 27
-  | Float64add -> 28
-  | Float64sub -> 29
-  | Float64mul -> 30
-  | Float64div -> 31
-  | Float64sqrt -> 32
-  | Float64ofInt63 -> 33
-  | Float64normfr_mantissa -> 34
-  | Float64frshiftexp -> 35
-  | Float64ldshiftexp -> 36
+  | Float64classify -> 28
+  | Float64add -> 29
+  | Float64sub -> 30
+  | Float64mul -> 31
+  | Float64div -> 32
+  | Float64sqrt -> 33
+  | Float64ofInt63 -> 34
+  | Float64normfr_mantissa -> 35
+  | Float64frshiftexp -> 36
+  | Float64ldshiftexp -> 37
 
 (* Should match names in nativevalues.ml *)
 let to_string = function
@@ -116,6 +118,7 @@ let to_string = function
   | Float64opp -> "fopp"
   | Float64abs -> "fabs"
   | Float64compare -> "fcompare"
+  | Float64classify -> "fclassify"
   | Float64add -> "fadd"
   | Float64sub -> "fsub"
   | Float64mul -> "fmul"
@@ -136,6 +139,7 @@ type 'a prim_ind =
   | PIT_pair : (prim_type * prim_type) prim_ind
   | PIT_cmp : unit prim_ind
   | PIT_f_cmp : unit prim_ind
+  | PIT_f_class : unit prim_ind
 
 type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex
 
@@ -166,6 +170,7 @@ let types =
   | Float64normfr_mantissa -> [float_ty; int_ty]
   | Float64frshiftexp -> [float_ty; PITT_ind (PIT_pair, (PT_float64, PT_int63))]
   | Float64compare -> [float_ty; float_ty; PITT_ind (PIT_f_cmp, ())]
+  | Float64classify -> [float_ty; PITT_ind (PIT_f_class, ())]
   | Float64add | Float64sub | Float64mul
   | Float64div -> [float_ty; float_ty; float_ty]
   | Float64ldshiftexp -> [float_ty; int_ty; float_ty]
@@ -198,6 +203,7 @@ let prim_ind_to_string (type a) (p : a prim_ind) = match p with
   | PIT_pair -> "pair"
   | PIT_cmp -> "cmp"
   | PIT_f_cmp -> "f_cmp"
+  | PIT_f_class -> "f_class"
 
 let prim_type_to_string = function
   | PT_int63 -> "int63_type"
diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli
index 3e6ec8dbcc..af95f6c6d7 100644
--- a/kernel/cPrimitives.mli
+++ b/kernel/cPrimitives.mli
@@ -36,6 +36,7 @@ type t =
   | Float64opp
   | Float64abs
   | Float64compare
+  | Float64classify
   | Float64add
   | Float64sub
   | Float64mul
@@ -75,6 +76,7 @@ type 'a prim_ind =
   | PIT_pair : (prim_type * prim_type) prim_ind
   | PIT_cmp : unit prim_ind
   | PIT_f_cmp : unit prim_ind
+  | PIT_f_class : unit prim_ind
 
 type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex
 
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 82dd7bd85d..535034d8fa 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -237,6 +237,7 @@ let check_prim_op = function
   | Float64opp     -> opCHECKOPPFLOAT
   | Float64abs     -> opCHECKABSFLOAT
   | Float64compare -> opCHECKCOMPAREFLOAT
+  | Float64classify -> opCHECKCLASSIFYFLOAT
   | Float64add     -> opCHECKADDFLOAT
   | Float64sub     -> opCHECKSUBFLOAT
   | Float64mul     -> opCHECKMULFLOAT
diff --git a/kernel/float64.ml b/kernel/float64.ml
index eebc8f35ef..7b54fd0c4b 100644
--- a/kernel/float64.ml
+++ b/kernel/float64.ml
@@ -38,6 +38,17 @@ let compare x y =
     )
   )
 
+type float_class =
+  | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN
+
+let classify x =
+  match classify_float x with
+  | FP_normal -> if 0. < x then PNormal else NNormal
+  | FP_subnormal -> if 0. < x then PSubn else NSubn
+  | FP_zero -> if 0. < 1. /. x then PZero else NZero
+  | FP_infinite -> if 0. < x then PInf else NInf
+  | FP_nan -> NaN
+
 let mul = ( *. )
 let add = ( +. )
 let sub = ( -. )
diff --git a/kernel/float64.mli b/kernel/float64.mli
index c82f1d84da..1ad980a691 100644
--- a/kernel/float64.mli
+++ b/kernel/float64.mli
@@ -30,6 +30,11 @@ type float_comparison = FEq | FLt | FGt | FNotComparable
  * NotComparable is returned if there is a NaN in the arguments *)
 val compare : t -> t -> float_comparison
 
+type float_class =
+  | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN
+
+val classify : t -> float_class
+
 val mul : t -> t -> t
 val add : t -> t -> t
 val sub : t -> t -> t
diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml
index 7deffd030b..045a1e361d 100644
--- a/kernel/genOpcodeFiles.ml
+++ b/kernel/genOpcodeFiles.ml
@@ -140,6 +140,7 @@ let opcodes =
     "CHECKOPPFLOAT";
     "CHECKABSFLOAT";
     "CHECKCOMPAREFLOAT";
+    "CHECKCLASSIFYFLOAT";
     "CHECKADDFLOAT";
     "CHECKSUBFLOAT";
     "CHECKMULFLOAT";
diff --git a/kernel/primred.ml b/kernel/primred.ml
index 5fe700cb9a..cfe6c8effe 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -55,6 +55,15 @@ let add_retroknowledge env action =
           | None -> ((ind,1), (ind,2), (ind,3), (ind,4))
           | Some (((ind',_),_,_,_) as t) -> assert (eq_ind ind ind'); t in
         { retro with retro_f_cmp = Some r }
+      | PIT_f_class ->
+        let r =
+          match retro.retro_f_class with
+          | None -> ((ind,1), (ind,2), (ind,3), (ind,4),
+                     (ind,5), (ind,6), (ind,7), (ind,8),
+                     (ind,9))
+          | Some (((ind',_),_,_,_,_,_,_,_,_) as t) ->
+             assert (eq_ind ind ind'); t in
+        { retro with retro_f_class = Some r }
     in
     set_retroknowledge env retro
 
@@ -99,6 +108,11 @@ let get_f_cmp_constructors env =
   | Some r -> r
   | None -> anomaly Pp.(str"Reduction of primitive: fcmp not registered")
 
+let get_f_class_constructors env =
+  match env.retroknowledge.retro_f_class with
+  | Some r -> r
+  | None -> anomaly Pp.(str"Reduction of primitive: fclass not registered")
+
 exception NativeDestKO
 
 module type RedNativeEntries =
@@ -123,6 +137,15 @@ module type RedNativeEntries =
     val mkFEq : env -> elem
     val mkFGt : env -> elem
     val mkFNotComparable : env -> elem
+    val mkPNormal : env -> elem
+    val mkNNormal : env -> elem
+    val mkPSubn : env -> elem
+    val mkNSubn : env -> elem
+    val mkPZero : env -> elem
+    val mkNZero : env -> elem
+    val mkPInf : env -> elem
+    val mkNInf : env -> elem
+    val mkNaN : env -> elem
   end
 
 module type RedNative =
@@ -245,6 +268,18 @@ struct
       | Float64.FLt -> E.mkFLt env
       | Float64.FGt -> E.mkFGt env
       | Float64.FNotComparable -> E.mkFNotComparable env)
+    | Float64classify ->
+      let f = get_float1 evd args in
+      (match Float64.classify f with
+      | Float64.PNormal -> E.mkPNormal env
+      | Float64.NNormal -> E.mkNNormal env
+      | Float64.PSubn -> E.mkPSubn env
+      | Float64.NSubn -> E.mkNSubn env
+      | Float64.PZero -> E.mkPZero env
+      | Float64.NZero -> E.mkNZero env
+      | Float64.PInf -> E.mkPInf env
+      | Float64.NInf -> E.mkNInf env
+      | Float64.NaN -> E.mkNaN env)
     | Float64add ->
       let f1, f2 = get_float2 evd args in E.mkFloat env (Float64.add f1 f2)
     | Float64sub ->
diff --git a/kernel/primred.mli b/kernel/primred.mli
index 5531c81550..bbe564d8e7 100644
--- a/kernel/primred.mli
+++ b/kernel/primred.mli
@@ -12,6 +12,10 @@ val get_carry_constructors : env -> constructor * constructor
 val get_pair_constructor : env -> constructor
 val get_cmp_constructors : env -> constructor * constructor * constructor
 val get_f_cmp_constructors : env -> constructor * constructor * constructor * constructor
+val get_f_class_constructors :
+  env -> constructor * constructor * constructor * constructor
+         * constructor * constructor * constructor * constructor
+         * constructor
 
 exception NativeDestKO (* Should be raised by get_* functions on failure *)
 
@@ -37,6 +41,15 @@ module type RedNativeEntries =
     val mkFEq : env -> elem
     val mkFGt : env -> elem
     val mkFNotComparable : env -> elem
+    val mkPNormal : env -> elem
+    val mkNNormal : env -> elem
+    val mkPSubn : env -> elem
+    val mkNSubn : env -> elem
+    val mkPZero : env -> elem
+    val mkNZero : env -> elem
+    val mkPInf : env -> elem
+    val mkNInf : env -> elem
+    val mkNaN : env -> elem
   end
 
 module type RedNative =
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index e897be6141..479fe02295 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -27,7 +27,14 @@ type retroknowledge = {
     retro_f_cmp : (constructor * constructor * constructor * constructor)
                   option;
                   (* FEq, FLt, FGt, FNotComparable *)
-    retro_refl : constructor option;
+    retro_f_class : (constructor * constructor * constructor * constructor
+                     * constructor * constructor * constructor * constructor
+                     * constructor)
+                      option;
+                    (* PNormal, NNormal, PSubn, NSubn,
+                       PZero, NZero, PInf, NInf,
+                       NaN *)
+    retro_refl : constructor option
 }
 
 let empty = {
@@ -38,6 +45,7 @@ let empty = {
     retro_pair = None;
     retro_cmp = None;
     retro_f_cmp = None;
+    retro_f_class = None;
     retro_refl = None;
 }
 
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 7aaf14e176..2df8a00465 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -21,7 +21,14 @@ type retroknowledge = {
     retro_f_cmp : (constructor * constructor * constructor * constructor)
                   option;
                     (* FEq, FLt, FGt, FNotComparable *)
-    retro_refl : constructor option;
+    retro_f_class : (constructor * constructor * constructor * constructor
+                     * constructor * constructor * constructor * constructor
+                     * constructor)
+                      option;
+                    (* PNormal, NNormal, PSubn, NSubn,
+                       PZero, NZero, PInf, NInf,
+                       NaN *)
+    retro_refl : constructor option
 }
 
 val empty : retroknowledge
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 241ee8ada3..d3cffd1546 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -1413,6 +1413,26 @@ let check_register_ind (type t) ind (r : t CPrimitives.prim_ind) env =
     check_type_cte 2;
     check_name 3 "FNotComparable";
     check_type_cte 3
+  | CPrimitives.PIT_f_class ->
+    check_nconstr 9;
+    check_name 0 "PNormal";
+    check_type_cte 0;
+    check_name 1 "NNormal";
+    check_type_cte 1;
+    check_name 2 "PSubn";
+    check_type_cte 2;
+    check_name 3 "NSubn";
+    check_type_cte 3;
+    check_name 4 "PZero";
+    check_type_cte 4;
+    check_name 5 "NZero";
+    check_type_cte 5;
+    check_name 6 "PInf";
+    check_type_cte 6;
+    check_name 7 "NInf";
+    check_type_cte 7;
+    check_name 8 "NaN";
+    check_type_cte 8
 
 let register_inductive ind prim senv =
   check_register_ind ind prim senv.env;
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 3e79b174b8..1cc40a6707 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -246,6 +246,11 @@ let type_of_prim env t =
     | Some ((ind,_),_,_,_) -> Constr.mkInd ind
     | None -> CErrors.user_err Pp.(str"The type float_comparison must be registered before this primitive.")
   in
+  let f_class_ty () =
+    match env.retroknowledge.Retroknowledge.retro_f_class with
+    | Some ((ind,_),_,_,_,_,_,_,_,_) -> Constr.mkInd ind
+    | None -> CErrors.user_err Pp.(str"The type float_class must be registered before this primitive.")
+  in
   let pair_ty fst_ty snd_ty =
     match env.retroknowledge.Retroknowledge.retro_pair with
     | Some (ind,_) -> Constr.mkApp(Constr.mkInd ind, [|fst_ty;snd_ty|])
@@ -265,7 +270,8 @@ let type_of_prim env t =
     | PIT_carry, t -> carry_ty (tr_prim_type t)
     | PIT_pair, (t1, t2) -> pair_ty (tr_prim_type t1) (tr_prim_type t2)
     | PIT_cmp, () -> compare_ty ()
-    | PIT_f_cmp, () -> f_compare_ty () in
+    | PIT_f_cmp, () -> f_compare_ty ()
+    | PIT_f_class, () -> f_class_ty () in
   let tr_type = function
     | PITT_ind (i, a) -> tr_ind i a
     | PITT_type t -> tr_prim_type t in
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index bac13a0bd7..c78f791a5a 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -228,7 +228,6 @@ module VNativeEntries =
         | _ -> raise Primred.NativeDestKO)
       | _ -> raise Primred.NativeDestKO
 
-
     let mkInt env i = VAL(0, mkInt i)
 
     let mkFloat env f = VAL(0, mkFloat f)
@@ -283,6 +282,51 @@ module VNativeEntries =
     let mkFNotComparable env =
       let (_eq,_lt,_gt,nc) = get_f_cmp_constructors env in
       CONSTR(Univ.in_punivs nc, [||])
+
+    let mkPNormal env =
+      let (pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,_nan) =
+        get_f_class_constructors env in
+      CONSTR(Univ.in_punivs pNormal, [||])
+
+    let mkNNormal env =
+      let (_pNormal,nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,_nan) =
+        get_f_class_constructors env in
+      CONSTR(Univ.in_punivs nNormal, [||])
+
+    let mkPSubn env =
+      let (_pNormal,_nNormal,pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,_nan) =
+        get_f_class_constructors env in
+      CONSTR(Univ.in_punivs pSubn, [||])
+
+    let mkNSubn env =
+      let (_pNormal,_nNormal,_pSubn,nSubn,_pZero,_nZero,_pInf,_nInf,_nan) =
+        get_f_class_constructors env in
+      CONSTR(Univ.in_punivs nSubn, [||])
+
+    let mkPZero env =
+      let (_pNormal,_nNormal,_pSubn,_nSubn,pZero,_nZero,_pInf,_nInf,_nan) =
+        get_f_class_constructors env in
+      CONSTR(Univ.in_punivs pZero, [||])
+
+    let mkNZero env =
+      let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,nZero,_pInf,_nInf,_nan) =
+        get_f_class_constructors env in
+      CONSTR(Univ.in_punivs nZero, [||])
+
+    let mkPInf env =
+      let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,pInf,_nInf,_nan) =
+        get_f_class_constructors env in
+      CONSTR(Univ.in_punivs pInf, [||])
+
+    let mkNInf env =
+      let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,nInf,_nan) =
+        get_f_class_constructors env in
+      CONSTR(Univ.in_punivs nInf, [||])
+
+    let mkNaN env =
+      let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,nan) =
+        get_f_class_constructors env in
+      CONSTR(Univ.in_punivs nan, [||])
   end
 
 module VredNative = RedNative(VNativeEntries)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 321c64e411..2952466fbb 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -906,6 +906,51 @@ struct
   let mkFNotComparable env =
     let (_eq, _lt, _gt, nc) = get_f_cmp_constructors env in
     mkConstruct nc
+
+  let mkPNormal env =
+    let (pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,_nan) =
+      get_f_class_constructors env in
+    mkConstruct pNormal
+
+  let mkNNormal env =
+    let (_pNormal,nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,_nan) =
+      get_f_class_constructors env in
+    mkConstruct nNormal
+
+  let mkPSubn env =
+    let (_pNormal,_nNormal,pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,_nan) =
+      get_f_class_constructors env in
+    mkConstruct pSubn
+
+  let mkNSubn env =
+    let (_pNormal,_nNormal,_pSubn,nSubn,_pZero,_nZero,_pInf,_nInf,_nan) =
+      get_f_class_constructors env in
+    mkConstruct nSubn
+
+  let mkPZero env =
+    let (_pNormal,_nNormal,_pSubn,_nSubn,pZero,_nZero,_pInf,_nInf,_nan) =
+      get_f_class_constructors env in
+    mkConstruct pZero
+
+  let mkNZero env =
+    let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,nZero,_pInf,_nInf,_nan) =
+      get_f_class_constructors env in
+    mkConstruct nZero
+
+  let mkPInf env =
+    let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,pInf,_nInf,_nan) =
+      get_f_class_constructors env in
+    mkConstruct pInf
+
+  let mkNInf env =
+    let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,nInf,_nan) =
+      get_f_class_constructors env in
+    mkConstruct nInf
+
+  let mkNaN env =
+    let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,nan) =
+      get_f_class_constructors env in
+    mkConstruct nan
 end
 
 module CredNative = RedNative(CNativeEntries)
diff --git a/test-suite/primitive/float/classify.v b/test-suite/primitive/float/classify.v
new file mode 100644
index 0000000000..e4373415cb
--- /dev/null
+++ b/test-suite/primitive/float/classify.v
@@ -0,0 +1,23 @@
+Require Import ZArith Floats.
+
+Definition epsilon := Eval compute in ldexp one (-1024)%Z.
+
+Check (eq_refl : classify one = PNormal).
+Check (eq_refl : classify (- one)%float = NNormal).
+Check (eq_refl : classify epsilon = PSubn).
+Check (eq_refl : classify (- epsilon)%float = NSubn).
+Check (eq_refl : classify zero = PZero).
+Check (eq_refl : classify neg_zero = NZero).
+Check (eq_refl : classify infinity = PInf).
+Check (eq_refl : classify neg_infinity = NInf).
+Check (eq_refl : classify nan = NaN).
+
+Check (eq_refl PNormal <: classify one = PNormal).
+Check (eq_refl NNormal <: classify (- one)%float = NNormal).
+Check (eq_refl PSubn <: classify epsilon = PSubn).
+Check (eq_refl NSubn <: classify (- epsilon)%float = NSubn).
+Check (eq_refl PZero <: classify zero = PZero).
+Check (eq_refl NZero <: classify neg_zero = NZero).
+Check (eq_refl PInf <: classify infinity = PInf).
+Check (eq_refl NInf <: classify neg_infinity = NInf).
+Check (eq_refl NaN <: classify nan = NaN).
diff --git a/theories/Floats/FloatAxioms.v b/theories/Floats/FloatAxioms.v
index d835e87ee0..d78e3192e7 100644
--- a/theories/Floats/FloatAxioms.v
+++ b/theories/Floats/FloatAxioms.v
@@ -2,6 +2,7 @@ Require Import ZArith Int63 SpecFloat PrimFloat FloatOps.
 
 Notation valid_binary := (valid_binary prec emax).
 
+Definition SF64classify := SFclassify prec.
 Definition SF64mul := SFmul prec emax.
 Definition SF64add := SFadd prec emax.
 Definition SF64sub := SFsub prec emax.
@@ -32,6 +33,7 @@ Definition flatten_cmp_opt c :=
   end.
 Axiom compare_spec : forall x y, (x ?= y)%float = flatten_cmp_opt (SFcompare (Prim2SF x) (Prim2SF y)).
 
+Axiom classify_spec : forall x, classify x = SF64classify (Prim2SF x).
 Axiom mul_spec : forall x y, Prim2SF (x * y)%float = SF64mul (Prim2SF x) (Prim2SF y).
 Axiom add_spec : forall x y, Prim2SF (x + y)%float = SF64add (Prim2SF x) (Prim2SF y).
 Axiom sub_spec : forall x y, Prim2SF (x - y)%float = SF64sub (Prim2SF x) (Prim2SF y).
diff --git a/theories/Floats/FloatClass.v b/theories/Floats/FloatClass.v
new file mode 100644
index 0000000000..3241035aef
--- /dev/null
+++ b/theories/Floats/FloatClass.v
@@ -0,0 +1,2 @@
+Inductive float_class : Set :=
+  | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN.
diff --git a/theories/Floats/Floats.v b/theories/Floats/Floats.v
index a1d49e87ee..53dd73f6d0 100644
--- a/theories/Floats/Floats.v
+++ b/theories/Floats/Floats.v
@@ -1,3 +1,4 @@
+Require Export FloatClass.
 Require Export SpecFloat.
 Require Export PrimFloat.
 Require Export FloatOps.
diff --git a/theories/Floats/PrimFloat.v b/theories/Floats/PrimFloat.v
index 13763a39d1..bc5c49d085 100644
--- a/theories/Floats/PrimFloat.v
+++ b/theories/Floats/PrimFloat.v
@@ -1,8 +1,9 @@
-Require Import Int63.
+Require Import Int63 FloatClass.
 
 Inductive float_comparison : Set := FEq | FLt | FGt | FNotComparable.
 
 Register float_comparison as kernel.ind_f_cmp.
+Register float_class as kernel.ind_f_class.
 
 Primitive float := #float64_type.
 
@@ -18,6 +19,8 @@ Primitive abs := #float64_abs.
 Primitive compare := #float64_compare.
 Notation "x ?= y" := (compare x y) (at level 70, no associativity) : float_scope.
 
+Primitive classify := #float64_classify.
+
 Primitive mul := #float64_mul.
 Notation "x * y" := (mul x y) : float_scope.
 
diff --git a/theories/Floats/SpecFloat.v b/theories/Floats/SpecFloat.v
index 337c00b20f..fc26ba8cab 100644
--- a/theories/Floats/SpecFloat.v
+++ b/theories/Floats/SpecFloat.v
@@ -1,4 +1,4 @@
-Require Import ZArith.
+Require Import ZArith FloatClass.
 
 Variant spec_float :=
   | S754_zero (s : bool)
@@ -183,6 +183,21 @@ Section FloatOps.
       end
     end.
 
+  Definition SFclassify f :=
+    match f with
+    | S754_nan => NaN
+    | S754_infinity false => PInf
+    | S754_infinity true => NInf
+    | S754_zero false => NZero
+    | S754_zero true => PZero
+    | S754_finite false m _ =>
+      if (digits2_pos m =? Z.to_pos prec)%positive then PNormal
+      else PSubn
+    | S754_finite true m _ =>
+      if (digits2_pos m =? Z.to_pos prec)%positive then NNormal
+      else NSubn
+    end.
+
   Definition SFmul x y :=
     match x, y with
     | S754_nan, _ | _, S754_nan => S754_nan
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 78e4c89521..aeae86e1f7 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -276,6 +276,7 @@ GRAMMAR EXTEND Gram
        | "#float64_opp" -> { CPrimitives.Float64opp }
        | "#float64_abs" -> { CPrimitives.Float64abs }
        | "#float64_compare" -> { CPrimitives.Float64compare }
+       | "#float64_classify" -> { CPrimitives.Float64classify }
        | "#float64_add" -> { CPrimitives.Float64add }
        | "#float64_sub" -> { CPrimitives.Float64sub }
        | "#float64_mul" -> { CPrimitives.Float64mul }
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index c86b70c78e..c4892736ae 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1848,6 +1848,7 @@ let vernac_register qid r =
         | "ind_pair" -> CPrimitives.(PIE PIT_pair)
         | "ind_cmp" -> CPrimitives.(PIE PIT_cmp)
         | "ind_f_cmp" -> CPrimitives.(PIE PIT_f_cmp)
+        | "ind_f_class" -> CPrimitives.(PIE PIT_f_class)
         | k -> CErrors.user_err Pp.(str "Register: unknown identifier “" ++ str k ++ str "” in the “kernel” namespace")
       in
       match gr with