mod change (-x)

[helm.git] / helm / software / matita / contribs / ng_assembly / emulator / read_write / IP2022_read_write.ma

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_read_write.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_read_write.ma
old mode 100755 (executable)
new mode 100644 (file)
index 3cb7b1f..8ed36c3
--- a/helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_read_write.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_read_write.ma
@@ -149,7 +149,7 @@ ndefinition IP2022_memory_filter_read_bit ≝
 ndefinition high_write_aux_w16 ≝
 λf:byte8 → byte8.λw:word16.〈(f (cnH ? w)):(cnL ? w)〉.
 
-ndefinition low_write_aux_w16 ≝
+ndefinition lowc_write_aux_w16 ≝
 λf:byte8 → byte8.λw:word16.λflag:aux_mod_type.
  〈((match flag with
     [ auxMode_ok ⇒ λx.x
@@ -157,6 +157,9 @@ ndefinition low_write_aux_w16 ≝
     | auxMode_dec ⇒ pred_b8 ]) (cnH ? w)):
   (f (cnL ? w))〉.
 
+ndefinition lownc_write_aux_w16 ≝
+λf:byte8 → byte8.λw:word16.〈(cnH ? w):(f (cnL ? w))〉.
+
 ndefinition ext_write_aux_w24 ≝
 λf:byte8 → byte8.λw:word24.〈(f (w24x w));(w24h w);(w24l w)〉.
 
@@ -172,13 +175,14 @@ ndefinition low_write_aux_w24 ≝
   [ mk_comp_num wx' wh' ⇒ 〈wx';wh';(w24l w)〉 ].
 
 (* flag di carry: riportare il carry al byte logicamente superiore *)
