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, 29 insertions, 19 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 520bcd6b41..bac13a0bd7 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -241,8 +241,6 @@ module VNativeEntries =
 
     let float_ty env = VAL(0, mkConst @@ get_float_type env)
 
-    let cmp_ty env = VAL(0, mkConst @@ get_cmp_type env)
-
     let mkCarry env b e =
       let (c0,c1) = get_carry_constructors env in
       CONSTR(Univ.in_punivs (if b then c1 else c0), [|int_ty env;e|])
@@ -270,15 +268,21 @@ module VNativeEntries =
       let (_eq,_lt,gt) = get_cmp_constructors env in
       CONSTR(Univ.in_punivs gt, [||])
 
-    let mkSomeCmp env v =
-      let cmp_ty = cmp_ty env in
-      let (some,_none) = get_option_constructors env in
-      CONSTR(Univ.in_punivs some, [|cmp_ty;v|])
+    let mkFLt env =
+      let (_eq,lt,_gt,_nc) = get_f_cmp_constructors env in
+      CONSTR(Univ.in_punivs lt, [||])
+
+    let mkFEq env =
+      let (eq,_lt,_gt,_nc) = get_f_cmp_constructors env in
+      CONSTR(Univ.in_punivs eq, [||])
+
+    let mkFGt env =
+      let (_eq,_lt,gt,_nc) = get_f_cmp_constructors env in
+      CONSTR(Univ.in_punivs gt, [||])
 
-    let mkNoneCmp env =
-      let cmp_ty = cmp_ty env in
-      let (_some,none) = get_option_constructors env in
-      CONSTR(Univ.in_punivs none, [|cmp_ty|])
+    let mkFNotComparable env =
+      let (_eq,_lt,_gt,nc) = get_f_cmp_constructors env in
+      CONSTR(Univ.in_punivs nc, [||])
   end
 
 module VredNative = RedNative(VNativeEntries)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 12419c04bc..321c64e411 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -891,15 +891,21 @@ struct
     let (_eq, _lt, gt) = get_cmp_constructors env in
     mkConstruct gt
 
-  let mkSomeCmp env v =
-    let cmp_ty = mkConst @@ get_cmp_type env in
-    let (some, _none) = get_option_constructors env in
-    mkApp(mkConstruct some, [|cmp_ty;v|])
-
-  let mkNoneCmp env =
-    let cmp_ty = mkConst @@ get_cmp_type env in
-    let (_some, none) = get_option_constructors env in
-    mkApp(mkConstruct none, [|cmp_ty|])
+  let mkFLt env =
+    let (_eq, lt, _gt, _nc) = get_f_cmp_constructors env in
+    mkConstruct lt
+
+  let mkFEq env =
+    let (eq, _lt, _gt, _nc) = get_f_cmp_constructors env in
+    mkConstruct eq
+
+  let mkFGt env =
+    let (_eq, _lt, gt, _nc) = get_f_cmp_constructors env in
+    mkConstruct gt
+
+  let mkFNotComparable env =
+    let (_eq, _lt, _gt, nc) = get_f_cmp_constructors env in
+    mkConstruct nc
 end
 
 module CredNative = RedNative(CNativeEntries)