Asmblock: Rename arith_name_<...> -> arith_name_<...>

Following the example of 6fd50b46 where arith_name_r was renamed to
arith_r

1 files changed, 62 insertions, 62 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index c8172d1c..21061747 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -283,7 +283,7 @@ Inductive arith_r : Type :=
 
 (* Arithmetic instructions with conditional execution *)
 (* TODO matching case in ar_instruction *)
-Inductive arith_name_c_r : Type :=
+Inductive arith_c_r : Type :=
   (** Conditional data processing *)
   | Pcset                                       (**r set to 1/0 if cond is true/false *)
 (*
@@ -291,12 +291,12 @@ Inductive arith_name_c_r : Type :=
 *)
 .
 
-Inductive arith_name_comparison_f : Type :=
+Inductive arith_comparison_f : Type :=
   (** Floating-point comparison *)
   | Pfcmp0 (sz: fsize)                                     (**r compare [r1] and [+0.0] *)
 .
 
-Inductive arith_name_rr : Type :=
+Inductive arith_rr : Type :=
   (** Move integer register *)
   | Pmov
   (** PC-relative addressing *)
@@ -315,7 +315,7 @@ Inductive arith_name_rr : Type :=
 *)
 .
 
-Inductive arith_name_comparison_w_r0r : Type :=
+Inductive arith_comparison_w_r0r : Type :=
   (** Integer arithmetic, shifted register *)
   | PcmpW (s: shift_op)             (**r compare *)
   | PcmnW (s: shift_op)             (**r compare negative *)
@@ -323,7 +323,7 @@ Inductive arith_name_comparison_w_r0r : Type :=
   | PtstW (s: shift_op)             (**r and, then set flags *)
 .
 
-Inductive arith_name_comparison_x_r0r : Type :=
+Inductive arith_comparison_x_r0r : Type :=
   (** Integer arithmetic, shifted register *)
   | PcmpX (s: shift_op)             (**r compare *)
   | PcmnX (s: shift_op)             (**r compare negative *)
@@ -331,13 +331,13 @@ Inductive arith_name_comparison_x_r0r : Type :=
   | PtstX (s: shift_op)             (**r and, then set flags *)
 .
 
-Inductive arith_name_comparison_rr : Type :=
+Inductive arith_comparison_rr : Type :=
   (** Integer arithmetic, extending register *)
   | Pcmpext (x: extend_op)                      (**r int64-int32 cmp *)
   | Pcmnext (x: extend_op)                      (**r int64-int32 cmn *)
 .
 
-Inductive arith_name_ff : Type :=
+Inductive arith_ff : Type :=
   (** Floating-point move *)
   | Pfmov
   (** Floating-point conversions *)
@@ -350,39 +350,39 @@ Inductive arith_name_ff : Type :=
   | Pfsqrt (sz: fsize)                                (**r square root *) *)
 .
 
-Inductive arith_name_comparison_ff : Type :=
+Inductive arith_comparison_ff : Type :=
   (** Floating-point comparison *)
   | Pfcmp (sz: fsize)                                 (**r compare [r1] and [r2] *)
 .
 
