X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Ffreescale%2Fmultivm.ma;h=b78efba70dad77b5371bac1bf15e873ccffefe5b;hb=f538a0b46ba4164a21a76e47a6ed3b3e9deb5041;hp=00de15cfa5cccec9a9ad039a4927db8b3e9ce333;hpb=84ef7e61acf6d6bc785fced0ed5790897f86c746;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/freescale/multivm.ma b/helm/software/matita/contribs/assembly/freescale/multivm.ma
index 00de15cfa..b78efba70 100644
--- a/helm/software/matita/contribs/assembly/freescale/multivm.ma
+++ b/helm/software/matita/contribs/assembly/freescale/multivm.ma
@@ -45,7 +45,7 @@ include "freescale/load_write.ma".
 definition execute_ADC_ADD_aux ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
 λfAMC:byte8 → byte8 → bool → Prod byte8 bool.
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
     let A_op ≝ get_acc_8_low_reg m t s_tmp1 in
@@ -74,7 +74,7 @@ definition execute_ADC_ADD_aux ≝
 definition execute_AND_BIT_EOR_ORA_aux ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
 λfAM:byte8 → byte8 → byte8.
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
     let R_op ≝ fAM (get_acc_8_low_reg m t s_tmp1) M_op in
@@ -94,12 +94,12 @@ definition execute_AND_BIT_EOR_ORA_aux ≝
 definition execute_ASL_ASR_LSR_ROL_ROR_aux ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
 λfMC:byte8 → bool → Prod byte8 bool.
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op _ ⇒
     match fMC M_op (get_c_flag m t s_tmp1) with [ pair R_op carry ⇒
     (* M = fMC(M,C) *)
-    opt_map ?? (multi_mode_write m t true s_tmp1 cur_pc i R_op)
+    opt_map ?? (multi_mode_write true m t s_tmp1 cur_pc i R_op)
      (λS_PC.match S_PC with
       [ pair s_tmp2 new_pc ⇒
       (* C = carry *)
@@ -126,7 +126,7 @@ definition branched_pc ≝
 (* tutti i branch calcoleranno la condizione e la passeranno qui *)
 definition execute_any_BRANCH ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λfCOND:bool.
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
     (* if true, branch *) 
@@ -141,7 +141,7 @@ definition execute_any_BRANCH ≝
 definition execute_BCLRn_BSETn_aux ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λoptval:byte8.
  (* Mn = filtered optval *)
- opt_map ?? (multi_mode_write m t true s cur_pc i optval)
+ opt_map ?? (multi_mode_write true m t s cur_pc i optval)
   (λS_PC.match S_PC with
    (* newpc = nextpc *)
    [ pair s_tmp1 new_pc ⇒ Some ? (pair ?? s_tmp1 new_pc) ]).
@@ -150,7 +150,7 @@ definition execute_BCLRn_BSETn_aux ≝
 (* il chiamante passa la logica da testare (0x00,¬0x00) e poi si salta *)
 definition execute_BRCLRn_BRSETn_aux ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λfCOND:byte8 → bool.
- opt_map ?? (multi_mode_load m t false s cur_pc i)
+ opt_map ?? (multi_mode_load false m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒ match M_op with
     [ mk_word16 MH_op ML_op ⇒
@@ -166,12 +166,12 @@ definition execute_BRCLRn_BRSETn_aux ≝
 definition execute_COM_DEC_INC_NEG_aux ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
 λfM:byte8 → byte8.λfV:bool → bool → bool.λfC:bool → byte8 → bool.
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op _ ⇒
     let R_op ≝ fM M_op in
     (* M = fM(M) *)
-    opt_map ?? (multi_mode_write m t true s_tmp1 cur_pc i R_op)
+    opt_map ?? (multi_mode_write true m t s_tmp1 cur_pc i R_op)
      (λS_PC.match S_PC with
       [ pair s_tmp2 new_pc ⇒
       (* C = fCR (C,R) *)
@@ -191,7 +191,7 @@ definition execute_COM_DEC_INC_NEG_aux ≝
 definition execute_SBC_SUB_aux ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
 λfAMC:byte8 → byte8 → bool → Prod byte8 bool.
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
     let A_op ≝ get_acc_8_low_reg m t s_tmp1 in
@@ -282,7 +282,7 @@ definition execute_ADD ≝
 (* SP += extended M *)
 definition execute_AIS ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
    opt_map ?? (get_sp_reg m t s_tmp1)
@@ -293,7 +293,7 @@ definition execute_AIS ≝
 (* H:X += extended M *)
 definition execute_AIX ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
    opt_map ?? (get_indX_16_reg m t s_tmp1)
@@ -468,7 +468,7 @@ definition execute_BSETn ≝
 (* HC05/HC08/HCS08 si appoggiano allo stack, RS08 a SPC *)
 definition execute_BSR ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t .λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒ let aux ≝
     (* push (new_pc low) *)
@@ -489,7 +489,7 @@ definition execute_BSR ≝
 (* if A=M, branch *)
 definition execute_CBEQA ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load m t false s cur_pc i)
+ opt_map ?? (multi_mode_load false m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
     match M_op with
@@ -505,7 +505,7 @@ definition execute_CBEQA ≝
 (* if X=M, branch *)
 definition execute_CBEQX ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load m t false s cur_pc i)
+ opt_map ?? (multi_mode_load false m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
     match M_op with
@@ -534,7 +534,7 @@ definition execute_CLI ≝
 definition execute_CLR ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
  (* M = 0 *)
- opt_map ?? (multi_mode_write m t true s cur_pc i 〈x0,x0〉)
+ opt_map ?? (multi_mode_write true m t s cur_pc i 〈x0,x0〉)
   (λS_PC.match S_PC with
    [ pair s_tmp1 new_pc ⇒
    (* Z = 1 *)
@@ -563,7 +563,7 @@ definition execute_COM ≝
 (* flags = H:X - M *)
 definition execute_CPHX ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load m t false s cur_pc i)
+ opt_map ?? (multi_mode_load false m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
     opt_map ?? (get_indX_16_reg m t s_tmp1)
@@ -585,7 +585,7 @@ definition execute_CPHX ≝
 (* flags = X - M *)
 definition execute_CPX ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
     opt_map ?? (get_indX_8_low_reg m t s_tmp1)
@@ -629,14 +629,14 @@ definition execute_DAA ≝
 (* if (--M)≠0, branch *)
 definition execute_DBNZ ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load m t false s cur_pc i)
+ opt_map ?? (multi_mode_load false m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
     match M_op with
      [ mk_word16 MH_op ML_op ⇒
      (* --M *)
      let MH_op' ≝ pred_b8 MH_op in
-     opt_map ?? (multi_mode_write m t true s_tmp1 cur_pc i MH_op')
+     opt_map ?? (multi_mode_write true m t s_tmp1 cur_pc i MH_op')
       (λS_PC.match S_PC with
        [ pair s_tmp2 _ ⇒
         (* if (--M)≠0, branch *)
@@ -695,7 +695,7 @@ definition execute_INC ≝
 (* jmp, il nuovo indirizzo e' una WORD *)
 definition execute_JMP ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load m t false s cur_pc i)
+ opt_map ?? (multi_mode_load false m t s cur_pc i)
   (λS_M_PC.
    (* newpc = M_op *)
    Some ? (pair ?? (fst3T ??? S_M_PC) (snd3T ??? S_M_PC))).
@@ -704,7 +704,7 @@ definition execute_JMP ≝
 (* HC05/HC08/HCS08 si appoggiano allo stack, RS08 a SPC *)
 definition execute_JSR ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load m t false s cur_pc i)
+ opt_map ?? (multi_mode_load false m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒ let aux ≝
     (* push (new_pc low) *)
@@ -725,7 +725,7 @@ definition execute_JSR ≝
 (* A = M *)
 definition execute_LDA ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
     (* A = M *) 
@@ -742,7 +742,7 @@ definition execute_LDA ≝
 (* H:X = M *)
 definition execute_LDHX ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load m t false s cur_pc i)
+ opt_map ?? (multi_mode_load false m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
     opt_map ?? (set_indX_16_reg m t s_tmp1 M_op)
@@ -759,7 +759,7 @@ definition execute_LDHX ≝
 (* X = M *)
 definition execute_LDX ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
     opt_map ?? (set_indX_8_low_reg m t s_tmp1 M_op)
@@ -782,11 +782,11 @@ definition execute_LSR ≝
 definition execute_MOV ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
  (* R_op = M1 *)
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
   (λS_R_PC.match S_R_PC with
    [ tripleT s_tmp1 R_op tmp_pc ⇒
     (* M2 = R_op *)
-    opt_map ?? (multi_mode_write m t true s_tmp1 tmp_pc i R_op)
+    opt_map ?? (multi_mode_write true m t s_tmp1 tmp_pc i R_op)
      (λS_PC.match S_PC with
       [ pair s_tmp2 new_pc ⇒
        (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
@@ -983,7 +983,7 @@ definition execute_STA ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
  (* M = A *)
  let A_op ≝ (get_acc_8_low_reg m t s) in
- opt_map ?? (multi_mode_write m t true s cur_pc i A_op)
+ opt_map ?? (multi_mode_write true m t s cur_pc i A_op)
   (λS_op_and_PC.match S_op_and_PC with
    [ pair s_tmp1 new_pc ⇒
    (* Z = nA7&nA6&nA5&nA4&nA3&nA2&nA1&nA0 *)
@@ -1000,7 +1000,7 @@ definition execute_STHX ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
  (* M = H:X *)
  opt_map ?? (get_indX_16_reg m t s)
-  (λX_op.opt_map ?? (multi_mode_write m t false s cur_pc i X_op)
+  (λX_op.opt_map ?? (multi_mode_write false m t s cur_pc i X_op)
    (λS_op_and_PC.match S_op_and_PC with
     [ pair s_tmp1 new_pc ⇒
      (* Z = nR15&nR14&nR13nR12&nR11&nR10&nR9&nR8nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
@@ -1022,7 +1022,7 @@ definition execute_STX ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
  (* M = X *)
  opt_map ?? (get_indX_8_low_reg m t s)
-  (λX_op.opt_map ?? (multi_mode_write m t true s cur_pc i X_op)
+  (λX_op.opt_map ?? (multi_mode_write true m t s cur_pc i X_op)
    (λS_op_and_PC.match S_op_and_PC with
     [ pair s_tmp1 new_pc ⇒
      (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
@@ -1085,7 +1085,7 @@ definition execute_TPA ≝
    e' immediata *)
 definition execute_TST ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
   (λS_M_PC.match S_M_PC with
    [ tripleT s_tmp1 M_op new_pc ⇒
     (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)