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   → x →
  33   match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
  34
  35 (* funzione ausiliaria per il tipaggio dei setter deboli *)
  36 ndefinition aux_set_type_opt ≝ λx:Type.λm:mcu_type.option
  37  (match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]
  38   → x →
  39   match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]).
  40
  41 (* DESCRITTORI ESTERNI ALLA ALU *)
  42
  43 (* setter forte della ALU *)
  44 ndefinition set_alu ≝
  45 λm:mcu_type.λt:memory_impl.λs:any_status m t.λalu'.
  46  mk_any_status m t alu' (mem_desc m t s) (chk_desc m t s) (clk_desc m t s).
  47
  48 (* setter forte della memoria *)
  49 ndefinition set_mem_desc ≝
  50 λm:mcu_type.λt:memory_impl.λs:any_status m t.λmem':aux_mem_type t.
  51  mk_any_status m t (alu m t s) mem' (chk_desc m t s) (clk_desc m t s).
  52
  53 (* setter forte del descrittore *)
  54 ndefinition set_chk_desc ≝
  55 λm:mcu_type.λt:memory_impl.λs:any_status m t.λchk':aux_chk_type t.
  56  mk_any_status m t (alu m t s) (mem_desc m t s) chk' (clk_desc m t s).
  57
  58 (* setter forte del clik *)
  59 ndefinition set_clk_desc ≝
  60 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  61 λclk':option (aux_clk_type m).
  62  mk_any_status m t (alu m t s) (mem_desc m t s) (chk_desc m t s) clk'.
  63
  64 (* REGISTRO A *)
  65
  66 (* setter specifico HC05 di A *)
  67 ndefinition set_acc_8_low_reg_HC05 ≝
  68 λalu.λacclow':byte8.
  69  mk_alu_HC05
  70   acclow'
  71   (indX_low_reg_HC05 alu)
  72   (sp_reg_HC05 alu)
  73   (sp_mask_HC05 alu)
  74   (sp_fix_HC05 alu)
  75   (pc_reg_HC05 alu)
  76   (pc_mask_HC05 alu)
  77   (h_flag_HC05 alu)
  78   (i_flag_HC05 alu)
  79   (n_flag_HC05 alu)
  80   (z_flag_HC05 alu)
  81   (c_flag_HC05 alu)
  82   (irq_flag_HC05 alu).
  83
  84 (* setter specifico HC08/HCS08 di A *)
  85 ndefinition set_acc_8_low_reg_HC08 ≝
  86 λalu.λacclow':byte8.
  87  mk_alu_HC08
  88   acclow'
  89   (indX_low_reg_HC08 alu)
  90   (indX_high_reg_HC08 alu)
  91   (sp_reg_HC08 alu)
  92   (pc_reg_HC08 alu)
  93   (v_flag_HC08 alu)
  94   (h_flag_HC08 alu)
  95   (i_flag_HC08 alu)
  96   (n_flag_HC08 alu)
  97   (z_flag_HC08 alu)
  98   (c_flag_HC08 alu)
  99   (irq_flag_HC08 alu).
 100
 101 (* setter specifico RS08 di A *)
 102 ndefinition set_acc_8_low_reg_RS08 ≝
 103 λalu.λacclow':byte8.
 104  mk_alu_RS08
 105   acclow'
 106   (pc_reg_RS08 alu)
 107   (pc_mask_RS08 alu)
 108   (spc_reg_RS08 alu)
 109   (x_map_RS08 alu)
 110   (ps_map_RS08 alu)
 111   (z_flag_RS08 alu)
 112   (c_flag_RS08 alu).
 113
 114 (* setter forte di A *)
 115 ndefinition set_acc_8_low_reg ≝
 116 λm:mcu_type.λt:memory_impl.λs:any_status m t.λacclow':byte8.
 117  set_alu m t s
 118  (match m return aux_set_type byte8 with
 119   [ HC05 ⇒ set_acc_8_low_reg_HC05
 120   | HC08 ⇒ set_acc_8_low_reg_HC08
 121   | HCS08 ⇒ set_acc_8_low_reg_HC08
 122   | RS08 ⇒ set_acc_8_low_reg_RS08
 123   ] (alu m t s) acclow').
 124
 125 (* REGISTRO X *)
 126
 127 (* setter specifico HC05 di X *)
 128 ndefinition set_indX_8_low_reg_HC05 ≝
 129 λalu.λindxlow':byte8.
 130  mk_alu_HC05
 131   (acc_low_reg_HC05 alu)
 132   indxlow'
 133   (sp_reg_HC05 alu)
 134   (sp_mask_HC05 alu)
 135   (sp_fix_HC05 alu)
 136   (pc_reg_HC05 alu)
 137   (pc_mask_HC05 alu)
 138   (h_flag_HC05 alu)
 139   (i_flag_HC05 alu)
 140   (n_flag_HC05 alu)
 141   (z_flag_HC05 alu)
 142   (c_flag_HC05 alu)
 143   (irq_flag_HC05 alu).
 144
 145 (* setter specifico HC08/HCS08 di X *)
 146 ndefinition set_indX_8_low_reg_HC08 ≝
 147 λalu.λindxlow':byte8.
 148  mk_alu_HC08
 149   (acc_low_reg_HC08 alu)
 150   indxlow'
 151   (indX_high_reg_HC08 alu)
 152   (sp_reg_HC08 alu)
 153   (pc_reg_HC08 alu)
 154   (v_flag_HC08 alu)
 155   (h_flag_HC08 alu)
 156   (i_flag_HC08 alu)
 157   (n_flag_HC08 alu)
 158   (z_flag_HC08 alu)
 159   (c_flag_HC08 alu)
 160   (irq_flag_HC08 alu).
 161
 162 (* setter forte di X *)
 163 ndefinition set_indX_8_low_reg ≝
 164 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
 165  opt_map … (match m return aux_set_type_opt byte8 with
 166              [ HC05 ⇒ Some ? set_indX_8_low_reg_HC05
 167              | HC08 ⇒ Some ? set_indX_8_low_reg_HC08
 168              | HCS08 ⇒ Some ? set_indX_8_low_reg_HC08
 169              | RS08 ⇒ None ? ])
 170  (λf.Some ? (set_alu m t s (f (alu m t s) indxlow'))).
 171
 172 (* setter debole di X *)
 173 ndefinition setweak_indX_8_low_reg ≝
 174 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
 175  match set_indX_8_low_reg m t s indxlow' with
 176   [ None ⇒ s | Some s' ⇒ s' ].
 177
 178 (* REGISTRO H *)
 179
 180 (* setter specifico HC08/HCS08 di H *)
 181 ndefinition set_indX_8_high_reg_HC08 ≝
 182 λalu.λindxhigh':byte8.
 183  mk_alu_HC08
 184   (acc_low_reg_HC08 alu)
 185   (indX_low_reg_HC08 alu)
 186   indxhigh'
 187   (sp_reg_HC08 alu)
 188   (pc_reg_HC08 alu)
 189   (v_flag_HC08 alu)
 190   (h_flag_HC08 alu)
 191   (i_flag_HC08 alu)
 192   (n_flag_HC08 alu)
 193   (z_flag_HC08 alu)
 194   (c_flag_HC08 alu)
 195   (irq_flag_HC08 alu).
 196
 197 (* setter forte di H *)
 198 ndefinition set_indX_8_high_reg ≝
 199 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
 200  opt_map … (match m return aux_set_type_opt byte8 with
 201              [ HC05 ⇒ None ?
 202              | HC08 ⇒ Some ? set_indX_8_high_reg_HC08
 203              | HCS08 ⇒ Some ? set_indX_8_high_reg_HC08
 204              | RS08 ⇒ None ? ])
 205  (λf.Some ? (set_alu m t s (f (alu m t s) indxhigh'))).
 206
 207 (* setter debole di H *)
 208 ndefinition setweak_indX_8_high_reg ≝
 209 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
 210  match set_indX_8_high_reg m t s indxhigh' with
 211   [ None ⇒ s | Some s' ⇒ s' ].
 212
 213 (* REGISTRO H:X *)
 214
 215 (* setter specifico HC08/HCS08 di H:X *)
 216 ndefinition set_indX_16_reg_HC08 ≝
 217 λalu.λindx16:word16.
 218  mk_alu_HC08
 219   (acc_low_reg_HC08 alu)
 220   (w16l indx16)
 221   (w16h indx16)
 222   (sp_reg_HC08 alu)
 223   (pc_reg_HC08 alu)
 224   (v_flag_HC08 alu)
 225   (h_flag_HC08 alu)
 226   (i_flag_HC08 alu)
 227   (n_flag_HC08 alu)
 228   (z_flag_HC08 alu)
 229   (c_flag_HC08 alu)
 230   (irq_flag_HC08 alu).
 231
 232 (* setter forte di H:X *)
 233 ndefinition set_indX_16_reg ≝
 234 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
 235  opt_map … (match m return aux_set_type_opt word16 with
 236              [ HC05 ⇒ None ?
 237              | HC08 ⇒ Some ? set_indX_16_reg_HC08
 238              | HCS08 ⇒ Some ? set_indX_16_reg_HC08
 239              | RS08 ⇒ None ? ])
 240  (λf.Some ? (set_alu m t s (f (alu m t s) indx16))).
 241
 242 (* setter debole di H:X *)
 243 ndefinition setweak_indX_16_reg ≝
 244 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
 245  match set_indX_16_reg m t s indx16 with
 246   [ None ⇒ s | Some s' ⇒ s' ].
 247
 248 (* REGISTRO SP *)
 249
 250 (* setter specifico HC05 di SP, effettua (SP∧mask)∨fix *)
 251 ndefinition set_sp_reg_HC05 ≝
 252 λalu.λsp':word16.
 253  mk_alu_HC05
 254   (acc_low_reg_HC05 alu)
 255   (indX_low_reg_HC05 alu)
 256   (or_w16 (and_w16 sp' (sp_mask_HC05 alu)) (sp_fix_HC05 alu))
 257   (sp_mask_HC05 alu)
 258   (sp_fix_HC05 alu)
 259   (pc_reg_HC05 alu)
 260   (pc_mask_HC05 alu)
 261   (h_flag_HC05 alu)
 262   (i_flag_HC05 alu)
 263   (n_flag_HC05 alu)
 264   (z_flag_HC05 alu)
 265   (c_flag_HC05 alu)
 266   (irq_flag_HC05 alu).
 267
 268 (* setter specifico HC08/HCS08 di SP *)
 269 ndefinition set_sp_reg_HC08 ≝
 270 λalu.λsp':word16.
 271  mk_alu_HC08
 272   (acc_low_reg_HC08 alu)
 273   (indX_low_reg_HC08 alu)
 274   (indX_high_reg_HC08 alu)
 275   sp'
 276   (pc_reg_HC08 alu)
 277   (v_flag_HC08 alu)
 278   (h_flag_HC08 alu)
 279   (i_flag_HC08 alu)
 280   (n_flag_HC08 alu)
 281   (z_flag_HC08 alu)
 282   (c_flag_HC08 alu)
 283   (irq_flag_HC08 alu).
 284
 285 (* setter forte di SP *)
 286 ndefinition set_sp_reg ≝
 287 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
 288  opt_map … (match m return aux_set_type_opt word16 with
 289              [ HC05 ⇒ Some ? set_sp_reg_HC05
 290              | HC08 ⇒ Some ? set_sp_reg_HC08
 291              | HCS08 ⇒ Some ? set_sp_reg_HC08
 292              | RS08 ⇒ None ? ])
 293  (λf.Some ? (set_alu m t s (f (alu m t s) sp'))).
 294
 295 (* setter debole di SP *)
 296 ndefinition setweak_sp_reg ≝
 297 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
 298  match set_sp_reg m t s sp' with
 299   [ None ⇒ s | Some s' ⇒ s' ].
 300
 301 (* REGISTRO PC *)
 302
 303 (* setter specifico HC05 di PC, effettua PC∧mask *)
 304 ndefinition set_pc_reg_HC05 ≝
 305 λalu.λpc':word16.
 306  mk_alu_HC05
 307   (acc_low_reg_HC05 alu)
 308   (indX_low_reg_HC05 alu)
 309   (sp_reg_HC05 alu)
 310   (sp_mask_HC05 alu)
 311   (sp_fix_HC05 alu)
 312   (and_w16 pc' (pc_mask_HC05 alu))
 313   (pc_mask_HC05 alu)
 314   (h_flag_HC05 alu)
 315   (i_flag_HC05 alu)
 316   (n_flag_HC05 alu)
 317   (z_flag_HC05 alu)
 318   (c_flag_HC05 alu)
 319   (irq_flag_HC05 alu).
 320
 321 (* setter specifico HC08/HCS08 di PC *)
 322 ndefinition set_pc_reg_HC08 ≝
 323 λalu.λpc':word16.
 324  mk_alu_HC08
 325   (acc_low_reg_HC08 alu)
 326   (indX_low_reg_HC08 alu)
 327   (indX_high_reg_HC08 alu)
 328   (sp_reg_HC08 alu)
 329   pc'
 330   (v_flag_HC08 alu)
 331   (h_flag_HC08 alu)
 332   (i_flag_HC08 alu)
 333   (n_flag_HC08 alu)
 334   (z_flag_HC08 alu)
 335   (c_flag_HC08 alu)
 336   (irq_flag_HC08 alu).
 337
 338 (* setter specifico RS08 di PC, effettua PC∧mask *)
 339 ndefinition set_pc_reg_RS08 ≝
 340 λalu.λpc':word16.
 341  mk_alu_RS08
 342   (acc_low_reg_RS08 alu)
 343   (and_w16 pc' (pc_mask_RS08 alu))
 344   (pc_mask_RS08 alu)
 345   (spc_reg_RS08 alu)
 346   (x_map_RS08 alu)
 347   (ps_map_RS08 alu)
 348   (z_flag_RS08 alu)
 349   (c_flag_RS08 alu).
 350
 351 (* setter forte di PC *)
 352 ndefinition set_pc_reg ≝
 353 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpc':word16.
 354  set_alu m t s
 355  (match m return aux_set_type word16 with
 356   [ HC05 ⇒ set_pc_reg_HC05
 357   | HC08 ⇒ set_pc_reg_HC08
 358   | HCS08 ⇒ set_pc_reg_HC08
 359   | RS08 ⇒ set_pc_reg_RS08
 360   ] (alu m t s) pc').
 361
 362 (* REGISTRO SPC *)
 363
 364 (* setter specifico RS08 di SPC, effettua SPC∧mask *)
 365 ndefinition set_spc_reg_RS08 ≝
 366 λalu.λspc':word16.
 367  mk_alu_RS08
 368   (acc_low_reg_RS08 alu)
 369   (pc_reg_RS08 alu)
 370   (pc_mask_RS08 alu)
 371   (and_w16 spc' (pc_mask_RS08 alu))
 372   (x_map_RS08 alu)
 373   (ps_map_RS08 alu)
 374   (z_flag_RS08 alu)
 375   (c_flag_RS08 alu).
 376
 377 (* setter forte di SPC *)
 378 ndefinition set_spc_reg ≝
 379 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
 380  opt_map … (match m return aux_set_type_opt word16 with
 381              [ HC05 ⇒ None ?
 382              | HC08 ⇒ None ?
 383              | HCS08 ⇒ None ?
 384              | RS08 ⇒ Some ? set_spc_reg_RS08 ])
 385  (λf.Some ? (set_alu m t s (f (alu m t s) spc'))).
 386
 387 (* setter debole di SPC *)
 388 ndefinition setweak_spc_reg ≝
 389 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
 390  match set_spc_reg m t s spc' with
 391   [ None ⇒ s | Some s' ⇒ s' ].
 392
 393 (* REGISTRO MEMORY MAPPED X *)
 394
 395 (* setter specifico RS08 di memory mapped X *)
 396 ndefinition set_x_map_RS08 ≝
 397 λalu.λxm':byte8.
 398  mk_alu_RS08
 399   (acc_low_reg_RS08 alu)
 400   (pc_reg_RS08 alu)
 401   (pc_mask_RS08 alu)
 402   (spc_reg_RS08 alu)
 403   xm'
 404   (ps_map_RS08 alu)
 405   (z_flag_RS08 alu)
 406   (c_flag_RS08 alu).
 407
 408 (* setter forte di memory mapped X *)
 409 ndefinition set_x_map ≝
 410 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
 411  opt_map … (match m return aux_set_type_opt byte8 with
 412              [ HC05 ⇒ None ?
 413              | HC08 ⇒ None ?
 414              | HCS08 ⇒ None ?
 415              | RS08 ⇒ Some ? set_x_map_RS08 ])
 416  (λf.Some ? (set_alu m t s (f (alu m t s) xm'))).
 417
 418 (* setter debole di memory mapped X *)
 419 ndefinition setweak_x_map ≝
 420 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
 421  match set_x_map m t s xm' with
 422   [ None ⇒ s | Some s' ⇒ s' ].
 423
 424 (* REGISTRO MEMORY MAPPED PS *)
 425
 426 (* setter specifico RS08 di memory mapped PS *)
 427 ndefinition set_ps_map_RS08 ≝
 428 λalu.λpsm':byte8.
 429  mk_alu_RS08
 430   (acc_low_reg_RS08 alu)
 431   (pc_reg_RS08 alu)
 432   (pc_mask_RS08 alu)
 433   (spc_reg_RS08 alu)
 434   (x_map_RS08 alu)
 435   psm'
 436   (z_flag_RS08 alu)
 437   (c_flag_RS08 alu).
 438
 439 (* setter forte di memory mapped PS *)
 440 ndefinition set_ps_map ≝
 441 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
 442  opt_map … (match m return aux_set_type_opt byte8 with
 443              [ HC05 ⇒ None ?
 444              | HC08 ⇒ None ?
 445              | HCS08 ⇒ None ?
 446              | RS08 ⇒ Some ? set_ps_map_RS08 ])
 447  (λf.Some ? (set_alu m t s (f (alu m t s) psm'))).
 448
 449 (* setter debole di memory mapped PS *)
 450 ndefinition setweak_ps_map ≝
 451 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
 452  match set_ps_map m t s psm' with
 453   [ None ⇒ s | Some s' ⇒ s' ].
 454
 455 (* FLAG V *)
 456
 457 (* setter specifico HC08/HCS08 di V *)
 458 ndefinition set_v_flag_HC08 ≝
 459 λalu.λvfl':bool.
 460  mk_alu_HC08
 461   (acc_low_reg_HC08 alu)
 462   (indX_low_reg_HC08 alu)
 463   (indX_high_reg_HC08 alu)
 464   (sp_reg_HC08 alu)
 465   (pc_reg_HC08 alu)
 466   vfl'
 467   (h_flag_HC08 alu)
 468   (i_flag_HC08 alu)
 469   (n_flag_HC08 alu)
 470   (z_flag_HC08 alu)
 471   (c_flag_HC08 alu)
 472   (irq_flag_HC08 alu).
 473
 474 (* setter forte di V *)
 475 ndefinition set_v_flag ≝
 476 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
 477  opt_map … (match m return aux_set_type_opt bool with
 478              [ HC05 ⇒ None ?
 479              | HC08 ⇒ Some ? set_v_flag_HC08
 480              | HCS08 ⇒ Some ? set_v_flag_HC08
 481              | RS08 ⇒ None ? ])
 482  (λf.Some ? (set_alu m t s (f (alu m t s) vfl'))).
 483
 484 (* setter debole  di V *)
 485 ndefinition setweak_v_flag ≝
 486 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
 487  match set_v_flag m t s vfl' with
 488   [ None ⇒ s | Some s' ⇒ s' ].
 489
 490 (* FLAG H *)
 491
 492 (* setter specifico HC05 di H *)
 493 ndefinition set_h_flag_HC05 ≝
 494 λalu.λhfl':bool.
 495  mk_alu_HC05
 496   (acc_low_reg_HC05 alu)
 497   (indX_low_reg_HC05 alu)
 498   (sp_reg_HC05 alu)
 499   (sp_mask_HC05 alu)
 500   (sp_fix_HC05 alu)
 501   (pc_reg_HC05 alu)
 502   (pc_mask_HC05 alu)
 503   hfl'
 504   (i_flag_HC05 alu)
 505   (n_flag_HC05 alu)
 506   (z_flag_HC05 alu)
 507   (c_flag_HC05 alu)
 508   (irq_flag_HC05 alu).
 509
 510 (* setter specifico HC08/HCS08 di H *)
 511 ndefinition set_h_flag_HC08 ≝
 512 λalu.λhfl':bool.
 513  mk_alu_HC08
 514   (acc_low_reg_HC08 alu)
 515   (indX_low_reg_HC08 alu)
 516   (indX_high_reg_HC08 alu)
 517   (sp_reg_HC08 alu)
 518   (pc_reg_HC08 alu)
 519   (v_flag_HC08 alu)
 520   hfl'
 521   (i_flag_HC08 alu)
 522   (n_flag_HC08 alu)
 523   (z_flag_HC08 alu)
 524   (c_flag_HC08 alu)
 525   (irq_flag_HC08 alu).
 526
 527 (* setter forte di H *)
 528 ndefinition set_h_flag ≝
 529 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
 530  opt_map … (match m return aux_set_type_opt bool with
 531              [ HC05 ⇒ Some ? set_h_flag_HC05
 532              | HC08 ⇒ Some ? set_h_flag_HC08
 533              | HCS08 ⇒ Some ? set_h_flag_HC08
 534              | RS08 ⇒ None ? ])
 535  (λf.Some ? (set_alu m t s (f (alu m t s) hfl'))).
 536
 537 (* setter debole di H *)
 538 ndefinition setweak_h_flag ≝
 539 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
 540  match set_h_flag m t s hfl' with
 541   [ None ⇒ s | Some s' ⇒ s' ].
 542
 543 (* FLAG I *)
 544
 545 (* setter specifico HC05 di I *)
 546 ndefinition set_i_flag_HC05 ≝
 547 λalu.λifl':bool.
 548  mk_alu_HC05
 549   (acc_low_reg_HC05 alu)
 550   (indX_low_reg_HC05 alu)
 551   (sp_reg_HC05 alu)
 552   (sp_mask_HC05 alu)
 553   (sp_fix_HC05 alu)
 554   (pc_reg_HC05 alu)
 555   (pc_mask_HC05 alu)
 556   (h_flag_HC05 alu)
 557   ifl'
 558   (n_flag_HC05 alu)
 559   (z_flag_HC05 alu)
 560   (c_flag_HC05 alu)
 561   (irq_flag_HC05 alu).
 562
 563 (* setter specifico HC08/HCS08 di I *)
 564 ndefinition set_i_flag_HC08 ≝
 565 λalu.λifl':bool.
 566  mk_alu_HC08
 567   (acc_low_reg_HC08 alu)
 568   (indX_low_reg_HC08 alu)
 569   (indX_high_reg_HC08 alu)
 570   (sp_reg_HC08 alu)
 571   (pc_reg_HC08 alu)
 572   (v_flag_HC08 alu)
 573   (h_flag_HC08 alu)
 574   ifl'
 575   (n_flag_HC08 alu)
 576   (z_flag_HC08 alu)
 577   (c_flag_HC08 alu)
 578   (irq_flag_HC08 alu).
 579
 580 (* setter forte di I *)
 581 ndefinition set_i_flag ≝
 582 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
 583  opt_map … (match m return aux_set_type_opt bool with
 584              [ HC05 ⇒ Some ? set_i_flag_HC05
 585              | HC08 ⇒ Some ? set_i_flag_HC08
 586              | HCS08 ⇒ Some ? set_i_flag_HC08
 587              | RS08 ⇒ None ? ])
 588  (λf.Some ? (set_alu m t s (f (alu m t s) ifl'))).
 589
 590 (* setter debole di I *)
 591 ndefinition setweak_i_flag ≝
 592 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
 593  match set_i_flag m t s ifl' with
 594   [ None ⇒ s | Some s' ⇒ s' ].
 595
 596 (* FLAG N *)
 597
 598 (* setter specifico HC05 di N *)
 599 ndefinition set_n_flag_HC05 ≝
 600 λalu.λnfl':bool.
 601  mk_alu_HC05
 602   (acc_low_reg_HC05 alu)
 603   (indX_low_reg_HC05 alu)
 604   (sp_reg_HC05 alu)
 605   (sp_mask_HC05 alu)
 606   (sp_fix_HC05 alu)
 607   (pc_reg_HC05 alu)
 608   (pc_mask_HC05 alu)
 609   (h_flag_HC05 alu)
 610   (i_flag_HC05 alu)
 611   nfl'
 612   (z_flag_HC05 alu)
 613   (c_flag_HC05 alu)
 614   (irq_flag_HC05 alu).
 615
 616 (* setter specifico HC08/HCS08 di N *)
 617 ndefinition set_n_flag_HC08 ≝
 618 λalu.λnfl':bool.
 619  mk_alu_HC08
 620   (acc_low_reg_HC08 alu)
 621   (indX_low_reg_HC08 alu)
 622   (indX_high_reg_HC08 alu)
 623   (sp_reg_HC08 alu)
 624   (pc_reg_HC08 alu)
 625   (v_flag_HC08 alu)
 626   (h_flag_HC08 alu)
 627   (i_flag_HC08 alu)
 628   nfl'
 629   (z_flag_HC08 alu)
 630   (c_flag_HC08 alu)
 631   (irq_flag_HC08 alu).
 632
 633 (* setter forte di N *)
 634 ndefinition set_n_flag ≝
 635 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
 636  opt_map … (match m return aux_set_type_opt bool with
 637              [ HC05 ⇒ Some ? set_n_flag_HC05
 638              | HC08 ⇒ Some ? set_n_flag_HC08
 639              | HCS08 ⇒ Some ? set_n_flag_HC08
 640              | RS08 ⇒ None ? ])
 641  (λf.Some ? (set_alu m t s (f (alu m t s) nfl'))).
 642
 643 (* setter debole di N *)
 644 ndefinition setweak_n_flag ≝
 645 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
 646  match set_n_flag m t s nfl' with
 647   [ None ⇒ s | Some s' ⇒ s' ].
 648
 649 (* FLAG Z *)
 650
 651 (* setter specifico HC05 di Z *)
 652 ndefinition set_z_flag_HC05 ≝
 653 λalu.λzfl':bool.
 654  mk_alu_HC05
 655   (acc_low_reg_HC05 alu)
 656   (indX_low_reg_HC05 alu)
 657   (sp_reg_HC05 alu)
 658   (sp_mask_HC05 alu)
 659   (sp_fix_HC05 alu)
 660   (pc_reg_HC05 alu)
 661   (pc_mask_HC05 alu)
 662   (h_flag_HC05 alu)
 663   (i_flag_HC05 alu)
 664   (n_flag_HC05 alu)
 665   zfl'
 666   (c_flag_HC05 alu)
 667   (irq_flag_HC05 alu).
 668
 669 (* setter specifico HC08/HCS08 di Z *)
 670 ndefinition set_z_flag_HC08 ≝
 671 λalu.λzfl':bool.
 672  mk_alu_HC08
 673   (acc_low_reg_HC08 alu)
 674   (indX_low_reg_HC08 alu)
 675   (indX_high_reg_HC08 alu)
 676   (sp_reg_HC08 alu)
 677   (pc_reg_HC08 alu)
 678   (v_flag_HC08 alu)
 679   (h_flag_HC08 alu)
 680   (i_flag_HC08 alu)
 681   (n_flag_HC08 alu)
 682   zfl'
 683   (c_flag_HC08 alu)
 684   (irq_flag_HC08 alu).
 685
 686 (* setter sprcifico RS08 di Z *)
 687 ndefinition set_z_flag_RS08 ≝
 688 λalu.λzfl':bool.
 689  mk_alu_RS08
 690   (acc_low_reg_RS08 alu)
 691   (pc_reg_RS08 alu)
 692   (pc_mask_RS08 alu)
 693   (spc_reg_RS08 alu)
 694   (x_map_RS08 alu)
 695   (ps_map_RS08 alu)
 696   zfl'
 697   (c_flag_RS08 alu).
 698
 699 (* setter forte di Z *)
 700 ndefinition set_z_flag ≝
 701 λm:mcu_type.λt:memory_impl.λs:any_status m t.λzfl':bool.
 702  set_alu m t s
 703  (match m return aux_set_type bool with
 704   [ HC05 ⇒ set_z_flag_HC05
 705   | HC08 ⇒ set_z_flag_HC08
 706   | HCS08 ⇒ set_z_flag_HC08
 707   | RS08 ⇒ set_z_flag_RS08
 708   ] (alu m t s) zfl').
 709
 710 (* FLAG C *)
 711
 712 (* setter specifico HC05 di C *)
 713 ndefinition set_c_flag_HC05 ≝
 714 λalu.λcfl':bool.
 715  mk_alu_HC05
 716   (acc_low_reg_HC05 alu)
 717   (indX_low_reg_HC05 alu)
 718   (sp_reg_HC05 alu)
 719   (sp_mask_HC05 alu)
 720   (sp_fix_HC05 alu)
 721   (pc_reg_HC05 alu)
 722   (pc_mask_HC05 alu)
 723   (h_flag_HC05 alu)
 724   (i_flag_HC05 alu)
 725   (n_flag_HC05 alu)
 726   (z_flag_HC05 alu)
 727   cfl'
 728   (irq_flag_HC05 alu).
 729
 730 (* setter specifico HC08/HCS08 di C *)
 731 ndefinition set_c_flag_HC08 ≝
 732 λalu.λcfl':bool.
 733  mk_alu_HC08
 734   (acc_low_reg_HC08 alu)
 735   (indX_low_reg_HC08 alu)
 736   (indX_high_reg_HC08 alu)
 737   (sp_reg_HC08 alu)
 738   (pc_reg_HC08 alu)
 739   (v_flag_HC08 alu)
 740   (h_flag_HC08 alu)
 741   (i_flag_HC08 alu)
 742   (n_flag_HC08 alu)
 743   (z_flag_HC08 alu)
 744   cfl'
 745   (irq_flag_HC08 alu).
 746
 747 (* setter specifico RS08 di C *)
 748 ndefinition set_c_flag_RS08 ≝
 749 λalu.λcfl':bool.
 750  mk_alu_RS08
 751   (acc_low_reg_RS08 alu)
 752   (pc_reg_RS08 alu)
 753   (pc_mask_RS08 alu)
 754   (spc_reg_RS08 alu)
 755   (x_map_RS08 alu)
 756   (ps_map_RS08 alu)
 757   (z_flag_RS08 alu)
 758   cfl'.
 759
 760 (* setter forte di C *)
 761 ndefinition set_c_flag ≝
 762 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcfl':bool.
 763  set_alu m t s
 764  (match m return aux_set_type bool with
 765   [ HC05 ⇒ set_c_flag_HC05
 766   | HC08 ⇒ set_c_flag_HC08
 767   | HCS08 ⇒ set_c_flag_HC08
 768   | RS08 ⇒ set_c_flag_RS08
 769   ] (alu m t s) cfl').
 770
 771 (* FLAG IRQ *)
 772
 773 (* setter specifico HC05 di IRQ *)
 774 ndefinition set_irq_flag_HC05 ≝
 775 λalu.λirqfl':bool.
 776  mk_alu_HC05
 777   (acc_low_reg_HC05 alu)
 778   (indX_low_reg_HC05 alu)
 779   (sp_reg_HC05 alu)
 780   (sp_mask_HC05 alu)
 781   (sp_fix_HC05 alu)
 782   (pc_reg_HC05 alu)
 783   (pc_mask_HC05 alu)
 784   (h_flag_HC05 alu)
 785   (i_flag_HC05 alu)
 786   (n_flag_HC05 alu)
 787   (z_flag_HC05 alu)
 788   (c_flag_HC05 alu)
 789   irqfl'.
 790
 791 (* setter specifico HC08/HCS08 di IRQ *)
 792 ndefinition set_irq_flag_HC08 ≝
 793 λalu.λirqfl':bool.
 794  mk_alu_HC08
 795   (acc_low_reg_HC08 alu)
 796   (indX_low_reg_HC08 alu)
 797   (indX_high_reg_HC08 alu)
 798   (sp_reg_HC08 alu)
 799   (pc_reg_HC08 alu)
 800   (v_flag_HC08 alu)
 801   (h_flag_HC08 alu)
 802   (i_flag_HC08 alu)
 803   (n_flag_HC08 alu)
 804   (z_flag_HC08 alu)
 805   (c_flag_HC08 alu)
 806   irqfl'.
 807
 808 (* setter forte di IRQ *)
 809 ndefinition set_irq_flag ≝
 810 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
 811  opt_map … (match m return aux_set_type_opt bool with
 812              [ HC05 ⇒ Some ? set_irq_flag_HC05
 813              | HC08 ⇒ Some ? set_irq_flag_HC08
 814              | HCS08 ⇒ Some ? set_irq_flag_HC08
 815              | RS08 ⇒ None ? ])
 816  (λf.Some ? (set_alu m t s (f (alu m t s) irqfl'))).
 817
 818 (* setter debole di IRQ *)
 819 ndefinition setweak_irq_flag ≝
 820 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
 821  match set_irq_flag m t s irqfl' with
 822   [ None ⇒ s | Some s' ⇒ s' ].