aarch64/Asmblock: Merge arith_comparison_(r|f)

1 files changed, 12 insertions, 26 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 40219c5d..7373e926 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -296,9 +296,14 @@ Inductive arith_c_p : Type :=
 *)
 .
 
-Inductive arith_comparison_f : Type :=
+Inductive arith_comparison_p : Type :=
   (** Floating-point comparison *)
   | Pfcmp0 (sz: fsize)                                     (**r compare [r1] and [+0.0] *)
+  (** Integer arithmetic, immediate *)
+  | Pcmpimm (sz: isize) (n: Z)                        (**r compare *)
+  | Pcmnimm (sz: isize) (n: Z)                        (**r compare negative *)
+  (** Logical, immediate *)
+  | Ptstimm (sz: isize) (n: Z)                        (**r and, then set flags *)
 .
 
 Inductive arith_rr : Type :=
@@ -386,15 +391,6 @@ Inductive arith_rf : Type :=
   | Pfcvtzu (isz: isize) (fsz: fsize)                 (**r convert float to unsigned int *)
 .
 
-
-Inductive arith_comparison_r : Type :=
-  (** Integer arithmetic, immediate *)
-  | Pcmpimm (sz: isize) (n: Z)                        (**r compare *)
-  | Pcmnimm (sz: isize) (n: Z)                        (**r compare negative *)
-  (** Logical, immediate *)
-  | Ptstimm (sz: isize) (n: Z)                        (**r and, then set flags *)
-.
-
 Inductive arith_rrr : Type :=
   (** Variable shifts *)
   | Pasrv (sz: isize)                                 (**r arithmetic right shift *)
@@ -553,8 +549,7 @@ Inductive ar_instruction : Type :=
   | PArithComparisonRR (i : arith_comparison_rr) (r1 r2 : ireg)
   | PArithComparisonWR0R (i : arith_comparison_w_r0r) (r1 : ireg0) (r2 : ireg)
   | PArithComparisonXR0R (i : arith_comparison_x_r0r) (r1 : ireg0) (r2 : ireg)
-  | PArithComparisonR (i : arith_comparison_r) (r1 : ireg)
-  | PArithComparisonF (i: arith_comparison_f) (r1 : freg)
+  | PArithComparisonP (i : arith_comparison_p) (r1 : preg)
   | PArithComparisonFF (i : arith_comparison_ff) (rd rs : freg)
 .
 
@@ -1517,7 +1512,7 @@ Definition arith_prepare_comparison_x_r0r i v1 v2 :=
   | PtstX s => ((Val.andl v1 (eval_shift_op_long v2 s)), (Vlong Int64.zero))
   end.
 
-Definition arith_prepare_comparison_r i v :=
+Definition arith_prepare_comparison_p i v :=
   match i with
   | Pcmpimm W n => (v, (Vint (Int.repr n)))
   | Pcmpimm X n => (v, (Vlong (Int64.repr n)))
@@ -1525,11 +1520,6 @@ Definition arith_prepare_comparison_r i v :=
   | Pcmnimm X n => (v, (Vlong (Int64.neg (Int64.repr n))))
   | Ptstimm W n => ((Val.and v (Vint (Int.repr n))), (Vint Int.zero))
   | Ptstimm X n => ((Val.andl v (Vlong (Int64.repr n))), (Vlong Int64.zero))
-  end.
-
-(* Without val annotation unification fails *)
-Definition arith_prepare_comparison_f i (v : val) :=
-  match i with
   | Pfcmp0 S => (v, (Vsingle Float32.zero))
   | Pfcmp0 D => (v, (Vfloat Float.zero))
   end.
@@ -1579,18 +1569,14 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   | PArithComparisonXR0R i s1 s2 =>
     let (v1, v2) := arith_prepare_comparison_x_r0r i rs###s1 rs#s2 in
       compare_long rs v1 v2
-  | PArithComparisonR i s =>
-    let (v1, v2) := arith_prepare_comparison_r i rs#s in
+  | PArithComparisonP i s =>
+    let (v1, v2) := arith_prepare_comparison_p i rs#s in
       (match i with
       | Pcmpimm W _ | Pcmnimm W _ | Ptstimm W _ => compare_int rs v1 v2
       | Pcmpimm X _ | Pcmnimm X _ | Ptstimm X _ => compare_long rs v1 v2
+      | Pfcmp0 S => compare_single rs v1 v2
+      | Pfcmp0 D => compare_float rs v1 v2
       end)
-  | PArithComparisonF i s =>
-    let (v1, v2) := arith_prepare_comparison_f i rs#s in
-    (match i with
-    | Pfcmp0 S => compare_single rs v1 v2
-    | Pfcmp0 D => compare_float rs v1 v2
-    end)
   | PArithComparisonFF i s1 s2 =>
     let (v1, v2) := arith_prepare_comparison_ff i rs#s1 rs#s2 in
     (match i with