Change return type of primitive float comparison

Replace `option comparison` with `float_comparison` (:= `FEq | FLt |
FGt | FNotComparable`) as suggested by Guillaume Melquiond to avoid
boxing and an extra match when using primitive float comparison.

2 files changed, 20 insertions, 8 deletions

diff --git a/theories/Floats/FloatAxioms.v b/theories/Floats/FloatAxioms.v
index d057d641da..d835e87ee0 100644
--- a/theories/Floats/FloatAxioms.v
+++ b/theories/Floats/FloatAxioms.v
@@ -22,7 +22,16 @@ Qed.
 
 Axiom opp_spec : forall x, Prim2SF (-x)%float = SFopp (Prim2SF x).
 Axiom abs_spec : forall x, Prim2SF (abs x) = SFabs (Prim2SF x).
-Axiom compare_spec : forall x y, (x ?= y)%float = SFcompare (Prim2SF x) (Prim2SF y).
+
+Definition flatten_cmp_opt c :=
+  match c with
+  | None => FNotComparable
+  | Some Eq => FEq
+  | Some Lt => FLt
+  | Some Gt => FGt
+  end.
+Axiom compare_spec : forall x y, (x ?= y)%float = flatten_cmp_opt (SFcompare (Prim2SF x) (Prim2SF y)).
+
 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/PrimFloat.v b/theories/Floats/PrimFloat.v
index 21a1be8708..13763a39d1 100644
--- a/theories/Floats/PrimFloat.v
+++ b/theories/Floats/PrimFloat.v
@@ -1,5 +1,9 @@
 Require Import Int63.
 
+Inductive float_comparison : Set := FEq | FLt | FGt | FNotComparable.
+
+Register float_comparison as kernel.ind_f_cmp.
+
 Primitive float := #float64_type.
 
 Declare Scope float_scope.
@@ -11,7 +15,6 @@ Notation "- x" := (opp x) : float_scope.
 
 Primitive abs := #float64_abs.
 
-Register option as kernel.ind_option.
 Primitive compare := #float64_compare.
 Notation "x ?= y" := (compare x y) (at level 70, no associativity) : float_scope.
 
@@ -58,21 +61,21 @@ Definition two := Eval compute in (of_int63 2).
 
 Definition is_nan f :=
   match f ?= f with
-  | None => true
+  | FNotComparable => true
   | _ => false
   end.
 
 Definition is_zero f :=
   match f ?= zero with
-  | Some Eq => true (* note: 0 == -0 with floats *)
+  | FEq => true (* note: 0 == -0 with floats *)
   | _ => false
   end.
 
 Definition is_infinity f :=
   match f ?= infinity with
-  | Some Eq => true
-  | Some Lt => match f ?= neg_infinity with
-           | Some Eq => true
+  | FEq => true
+  | FLt => match f ?= neg_infinity with
+           | FEq => true
            | _ => false
            end
   | _ => false
@@ -81,7 +84,7 @@ Definition is_infinity f :=
 Definition get_sign f := (* + => false, - => true *)
   let f := if is_zero f then one / f else f in
   match f ?= zero with
-  | Some Gt => false
+  | FGt => false
   | _ => true
   end.