Implement classify on primitive float

5 files changed, 25 insertions, 2 deletions

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