Small refactoring and renaming of Stores and Loads

3 files changed, 50 insertions, 70 deletions

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 3656b91f..9d7b372e 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -244,7 +244,7 @@ Inductive cf_instruction : Type :=
 .
 
 (** Loads **)
-Inductive load_name_rro : Type :=
+Inductive load_name : Type :=
   | Plb                                             (**r load byte *)
   | Plbu                                            (**r load byte unsigned *)
   | Plh                                             (**r load half word *)
@@ -258,15 +258,15 @@ Inductive load_name_rro : Type :=
 .
 
 Inductive ld_instruction : Type :=
-  | PLoadRRO   (i: load_name_rro) (rd: ireg) (ra: ireg) (ofs: offset)
-  | PLoadRRR   (i: load_name_rro) (rd: ireg) (ra: ireg) (rofs: ireg)
+  | PLoadRRO   (i: load_name) (rd: ireg) (ra: ireg) (ofs: offset)
+  | PLoadRRR   (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg)
 .
 
-Coercion PLoadRRO:       load_name_rro        >-> Funclass.
-Coercion PLoadRRR:       load_name_rro        >-> Funclass.
+Coercion PLoadRRO:       load_name        >-> Funclass.
+Coercion PLoadRRR:       load_name        >-> Funclass.
 
 (** Stores **)
-Inductive store_name_rro : Type :=
+Inductive store_name : Type :=
   | Psb                                             (**r store byte *)
   | Psh                                             (**r store half byte *)
   | Psw                                             (**r store int32 *)
@@ -278,12 +278,12 @@ Inductive store_name_rro : Type :=
 .
 
 Inductive st_instruction : Type :=
-  | PStoreRRO  (i: store_name_rro) (rs: ireg) (ra: ireg) (ofs: offset)
-  | PStoreRRR  (i: store_name_rro) (rs: ireg) (ra: ireg) (rofs: ireg)
+  | PStoreRRO  (i: store_name) (rs: ireg) (ra: ireg) (ofs: offset)
+  | PStoreRRR  (i: store_name) (rs: ireg) (ra: ireg) (rofs: ireg)
 .
 
-Coercion PStoreRRO:       store_name_rro        >-> Funclass.
-Coercion PStoreRRR:       store_name_rro        >-> Funclass.
+Coercion PStoreRRO:       store_name        >-> Funclass.
+Coercion PStoreRRR:       store_name        >-> Funclass.
 
 (** Arithmetic instructions **)
 Inductive arith_name_r : Type :=
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 7e332895..e038a5ae 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -71,18 +71,18 @@ Coercion OArithRRI32: arith_name_rri32 >-> Funclass.
 Coercion OArithRRI64: arith_name_rri64 >-> Funclass.
 
 Inductive load_op :=
-  | OLoadRRO (n: load_name_rro) (ofs: offset)
-  | OLoadRRR (n: load_name_rro)
+  | OLoadRRO (n: load_name) (ofs: offset)
+  | OLoadRRR (n: load_name)
 .
 
-Coercion OLoadRRO: load_name_rro >-> Funclass.
+Coercion OLoadRRO: load_name >-> Funclass.
 
 Inductive store_op :=
-  | OStoreRRO (n: store_name_rro) (ofs: offset)
-  | OStoreRRR (n: store_name_rro)
+  | OStoreRRO (n: store_name) (ofs: offset)
+  | OStoreRRR (n: store_name)
 .
 
-Coercion OStoreRRO: store_name_rro >-> Funclass.
+Coercion OStoreRRO: store_name >-> Funclass.
 
 Inductive op_wrap :=
   | Arith (ao: arith_op)
@@ -1571,7 +1571,7 @@ Definition string_of_arith (op: arith_op): pstring :=
   | OArithARRI64 n _ => string_of_name_arri64 n
   end.
 
-Definition string_of_name_lrro (n: load_name_rro) : pstring :=
+Definition string_of_load_name (n: load_name) : pstring :=
   match n with
     Plb => "Plb"
   | Plbu => "Plbu"
@@ -1587,11 +1587,11 @@ Definition string_of_name_lrro (n: load_name_rro) : pstring :=
 
 Definition string_of_load (op: load_op): pstring :=
   match op with
-  | OLoadRRO n _ => string_of_name_lrro n
-  | OLoadRRR n => string_of_name_lrro n
+  | OLoadRRO n _ => string_of_load_name n
+  | OLoadRRR n => string_of_load_name n
   end.
 
