X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Fstatus%2Fstatus_setter.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Fstatus%2Fstatus_setter.ma;h=3a25c0f381bdad3d9800f4dce92cf00c102c76ad;hb=2c38e6a237e6a0e263abccf8d8ef3e7a31272443;hp=e28410878155af6677e758afb3766818f11c99ac;hpb=221472ea1597505d12677f5742e388125a15e2b9;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/status_setter.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/status_setter.ma
index e28410878..3a25c0f38 100755
--- a/helm/software/matita/contribs/ng_assembly/emulator/status/status_setter.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/status/status_setter.ma
@@ -69,7 +69,7 @@ ndefinition set_clk_desc ≝
 
 (* setter forte di A *)
 ndefinition set_acc_8_low_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λacclow':byte8.
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval:byte8.
  set_alu m t s 
  (match m return aux_set_type byte8 with
   [ HC05 ⇒ set_acc_8_low_reg_HC05
@@ -77,82 +77,134 @@ ndefinition set_acc_8_low_reg ≝
   | HCS08 ⇒ set_acc_8_low_reg_HC08
   | RS08 ⇒ set_acc_8_low_reg_RS08
   | IP2022 ⇒ set_acc_8_low_reg_IP2022
-  ] (alu m t s) acclow').
+  ] (alu m t s) val).
 
 (* REGISTRO X *)
 
+ndefinition set_indX_8_low_reg_sHC05 ≝
+λt:memory_impl.λs:any_status HC05 t.λval.
+ set_alu … s (set_indX_8_low_reg_HC05 (alu … s) val).
+
+ndefinition set_indX_8_low_reg_sHC08 ≝
+λt:memory_impl.λs:any_status HC08 t.λval.
+ set_alu … s (set_indX_8_low_reg_HC08 (alu … s) val).
+
+ndefinition set_indX_8_low_reg_sHCS08 ≝
+λt:memory_impl.λs:any_status HCS08 t.λval.
+ set_alu … s (set_indX_8_low_reg_HC08 (alu … s) val).
+
 (* setter forte di X *)
 ndefinition set_indX_8_low_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
- opt_map … (match m return aux_set_type_opt byte8 with
-             [ HC05 ⇒ Some ? set_indX_8_low_reg_HC05
-             | HC08 ⇒ Some ? set_indX_8_low_reg_HC08
-             | HCS08 ⇒ Some ? set_indX_8_low_reg_HC08
-             | RS08 ⇒ None ?
-             | IP2022 ⇒ None ? ])
- (λf.Some ? (set_alu m t s (f (alu m t s) indxlow'))).
+λm:mcu_type.λt.
+ match m
+  return λm.any_status m t → byte8 → option (any_status m t)
+ with
+  [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_indX_8_low_reg_sHC05 t s val)
+  | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_8_low_reg_sHC08 t s val)
+  | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_8_low_reg_sHCS08 t s val)
+  | RS08 ⇒ λs:any_status ? t.λval.None ?
+  | IP2022 ⇒ λs:any_status ? t.λval.None ?
+  ].
 
 (* setter debole di X *)
 ndefinition setweak_indX_8_low_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
- match set_indX_8_low_reg m t s indxlow' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_indX_8_low_reg m t s val with
   [ None ⇒ s | Some s' ⇒ s' ].
 
 (* REGISTRO H *)
 
+ndefinition set_indX_8_high_reg_sHC08 ≝
+λt:memory_impl.λs:any_status HC08 t.λval.
+ set_alu … s (set_indX_8_high_reg_HC08 (alu … s) val).
+
+ndefinition set_indX_8_high_reg_sHCS08 ≝
+λt:memory_impl.λs:any_status HCS08 t.λval.
+ set_alu … s (set_indX_8_high_reg_HC08 (alu … s) val).
+
 (* setter forte di H *)
 ndefinition set_indX_8_high_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
