helm/software/matita/contribs/ng_assembly/emulator/status/status_setter.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "emulator/status/status.ma".
  24
  25 (* ***************************** *)
  26 (* SETTER SPECIFICI FORTI/DEBOLI *)
  27 (* ***************************** *)
  28
  29 (* funzione ausiliaria per il tipaggio dei setter forti *)
  30 ndefinition aux_set_type ≝ λx:Type.λm:mcu_type.
  31   match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
  32                | IP2022 ⇒ alu_IP2022 ]
  33   → x →
  34   match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
  35                | IP2022 ⇒ alu_IP2022 ].
  36
  37 (* funzione ausiliaria per il tipaggio dei setter deboli *)
  38 ndefinition aux_set_type_opt ≝ λx:Type.λm:mcu_type.option
  39  (match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
  40                | IP2022 ⇒ alu_IP2022 ]
  41   → x →
  42   match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
  43                | IP2022 ⇒ alu_IP2022 ]).
  44
  45 (* DESCRITTORI ESTERNI ALLA ALU *)
  46
  47 (* setter forte della ALU *)
  48 ndefinition set_alu ≝
  49 λm:mcu_type.λt:memory_impl.λs:any_status m t.λalu'.
  50  mk_any_status m t alu' (mem_desc m t s) (chk_desc m t s) (clk_desc m t s).
  51
  52 (* setter forte della memoria *)
  53 ndefinition set_mem_desc ≝
  54 λm:mcu_type.λt:memory_impl.λs:any_status m t.λmem':aux_mem_type t.
  55  mk_any_status m t (alu m t s) mem' (chk_desc m t s) (clk_desc m t s).
  56
  57 (* setter forte del descrittore *)
  58 ndefinition set_chk_desc ≝
  59 λm:mcu_type.λt:memory_impl.λs:any_status m t.λchk':aux_chk_type t.
  60  mk_any_status m t (alu m t s) (mem_desc m t s) chk' (clk_desc m t s).
  61
  62 (* setter forte del clik *)
  63 ndefinition set_clk_desc ≝
  64 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  65 λclk':option (aux_clk_type m).
  66  mk_any_status m t (alu m t s) (mem_desc m t s) (chk_desc m t s) clk'.
  67
  68 (* REGISTRO A *)
  69
  70 (* setter forte di A *)
  71 ndefinition set_acc_8_low_reg ≝
  72 λm:mcu_type.λt:memory_impl.λs:any_status m t.λacclow':byte8.
  73  set_alu m t s
  74  (match m return aux_set_type byte8 with
  75   [ HC05 ⇒ set_acc_8_low_reg_HC05
  76   | HC08 ⇒ set_acc_8_low_reg_HC08
  77   | HCS08 ⇒ set_acc_8_low_reg_HC08
  78   | RS08 ⇒ set_acc_8_low_reg_RS08
  79   | IP2022 ⇒ set_acc_8_low_reg_IP2022
  80   ] (alu m t s) acclow').
  81
  82 (* REGISTRO X *)
  83
  84 (* setter forte di X *)
  85 ndefinition set_indX_8_low_reg ≝
  86 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
  87  opt_map … (match m return aux_set_type_opt byte8 with
  88              [ HC05 ⇒ Some ? set_indX_8_low_reg_HC05
  89              | HC08 ⇒ Some ? set_indX_8_low_reg_HC08
  90              | HCS08 ⇒ Some ? set_indX_8_low_reg_HC08
  91              | RS08 ⇒ None ?
  92              | IP2022 ⇒ None ? ])
  93  (λf.Some ? (set_alu m t s (f (alu m t s) indxlow'))).
  94
  95 (* setter debole di X *)
  96 ndefinition setweak_indX_8_low_reg ≝
  97 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
  98  match set_indX_8_low_reg m t s indxlow' with
  99   [ None ⇒ s | Some s' ⇒ s' ].
 100
 101 (* REGISTRO H *)
 102
 103 (* setter forte di H *)
 104 ndefinition set_indX_8_high_reg ≝
 105 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
 106  opt_map … (match m return aux_set_type_opt byte8 with
 107              [ HC05 ⇒ None ?
 108              | HC08 ⇒ Some ? set_indX_8_high_reg_HC08
 109              | HCS08 ⇒ Some ? set_indX_8_high_reg_HC08
 110              | RS08 ⇒ None ?
 111              | IP2022 ⇒ None ? ])
 112  (λf.Some ? (set_alu m t s (f (alu m t s) indxhigh'))).
 113
 114 (* setter debole di H *)
 115 ndefinition setweak_indX_8_high_reg ≝
 116 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
 117  match set_indX_8_high_reg m t s indxhigh' with
 118   [ None ⇒ s | Some s' ⇒ s' ].
 119
 120 (* REGISTRO H:X *)
 121
 122 (* setter forte di H:X *)
 123 ndefinition set_indX_16_reg ≝
 124 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
 125  opt_map … (match m return aux_set_type_opt word16 with
 126              [ HC05 ⇒ None ?
 127              | HC08 ⇒ Some ? set_indX_16_reg_HC08
 128              | HCS08 ⇒ Some ? set_indX_16_reg_HC08
 129              | RS08 ⇒ None ?
 130              | IP2022 ⇒ None ? ])
 131  (λf.Some ? (set_alu m t s (f (alu m t s) indx16))).
 132
 133 (* setter debole di H:X *)
 134 ndefinition setweak_indX_16_reg ≝
 135 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
 136  match set_indX_16_reg m t s indx16 with
 137   [ None ⇒ s | Some s' ⇒ s' ].
 138
 139 (* REGISTRO SP *)
 140
 141 (* setter forte di SP *)
 142 ndefinition set_sp_reg ≝
 143 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
 144  opt_map … (match m return aux_set_type_opt word16 with
 145              [ HC05 ⇒ Some ? set_sp_reg_HC05
 146              | HC08 ⇒ Some ? set_sp_reg_HC08
 147              | HCS08 ⇒ Some ? set_sp_reg_HC08
 148              | RS08 ⇒ None ?
 149              | IP2022 ⇒ Some ? set_sp_reg_IP2022 ])
 150  (λf.Some ? (set_alu m t s (f (alu m t s) sp'))).
 151
 152 (* setter debole di SP *)
 153 ndefinition setweak_sp_reg ≝
 154 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
 155  match set_sp_reg m t s sp' with
 156   [ None ⇒ s | Some s' ⇒ s' ].
 157
 158 (* REGISTRO PC *)
 159
 160 (* setter forte di PC *)
 161 ndefinition set_pc_reg ≝
 162 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpc':word16.
 163  set_alu m t s
 164  (match m return aux_set_type word16 with
 165   [ HC05 ⇒ set_pc_reg_HC05
 166   | HC08 ⇒ set_pc_reg_HC08
 167   | HCS08 ⇒ set_pc_reg_HC08
 168   | RS08 ⇒ set_pc_reg_RS08
 169   | IP2022 ⇒ set_pc_reg_IP2022
 170   ] (alu m t s) pc').
 171
 172 (* REGISTRO SPC *)
 173
 174 (* setter forte di SPC *)
 175 ndefinition set_spc_reg ≝
 176 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
 177  opt_map … (match m return aux_set_type_opt word16 with
 178              [ HC05 ⇒ None ?
 179              | HC08 ⇒ None ?
 180              | HCS08 ⇒ None ?
 181              | RS08 ⇒ Some ? set_spc_reg_RS08
 182              | IP2022 ⇒ None ? ])
 183  (λf.Some ? (set_alu m t s (f (alu m t s) spc'))).
 184
 185 (* setter debole di SPC *)
 186 ndefinition setweak_spc_reg ≝
 187 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
 188  match set_spc_reg m t s spc' with
 189   [ None ⇒ s | Some s' ⇒ s' ].
 190
 191 (* REGISTRO MULH *)
 192
 193 (* setter forte di MULH *)
 194 ndefinition set_mulh_reg ≝
 195 λm:mcu_type.λt:memory_impl.λs:any_status m t.λmulh':byte8.
 196  opt_map … (match m return aux_set_type_opt byte8 with
 197              [ HC05 ⇒ None ?
 198              | HC08 ⇒ None ?
 199              | HCS08 ⇒ None ?
 200              | RS08 ⇒ None ?
 201              | IP2022 ⇒ Some ? set_mulh_reg_IP2022 ])
 202  (λf.Some ? (set_alu m t s (f (alu m t s) mulh'))).
 203
 204 (* setter debole di MULH *)
 205 ndefinition setweak_mulh_reg ≝
 206 λm:mcu_type.λt:memory_impl.λs:any_status m t.λmulh':byte8.
 207  match set_mulh_reg m t s mulh' with
 208   [ None ⇒ s | Some s' ⇒ s' ].
 209
 210 (* REGISTRO ADDRSEL *)
 211
 212 (* setter forte di ADDRSEL *)
 213 ndefinition set_addrsel_reg ≝
 214 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddrsel':byte8.
 215  opt_map … (match m return aux_set_type_opt byte8 with
 216              [ HC05 ⇒ None ?
 217              | HC08 ⇒ None ?
 218              | HCS08 ⇒ None ?
 219              | RS08 ⇒ None ?
 220              | IP2022 ⇒ Some ? set_addrsel_reg_IP2022 ])
 221  (λf.Some ? (set_alu m t s (f (alu m t s) addrsel'))).
 222
 223 (* setter debole di ADDRSEL *)
 224 ndefinition setweak_addrsel_reg ≝
 225 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddrsel':byte8.
 226  match set_addrsel_reg m t s addrsel' with
 227   [ None ⇒ s | Some s' ⇒ s' ].
 228
 229 (* REGISTRO ADDR *)
 230
 231 (* setter forte di ADDR *)
 232 ndefinition set_addr_reg ≝
 233 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr':word24.
 234  opt_map … (match m return aux_set_type_opt word24 with
 235              [ HC05 ⇒ None ?
 236              | HC08 ⇒ None ?
 237              | HCS08 ⇒ None ?
 238              | RS08 ⇒ None ?
 239              | IP2022 ⇒ Some ? set_addr_reg_IP2022 ])
 240  (λf.Some ? (set_alu m t s (f (alu m t s) addr'))).
 241
 242 (* setter debole di ADDR *)
 243 ndefinition setweak_addr_reg ≝
 244 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr':word24.
 245  match set_addr_reg m t s addr' with
 246   [ None ⇒ s | Some s' ⇒ s' ].
 247
 248 (* REGISTRO CALL *)
 249
 250 (* setter forte di CALL *)
 251 ndefinition set_call_reg ≝
 252 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcall':word16.
 253  opt_map … (match m return aux_set_type_opt word16 with
 254              [ HC05 ⇒ None ?
 255              | HC08 ⇒ None ?
 256              | HCS08 ⇒ None ?
 257              | RS08 ⇒ None ?
 258              | IP2022 ⇒ Some ? set_call_reg_IP2022 ])
 259  (λf.Some ? (set_alu m t s (f (alu m t s) call'))).
 260
 261 (* setter debole di CALL *)
 262 ndefinition setweak_call_reg ≝
 263 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcall':word16.
 264  match set_call_reg m t s call' with
 265   [ None ⇒ s | Some s' ⇒ s' ].
 266
 267 (* push forte di CALL *)
 268 ndefinition push_call_reg ≝
 269 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcall':word16.
 270  opt_map … (match m return aux_set_type_opt word16 with
 271              [ HC05 ⇒ None ?
 272              | HC08 ⇒ None ?
 273              | HCS08 ⇒ None ?
 274              | RS08 ⇒ None ?
 275              | IP2022 ⇒ Some ? push_call_reg_IP2022 ])
 276  (λf.Some ? (set_alu m t s (f (alu m t s) call'))).
 277
 278 (* pop forte di CALL *)
 279 ndefinition pop_call_reg ≝
 280 λm:mcu_type.
 281  match m
 282   return λm.Πt.any_status m t → option (ProdT word16 (any_status m t))
 283  with
 284   [ HC05 ⇒ λt:memory_impl.λs:any_status HC05 t.None ?
 285   | HC08 ⇒ λt:memory_impl.λs:any_status HC08 t.None ?
 286   | HCS08 ⇒ λt:memory_impl.λs:any_status HCS08 t.None ?
 287   | RS08 ⇒ λt:memory_impl.λs:any_status RS08 t.None ?
 288   | IP2022 ⇒ λt:memory_impl.λs:any_status IP2022 t.
 289    match pop_call_reg_IP2022 (alu … s) with
 290     [ pair val alu' ⇒ Some ? (pair … val (set_alu … s alu')) ]
 291   ].
 292
 293 (* REGISTRO IP *)
 294
 295 (* setter forte di IP *)
 296 ndefinition set_ip_reg ≝
 297 λm:mcu_type.λt:memory_impl.λs:any_status m t.λip':word16.
 298  opt_map … (match m return aux_set_type_opt word16 with
 299              [ HC05 ⇒ None ?
 300              | HC08 ⇒ None ?
 301              | HCS08 ⇒ None ?
 302              | RS08 ⇒ None ?
 303              | IP2022 ⇒ Some ? set_ip_reg_IP2022 ])
 304  (λf.Some ? (set_alu m t s (f (alu m t s) ip'))).
 305
 306 (* setter debole di IP *)
 307 ndefinition setweak_ip_reg ≝
 308 λm:mcu_type.λt:memory_impl.λs:any_status m t.λip':word16.
 309  match set_ip_reg m t s ip' with
 310   [ None ⇒ s | Some s' ⇒ s' ].
 311
 312 (* REGISTRO DP *)
 313
 314 (* setter forte di DP *)
 315 ndefinition set_dp_reg ≝
 316 λm:mcu_type.λt:memory_impl.λs:any_status m t.λdp':word16.
 317  opt_map … (match m return aux_set_type_opt word16 with
 318              [ HC05 ⇒ None ?
 319              | HC08 ⇒ None ?
 320              | HCS08 ⇒ None ?
 321              | RS08 ⇒ None ?
 322              | IP2022 ⇒ Some ? set_dp_reg_IP2022 ])
 323  (λf.Some ? (set_alu m t s (f (alu m t s) dp'))).
 324
 325 (* setter debole di DP *)
 326 ndefinition setweak_dp_reg ≝
 327 λm:mcu_type.λt:memory_impl.λs:any_status m t.λdp':word16.
 328  match set_dp_reg m t s dp' with
 329   [ None ⇒ s | Some s' ⇒ s' ].
 330
 331 (* REGISTRO DATA *)
 332
 333 (* setter forte di DATA *)
 334 ndefinition set_data_reg ≝
 335 λm:mcu_type.λt:memory_impl.λs:any_status m t.λdata':word16.
 336  opt_map … (match m return aux_set_type_opt word16 with
 337              [ HC05 ⇒ None ?
 338              | HC08 ⇒ None ?
 339              | HCS08 ⇒ None ?
 340              | RS08 ⇒ None ?
 341              | IP2022 ⇒ Some ? set_data_reg_IP2022 ])
 342  (λf.Some ? (set_alu m t s (f (alu m t s) data'))).
 343
 344 (* setter debole di DATA *)
 345 ndefinition setweak_data_reg ≝
 346 λm:mcu_type.λt:memory_impl.λs:any_status m t.λdata':word16.
 347  match set_data_reg m t s data' with
 348   [ None ⇒ s | Some s' ⇒ s' ].
 349
 350 (* REGISTRO SPEED *)
 351
 352 (* setter forte di SPEED *)
 353 ndefinition set_speed_reg ≝
 354 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspeed':exadecim.
 355  opt_map … (match m return aux_set_type_opt exadecim with
 356              [ HC05 ⇒ None ?
 357              | HC08 ⇒ None ?
 358              | HCS08 ⇒ None ?
 359              | RS08 ⇒ None ?
 360              | IP2022 ⇒ Some ? set_speed_reg_IP2022 ])
 361  (λf.Some ? (set_alu m t s (f (alu m t s) speed'))).
 362
 363 (* setter debole di SPEED *)
 364 ndefinition setweak_speed_reg ≝
 365 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspeed':exadecim.
 366  match set_speed_reg m t s speed' with
 367   [ None ⇒ s | Some s' ⇒ s' ].
 368
 369 (* REGISTRO PAGE *)
 370
 371 (* setter forte di PAGE *)
 372 ndefinition set_page_reg ≝
 373 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpage':oct.
 374  opt_map … (match m return aux_set_type_opt oct with
 375              [ HC05 ⇒ None ?
 376              | HC08 ⇒ None ?
 377              | HCS08 ⇒ None ?
 378              | RS08 ⇒ None ?
 379              | IP2022 ⇒ Some ? set_page_reg_IP2022 ])
 380  (λf.Some ? (set_alu m t s (f (alu m t s) page'))).
 381
 382 (* setter debole di PAGE *)
 383 ndefinition setweak_page_reg ≝
 384 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpage':oct.
 385  match set_page_reg m t s page' with
 386   [ None ⇒ s | Some s' ⇒ s' ].
 387
 388 (* REGISTRO MEMORY MAPPED X *)
 389
 390 (* setter forte di memory mapped X *)
 391 ndefinition set_x_map ≝
 392 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
 393  opt_map … (match m return aux_set_type_opt byte8 with
 394              [ HC05 ⇒ None ?
 395              | HC08 ⇒ None ?
 396              | HCS08 ⇒ None ?
 397              | RS08 ⇒ Some ? set_x_map_RS08
 398              | IP2022 ⇒ None ? ])
 399  (λf.Some ? (set_alu m t s (f (alu m t s) xm'))).
 400
 401 (* setter debole di memory mapped X *)
 402 ndefinition setweak_x_map ≝
 403 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
 404  match set_x_map m t s xm' with
 405   [ None ⇒ s | Some s' ⇒ s' ].
 406
 407 (* REGISTRO MEMORY MAPPED PS *)
 408
 409 (* setter forte di memory mapped PS *)
 410 ndefinition set_ps_map ≝
 411 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
 412  opt_map … (match m return aux_set_type_opt byte8 with
 413              [ HC05 ⇒ None ?
 414              | HC08 ⇒ None ?
 415              | HCS08 ⇒ None ?
 416              | RS08 ⇒ Some ? set_ps_map_RS08
 417              | IP2022 ⇒ None ? ])
 418  (λf.Some ? (set_alu m t s (f (alu m t s) psm'))).
 419
 420 (* setter debole di memory mapped PS *)
 421 ndefinition setweak_ps_map ≝
 422 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
 423  match set_ps_map m t s psm' with
 424   [ None ⇒ s | Some s' ⇒ s' ].
 425
 426 (* MODALITA SKIP *)
 427
 428 (* setter forte di SKIP *)
 429 ndefinition set_skip_mode ≝
 430 λm:mcu_type.λt:memory_impl.λs:any_status m t.λskipmode':bool.
 431  opt_map … (match m return aux_set_type_opt bool with
 432              [ HC05 ⇒ None ?
 433              | HC08 ⇒ None ?
 434              | HCS08 ⇒ None ?
 435              | RS08 ⇒ None ?
 436              | IP2022 ⇒ Some ? set_skip_mode_IP2022 ])
 437  (λf.Some ? (set_alu m t s (f (alu m t s) skipmode'))).
 438
 439 (* setter debole  di SKIP *)
 440 ndefinition setweak_skip_mode ≝
 441 λm:mcu_type.λt:memory_impl.λs:any_status m t.λskipmode':bool.
 442  match set_skip_mode m t s skipmode' with
 443   [ None ⇒ s | Some s' ⇒ s' ].
 444
 445 (* FLAG V *)
 446
 447 (* setter forte di V *)
 448 ndefinition set_v_flag ≝
 449 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
 450  opt_map … (match m return aux_set_type_opt bool with
 451              [ HC05 ⇒ None ?
 452              | HC08 ⇒ Some ? set_v_flag_HC08
 453              | HCS08 ⇒ Some ? set_v_flag_HC08
 454              | RS08 ⇒ None ?
 455              | IP2022 ⇒ None ? ])
 456  (λf.Some ? (set_alu m t s (f (alu m t s) vfl'))).
 457
 458 (* setter debole  di V *)
 459 ndefinition setweak_v_flag ≝
 460 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
 461  match set_v_flag m t s vfl' with
 462   [ None ⇒ s | Some s' ⇒ s' ].
 463
 464 (* FLAG H *)
 465
 466 (* setter forte di H *)
 467 ndefinition set_h_flag ≝
 468 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
 469  opt_map … (match m return aux_set_type_opt bool with
 470              [ HC05 ⇒ Some ? set_h_flag_HC05
 471              | HC08 ⇒ Some ? set_h_flag_HC08
 472              | HCS08 ⇒ Some ? set_h_flag_HC08
 473              | RS08 ⇒ None ?
 474              | IP2022 ⇒ Some ? set_h_flag_IP2022 ])
 475  (λf.Some ? (set_alu m t s (f (alu m t s) hfl'))).
 476
 477 (* setter debole di H *)
 478 ndefinition setweak_h_flag ≝
 479 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
 480  match set_h_flag m t s hfl' with
 481   [ None ⇒ s | Some s' ⇒ s' ].
 482
 483 (* FLAG I *)
 484
 485 (* setter forte di I *)
 486 ndefinition set_i_flag ≝
 487 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
 488  opt_map … (match m return aux_set_type_opt bool with
 489              [ HC05 ⇒ Some ? set_i_flag_HC05
 490              | HC08 ⇒ Some ? set_i_flag_HC08
 491              | HCS08 ⇒ Some ? set_i_flag_HC08
 492              | RS08 ⇒ None ?
 493              | IP2022 ⇒ None ? ])
 494  (λf.Some ? (set_alu m t s (f (alu m t s) ifl'))).
 495
 496 (* setter debole di I *)
 497 ndefinition setweak_i_flag ≝
 498 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
 499  match set_i_flag m t s ifl' with
 500   [ None ⇒ s | Some s' ⇒ s' ].
 501
 502 (* FLAG N *)
 503
 504 (* setter forte di N *)
 505 ndefinition set_n_flag ≝
 506 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
 507  opt_map … (match m return aux_set_type_opt bool with
 508              [ HC05 ⇒ Some ? set_n_flag_HC05
 509              | HC08 ⇒ Some ? set_n_flag_HC08
 510              | HCS08 ⇒ Some ? set_n_flag_HC08
 511              | RS08 ⇒ None ?
 512              | IP2022 ⇒ None ? ])
 513  (λf.Some ? (set_alu m t s (f (alu m t s) nfl'))).
 514
 515 (* setter debole di N *)
 516 ndefinition setweak_n_flag ≝
 517 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
 518  match set_n_flag m t s nfl' with
 519   [ None ⇒ s | Some s' ⇒ s' ].
 520
 521 (* FLAG Z *)
 522
 523 (* setter forte di Z *)
 524 ndefinition set_z_flag ≝
 525 λm:mcu_type.λt:memory_impl.λs:any_status m t.λzfl':bool.
 526  set_alu m t s
 527  (match m return aux_set_type bool with
 528   [ HC05 ⇒ set_z_flag_HC05
 529   | HC08 ⇒ set_z_flag_HC08
 530   | HCS08 ⇒ set_z_flag_HC08
 531   | RS08 ⇒ set_z_flag_RS08
 532   | IP2022 ⇒ set_z_flag_IP2022
 533   ] (alu m t s) zfl').
 534
 535 (* FLAG C *)
 536
 537 (* setter forte di C *)
 538 ndefinition set_c_flag ≝
 539 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcfl':bool.
 540  set_alu m t s
 541  (match m return aux_set_type bool with
 542   [ HC05 ⇒ set_c_flag_HC05
 543   | HC08 ⇒ set_c_flag_HC08
 544   | HCS08 ⇒ set_c_flag_HC08
 545   | RS08 ⇒ set_c_flag_RS08
 546   | IP2022 ⇒ set_c_flag_IP2022
 547   ] (alu m t s) cfl').
 548
 549 (* FLAG IRQ *)
 550
 551 (* setter forte di IRQ *)
 552 ndefinition set_irq_flag ≝
 553 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
 554  opt_map … (match m return aux_set_type_opt bool with
 555              [ HC05 ⇒ Some ? set_irq_flag_HC05
 556              | HC08 ⇒ Some ? set_irq_flag_HC08
 557              | HCS08 ⇒ Some ? set_irq_flag_HC08
 558              | RS08 ⇒ None ?
 559              | IP2022 ⇒ None ? ])
 560  (λf.Some ? (set_alu m t s (f (alu m t s) irqfl'))).
 561
 562 (* setter debole di IRQ *)
 563 ndefinition setweak_irq_flag ≝
 564 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
 565  match set_irq_flag m t s irqfl' with
 566   [ None ⇒ s | Some s' ⇒ s' ].