-Definition string_of_name_srro (n: store_name_rro) : pstring :=
+Definition string_of_store_name (n: store_name) : pstring :=
   match n with
     Psb => "Psb"
   | Psh => "Psh"
@@ -1605,8 +1605,8 @@ Definition string_of_name_srro (n: store_name_rro) : pstring :=
 
 Definition string_of_store (op: store_op) : pstring :=
   match op with
-  | OStoreRRO n _ => string_of_name_srro n
-  | OStoreRRR n => string_of_name_srro n
+  | OStoreRRO n _ => string_of_store_name n
+  | OStoreRRR n => string_of_store_name n
   end.
 
 Definition string_of_control (op: control_op) : pstring :=
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 1afb627a..f207b64d 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -792,61 +792,41 @@ Definition transl_memory_access
       Error(msg "Asmblockgen.transl_memory_access")
   end.
 
+Definition chunk2load (chunk: memory_chunk) :=
+  match chunk with
+  | Mint8signed => Plb
+  | Mint8unsigned => Plbu
+  | Mint16signed => Plh
+  | Mint16unsigned => Plhu
+  | Mint32 => Plw
+  | Mint64 => Pld
+  | Mfloat32 => Pfls
+  | Mfloat64 => Pfld
+  | Many32 => Plw_a
+  | Many64 => Pld_a
+  end.
+
 Definition transl_load (chunk: memory_chunk) (addr: addressing)
            (args: list mreg) (dst: mreg) (k: bcode) : res bcode :=
+  do r <- ireg_of dst;
+  transl_memory_access (chunk2load chunk r) addr args k.
+
+Definition chunk2store (chunk: memory_chunk) :=
   match chunk with
-  | Mint8signed =>
-      do r <- ireg_of dst;
-      transl_memory_access (Plb r)  addr args k
-  | Mint8unsigned =>
-      do r <- ireg_of dst;
-      transl_memory_access (Plbu r) addr args k
-  | Mint16signed =>
-      do r <- ireg_of dst;
-      transl_memory_access (Plh r)  addr args k
-  | Mint16unsigned =>
-      do r <- ireg_of dst;
-      transl_memory_access (Plhu r) addr args k
-  | Mint32 =>
-      do r <- ireg_of dst;
-      transl_memory_access (Plw r)  addr args k
-  | Mint64 =>
-      do r <- ireg_of dst;
-      transl_memory_access (Pld r)  addr args k
-  | Mfloat32 =>
-      do r <- freg_of dst;
-      transl_memory_access (Pfls r) addr args k
-  | Mfloat64 =>
-      do r <- freg_of dst;
-      transl_memory_access (Pfld r) addr args k
-  | _ =>
-      Error (msg "Asmblockgen.transl_load")
+  | Mint8signed | Mint8unsigned => Psb
+  | Mint16signed | Mint16unsigned => Psh
+  | Mint32 => Psw
+  | Mint64 => Psd
+  | Mfloat32 => Pfss
+  | Mfloat64 => Pfsd
+  | Many32 => Psw_a
+  | Many64 => Psd_a
   end.
 
 Definition transl_store (chunk: memory_chunk) (addr: addressing)
            (args: list mreg) (src: mreg) (k: bcode) : res bcode :=
-  match chunk with
-  | Mint8signed | Mint8unsigned =>
-      do r <- ireg_of src;
-      transl_memory_access (Psb r)  addr args k
-  | Mint16signed | Mint16unsigned =>
-      do r <- ireg_of src;
-      transl_memory_access (Psh r)  addr args k
-  | Mint32 =>
-      do r <- ireg_of src;
-      transl_memory_access (Psw r)  addr args k
-  | Mint64 =>
-      do r <- ireg_of src;
-      transl_memory_access (Psd r)  addr args k
-  | Mfloat32 =>
-      do r <- freg_of src;
-      transl_memory_access (Pfss r) addr args k
-  | Mfloat64 =>
-      do r <- freg_of src;
-      transl_memory_access (Pfsd r) addr args k
-  | _ =>
-      Error (msg "Asmblockgen.transl_store")
-  end.
+  do r <- ireg_of src;
+  transl_memory_access (chunk2store chunk r) addr args k.
 
 (** Function epilogue *)