aarch64/Asmblock: Change preg to simplify preg-ification

Since ireg and iregsp coerces to preg, and iregsp subsumes ireg define
preg's IR constructor with iregsp and remove SP.

This is the first step in the "preg-ification" of aarch64/Asmblock.
The goal is to unify instructions that only differ in the types of
registers they use. That is, we want to group together instructions
e.g. `rd <- op r1 ...` even if r1 is ireg for one op and freg for
another operation.
(NB: This currently excludes operations that use ireg0 which will are
and will be grouped separately for now.)

1 files changed, 12 insertions, 10 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 21061747..1b503f24 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -62,6 +62,9 @@ Coercion RR1: ireg >-> iregsp.
 Lemma ireg_eq: forall (x y: ireg), {x=y} + {x<>y}.
 Proof. decide equality. Defined.
 
+Lemma iregsp_eq: forall (x y: iregsp), {x=y} + {x<>y}.
+Proof. decide equality; apply ireg_eq. Defined.
+
 (** In assembly files, [Dn] denotes the low 64-bit of a vector register,
     and [Sn] the low 32 bits. *)
 
@@ -88,18 +91,19 @@ Proof. decide equality. Defined.
 (** We model the following registers of the ARM architecture. *)
 
 Inductive preg: Type :=
-  | IR: ireg -> preg   (**r 64- or 32-bit integer registers *)
-  | FR: freg -> preg   (**r double- or single-precision float registers *)
-  | CR: crbit -> preg  (**r bits in the condition register *)
-  | SP: preg           (**r register X31 used as stack pointer *)
-  | PC: preg.          (**r program counter *)
-
-Coercion IR: ireg >-> preg.
+  | IR: iregsp -> preg   (**r 64- or 32-bit integer registers *)
+  | FR: freg -> preg     (**r double- or single-precision float registers *)
+  | CR: crbit -> preg    (**r bits in the condition register *)
+  | PC: preg.            (**r program counter *)
+
+(* XXX: ireg no longer coerces to preg *)
+Coercion IR: iregsp >-> preg.
+Definition SP:preg := XSP.
 Coercion FR: freg >-> preg.
 Coercion CR: crbit >-> preg.
 
 Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}.
-Proof. decide equality. apply ireg_eq. apply freg_eq. apply crbit_eq. Defined.
+Proof. decide equality. apply iregsp_eq. apply freg_eq. apply crbit_eq. Defined.
 
 Module PregEq.
   Definition t := preg.
@@ -111,8 +115,6 @@ Module Pregmap := EMap(PregEq).
 Definition preg_of_iregsp (r: iregsp) : preg :=
   match r with RR1 r => IR r | XSP => SP end.
 
-Coercion preg_of_iregsp: iregsp >-> preg.
-
 (** Conventional name for return address ([RA]) *)
 
 Notation "'RA'" := X30 (only parsing) : asm.