Introduce and use the type fp_comparison for floating-point comparisons

With FP arithmetic, the negation of "x < y" is not "x >= y".  For this reason, the back-end intermediate languages of CompCert used to have both "Ccompf c" and "Cnotcompf c" comparison operators, where "c" is of type Integers.comparison and "Cnotcompf c" denotes the negation of FP comparison c.

There are some problems with this approach:
- Beyond Cnotcompf we also need Cnotcompfs (for single precision FP) and, in case of ARM, special forms for not-comparison against 0.0.  This duplication of comparison constructors inevitably causes some code and proof duplication.
- Cnotcompf Ceq is really Ccompf Cne, and likewise Cnotcompf Cne is really Ccompf Ceq, hence the representation of FP comparisons is not canonical, adding to the code and proof duplication mentioned above.
- Cnotcompf is introduced in CminorSel, but in Cminor we don't have it, making it impossible to express some transformations over comparisons at the machine-independent Cminor level.

This commit develops an alternate approach, whereas FP comparisons have their own type, defined as Floats.fp_comparison, and which includes constructors for "not <", "not <=", "not >" and "not >=".  Hence this type is closed under boolean negation, so to speak, and there is no longer a need for "Cnotcompf", given that "Ccompf" takes a fp_comparison and can therefore express all FP comparisons of interest.

2 files changed, 59 insertions, 14 deletions

diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index e477957a..6e115a14 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -18,6 +18,8 @@
 open Printf
 open Camlcoq
 open AST
+open Integers
+open Floats
 
 let name_of_type = function
   | Tint -> "int"
@@ -90,3 +92,22 @@ let rec print_builtin_res px oc = function
       fprintf oc "splitlong(%a, %a)"
                  (print_builtin_res px) hi (print_builtin_res px) lo
 
+let comparison_name = function
+  | Ceq -> "=="
+  | Cne -> "!="
+  | Clt -> "<"
+  | Cle -> "<="
+  | Cgt -> ">"
+  | Cge -> ">="
+
+let fp_comparison_name = function
+  | FCeq -> "=="
+  | FCne -> "!="
+  | FClt -> "<"
+  | FCle -> "<="
+  | FCgt -> ">"
+  | FCge -> ">="
+  | FCnotlt -> "!<"
+  | FCnotle -> "!<="
+  | FCnotgt -> "!>"
+  | FCnotge -> "!>="
diff --git a/common/Values.v b/common/Values.v
index a20dd567..6a1ffd26 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -815,13 +815,13 @@ Definition cmpu_bool (c: comparison) (v1 v2: val): option bool :=
   | _, _ => None
   end.
 
-Definition cmpf_bool (c: comparison) (v1 v2: val): option bool :=
+Definition cmpf_bool (c: fp_comparison) (v1 v2: val): option bool :=
   match v1, v2 with
   | Vfloat f1, Vfloat f2 => Some (Float.cmp c f1 f2)
   | _, _ => None
   end.
 
-Definition cmpfs_bool (c: comparison) (v1 v2: val): option bool :=
+Definition cmpfs_bool (c: fp_comparison) (v1 v2: val): option bool :=
   match v1, v2 with
   | Vsingle f1, Vsingle f2 => Some (Float32.cmp c f1 f2)
   | _, _ => None
@@ -870,10 +870,10 @@ Definition cmp (c: comparison) (v1 v2: val): val :=
 Definition cmpu (c: comparison) (v1 v2: val): val :=
   of_optbool (cmpu_bool c v1 v2).
 
-Definition cmpf (c: comparison) (v1 v2: val): val :=
+Definition cmpf (c: fp_comparison) (v1 v2: val): val :=
   of_optbool (cmpf_bool c v1 v2).
 
-Definition cmpfs (c: comparison) (v1 v2: val): val :=
+Definition cmpfs (c: fp_comparison) (v1 v2: val): val :=
   of_optbool (cmpfs_bool c v1 v2).
 
 Definition cmpl (c: comparison) (v1 v2: val): option val :=
@@ -1672,6 +1672,20 @@ Proof.
 - rewrite Int64.negate_cmpu. auto.
 Qed.
 