- opt_map … (match m return aux_set_type_opt byte8 with
-             [ HC05 ⇒ None ?
-             | HC08 ⇒ Some ? set_indX_8_high_reg_HC08
-             | HCS08 ⇒ Some ? set_indX_8_high_reg_HC08
-             | RS08 ⇒ None ?
-             | IP2022 ⇒ None ? ])
- (λf.Some ? (set_alu m t s (f (alu m t s) indxhigh'))).
+λm:mcu_type.λt.
+ match m
+  return λm.any_status m t → byte8 → option (any_status m t)
+ with
+  [ HC05 ⇒ λs:any_status ? t.λval.None ?
+  | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_8_high_reg_sHC08 t s val)
+  | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_8_high_reg_sHCS08 t s val)
+  | RS08 ⇒ λs:any_status ? t.λval.None ?
+  | IP2022 ⇒ λs:any_status ? t.λval.None ?
+  ].
 
 (* setter debole di H *)
 ndefinition setweak_indX_8_high_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
- match set_indX_8_high_reg m t s indxhigh' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_indX_8_high_reg m t s val with
   [ None ⇒ s | Some s' ⇒ s' ].
 
 (* REGISTRO H:X *)
 
+ndefinition set_indX_16_reg_sHC08 ≝
+λt:memory_impl.λs:any_status HC08 t.λval.
+ set_alu … s (set_indX_16_reg_HC08 (alu … s) val).
+
+ndefinition set_indX_16_reg_sHCS08 ≝
+λt:memory_impl.λs:any_status HCS08 t.λval.
+ set_alu … s (set_indX_16_reg_HC08 (alu … s) val).
+
 (* setter forte di H:X *)
 ndefinition set_indX_16_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
- opt_map … (match m return aux_set_type_opt word16 with
-             [ HC05 ⇒ None ?
-             | HC08 ⇒ Some ? set_indX_16_reg_HC08
-             | HCS08 ⇒ Some ? set_indX_16_reg_HC08
-             | RS08 ⇒ None ?
-             | IP2022 ⇒ None ? ])
- (λf.Some ? (set_alu m t s (f (alu m t s) indx16))).
+λm:mcu_type.λt.
+ match m
+  return λm.any_status m t → word16 → option (any_status m t)
+ with
+  [ HC05 ⇒ λs:any_status ? t.λval.None ?
+  | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_16_reg_sHC08 t s val)
+  | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_16_reg_sHCS08 t s val)
+  | RS08 ⇒ λs:any_status ? t.λval.None ?
+  | IP2022 ⇒ λs:any_status ? t.λval.None ?
+  ].
 
 (* setter debole di H:X *)
 ndefinition setweak_indX_16_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
- match set_indX_16_reg m t s indx16 with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_indX_16_reg m t s val with
   [ None ⇒ s | Some s' ⇒ s' ].
 
 (* REGISTRO SP *)
 
+ndefinition set_sp_reg_sHC05 ≝
+λt:memory_impl.λs:any_status HC05 t.λval.
+ set_alu … s (set_sp_reg_HC05 (alu … s) val).
+
+ndefinition set_sp_reg_sHC08 ≝
+λt:memory_impl.λs:any_status HC08 t.λval.
+ set_alu … s (set_sp_reg_HC08 (alu … s) val).
+
+ndefinition set_sp_reg_sHCS08 ≝
+λt:memory_impl.λs:any_status HCS08 t.λval.
+ set_alu … s (set_sp_reg_HC08 (alu … s) val).
+
+ndefinition set_sp_reg_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.λval.
+ set_alu … s (set_sp_reg_IP2022 (alu … s) val).
+
 (* setter forte di SP *)
 ndefinition set_sp_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
- opt_map … (match m return aux_set_type_opt word16 with
-             [ HC05 ⇒ Some ? set_sp_reg_HC05
-             | HC08 ⇒ Some ? set_sp_reg_HC08
-             | HCS08 ⇒ Some ? set_sp_reg_HC08
-             | RS08 ⇒ None ?
-             | IP2022 ⇒ Some ? set_sp_reg_IP2022 ])
- (λf.Some ? (set_alu m t s (f (alu m t s) sp'))).
+λm:mcu_type.λt.
+ match m
+  return λm.any_status m t → word16 → option (any_status m t)
+ with
+  [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_sp_reg_sHC05 t s val)
+  | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_sp_reg_sHC08 t s val)
+  | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_sp_reg_sHCS08 t s val)
+  | RS08 ⇒ λs:any_status ? t.λval.None ?
+  | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_sp_reg_sIP2022 t s val)
+  ].
 
 (* setter debole di SP *)
 ndefinition setweak_sp_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
- match set_sp_reg m t s sp' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_sp_reg m t s val with
   [ None ⇒ s | Some s' ⇒ s' ].
 
 (* REGISTRO PC *)
@@ -171,351 +223,498 @@ ndefinition set_pc_reg ≝
 
 (* REGISTRO SPC *)
 
+ndefinition set_spc_reg_sRS08 ≝
+λt:memory_impl.λs:any_status RS08 t.λval.
+ set_alu … s (set_spc_reg_RS08 (alu … s) val).
+
 (* setter forte di SPC *)
 ndefinition set_spc_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