-(* TODO? Can arith_name_fr and arith_name_rf be collapsed into one type
+(* TODO? Can arith_fr and arith_rf be collapsed into one type
  * (switching the argument order when evaluating for one of them)?
  * Or must these be two different types since the target register is
  * either an integer or a floating point register? *)
-Inductive arith_name_fr : Type :=
+Inductive arith_fr : Type :=
   (** Floating-point conversions *)
   | Pscvtf (fsz: fsize) (isz: isize)                  (**r convert signed int to float *)
   | Pucvtf (fsz: fsize) (isz: isize)                  (**r convert unsigned int to float *)
 .
 
-Inductive arith_name_sw_fr0 : Type :=
+Inductive arith_sw_fr0 : Type :=
   (** Floating-point move *)
   | PfmoviSW                                          (**r copy int reg to FP reg *)
 .
 
-Inductive arith_name_dx_fr0 : Type :=
+Inductive arith_dx_fr0 : Type :=
   (** Floating-point move *)
   | PfmoviDX                                          (**r copy int reg to FP reg *)
 .
 
-Inductive arith_name_rf : Type := 
+Inductive arith_rf : Type := 
   (** Floating-point conversions *)
   | Pfcvtzs (isz: isize) (fsz: fsize)                 (**r convert float to signed int *)
   | Pfcvtzu (isz: isize) (fsz: fsize)                 (**r convert float to unsigned int *)
 .
 
 
-Inductive arith_name_comparison_r : Type :=
+Inductive arith_comparison_r : Type :=
   (** Integer arithmetic, immediate *)
   | Pcmpimm (sz: isize) (n: Z)                        (**r compare *)
   | Pcmnimm (sz: isize) (n: Z)                        (**r compare negative *)
@@ -390,13 +390,13 @@ Inductive arith_name_comparison_r : Type :=
   | Ptstimm (sz: isize) (n: Z)                        (**r and, then set flags *)
 .
 
-Inductive arith_name_f : Type :=
+Inductive arith_f : Type :=
   (** Floating-point move *)
   | Pfmovimms (f: float32)                            (**r load float32 constant *)
   | Pfmovimmd (f: float)                              (**r load float64 constant *)
 .
 
-Inductive arith_name_rrr : Type :=
+Inductive arith_rrr : Type :=
   (** Variable shifts *)
   | Pasrv (sz: isize)                                 (**r arithmetic right shift *)
   | Plslv (sz: isize)                                 (**r left shift *)
@@ -410,18 +410,18 @@ Inductive arith_name_rrr : Type :=
 .
 
 (* TODO matching case in ar_instruction *)
-Inductive arith_name_c_rrr : Type :=
+Inductive arith_c_rrr : Type :=
   (** Conditional data processing *)
   | Pcsel                                             (**r int conditional move *)
 .
 
-Inductive arith_name_rsprspr : Type :=
+Inductive arith_rsprspr : Type :=
   (** Integer arithmetic, extending register *)
   | Paddext (x: extend_op)                            (**r int64-int32 add *)
   | Psubext (x: extend_op)                            (**r int64-int32 sub *)
 .
 
-Inductive arith_name_w_rr0r : Type :=
+Inductive arith_w_rr0r : Type :=
   (** Integer arithmetic, shifted register *)
   | PaddW (s: shift_op)                               (**r addition *)
   | PsubW (s: shift_op)                               (**r subtraction *)
@@ -434,7 +434,7 @@ Inductive arith_name_w_rr0r : Type :=
   | PornW (s: shift_op)                               (**r or-not *)
 .
 
-Inductive arith_name_x_rr0r : Type :=
+Inductive arith_x_rr0r : Type :=
   (** Integer arithmetic, shifted register *)
   | PaddX (s: shift_op)                               (**r addition *)
   | PsubX (s: shift_op)                               (**r subtraction *)
@@ -447,7 +447,7 @@ Inductive arith_name_x_rr0r : Type :=
   | PornX (s: shift_op)                               (**r or-not *)
 .
 
-Inductive arith_name_fff : Type :=
+Inductive arith_fff : Type :=
   (** Floating-point arithmetic *)
   | Pfadd (sz: fsize)                                (**r addition *)
   | Pfdiv (sz: fsize)                                (**r division *)
@@ -456,25 +456,25 @@ Inductive arith_name_fff : Type :=
 .
 
 (* TODO matching case in ar_instruction *)
-Inductive arith_name_c_fff : Type :=
+Inductive arith_c_fff : Type :=
   (** Floating-point conditional select *)
   | Pfsel
 .
 
-Inductive arith_name_rsprsp : Type :=
+Inductive arith_rsprsp : Type :=
   (** Integer arithmetic, immediate *)
   | Paddimm (sz: isize) (n: Z)                      (**r addition *)
   | Psubimm (sz: isize) (n: Z)                      (**r subtraction *)
 .
 
-Inductive arith_name_w_rr0 : Type :=
+Inductive arith_w_rr0 : Type :=
   (** Logical, immediate *)
   | PandimmW (n: Z)                                 (**r and *)
   | PeorimmW (n: Z)                                 (**r xor *)
   | PorrimmW (n: Z)                                 (**r or *)
 .
 
-Inductive arith_name_x_rr0 : Type :=
+Inductive arith_x_rr0 : Type :=
   (** Logical, immediate *)
   | PandimmX (n: Z)                                 (**r and *)
   | PeorimmX (n: Z)                                 (**r xor *)
@@ -482,30 +482,30 @@ Inductive arith_name_x_rr0 : Type :=
 .
 
 
-Inductive arith_name_w_arrrr0 : Type :=
+Inductive arith_w_arrrr0 : Type :=
   (** Integer multiply/divide *)
   | PmaddW                                          (**r multiply-add *)
   | PmsubW                                          (**r multiply-sub *)
 .
 
-Inductive arith_name_x_arrrr0 : Type :=
+Inductive arith_x_arrrr0 : Type :=
   (** Integer multiply/divide *)
   | PmaddX                                          (**r multiply-add *)
   | PmsubX                                          (**r multiply-sub *)
 .
 
-Inductive arith_name_afff : Type :=
+Inductive arith_afff : Type :=
   (** Floating-point arithmetic *)
   | Pfnmul (sz: fsize)                              (**r multiply-negate *)
 .
 
-Inductive arith_name_affff : Type :=
+Inductive arith_affff : Type :=
   (** Floating-point arithmetic *)
   | Pfmadd (sz: fsize)                              (**r [rd = r3 + r1 * r2] *)
   | Pfmsub (sz: fsize)                              (**r [rd = r3 - r1 * r2] *)
 .
 
-Inductive arith_name_aaffff : Type :=
+Inductive arith_aaffff : Type :=
   (** Floating-point arithmetic *)
   | Pfnmadd (sz: fsize)                             (**r [rd = - r3 - r1 * r2] *)
   | Pfnmsub (sz: fsize)                             (**r [rd = - r3 + r1 * r2] *)
@@ -527,37 +527,37 @@ Inductive arith_name_aaffff : Type :=
  *)
 Inductive ar_instruction : Type :=
   | PArithR (i : arith_r) (rd : ireg)