+Theorem negate_cmpf_bool:
+  forall c v1 v2, cmpf_bool (negate_fp_comparison c) v1 v2 = option_map negb (cmpf_bool c v1 v2).
+Proof.
+  intros; unfold cmpf; destruct v1; auto; destruct v2; auto.
+  simpl. rewrite Float.cmp_negate. auto.
+Qed. 
+
+Theorem negate_cmpfs_bool:
+  forall c v1 v2, cmpfs_bool (negate_fp_comparison c) v1 v2 = option_map negb (cmpfs_bool c v1 v2).
+Proof.
+  intros; unfold cmpf; destruct v1; auto; destruct v2; auto.
+  simpl. rewrite Float32.cmp_negate. auto.
+Qed. 
+
 Lemma not_of_optbool:
   forall ob, of_optbool (option_map negb ob) = notbool (of_optbool ob).
 Proof.
@@ -1693,6 +1707,18 @@ Proof.
   intros. unfold cmpu. rewrite negate_cmpu_bool. apply not_of_optbool.
 Qed.
 
+Theorem negate_cmpf:
+  forall c v1 v2, cmpf (negate_fp_comparison c) v1 v2 = notbool (cmpf c v1 v2).
+Proof.
+  intros; unfold cmpf. rewrite negate_cmpf_bool. apply not_of_optbool.
+Qed. 
+
+Theorem negate_cmpfs:
+  forall c v1 v2, cmpfs (negate_fp_comparison c) v1 v2 = notbool (cmpfs c v1 v2).
+Proof.
+  intros; unfold cmpfs. rewrite negate_cmpfs_bool. apply not_of_optbool.
+Qed. 
+
 Theorem swap_cmp_bool:
   forall c x y,
   cmp_bool (swap_comparison c) x y = cmp_bool c y x.
@@ -1749,33 +1775,31 @@ Proof.
 Qed.
 
 Theorem negate_cmpf_eq:
-  forall v1 v2, notbool (cmpf Cne v1 v2) = cmpf Ceq v1 v2.
+  forall v1 v2, notbool (cmpf FCne v1 v2) = cmpf FCeq v1 v2.
 Proof.
-  destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool.
-  rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq f f0); auto.
+  intros; symmetry; apply (negate_cmpf FCne).
 Qed.
 
 Theorem negate_cmpf_ne:
-  forall v1 v2, notbool (cmpf Ceq v1 v2) = cmpf Cne v1 v2.
+  forall v1 v2, notbool (cmpf FCeq v1 v2) = cmpf FCne v1 v2.
 Proof.
-  destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool.
-  rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq f f0); auto.
+  intros; symmetry; apply (negate_cmpf FCeq).
 Qed.
 
 Theorem cmpf_le:
-  forall v1 v2, cmpf Cle v1 v2 = or (cmpf Clt v1 v2) (cmpf Ceq v1 v2).
+  forall v1 v2, cmpf FCle v1 v2 = or (cmpf FClt v1 v2) (cmpf FCeq v1 v2).
 Proof.
   destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool.
   rewrite Float.cmp_le_lt_eq.
-  destruct (Float.cmp Clt f f0); destruct (Float.cmp Ceq f f0); auto.
+  destruct (Float.cmp FClt f f0); destruct (Float.cmp FCeq f f0); auto.
 Qed.
 
 Theorem cmpf_ge:
-  forall v1 v2, cmpf Cge v1 v2 = or (cmpf Cgt v1 v2) (cmpf Ceq v1 v2).
+  forall v1 v2, cmpf FCge v1 v2 = or (cmpf FCgt v1 v2) (cmpf FCeq v1 v2).
 Proof.
   destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool.
   rewrite Float.cmp_ge_gt_eq.
-  destruct (Float.cmp Cgt f f0); destruct (Float.cmp Ceq f f0); auto.
+  destruct (Float.cmp FCgt f f0); destruct (Float.cmp FCeq f f0); auto.
 Qed.
 
 Theorem cmp_ne_0_optbool: