Asmblock: PArithWRR0I -> PArithWRR0, PArithXRR0I -> PArithXRR0

1 files changed, 22 insertions, 22 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 06d80425..e98eeadd 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -467,18 +467,18 @@ Inductive arith_name_rsprsp : Type :=
   | Psubimm (sz: isize) (n: Z)                      (**r subtraction *)
 .
 
-Inductive arith_name_w_rr0i : Type :=
+Inductive arith_name_w_rr0 : Type :=
   (** Logical, immediate *)
-  | PandimmW                                        (**r and *)
-  | PeorimmW                                        (**r xor *)
-  | PorrimmW                                        (**r or *)
+  | PandimmW (n: Z)                                 (**r and *)
+  | PeorimmW (n: Z)                                 (**r xor *)
+  | PorrimmW (n: Z)                                 (**r or *)
 .
 
-Inductive arith_name_x_rr0i : Type :=
+Inductive arith_name_x_rr0 : Type :=
   (** Logical, immediate *)
-  | PandimmX                                        (**r and *)
-  | PeorimmX                                        (**r xor *)
-  | PorrimmX                                        (**r or *)
+  | PandimmX (n: Z)                                 (**r and *)
+  | PeorimmX (n: Z)                                 (**r xor *)
+  | PorrimmX (n: Z)                                 (**r or *)
 .
 
 
@@ -532,8 +532,8 @@ Inductive ar_instruction : Type :=
   | PArithRRR (i : arith_name_rrr) (rd r1 r2 : ireg)
   | PArithWRR0R (i : arith_name_w_rr0r) (rd : ireg) (r1 : ireg0) (r2 : ireg)
   | PArithXRR0R (i : arith_name_x_rr0r) (rd : ireg) (r1 : ireg0) (r2 : ireg)
-  | PArithWRR0I (i : arith_name_w_rr0i) (rd : ireg) (r1 : ireg0) (n : Z)
-  | PArithXRR0I (i : arith_name_x_rr0i) (rd : ireg) (r1 : ireg0) (n : Z)
+  | 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)
@@ -1368,19 +1368,19 @@ Definition arith_eval_x_rr0r n v1 v2 :=
   end.
 
 (* obtain v by rs##r1 *)
-Definition arith_eval_w_rr0i n v i :=
-  match n with
-  | PandimmW => Val.and v (Vint (Int.repr i))
-  | PeorimmW => Val.xor v (Vint (Int.repr i))
-  | PorrimmW => Val.or v (Vint (Int.repr i))
+Definition arith_eval_w_rr0 i v :=
+  match i with
+  | PandimmW n => Val.and v (Vint (Int.repr n))
+  | PeorimmW n => Val.xor v (Vint (Int.repr n))
+  | PorrimmW n => Val.or v (Vint (Int.repr n))
   end.
 
 (* obtain v by rs###r1 *)
-Definition arith_eval_x_rr0i n v i :=
-  match n with
-  | PandimmX => Val.andl v (Vlong (Int64.repr i))
-  | PeorimmX => Val.xorl v (Vlong (Int64.repr i))
-  | PorrimmX => Val.orl v (Vlong (Int64.repr i))
+Definition arith_eval_x_rr0 i v :=
+  match i with
+  | PandimmX n => Val.andl v (Vlong (Int64.repr n))
+  | PeorimmX n => Val.xorl v (Vlong (Int64.repr n))
+  | PorrimmX n => Val.orl v (Vlong (Int64.repr n))
   end.
 
 Definition arith_eval_rsprspr n v1 v2 :=
@@ -1522,8 +1522,8 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   | PArithWRR0R n d s1 s2 => rs#d <- (arith_eval_w_rr0r n rs##s1 rs#s2)
   | PArithXRR0R n d s1 s2 => rs#d <- (arith_eval_x_rr0r n rs###s1 rs#s2)
 
-  | PArithWRR0I n d s i => rs#d <- (arith_eval_w_rr0i n rs##s i)
-  | PArithXRR0I n d s i => rs#d <- (arith_eval_x_rr0i n rs###s i)
+  | PArithWRR0 n d s => rs#d <- (arith_eval_w_rr0 n rs##s)
+  | PArithXRR0 n d s => rs#d <- (arith_eval_x_rr0 n rs###s)
 
   | PArithRspRspR n d s1 s2 => rs#d <- (arith_eval_rsprspr n rs#s1 rs#s2)
   | PArithRspRsp n d s => rs#d <- (arith_eval_rsprsp n rs#s)