-  | PArithCR (i : arith_name_c_r) (rd : ireg) (c : testcond)
-  | PArithRR (i : arith_name_rr) (rd rs : ireg)
-  | PArithRF (i : arith_name_rf) (rd : ireg) (rs : freg)
-  | PArithRRR (i : arith_name_rrr) (rd r1 r2 : ireg)
-  | PArithCRRR (i : arith_name_c_rrr) (rd r1 r2 : ireg) (c : testcond)
-  | PArithWRR0R (i : arith_name_w_rr0r) (rd : ireg) (r1 : ireg0) (r2 : ireg)
-  | PArithXRR0R (i : arith_name_x_rr0r) (rd : ireg) (r1 : ireg0) (r2 : ireg)
-  | PArithWRR0 (i : arith_name_w_rr0) (rd : ireg) (r1 : ireg0)
-  | PArithXRR0 (i : arith_name_x_rr0) (rd : ireg) (r1 : ireg0)
-  | PArithRspRspR (i : arith_name_rsprspr) (rd r1 : iregsp) (r2 : ireg)
-  | PArithRspRsp (i : arith_name_rsprsp) (rd r1 : iregsp)
-  | PArithWARRRR0 (i : arith_name_w_arrrr0) (rd r1 r2 : ireg) (r3 : ireg0)
-  | PArithXARRRR0 (i : arith_name_x_arrrr0) (rd r1 r2 : ireg) (r3 : ireg0)
-  | PArithF (i : arith_name_f) (rd : freg)
-  | PArithFF (i : arith_name_ff) (rd rs : freg)
-  | PArithFR (i : arith_name_fr) (rd : freg) (rs : ireg)
-  | PArithSWFR0 (i : arith_name_sw_fr0) (rd : freg) (rs : ireg0)
-  | PArithDXFR0 (i : arith_name_dx_fr0) (rd : freg) (rs : ireg0)
-  | PArithFFF (i : arith_name_fff) (rd r1 r2 : freg)
-  | PArithCFFF (i : arith_name_c_fff) (rd r1 r2 : freg) (c : testcond)
-  | PArithAFFF (i : arith_name_afff) (rd r1 r2 : freg)
+  | PArithCR (i : arith_c_r) (rd : ireg) (c : testcond)
+  | PArithRR (i : arith_rr) (rd rs : ireg)
+  | PArithRF (i : arith_rf) (rd : ireg) (rs : freg)
+  | PArithRRR (i : arith_rrr) (rd r1 r2 : ireg)
+  | PArithCRRR (i : arith_c_rrr) (rd r1 r2 : ireg) (c : testcond)
+  | PArithWRR0R (i : arith_w_rr0r) (rd : ireg) (r1 : ireg0) (r2 : ireg)
+  | PArithXRR0R (i : arith_x_rr0r) (rd : ireg) (r1 : ireg0) (r2 : ireg)
+  | PArithWRR0 (i : arith_w_rr0) (rd : ireg) (r1 : ireg0)
+  | PArithXRR0 (i : arith_x_rr0) (rd : ireg) (r1 : ireg0)
+  | PArithRspRspR (i : arith_rsprspr) (rd r1 : iregsp) (r2 : ireg)
+  | PArithRspRsp (i : arith_rsprsp) (rd r1 : iregsp)
+  | PArithWARRRR0 (i : arith_w_arrrr0) (rd r1 r2 : ireg) (r3 : ireg0)
+  | PArithXARRRR0 (i : arith_x_arrrr0) (rd r1 r2 : ireg) (r3 : ireg0)
+  | PArithF (i : arith_f) (rd : freg)
+  | PArithFF (i : arith_ff) (rd rs : freg)
+  | PArithFR (i : arith_fr) (rd : freg) (rs : ireg)
+  | PArithSWFR0 (i : arith_sw_fr0) (rd : freg) (rs : ireg0)
+  | PArithDXFR0 (i : arith_dx_fr0) (rd : freg) (rs : ireg0)
+  | PArithFFF (i : arith_fff) (rd r1 r2 : freg)
+  | PArithCFFF (i : arith_c_fff) (rd r1 r2 : freg) (c : testcond)
+  | PArithAFFF (i : arith_afff) (rd r1 r2 : freg)
   (* Pfmadd and Pfmsub are currently not used by the semantics of aarch64/Asm
-  | PArithAFFFF (i : arith_name_affff) (rd r1 r2 r3 : freg) *)
+  | PArithAFFFF (i : arith_affff) (rd r1 r2 r3 : freg) *)
   (* Pfnmadd and Pfnmsub are currently not used by the semantics of aarch64/Asm
-  | PArithAAFFFF (i : arith_name_aaffff) (rd r1 r2 r3 : freg) *)
-  | PArithComparisonRR (i : arith_name_comparison_rr) (r1 r2 : ireg)
-  | PArithComparisonWR0R (i : arith_name_comparison_w_r0r) (r1 : ireg0) (r2 : ireg)
-  | PArithComparisonXR0R (i : arith_name_comparison_x_r0r) (r1 : ireg0) (r2 : ireg)
-  | PArithComparisonR (i : arith_name_comparison_r) (r1 : ireg)
-  | PArithComparisonF (i: arith_name_comparison_f) (r1 : freg)
-  | PArithComparisonFF (i : arith_name_comparison_ff) (rd rs : freg)
+  | PArithAAFFFF (i : arith_aaffff) (rd r1 r2 r3 : freg) *)
+  | 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)
+  | PArithComparisonFF (i : arith_comparison_ff) (rd rs : freg)
 .
 
 Inductive basic : Type :=