- opt_map … (match m return aux_set_type_opt word16 with
-             [ HC05 ⇒ None ?
-             | HC08 ⇒ None ?
-             | HCS08 ⇒ None ?
-             | RS08 ⇒ Some ? set_spc_reg_RS08
-             | IP2022 ⇒ None ? ])
- (λf.Some ? (set_alu m t s (f (alu m t s) spc'))).
+λm:mcu_type.λt.
+ match m
+  return λm.any_status m t → word16 → option (any_status m t)
+ with
+  [ HC05 ⇒ λs:any_status ? t.λval.None ?
+  | HC08 ⇒ λs:any_status ? t.λval.None ?
+  | HCS08 ⇒ λs:any_status ? t.λval.None ?
+  | RS08 ⇒ λs:any_status ? t.λval.Some ? (set_spc_reg_sRS08 t s val)
+  | IP2022 ⇒ λs:any_status ? t.λval.None ?
+  ].
 
 (* setter debole di SPC *)
 ndefinition setweak_spc_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
- match set_spc_reg m t s spc' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_spc_reg m t s val with
   [ None ⇒ s | Some s' ⇒ s' ].
 
 (* REGISTRO MULH *)
 
+ndefinition set_mulh_reg_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.λval.
+ set_alu … s (set_mulh_reg_IP2022 (alu … s) val).
+
 (* setter forte di MULH *)
 ndefinition set_mulh_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λmulh':byte8.
- opt_map … (match m return aux_set_type_opt byte8 with
-             [ HC05 ⇒ None ?
-             | HC08 ⇒ None ?
-             | HCS08 ⇒ None ?
-             | RS08 ⇒ None ?
-             | IP2022 ⇒ Some ? set_mulh_reg_IP2022 ])
- (λf.Some ? (set_alu m t s (f (alu m t s) mulh'))).
+λm:mcu_type.λt.
+ match m
+  return λm.any_status m t → byte8 → option (any_status m t)
+ with
+  [ HC05 ⇒ λs:any_status ? t.λval.None ?
+  | HC08 ⇒ λs:any_status ? t.λval.None ?
+  | HCS08 ⇒ λs:any_status ? t.λval.None ?
+  | RS08 ⇒ λs:any_status ? t.λval.None ?
+  | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_mulh_reg_sIP2022 t s val)
+  ].
 
 (* setter debole di MULH *)
 ndefinition setweak_mulh_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λmulh':byte8.
- match set_mulh_reg m t s mulh' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_mulh_reg m t s val with
   [ None ⇒ s | Some s' ⇒ s' ].
 
 (* REGISTRO ADDRSEL *)
 
+ndefinition set_addrsel_reg_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.λval.
+ set_alu … s (set_addrsel_reg_IP2022 (alu … s) val).
+
 (* setter forte di ADDRSEL *)
 ndefinition set_addrsel_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddrsel':byte8.
- opt_map … (match m return aux_set_type_opt byte8 with
-             [ HC05 ⇒ None ?
-             | HC08 ⇒ None ?
-             | HCS08 ⇒ None ?
-             | RS08 ⇒ None ?
-             | IP2022 ⇒ Some ? set_addrsel_reg_IP2022 ])
- (λf.Some ? (set_alu m t s (f (alu m t s) addrsel'))).
+λm:mcu_type.λt.
+ match m
+  return λm.any_status m t → byte8 → option (any_status m t)
+ with
+  [ HC05 ⇒ λs:any_status ? t.λval.None ?
+  | HC08 ⇒ λs:any_status ? t.λval.None ?
+  | HCS08 ⇒ λs:any_status ? t.λval.None ?
+  | RS08 ⇒ λs:any_status ? t.λval.None ?
+  | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_addrsel_reg_sIP2022 t s val)
+  ].
 
 (* setter debole di ADDRSEL *)
 ndefinition setweak_addrsel_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddrsel':byte8.
- match set_addrsel_reg m t s addrsel' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_addrsel_reg m t s val with
   [ None ⇒ s | Some s' ⇒ s' ].
 
 (* REGISTRO ADDR *)
 
+ndefinition set_addr_reg_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.λval.
+ set_alu … s (set_addr_reg_IP2022 (alu … s) val).
+
 (* setter forte di ADDR *)
 ndefinition set_addr_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr':word24.
- opt_map … (match m return aux_set_type_opt word24 with
-             [ HC05 ⇒ None ?
-             | HC08 ⇒ None ?
-             | HCS08 ⇒ None ?
-             | RS08 ⇒ None ?
-             | IP2022 ⇒ Some ? set_addr_reg_IP2022 ])
- (λf.Some ? (set_alu m t s (f (alu m t s) addr'))).
+λm:mcu_type.λt.
+ match m
+  return λm.any_status m t → word24 → option (any_status m t)
+ with
+  [ HC05 ⇒ λs:any_status ? t.λval.None ?
+  | HC08 ⇒ λs:any_status ? t.λval.None ?
+  | HCS08 ⇒ λs:any_status ? t.λval.None ?
+  | RS08 ⇒ λs:any_status ? t.λval.None ?
+  | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_addr_reg_sIP2022 t s val)
+  ].
 
 (* setter debole di ADDR *)
 ndefinition setweak_addr_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr':word24.
- match set_addr_reg m t s addr' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_addr_reg m t s val with
   [ None ⇒ s | Some s' ⇒ s' ].
 
 (* REGISTRO CALL *)
 
+ndefinition set_call_reg_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.λval.
+ set_alu … s (set_call_reg_IP2022 (alu … s) val).
+
 (* setter forte di CALL *)
 ndefinition set_call_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λcall':word16.
- opt_map … (match m return aux_set_type_opt word16 with
-             [ HC05 ⇒ None ?
-             | HC08 ⇒ None ?
-             | HCS08 ⇒ None ?
-             | RS08 ⇒ None ?
-             | IP2022 ⇒ Some ? set_call_reg_IP2022 ])
- (λf.Some ? (set_alu m t s (f (alu m t s) call'))).
+λm:mcu_type.λt.
+ match m
+  return λm.any_status m t → word16 → option (any_status m t)
+ with
+  [ HC05 ⇒ λs:any_status ? t.λval.None ?
+  | HC08 ⇒ λs:any_status ? t.λval.None ?
+  | HCS08 ⇒ λs:any_status ? t.λval.None ?
+  | RS08 ⇒ λs:any_status ? t.λval.None ?
+  | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_call_reg_sIP2022 t s val)
+  ].
 
 (* setter debole di CALL *)
 ndefinition setweak_call_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λcall':word16.
- match set_call_reg m t s call' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_call_reg m t s val with
   [ None ⇒ s | Some s' ⇒ s' ].
 
+(* REGISTRO CALL [push] *)
+
+ndefinition push_call_reg_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.λval.
+ set_alu … s (push_call_reg_IP2022 (alu … s) val).
+
 (* push forte di CALL *)
 ndefinition push_call_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λcall':word16.
- opt_map … (match m return aux_set_type_opt word16 with
-             [ HC05 ⇒ None ?
-             | HC08 ⇒ None ?
-             | HCS08 ⇒ None ?
-             | RS08 ⇒ None ?
-             | IP2022 ⇒ Some ? push_call_reg_IP2022 ])
- (λf.Some ? (set_alu m t s (f (alu m t s) call'))).
+λm:mcu_type.λt.
+ match m
+  return λm.any_status m t → word16 → option (any_status m t)
+ with
+  [ HC05 ⇒ λs:any_status ? t.λval.None ?
+  | HC08 ⇒ λs:any_status ? t.λval.None ?
+  | HCS08 ⇒ λs:any_status ? t.λval.None ?
+  | RS08 ⇒ λs:any_status ? t.λval.None ?
+  | IP2022 ⇒ λs:any_status ? t.λval.Some ? (push_call_reg_sIP2022 t s val)
+  ].
+
+(* REGISTRO CALL [pop] *)
+
+ndefinition pop_call_reg_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.
+ match pop_call_reg_IP2022 (alu … s) with
+  [ pair val alu' ⇒ pair … val (set_alu … s alu') ].
 
 (* pop forte di CALL *)
 ndefinition pop_call_reg ≝
-λm:mcu_type.
+λm:mcu_type.λt.
  match m
-  return λm.Πt.any_status m t → option (ProdT word16 (any_status m t))
+  return λm.any_status m t → option (ProdT word16 (any_status m t))
  with
-  [ HC05 ⇒ λt:memory_impl.λs:any_status HC05 t.None ?
-  | HC08 ⇒ λt:memory_impl.λs:any_status HC08 t.None ?
-  | HCS08 ⇒ λt:memory_impl.λs:any_status HCS08 t.None ?
-  | RS08 ⇒ λt:memory_impl.λs:any_status RS08 t.None ?
-  | IP2022 ⇒ λt:memory_impl.λs:any_status IP2022 t.
-   match pop_call_reg_IP2022 (alu … s) with
-    [ pair val alu' ⇒ Some ? (pair … val (set_alu … s alu')) ]
+  [ HC05 ⇒ λs:any_status ? t.None ?
+  | HC08 ⇒ λs:any_status ? t.None ?
+  | HCS08 ⇒ λs:any_status ? t.None ?
+  | RS08 ⇒ λs:any_status ? t.None ?
+  | IP2022 ⇒ λs:any_status ? t.Some ? (pop_call_reg_sIP2022 t s)
   ].
 
 (* REGISTRO IP *)
 
+ndefinition set_ip_reg_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.λval.
+ set_alu … s (set_ip_reg_IP2022 (alu … s) val).
+
 (* setter forte di IP *)
 ndefinition set_ip_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λip':word16.
- opt_map … (match m return aux_set_type_opt word16 with
-             [ HC05 ⇒ None ?
-             | HC08 ⇒ None ?
-             | HCS08 ⇒ None ?
-             | RS08 ⇒ None ?
-             | IP2022 ⇒ Some ? set_ip_reg_IP2022 ])
- (λf.Some ? (set_alu m t s (f (alu m t s) ip'))).
+λm:mcu_type.λt.
+ match m
+  return λm.any_status m t → word16 → option (any_status m t)
+ with
+  [ HC05 ⇒ λs:any_status ? t.λval.None ?
+  | HC08 ⇒ λs:any_status ? t.λval.None ?
+  | HCS08 ⇒ λs:any_status ? t.λval.None ?
+  | RS08 ⇒ λs:any_status ? t.λval.None ?
+  | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_ip_reg_sIP2022 t s val)
+  ].
 
 (* setter debole di IP *)
 ndefinition setweak_ip_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λip':word16.
- match set_ip_reg m t s ip' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_ip_reg m t s val with
   [ None ⇒ s | Some s' ⇒ s' ].
 
 (* REGISTRO DP *)
 
+ndefinition set_dp_reg_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.λval.
+ set_alu … s (set_dp_reg_IP2022 (alu … s) val).
+
 (* setter forte di DP *)
 ndefinition set_dp_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λdp':word16.
- opt_map … (match m return aux_set_type_opt word16 with
-             [ HC05 ⇒ None ?
-             | HC08 ⇒ None ?
-             | HCS08 ⇒ None ?
-             | RS08 ⇒ None ?
-             | IP2022 ⇒ Some ? set_dp_reg_IP2022 ])
- (λf.Some ? (set_alu m t s (f (alu m t s) dp'))).
+λm:mcu_type.λt.
+ match m
+  return λm.any_status m t → word16 → option (any_status m t)
+ with
+  [ HC05 ⇒ λs:any_status ? t.λval.None ?
+  | HC08 ⇒ λs:any_status ? t.λval.None ?
+  | HCS08 ⇒ λs:any_status ? t.λval.None ?
+  | RS08 ⇒ λs:any_status ? t.λval.None ?
+  | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_dp_reg_sIP2022 t s val)
+  ].
 
 (* setter debole di DP *)
 ndefinition setweak_dp_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λdp':word16.
- match set_dp_reg m t s dp' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_dp_reg m t s val with
   [ None ⇒ s | Some s' ⇒ s' ].
 
 (* REGISTRO DATA *)
 
+ndefinition set_data_reg_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.λval.
+ set_alu … s (set_data_reg_IP2022 (alu … s) val).
+
 (* setter forte di DATA *)
 ndefinition set_data_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λdata':word16.
- opt_map … (match m return aux_set_type_opt word16 with
-             [ HC05 ⇒ None ?
-             | HC08 ⇒ None ?
-             | HCS08 ⇒ None ?
-             | RS08 ⇒ None ?
-             | IP2022 ⇒ Some ? set_data_reg_IP2022 ])
- (λf.Some ? (set_alu m t s (f (alu m t s) data'))).
+λm:mcu_type.λt.
+ match m
+  return λm.any_status m t → word16 → option (any_status m t)
+ with
+  [ HC05 ⇒ λs:any_status ? t.λval.None ?
+  | HC08 ⇒ λs:any_status ? t.λval.None ?
+  | HCS08 ⇒ λs:any_status ? t.λval.None ?
+  | RS08 ⇒ λs:any_status ? t.λval.None ?
+  | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_data_reg_sIP2022 t s val)
+  ].
 
 (* setter debole di DATA *)
 ndefinition setweak_data_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λdata':word16.
- match set_data_reg m t s data' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_data_reg m t s val with
   [ None ⇒ s | Some s' ⇒ s' ].
 
 (* REGISTRO SPEED *)
 
+ndefinition set_speed_reg_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.λval.
+ set_alu … s (set_speed_reg_IP2022 (alu … s) val).
+
 (* setter forte di SPEED *)
 ndefinition set_speed_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λspeed':exadecim.
- opt_map … (match m return aux_set_type_opt exadecim with
-             [ HC05 ⇒ None ?
-             | HC08 ⇒ None ?
-             | HCS08 ⇒ None ?
-             | RS08 ⇒ None ?
-             | IP2022 ⇒ Some ? set_speed_reg_IP2022 ])
- (λf.Some ? (set_alu m t s (f (alu m t s) speed'))).
+λm:mcu_type.λt.
+ match m
+  return λm.any_status m t → exadecim → option (any_status m t)
+ with
+  [ HC05 ⇒ λs:any_status ? t.λval.None ?
+  | HC08 ⇒ λs:any_status ? t.λval.None ?
+  | HCS08 ⇒ λs:any_status ? t.λval.None ?
+  | RS08 ⇒ λs:any_status ? t.λval.None ?
+  | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_speed_reg_sIP2022 t s val)
+  ].
 
 (* setter debole di SPEED *)
 ndefinition setweak_speed_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λspeed':exadecim.
- match set_speed_reg m t s speed' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_speed_reg m t s val with
   [ None ⇒ s | Some s' ⇒ s' ].
 
 (* REGISTRO PAGE *)
 
+ndefinition set_page_reg_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.λval.
+ set_alu … s (set_page_reg_IP2022 (alu … s) val).
+
 (* setter forte di PAGE *)
 ndefinition set_page_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λpage':oct.
- opt_map … (match m return aux_set_type_opt oct with
-             [ HC05 ⇒ None ?
-             | HC08 ⇒ None ?
-             | HCS08 ⇒ None ?
-             | RS08 ⇒ None ?
-             | IP2022 ⇒ Some ? set_page_reg_IP2022 ])
- (λf.Some ? (set_alu m t s (f (alu m t s) page'))).
+λm:mcu_type.λt.
+ match m
+  return λm.any_status m t → oct → option (any_status m t)
+ with
+  [ HC05 ⇒ λs:any_status ? t.λval.None ?
+  | HC08 ⇒ λs:any_status ? t.λval.None ?
+  | HCS08 ⇒ λs:any_status ? t.λval.None ?
+  | RS08 ⇒ λs:any_status ? t.λval.None ?
+  | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_page_reg_sIP2022 t s val)
+  ].
 
 (* setter debole di PAGE *)
 ndefinition setweak_page_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λpage':oct.
- match set_page_reg m t s page' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_page_reg m t s val with
   [ None ⇒ s | Some s' ⇒ s' ].
 
 (* REGISTRO MEMORY MAPPED X *)
 
+ndefinition set_x_map_sRS08 ≝
+λt:memory_impl.λs:any_status RS08 t.λval.
+ set_alu … s (set_x_map_RS08 (alu … s) val).
+
 (* setter forte di memory mapped X *)
 ndefinition set_x_map ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
- opt_map … (match m return aux_set_type_opt byte8 with
-             [ HC05 ⇒ None ?
-             | HC08 ⇒ None ?
-             | HCS08 ⇒ None ?
-             | RS08 ⇒ Some ? set_x_map_RS08
-             | IP2022 ⇒ None ? ])
- (λf.Some ? (set_alu m t s (f (alu m t s) xm'))).
+λm:mcu_type.λt.
+ match m
+  return λm.any_status m t → byte8 → option (any_status m t)
+ with
+  [ HC05 ⇒ λs:any_status ? t.λval.None ?
+  | HC08 ⇒ λs:any_status ? t.λval.None ?
+  | HCS08 ⇒ λs:any_status ? t.λval.None ?
+  | RS08 ⇒ λs:any_status ? t.λval.Some ? (set_x_map_sRS08 t s val)
+  | IP2022 ⇒ λs:any_status ? t.λval.None ?
+  ].
 
 (* setter debole di memory mapped X *)
 ndefinition setweak_x_map ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
- match set_x_map m t s xm' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_x_map m t s val with
   [ None ⇒ s | Some s' ⇒ s' ].
 
 (* REGISTRO MEMORY MAPPED PS *)
 
+ndefinition set_ps_map_sRS08 ≝
+λt:memory_impl.λs:any_status RS08 t.λval.
+ set_alu … s (set_ps_map_RS08 (alu … s) val).
+
 (* setter forte di memory mapped PS *)
 ndefinition set_ps_map ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
- opt_map … (match m return aux_set_type_opt byte8 with
-             [ HC05 ⇒ None ?
-             | HC08 ⇒ None ?
-             | HCS08 ⇒ None ?
-             | RS08 ⇒ Some ? set_ps_map_RS08
-             | IP2022 ⇒ None ? ])
- (λf.Some ? (set_alu m t s (f (alu m t s) psm'))).
+λm:mcu_type.λt.
+ match m
+  return λm.any_status m t → byte8 → option (any_status m t)
+ with
+  [ HC05 ⇒ λs:any_status ? t.λval.None ?
+  | HC08 ⇒ λs:any_status ? t.λval.None ?
+  | HCS08 ⇒ λs:any_status ? t.λval.None ?
+  | RS08 ⇒ λs:any_status ? t.λval.Some ? (set_ps_map_sRS08 t s val)
+  | IP2022 ⇒ λs:any_status ? t.λval.None ?
+  ].
 
 (* setter debole di memory mapped PS *)
 ndefinition setweak_ps_map ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
- match set_ps_map m t s psm' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_ps_map m t s val with
   [ None ⇒ s | Some s' ⇒ s' ].
 
 (* MODALITA SKIP *)
 
-(* setter forte di SKIP *)
+ndefinition set_skip_mode_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.λval.
+ set_alu … s (set_skip_mode_IP2022 (alu … s) val).
+
+(* setter forte di modalita SKIP *)
 ndefinition set_skip_mode ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λskipmode':bool.
- opt_map … (match m return aux_set_type_opt bool with
-             [ HC05 ⇒ None ?
-             | HC08 ⇒ None ?
-             | HCS08 ⇒ None ?
-             | RS08 ⇒ None ?
-             | IP2022 ⇒ Some ? set_skip_mode_IP2022 ])
- (λf.Some ? (set_alu m t s (f (alu m t s) skipmode'))).
+λm:mcu_type.λt.
+ match m
+  return λm.any_status m t → bool → option (any_status m t)
+ with
+  [ HC05 ⇒ λs:any_status ? t.λval.None ?
+  | HC08 ⇒ λs:any_status ? t.λval.None ?
+  | HCS08 ⇒ λs:any_status ? t.λval.None ?
+  | RS08 ⇒ λs:any_status ? t.λval.None ?
+  | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_skip_mode_sIP2022 t s val)
+  ].
 
 (* setter debole  di SKIP *)
 ndefinition setweak_skip_mode ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λskipmode':bool.
- match set_skip_mode m t s skipmode' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_skip_mode m t s val with
   [ None ⇒ s | Some s' ⇒ s' ].
 
 (* FLAG V *)
 
+ndefinition set_v_flag_sHC08 ≝
+λt:memory_impl.λs:any_status HC08 t.λval.
+ set_alu … s (set_v_flag_HC08 (alu … s) val).
+
+ndefinition set_v_flag_sHCS08 ≝
+λt:memory_impl.λs:any_status HCS08 t.λval.
+ set_alu … s (set_v_flag_HC08 (alu … s) val).
+
 (* setter forte di V *)
 ndefinition set_v_flag ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
- opt_map … (match m return aux_set_type_opt bool with
-             [ HC05 ⇒ None ?
-             | HC08 ⇒ Some ? set_v_flag_HC08
-             | HCS08 ⇒ Some ? set_v_flag_HC08
-             | RS08 ⇒ None ?
-             | IP2022 ⇒ None ? ])
- (λf.Some ? (set_alu m t s (f (alu m t s) vfl'))).
+λm:mcu_type.λt.
+ match m
+  return λm.any_status m t → bool → option (any_status m t)
+ with
+  [ HC05 ⇒ λs:any_status ? t.λval.None ?
+  | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_v_flag_sHC08 t s val)
+  | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_v_flag_sHCS08 t s val)
+  | RS08 ⇒ λs:any_status ? t.λval.None ?
+  | IP2022 ⇒ λs:any_status ? t.λval.None ?
+  ].
 
 (* setter debole  di V *)
 ndefinition setweak_v_flag ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
- match set_v_flag m t s vfl' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_v_flag m t s val with
   [ None ⇒ s | Some s' ⇒ s' ].
 
 (* FLAG H *)
 
+ndefinition set_h_flag_sHC05 ≝
+λt:memory_impl.λs:any_status HC05 t.λval.
+ set_alu … s (set_h_flag_HC05 (alu … s) val).
+
+ndefinition set_h_flag_sHC08 ≝
+λt:memory_impl.λs:any_status HC08 t.λval.
+ set_alu … s (set_h_flag_HC08 (alu … s) val).
+
+ndefinition set_h_flag_sHCS08 ≝
+λt:memory_impl.λs:any_status HCS08 t.λval.
+ set_alu … s (set_h_flag_HC08 (alu … s) val).
+
+ndefinition set_h_flag_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.λval.
+ set_alu … s (set_h_flag_IP2022 (alu … s) val).
+
 (* setter forte di H *)
 ndefinition set_h_flag ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
- opt_map … (match m return aux_set_type_opt bool with
-             [ HC05 ⇒ Some ? set_h_flag_HC05
-             | HC08 ⇒ Some ? set_h_flag_HC08
-             | HCS08 ⇒ Some ? set_h_flag_HC08
-             | RS08 ⇒ None ?
-             | IP2022 ⇒ Some ? set_h_flag_IP2022 ])
- (λf.Some ? (set_alu m t s (f (alu m t s) hfl'))).
+λm:mcu_type.λt.
+ match m
+  return λm.any_status m t → bool → option (any_status m t)
+ with
+  [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_h_flag_sHC05 t s val)
+  | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_h_flag_sHC08 t s val)
+  | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_h_flag_sHCS08 t s val)
+  | RS08 ⇒ λs:any_status ? t.λval.None ?
+  | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_h_flag_sIP2022 t s val)
+  ].
 
 (* setter debole di H *)
 ndefinition setweak_h_flag ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
- match set_h_flag m t s hfl' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_h_flag m t s val with
   [ None ⇒ s | Some s' ⇒ s' ].
 
 (* FLAG I *)
 
+ndefinition set_i_flag_sHC05 ≝
+λt:memory_impl.λs:any_status HC05 t.λval.
+ set_alu … s (set_i_flag_HC05 (alu … s) val).
+
+ndefinition set_i_flag_sHC08 ≝
+λt:memory_impl.λs:any_status HC08 t.λval.
+ set_alu … s (set_i_flag_HC08 (alu … s) val).
+
+ndefinition set_i_flag_sHCS08 ≝
+λt:memory_impl.λs:any_status HCS08 t.λval.
+ set_alu … s (set_i_flag_HC08 (alu … s) val).
+
 (* setter forte di I *)
 ndefinition set_i_flag ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
- opt_map … (match m return aux_set_type_opt bool with
-             [ HC05 ⇒ Some ? set_i_flag_HC05
-             | HC08 ⇒ Some ? set_i_flag_HC08
-             | HCS08 ⇒ Some ? set_i_flag_HC08
-             | RS08 ⇒ None ?
-             | IP2022 ⇒ None ? ])
- (λf.Some ? (set_alu m t s (f (alu m t s) ifl'))).
+λm:mcu_type.λt.
+ match m
+  return λm.any_status m t → bool → option (any_status m t)
+ with
+  [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_i_flag_sHC05 t s val)
+  | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_i_flag_sHC08 t s val)
+  | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_i_flag_sHCS08 t s val)
+  | RS08 ⇒ λs:any_status ? t.λval.None ?
+  | IP2022 ⇒ λs:any_status ? t.λval.None ?
+  ].
 
 (* setter debole di I *)
 ndefinition setweak_i_flag ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
- match set_i_flag m t s ifl' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_i_flag m t s val with
   [ None ⇒ s | Some s' ⇒ s' ].
 
 (* FLAG N *)
 
+ndefinition set_n_flag_sHC05 ≝
+λt:memory_impl.λs:any_status HC05 t.λval.
+ set_alu … s (set_n_flag_HC05 (alu … s) val).
+
+ndefinition set_n_flag_sHC08 ≝
+λt:memory_impl.λs:any_status HC08 t.λval.
+ set_alu … s (set_n_flag_HC08 (alu … s) val).
+
+ndefinition set_n_flag_sHCS08 ≝
+λt:memory_impl.λs:any_status HCS08 t.λval.
+ set_alu … s (set_n_flag_HC08 (alu … s) val).
+
 (* setter forte di N *)
 ndefinition set_n_flag ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
- opt_map … (match m return aux_set_type_opt bool with
-             [ HC05 ⇒ Some ? set_n_flag_HC05
-             | HC08 ⇒ Some ? set_n_flag_HC08
-             | HCS08 ⇒ Some ? set_n_flag_HC08
-             | RS08 ⇒ None ?
-             | IP2022 ⇒ None ? ])
- (λf.Some ? (set_alu m t s (f (alu m t s) nfl'))).
+λm:mcu_type.λt.
+ match m
+  return λm.any_status m t → bool → option (any_status m t)
+ with
+  [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_n_flag_sHC05 t s val)
+  | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_n_flag_sHC08 t s val)
+  | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_n_flag_sHCS08 t s val)
+  | RS08 ⇒ λs:any_status ? t.λval.None ?
+  | IP2022 ⇒ λs:any_status ? t.λval.None ?
+  ].
 
 (* setter debole di N *)
 ndefinition setweak_n_flag ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
- match set_n_flag m t s nfl' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_n_flag m t s val with
   [ None ⇒ s | Some s' ⇒ s' ].
 
 (* FLAG Z *)
@@ -548,19 +747,33 @@ ndefinition set_c_flag ≝
 
 (* FLAG IRQ *)
 
+ndefinition set_irq_flag_sHC05 ≝
+λt:memory_impl.λs:any_status HC05 t.λval.
+ set_alu … s (set_irq_flag_HC05 (alu … s) val).
+
+ndefinition set_irq_flag_sHC08 ≝
+λt:memory_impl.λs:any_status HC08 t.λval.
+ set_alu … s (set_irq_flag_HC08 (alu … s) val).
+
+ndefinition set_irq_flag_sHCS08 ≝
+λt:memory_impl.λs:any_status HCS08 t.λval.
+ set_alu … s (set_irq_flag_HC08 (alu … s) val).
+
 (* setter forte di IRQ *)
 ndefinition set_irq_flag ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
- opt_map … (match m return aux_set_type_opt bool with
-             [ HC05 ⇒ Some ? set_irq_flag_HC05
-             | HC08 ⇒ Some ? set_irq_flag_HC08
-             | HCS08 ⇒ Some ? set_irq_flag_HC08
-             | RS08 ⇒ None ?
-             | IP2022 ⇒ None ? ])
- (λf.Some ? (set_alu m t s (f (alu m t s) irqfl'))).
+λm:mcu_type.λt.
+ match m
+  return λm.any_status m t → bool → option (any_status m t)
+ with
+  [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_irq_flag_sHC05 t s val)
+  | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_irq_flag_sHC08 t s val)
+  | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_irq_flag_sHCS08 t s val)
+  | RS08 ⇒ λs:any_status ? t.λval.None ?
+  | IP2022 ⇒ λs:any_status ? t.λval.None ?
+  ].
 
 (* setter debole di IRQ *)
 ndefinition setweak_irq_flag ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
- match set_irq_flag m t s irqfl' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_irq_flag m t s val with
   [ None ⇒ s | Some s' ⇒ s' ].