mod change (-x)

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

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_load_write.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_load_write.ma
old mode 100755 (executable)
new mode 100644 (file)
index eccc4ee..f7040de
--- a/helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_load_write.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_load_write.ma
@@ -25,8 +25,8 @@ include "emulator/read_write/load_write_base.ma".
 
 (* lettura da [OLD PC<<1 + 1] : argomento non caricato dal fetch word-aligned *)
 ndefinition mode_IMM1_load ≝
-λt:memory_impl.λs:any_status IP2022 t.λpco:word16.
- mem_read_s … s (rol_w32 〈〈〈x8,x1〉:〈x0,x0〉〉.pco〉).
+λt:memory_impl.λs:any_status IP2022 t.
+ mem_read_s … s (rol_w32 〈〈〈x8,x1〉:〈x0,x0〉〉.(get_pc_reg … s)〉).
 
 (* SCHEMA:
    ADDRX=0x00 [ADDRH|ADDRL] 16Kb PROGRAM RAM
@@ -55,8 +55,8 @@ ndefinition mode_ADDR_write ≝
 (* IMM1 > 0 : lettura/scrittura da [IMM1] *)
 (* else     : lettura/scrittura da [IP] : IP ≥ 0x20 *)
 ndefinition mode_DIR1IP_aux ≝
-λt:memory_impl.λs:any_status IP2022 t.λpco:word16.λT.λf:word32 → option T.
- opt_map … (mode_IMM1_load t s pco)
+λt:memory_impl.λs:any_status IP2022 t.λT.λf:word32 → option T.
+ opt_map … (mode_IMM1_load t s)
   (λaddr.match eq_b8 addr 〈x0,x0〉 with
    (* xxxxxxx0 00000000 → [IP] *)
    [ true ⇒ opt_map … (get_ip_reg … s)
@@ -71,8 +71,8 @@ ndefinition mode_DIR1IP_aux ≝
 (* IMM1 < 0x80 : lettura/scrittura da [DP+IMM1] : DP+IMM1 ≥ 0x20 *)
 (* else        : lettura/scrittura da [SP+IMM1] : SP+IMM1 ≥ 0x20 *)
 ndefinition mode_DPSP_aux ≝
-λt:memory_impl.λs:any_status IP2022 t.λpco:word16.λT.λf:word32 → option T.
- opt_map … (mode_IMM1_load t s pco)
+λt:memory_impl.λs:any_status IP2022 t.λT.λf:word32 → option T.
+ opt_map … (mode_IMM1_load t s)
   (λaddr.opt_map … (match getMSB_b8 addr with
                     (* xxxxxxx1 1nnnnnnn → [SP+IMM1] *)
                     [ true ⇒ get_sp_reg … s
@@ -85,37 +85,37 @@ ndefinition mode_DPSP_aux ≝
 
 (* FR0 *)
 ndefinition mode_FR0_load ≝
-λt:memory_impl.λs:any_status IP2022 t.λpco:word16.
- mode_DIR1IP_aux t s pco byte8 (memory_filter_read … s).
+λt:memory_impl.λs:any_status IP2022 t.
+ mode_DIR1IP_aux t s byte8 (memory_filter_read … s).
 
 ndefinition mode_FR0n_load ≝
-λt:memory_impl.λs:any_status IP2022 t.λpco:word16.λsub:oct.
- mode_DIR1IP_aux t s pco bool (λaddr.memory_filter_read_bit … s addr sub).
+λt:memory_impl.λs:any_status IP2022 t.λsub:oct.
+ mode_DIR1IP_aux t s bool (λaddr.memory_filter_read_bit … s addr sub).
 
 ndefinition mode_FR0_write ≝
-λt:memory_impl.λs:any_status IP2022 t.λpco:word16.λflag:aux_mod_type.λval:byte8.
- mode_DIR1IP_aux t s pco (any_status IP2022 t) (λaddr.memory_filter_write … s addr flag val).
+λt:memory_impl.λs:any_status IP2022 t.λflag:aux_mod_type.λval:byte8.
+ mode_DIR1IP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write … s addr flag val).
 
 ndefinition mode_FR0n_write ≝
-λt:memory_impl.λs:any_status IP2022 t.λpco:word16.λsub:oct.λval:bool.
- mode_DIR1IP_aux t s pco (any_status IP2022 t) (λaddr.memory_filter_write_bit … s addr sub val).
+λt:memory_impl.λs:any_status IP2022 t.λsub:oct.λval:bool.
+ mode_DIR1IP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write_bit … s addr sub val).
 
 (* FR1 *)
 ndefinition mode_FR1_load ≝
-λt:memory_impl.λs:any_status IP2022 t.λpco:word16.
- mode_DPSP_aux t s pco byte8 (memory_filter_read … s).
+λt:memory_impl.λs:any_status IP2022 t.
+ mode_DPSP_aux t s byte8 (memory_filter_read … s).
 
 ndefinition mode_FR1n_load ≝
-λt:memory_impl.λs:any_status IP2022 t.λpco:word16.λsub:oct.
- mode_DPSP_aux t s pco bool (λaddr.memory_filter_read_bit … s addr sub).
+λt:memory_impl.λs:any_status IP2022 t.λsub:oct.
+ mode_DPSP_aux t s bool (λaddr.memory_filter_read_bit … s addr sub).
 
 ndefinition mode_FR1_write ≝
-λt:memory_impl.λs:any_status IP2022 t.λpco:word16.λflag:aux_mod_type.λval:byte8.
- mode_DPSP_aux t s pco (any_status IP2022 t) (λaddr.memory_filter_write … s addr flag val).
+λt:memory_impl.λs:any_status IP2022 t.λflag:aux_mod_type.λval:byte8.
+ mode_DPSP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write … s addr flag val).
 
 ndefinition mode_FR1n_write ≝
-λt:memory_impl.λs:any_status IP2022 t.λpco:word16.λsub:oct.λval:bool.
- mode_DPSP_aux t s pco (any_status IP2022 t) (λaddr.memory_filter_write_bit … s addr sub val).
+λt:memory_impl.λs:any_status IP2022 t.λsub:oct.λval:bool.
+ mode_DPSP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write_bit … s addr sub val).
 
 (* ************************************** *)
 (* raccordo di tutte le possibili letture *)
@@ -127,7 +127,7 @@ ndefinition aux_inc_addr2 ≝
  set_addr_reg_sIP2022 t s (succ_w24 (succ_w24 (get_addr_reg_IP2022 (alu … s)))).
 
 ndefinition IP2022_multi_mode_load_auxb ≝
-λt.λs:any_status IP2022 t.λpco,cur_pc:word16.λi:IP2022_instr_mode.match i with
+λt.λs:any_status IP2022 t.λcur_pc:word16.λi:IP2022_instr_mode.match i with
 (* NO: non ci sono indicazioni *)
    [ MODE_INH ⇒ None ?
 (* NO: solo word *)
@@ -138,7 +138,7 @@ ndefinition IP2022_multi_mode_load_auxb ≝
 (* IMM3 *)
    | MODE_IMM3 o ⇒ Some ? (triple … s (extu_b8 (ex_of_oct o)) cur_pc)
 (* IMM8 *)
-   | MODE_IMM8 ⇒ opt_map … (mode_IMM1_load t s pco)
+   | MODE_IMM8 ⇒ opt_map … (mode_IMM1_load t s)
                   (λb.Some ? (triple … s b cur_pc))
 (* NO: solo lettura word *)
    | MODE_IMM13 _ ⇒ None ?
@@ -153,15 +153,15 @@ ndefinition IP2022_multi_mode_load_auxb ≝
    | MODE_W_and_FR1 ⇒ None ?
 
 (* [FRn] *)
-   | MODE_FR0n o ⇒ opt_map … (mode_FR0n_load t s pco o)
+   | MODE_FR0n o ⇒ opt_map … (mode_FR0n_load t s o)
                     (λb.Some ? (triple … s (extu_b8 (match b with [ true ⇒ x1 | false ⇒ x0 ])) cur_pc))
 (* [FRn] *)
-   | MODE_FR1n o ⇒ opt_map … (mode_FR1n_load t s pco o)
+   | MODE_FR1n o ⇒ opt_map … (mode_FR1n_load t s o)
                     (λb.Some ? (triple … s (extu_b8 (match b with [ true ⇒ x1 | false ⇒ x0 ])) cur_pc))
    ].
 
 ndefinition IP2022_multi_mode_load_auxw ≝
-λt.λs:any_status IP2022 t.λpco,cur_pc:word16.λi:IP2022_instr_mode.match i with
+λt.λs:any_status IP2022 t.λcur_pc:word16.λi:IP2022_instr_mode.match i with
 (* NO: non ci sono indicazioni *)
    [ MODE_INH ⇒ None ?
 (* [ADDR] *)
@@ -176,20 +176,20 @@ ndefinition IP2022_multi_mode_load_auxw ≝
 (* NO: solo lettura byte *)
    | MODE_IMM8 ⇒ None ?
 (* IMM13 *)
-   | MODE_IMM13 bt ⇒ opt_map … (mode_IMM1_load t s pco)
+   | MODE_IMM13 bt ⇒ opt_map … (mode_IMM1_load t s)
                       (λb.Some ? (triple … s 〈(b8_of_bit bt):b〉 cur_pc))
 
 (* FR, W → FR *)
-   | MODE_FR0_and_W ⇒ opt_map … (mode_FR0_load t s pco)
+   | MODE_FR0_and_W ⇒ opt_map … (mode_FR0_load t s)
                        (λfr.Some ? (triple … s 〈fr:(get_acc_8_low_reg … s)〉 cur_pc))
 (* FR, W → FR *)
-   | MODE_FR1_and_W ⇒ opt_map … (mode_FR1_load t s pco)
+   | MODE_FR1_and_W ⇒ opt_map … (mode_FR1_load t s)
                        (λfr.Some ? (triple … s 〈fr:(get_acc_8_low_reg … s)〉 cur_pc))
 (* W, FR → W *)
-   | MODE_W_and_FR0 ⇒ opt_map … (mode_FR0_load t s pco)
+   | MODE_W_and_FR0 ⇒ opt_map … (mode_FR0_load t s)
                        (λfr.Some ? (triple … s 〈(get_acc_8_low_reg … s):fr〉 cur_pc))
 (* W, FR → W *)
-   | MODE_W_and_FR1 ⇒ opt_map … (mode_FR1_load t s pco)
+   | MODE_W_and_FR1 ⇒ opt_map … (mode_FR1_load t s)
                        (λfr.Some ? (triple … s 〈(get_acc_8_low_reg … s):fr〉 cur_pc))
 
 (* NO: solo byte *)
@@ -203,7 +203,7 @@ ndefinition IP2022_multi_mode_load_auxw ≝
 (* **************************************** *)
 
 ndefinition IP2022_multi_mode_write_auxb ≝
-λt.λs:any_status IP2022 t.λpco,cur_pc:word16.λflag:aux_mod_type.λi:IP2022_instr_mode.λwriteb:byte8.match i with
+λt.λs:any_status IP2022 t.λcur_pc:word16.λflag:aux_mod_type.λi:IP2022_instr_mode.λwriteb:byte8.match i with
 (* NO: non ci sono indicazioni *)
    [ MODE_INH ⇒ None ?
 (* NO: solo word *)
@@ -219,10 +219,10 @@ ndefinition IP2022_multi_mode_write_auxb ≝
    | MODE_IMM13 _ ⇒ None ?
 
 (* FR, W → FR *)
-   | MODE_FR0_and_W ⇒ opt_map … (mode_FR0_write t s pco flag writeb)
+   | MODE_FR0_and_W ⇒ opt_map … (mode_FR0_write t s flag writeb)
                        (λs'.Some ? (pair … s' cur_pc))
 (* FR, W → FR *)
-   | MODE_FR1_and_W ⇒ opt_map … (mode_FR1_write t s pco flag writeb)
+   | MODE_FR1_and_W ⇒ opt_map … (mode_FR1_write t s flag writeb)
                        (λs'.Some ? (pair … s' cur_pc))
 (* W, FR → W *)
    | MODE_W_and_FR0 ⇒ Some ? (pair … (set_acc_8_low_reg … s writeb) cur_pc)
@@ -230,15 +230,15 @@ ndefinition IP2022_multi_mode_write_auxb ≝
    | MODE_W_and_FR1 ⇒ Some ? (pair … (set_acc_8_low_reg … s writeb) cur_pc)
 
 (* [FRn] *)
-   | MODE_FR0n o ⇒ opt_map … (mode_FR0n_write t s pco o (getn_array8T o ? (bits_of_byte8 writeb)))
+   | MODE_FR0n o ⇒ opt_map … (mode_FR0n_write t s o (getn_array8T o ? (bits_of_byte8 writeb)))
                     (λs'.Some ? (pair … s' cur_pc))
 (* [FRn] *)
-   | MODE_FR1n o ⇒ opt_map … (mode_FR1n_write t s pco o (getn_array8T o ? (bits_of_byte8 writeb)))
+   | MODE_FR1n o ⇒ opt_map … (mode_FR1n_write t s o (getn_array8T o ? (bits_of_byte8 writeb)))
                     (λs'.Some ? (pair … s' cur_pc))
    ].
 
 ndefinition IP2022_multi_mode_write_auxw ≝
-λt.λs:any_status IP2022 t.λpco,cur_pc:word16.λi:IP2022_instr_mode.λwritew:word16.match i with
+λt.λs:any_status IP2022 t.λcur_pc:word16.λi:IP2022_instr_mode.λwritew:word16.match i with
 (* NO: non ci sono indicazioni *)
    [ MODE_INH ⇒ None ?
 (* [ADDR] *)