@@ -1298,7 +1298,7 @@ Definition arith_eval_r (i:arith_r): val :=
   | Pmovk X pos => insert_in_long rs#rd n pos 16 *)
   end.
 
-Definition arith_eval_c_r (i : arith_name_c_r) (c : option bool) : val :=
+Definition arith_eval_c_r (i : arith_c_r) (c : option bool) : val :=
   match i with
   | Pcset =>
     (match c with
@@ -1354,7 +1354,7 @@ Definition arith_eval_rrr i v1 v2 :=
   | Pudiv X => Val.maketotal (Val.divlu v1 v2)
   end.
 
-Definition arith_eval_c_rrr (i : arith_name_c_rrr) (v1 v2 : val) (c : option bool) :=
+Definition arith_eval_c_rrr (i : arith_c_rrr) (v1 v2 : val) (c : option bool) :=
   match i with
   | Pcsel =>
     (match c with
@@ -1487,7 +1487,7 @@ Definition arith_eval_fff i v1 v2 :=
   | Pfsub D => Val.subf v1 v2
   end.
 
-Definition arith_eval_c_fff (i : arith_name_c_fff) (v1 v2 : val) (c : option bool) :=
+Definition arith_eval_c_fff (i : arith_c_fff) (v1 v2 : val) (c : option bool) :=
   match i with
   | Pfsel =>
     (match c with