Preparation for postpass in aarch64 and refactoring

1 files changed, 20 insertions, 20 deletions

diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v
index fc356d52..0a21485c 100644
--- a/aarch64/Asmblockgen.v
+++ b/aarch64/Asmblockgen.v
@@ -29,7 +29,7 @@ Local Open Scope error_monad_scope.
 
 Definition ireg_of (r: mreg) : res ireg :=
   match preg_of r with
-  |  IR' irs => match irs with
+  |  IR irs => match irs with
                 | RR1 mr => OK mr
                 | _ => Error(msg "Asmgenblock.ireg_of")
                 end
@@ -37,7 +37,7 @@ Definition ireg_of (r: mreg) : res ireg :=
   end.
 
 Definition freg_of (r: mreg) : res freg :=
-  match preg_of r with FR' mr => OK mr | _ => Error(msg "Asmgenblock.freg_of") end.
+  match preg_of r with FR mr => OK mr | _ => Error(msg "Asmgenblock.freg_of") end.
 
 (** Recognition of immediate arguments for logical integer operations.*)
 
@@ -247,25 +247,25 @@ Definition indexed_memory_access_bc (insn: addressing -> basic)
 
 Definition loadind (base: iregsp) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: bcode) :=
   match ty, preg_of dst with
-  | Tint,    IR' rd => OK (indexed_memory_access_bc (PLoad Pldrw rd) 4 base ofs k)
-  | Tlong,   IR' rd => OK (indexed_memory_access_bc (PLoad Pldrx rd) 8 base ofs k)
-  | Tsingle, FR' rd => OK (indexed_memory_access_bc (PLoad Pldrs rd) 4 base ofs k)
-  | Tfloat,  FR' rd => OK (indexed_memory_access_bc (PLoad Pldrd rd) 8 base ofs k)
-  | Tany32,  IR' rd => OK (indexed_memory_access_bc (PLoad Pldrw_a rd) 4 base ofs k)
-  | Tany64,  IR' rd => OK (indexed_memory_access_bc (PLoad Pldrx_a rd) 8 base ofs k)
-  | Tany64,  FR' rd => OK (indexed_memory_access_bc (PLoad Pldrd_a rd) 8 base ofs k)
+  | Tint,    IR rd => OK (indexed_memory_access_bc (PLoad Pldrw rd) 4 base ofs k)
+  | Tlong,   IR rd => OK (indexed_memory_access_bc (PLoad Pldrx rd) 8 base ofs k)
+  | Tsingle, FR rd => OK (indexed_memory_access_bc (PLoad Pldrs rd) 4 base ofs k)
+  | Tfloat,  FR rd => OK (indexed_memory_access_bc (PLoad Pldrd rd) 8 base ofs k)
+  | Tany32,  IR rd => OK (indexed_memory_access_bc (PLoad Pldrw_a rd) 4 base ofs k)
+  | Tany64,  IR rd => OK (indexed_memory_access_bc (PLoad Pldrx_a rd) 8 base ofs k)
+  | Tany64,  FR rd => OK (indexed_memory_access_bc (PLoad Pldrd_a rd) 8 base ofs k)
   | _, _           => Error (msg "Asmgen.loadind")
   end.
 
 Definition storeind (src: mreg) (base: iregsp) (ofs: ptrofs) (ty: typ) (k: bcode) :=
   match ty, preg_of src with
-  | Tint,    IR' rd => OK (indexed_memory_access_bc (PStore Pstrw rd) 4 base ofs k)
-  | Tlong,   IR' rd => OK (indexed_memory_access_bc (PStore Pstrx rd) 8 base ofs k)
-  | Tsingle, FR' rd => OK (indexed_memory_access_bc (PStore Pstrs rd) 4 base ofs k)
-  | Tfloat,  FR' rd => OK (indexed_memory_access_bc (PStore Pstrd rd) 8 base ofs k)
-  | Tany32,  IR' rd => OK (indexed_memory_access_bc (PStore Pstrw_a rd) 4 base ofs k)
-  | Tany64,  IR' rd => OK (indexed_memory_access_bc (PStore Pstrx_a rd) 8 base ofs k)
-  | Tany64,  FR' rd => OK (indexed_memory_access_bc (PStore Pstrd_a rd) 8 base ofs k)
+  | Tint,    IR rd => OK (indexed_memory_access_bc (PStore Pstrw rd) 4 base ofs k)
+  | Tlong,   IR rd => OK (indexed_memory_access_bc (PStore Pstrx rd) 8 base ofs k)
+  | Tsingle, FR rd => OK (indexed_memory_access_bc (PStore Pstrs rd) 4 base ofs k)
+  | Tfloat,  FR rd => OK (indexed_memory_access_bc (PStore Pstrd rd) 8 base ofs k)
+  | Tany32,  IR rd => OK (indexed_memory_access_bc (PStore Pstrw_a rd) 4 base ofs k)
+  | Tany64,  IR rd => OK (indexed_memory_access_bc (PStore Pstrx_a rd) 8 base ofs k)
+  | Tany64,  FR rd => OK (indexed_memory_access_bc (PStore Pstrd_a rd) 8 base ofs k)
   | _, _           => Error (msg "Asmgen.storeind")
   end.
 
@@ -621,8 +621,8 @@ Definition transl_op
   match op, args with
   | Omove, a1 :: nil =>
       match preg_of res, preg_of a1 with
-      | IR' r, IR' a => OK (Pmov r a ::bi k)
-      | FR' r, FR' a => OK (Pfmov r a ::bi k)
+      | IR r, IR a => OK (Pmov r a ::bi k)
+      | FR r, FR a => OK (Pfmov r a ::bi k)
       |  _  ,  _   => Error(msg "Asmgenblock.Omove")
       end
   | Ointconst n, nil =>
@@ -1009,10 +1009,10 @@ Definition transl_op
   (** Conditional move *)
   | Osel cmp ty, a1 :: a2 :: args =>
       match preg_of res with
-      | IR' r => 
+      | IR r => 
           do r1 <- ireg_of a1; do r2 <- ireg_of a2;
           transl_cond cmp args (Pcsel r r1 r2 (cond_for_cond cmp) ::bi k)
-      | FR' r =>
+      | FR r =>
           do r1 <- freg_of a1; do r2 <- freg_of a2;
           transl_cond cmp args (Pcsel r r1 r2 (cond_for_cond cmp) ::bi k)
       | _ =>