+(* modifica di pc: non inserita nella stato ma postposta *)
 ndefinition IP2022_memory_filter_write_aux ≝
 λt:memory_impl.λs:any_status IP2022 t.λaddr:word32.λflag:aux_mod_type.
 λfREG:byte8 → byte8.λfMEM:aux_mem_type t → aux_chk_type t → word32 → option (aux_mem_type t).
 (* intercettare le locazioni memory mapped *)
  match eq_w32 addr IP2022_ADDRSEL_loc with
   [ true ⇒ set_addrsel_reg … s (fREG (addrsel_reg_IP2022 (alu … s)))
-  | false ⇒
+  | false ⇒ 
  match eq_w32 addr IP2022_ADDRX_loc with
   [ true ⇒ set_addr_reg … s (ext_write_aux_w24 fREG (get_addrarray (addrsel_reg_IP2022 (alu … s))
                                                                    (addr_array_IP2022 (alu … s))))
@@ -187,16 +191,16 @@ ndefinition IP2022_memory_filter_write_aux ≝
   [ true ⇒ set_ip_reg … s (high_write_aux_w16 fREG (ip_reg_IP2022 (alu … s)))
   | false ⇒
  match eq_w32 addr IP2022_IPL_loc with
-  [ true ⇒ set_ip_reg … s (low_write_aux_w16 fREG (ip_reg_IP2022 (alu … s)) flag)
+  [ true ⇒ set_ip_reg … s (lowc_write_aux_w16 fREG (ip_reg_IP2022 (alu … s)) flag)
   | false ⇒
  match eq_w32 addr IP2022_SPH_loc with
   [ true ⇒ set_sp_reg … s (high_write_aux_w16 fREG (sp_reg_IP2022 (alu … s)))
   | false ⇒
  match eq_w32 addr IP2022_SPL_loc with
-  [ true ⇒ set_sp_reg … s (low_write_aux_w16 fREG (sp_reg_IP2022 (alu … s)) flag)
+  [ true ⇒ set_sp_reg … s (lowc_write_aux_w16 fREG (sp_reg_IP2022 (alu … s)) flag)
   | false ⇒
  match eq_w32 addr IP2022_PCL_loc with
-  [ true ⇒ Some ? (set_pc_reg … s (low_write_aux_w16 fREG (pc_reg_IP2022 (alu … s)) flag))
+  [ true ⇒ Some ? (set_pc_reg … s (lowc_write_aux_w16 fREG (pc_reg_IP2022 (alu … s)) flag))
   | false ⇒
  match eq_w32 addr IP2022_W_loc with
   [ true ⇒ Some ? (set_acc_8_low_reg … s (fREG (acc_low_reg_IP2022 (alu … s))))
@@ -205,7 +209,7 @@ ndefinition IP2022_memory_filter_write_aux ≝
   [ true ⇒ set_dp_reg … s (high_write_aux_w16 fREG (dp_reg_IP2022 (alu … s)))
   | false ⇒
  match eq_w32 addr IP2022_DPL_loc with
-  [ true ⇒ set_dp_reg … s (low_write_aux_w16 fREG (dp_reg_IP2022 (alu … s)) flag)
+  [ true ⇒ set_dp_reg … s (lowc_write_aux_w16 fREG (dp_reg_IP2022 (alu … s)) flag)
   | false ⇒
  match eq_w32 addr IP2022_MULH_loc with
   [ true ⇒ set_mulh_reg … s (fREG (mulh_reg_IP2022 (alu … s)))
@@ -221,17 +225,20 @@ ndefinition IP2022_memory_filter_write_aux ≝
  match eq_w32 addr IP2022_DATAH_loc with
   [ true ⇒ set_data_reg … s (high_write_aux_w16 fREG (data_reg_IP2022 (alu … s)))
   | false ⇒
+(* nessun riporto automatico *)
  match eq_w32 addr IP2022_DATAL_loc with
-  [ true ⇒ set_data_reg … s (low_write_aux_w16 fREG (data_reg_IP2022 (alu … s)) flag)
+  [ true ⇒ set_data_reg … s (lownc_write_aux_w16 fREG (data_reg_IP2022 (alu … s)))
   | false ⇒
  match eq_w32 addr IP2022_CALLH_loc with
   [ true ⇒ set_call_reg … s (high_write_aux_w16 fREG (getn_array16T x0 ? (call_stack_IP2022 (alu … s))))
   | false ⇒
+(* nessun riporto automatico *)
  match eq_w32 addr IP2022_CALLL_loc with
-  [ true ⇒ set_call_reg … s (low_write_aux_w16 fREG (getn_array16T x0 ? (call_stack_IP2022 (alu … s))) flag)
+  [ true ⇒ set_call_reg … s (lownc_write_aux_w16 fREG (getn_array16T x0 ? (call_stack_IP2022 (alu … s))))
 (* accesso normale *)
   | false ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s) addr)
-             (λmem'.Some ? (set_mem_desc … s mem')) ]]]]]]]]]]]]]]]]].
+             (λmem'.Some ? (set_mem_desc … s mem'))
+  ]]]]]]]]]]]]]]]]].
 
 (* scrittura IP2022 di un byte *)
 ndefinition IP2022_memory_filter_write ≝
@@ -239,15 +246,16 @@ ndefinition IP2022_memory_filter_write ≝
 λaddr:word32.λflag:aux_mod_type.λval:byte8.
  (* PAGE[7:5] Z[2] H[1] C [0] *)
  match eq_w32 addr IP2022_STATUS_loc with
-  [ true ⇒ Some ? (set_alu … s
-            (set_page_reg_IP2022
-             (set_z_flag_IP2022
-              (set_h_flag_IP2022
-               (set_c_flag_IP2022 (alu … s)
-                (getn_array8T o7 ? (bits_of_byte8 val)))
-               (getn_array8T o6 ? (bits_of_byte8 val)))
-              (getn_array8T o5 ? (bits_of_byte8 val)))
-             (oct_of_exH (cnH ? val))))
+  [ true ⇒ Some ? 
+            (set_alu … s
+             (set_page_reg_IP2022
+              (set_z_flag_IP2022
+               (set_h_flag_IP2022
+                (set_c_flag_IP2022 (alu … s)
+                 (getn_array8T o7 ? (bits_of_byte8 val)))
+                (getn_array8T o6 ? (bits_of_byte8 val)))
+               (getn_array8T o5 ? (bits_of_byte8 val)))
+              (oct_of_exH (cnH ? val))))
  (* accesso a registro_non_spezzato/normale *)
   | false ⇒ IP2022_memory_filter_write_aux t s addr flag
              (λb.val)