matita/matita/contribs/ng_assembly2/emulator/status/status_getter.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_setter.ma".
  24
  25 (* **************** *)
  26 (* GETTER SPECIFICI *)
  27 (* **************** *)
  28
  29 (* funzione ausiliaria per il tipaggio dei getter *)
  30 ndefinition aux_get_type ≝ λT:Type.λm:mcu_type.aux_alu_type m → T.
  31
  32 (* REGISTRI *)
  33
  34 (* getter di A, esiste sempre *)
  35 ndefinition get_acc_8_low_reg ≝
  36 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  37  match m
  38   return aux_get_type byte8 with
  39  [ HC05 ⇒ acc_low_reg_HC05
  40  | HC08 ⇒ acc_low_reg_HC08
  41  | HCS08 ⇒ acc_low_reg_HC08
  42  | RS08 ⇒ acc_low_reg_RS08
  43  | IP2022 ⇒ acc_low_reg_IP2022 ]
  44  (alu … s).
  45
  46 (* getter di X, non esiste sempre *)
  47 ndefinition get_indX_8_low_reg ≝
  48 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  49  match m
  50   return aux_get_type (option byte8) with
  51  [ HC05 ⇒ λalu.Some ? (indX_low_reg_HC05 alu)
  52  | HC08 ⇒ λalu.Some ? (indX_low_reg_HC08 alu)
  53  | HCS08 ⇒ λalu.Some ? (indX_low_reg_HC08 alu)
  54  | RS08 ⇒ λalu.None ?
  55  | IP2022 ⇒ λalu.None ? ]
  56  (alu … s).
  57
  58 (* getter di H, non esiste sempre *)
  59 ndefinition get_indX_8_high_reg ≝
  60 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  61  match m
  62   return aux_get_type (option byte8) with
  63  [ HC05 ⇒ λalu.None ?
  64  | HC08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
  65  | HCS08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
  66  | RS08 ⇒ λalu.None ?
  67  | IP2022 ⇒ λalu.None ? ]
  68  (alu … s).
  69
  70 (* getter di H:X, non esiste sempre *)
  71 ndefinition get_indX_16_reg ≝
  72 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  73  match m
  74   return aux_get_type (option word16) with
  75  [ HC05 ⇒ λalu.None ?
  76  | HC08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
  77  | HCS08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
  78  | RS08 ⇒ λalu.None ?
  79  | IP2022 ⇒ λalu.None ? ]
  80  (alu … s).
  81
  82 (* getter di SP, non esiste sempre *)
  83 ndefinition get_sp_reg ≝
  84 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  85  match m
  86   return aux_get_type (option word16) with
  87  [ HC05 ⇒ λalu.Some ? (sp_reg_HC05 alu)
  88  | HC08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
  89  | HCS08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
  90  | RS08 ⇒ λalu.None ?
  91  | IP2022 ⇒ λalu.Some ? (sp_reg_IP2022 alu) ]
  92  (alu … s).
  93
  94 (* getter di PC, esiste sempre *)
  95 ndefinition get_pc_reg ≝
  96 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  97  match m
  98   return aux_get_type word16 with
  99  [ HC05 ⇒ pc_reg_HC05
 100  | HC08 ⇒ pc_reg_HC08
 101  | HCS08 ⇒ pc_reg_HC08
 102  | RS08 ⇒ pc_reg_RS08
 103  | IP2022 ⇒ pc_reg_IP2022 ]
 104  (alu … s).
 105
 106 (* getter di SPC, non esiste sempre *)
 107 ndefinition get_spc_reg ≝
 108 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 109  match m
 110   return aux_get_type (option word16) with
 111  [ HC05 ⇒ λalu.None ?
 112  | HC08 ⇒ λalu.None ?
 113  | HCS08 ⇒ λalu.None ?
 114  | RS08 ⇒ λalu.Some ? (spc_reg_RS08 alu)
 115  | IP2022 ⇒ λalu.None ? ]
 116  (alu … s).
 117
 118 (* getter di MULH, non esiste sempre *)
 119 ndefinition get_mulh_reg ≝
 120 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 121  match m
 122   return aux_get_type (option byte8) with
 123  [ HC05 ⇒ λalu.None ?
 124  | HC08 ⇒ λalu.None ?
 125  | HCS08 ⇒ λalu.None ?
 126  | RS08 ⇒ λalu.None ?
 127  | IP2022 ⇒ λalu.Some ? (mulh_reg_IP2022 alu) ]
 128  (alu … s).
 129
 130 (* getter di ADDRSEL, non esiste sempre *)
 131 ndefinition get_addrsel_reg ≝
 132 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 133  match m
 134   return aux_get_type (option byte8) with
 135  [ HC05 ⇒ λalu.None ?
 136  | HC08 ⇒ λalu.None ?
 137  | HCS08 ⇒ λalu.None ?
 138  | RS08 ⇒ λalu.None ?
 139  | IP2022 ⇒ λalu.Some ? (addrsel_reg_IP2022 alu) ]
 140  (alu … s).
 141
 142 (* getter di ADDR, non esiste sempre *)
 143 ndefinition get_addr_reg ≝
 144 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 145  match m
 146   return aux_get_type (option word24) with
 147  [ HC05 ⇒ λalu.None ?
 148  | HC08 ⇒ λalu.None ?
 149  | HCS08 ⇒ λalu.None ?
 150  | RS08 ⇒ λalu.None ?
 151  | IP2022 ⇒ λalu.Some ? (get_addr_reg_IP2022 alu) ]
 152  (alu … s).
 153
 154 (* getter di CALL, non esiste sempre *)
 155 ndefinition get_call_reg ≝
 156 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 157  match m
 158   return aux_get_type (option word16) with
 159  [ HC05 ⇒ λalu.None ?
 160  | HC08 ⇒ λalu.None ?
 161  | HCS08 ⇒ λalu.None ?
 162  | RS08 ⇒ λalu.None ?
 163  | IP2022 ⇒ λalu.Some ? (get_call_reg_IP2022 alu) ]
 164  (alu … s).
 165
 166 (* getter di IP, non esiste sempre *)
 167 ndefinition get_ip_reg ≝
 168 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 169  match m
 170   return aux_get_type (option word16) with
 171  [ HC05 ⇒ λalu.None ?
 172  | HC08 ⇒ λalu.None ?
 173  | HCS08 ⇒ λalu.None ?
 174  | RS08 ⇒ λalu.None ?
 175  | IP2022 ⇒ λalu.Some ? (ip_reg_IP2022 alu) ]
 176  (alu … s).
 177
 178 (* getter di DP, non esiste sempre *)
 179 ndefinition get_dp_reg ≝
 180 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 181  match m
 182   return aux_get_type (option word16) with
 183  [ HC05 ⇒ λalu.None ?
 184  | HC08 ⇒ λalu.None ?
 185  | HCS08 ⇒ λalu.None ?
 186  | RS08 ⇒ λalu.None ?
 187  | IP2022 ⇒ λalu.Some ? (dp_reg_IP2022 alu) ]
 188  (alu … s).
 189
 190 (* getter di DATA, non esiste sempre *)
 191 ndefinition get_data_reg ≝
 192 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 193  match m
 194   return aux_get_type (option word16) with
 195  [ HC05 ⇒ λalu.None ?
 196  | HC08 ⇒ λalu.None ?
 197  | HCS08 ⇒ λalu.None ?
 198  | RS08 ⇒ λalu.None ?
 199  | IP2022 ⇒ λalu.Some ? (data_reg_IP2022 alu) ]
 200  (alu … s).
 201
 202 (* getter di SPEED, non esiste sempre *)
 203 ndefinition get_speed_reg ≝
 204 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 205  match m
 206   return aux_get_type (option exadecim) with
 207  [ HC05 ⇒ λalu.None ?
 208  | HC08 ⇒ λalu.None ?
 209  | HCS08 ⇒ λalu.None ?
 210  | RS08 ⇒ λalu.None ?
 211  | IP2022 ⇒ λalu.Some ? (speed_reg_IP2022 alu) ]
 212  (alu … s).
 213
 214 (* getter di PAGE, non esiste sempre *)
 215 ndefinition get_page_reg ≝
 216 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 217  match m
 218   return aux_get_type (option oct) with
 219  [ HC05 ⇒ λalu.None ?
 220  | HC08 ⇒ λalu.None ?
 221  | HCS08 ⇒ λalu.None ?
 222  | RS08 ⇒ λalu.None ?
 223  | IP2022 ⇒ λalu.Some ? (page_reg_IP2022 alu) ]
 224  (alu … s).
 225
 226 (* REGISTRI SPECIALI *)
 227
 228 (* getter di memory mapped X, non esiste sempre *)
 229 ndefinition get_x_map ≝
 230 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 231  match m
 232   return aux_get_type (option byte8) with
 233  [ HC05 ⇒ λalu.None ?
 234  | HC08 ⇒ λalu.None ?
 235  | HCS08 ⇒ λalu.None ?
 236  | RS08 ⇒ λalu.Some ? (x_map_RS08 alu)
 237  | IP2022 ⇒ λalu.None ? ]
 238  (alu … s).
 239
 240 (* getter di memory mapped PS, non esiste sempre *)
 241 ndefinition get_ps_map ≝
 242 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 243  match m
 244   return aux_get_type (option byte8) with
 245  [ HC05 ⇒ λalu.None ?
 246  | HC08 ⇒ λalu.None ?
 247  | HCS08 ⇒ λalu.None ?
 248  | RS08 ⇒ λalu.Some ? (ps_map_RS08 alu)
 249  | IP2022 ⇒ λalu.None ? ]
 250  (alu … s).
 251
 252 (* getter di skip mode, non esiste sempre *)
 253 ndefinition get_skip_mode ≝
 254 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 255  match m
 256   return aux_get_type (option bool) with
 257  [ HC05 ⇒ λalu.None ?
 258  | HC08 ⇒ λalu.None ?
 259  | HCS08 ⇒ λalu.None ?
 260  | RS08 ⇒ λalu.None ?
 261  | IP2022 ⇒ λalu.Some ? (skip_mode_IP2022 alu) ]
 262  (alu … s).
 263
 264 (* FLAG *)
 265
 266 (* getter di V, non esiste sempre *)
 267 ndefinition get_v_flag ≝
 268 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 269  match m
 270   return aux_get_type (option bool) with
 271  [ HC05 ⇒ λalu.None ?
 272  | HC08 ⇒ λalu.Some ? (v_flag_HC08 alu)
 273  | HCS08 ⇒ λalu.Some ? (v_flag_HC08 alu)
 274  | RS08 ⇒ λalu.None ?
 275  | IP2022 ⇒ λalu.None ? ]
 276  (alu … s).
 277
 278 (* getter di H, non esiste sempre *)
 279 ndefinition get_h_flag ≝
 280 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 281  match m
 282   return aux_get_type (option bool) with
 283  [ HC05 ⇒ λalu.Some ? (h_flag_HC05 alu)
 284  | HC08 ⇒ λalu.Some ? (h_flag_HC08 alu)
 285  | HCS08 ⇒ λalu.Some ? (h_flag_HC08 alu)
 286  | RS08 ⇒ λalu.None ?
 287  | IP2022 ⇒ λalu.Some ? (h_flag_IP2022 alu) ]
 288  (alu … s).
 289
 290 (* getter di I, non esiste sempre *)
 291 ndefinition get_i_flag ≝
 292 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 293  match m
 294   return aux_get_type (option bool) with
 295  [ HC05 ⇒ λalu.Some ? (i_flag_HC05 alu)
 296  | HC08 ⇒ λalu.Some ? (i_flag_HC08 alu)
 297  | HCS08 ⇒ λalu.Some ? (i_flag_HC08 alu)
 298  | RS08 ⇒ λalu.None ?
 299  | IP2022 ⇒ λalu.None ? ]
 300  (alu … s).
 301
 302 (* getter di N, non esiste sempre *)
 303 ndefinition get_n_flag ≝
 304 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 305  match m
 306   return aux_get_type (option bool) with
 307  [ HC05 ⇒ λalu.Some ? (n_flag_HC05 alu)
 308  | HC08 ⇒ λalu.Some ? (n_flag_HC08 alu)
 309  | HCS08 ⇒ λalu.Some ? (n_flag_HC08 alu)
 310  | RS08 ⇒ λalu.None ?
 311  | IP2022 ⇒ λalu.None ? ]
 312  (alu … s).
 313
 314 (* getter di Z, esiste sempre *)
 315 ndefinition get_z_flag ≝
 316 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 317  match m
 318   return aux_get_type bool with
 319  [ HC05 ⇒ z_flag_HC05
 320  | HC08 ⇒ z_flag_HC08
 321  | HCS08 ⇒ z_flag_HC08
 322  | RS08 ⇒ z_flag_RS08
 323  | IP2022 ⇒ z_flag_IP2022 ]
 324  (alu … s).
 325
 326 (* getter di C, esiste sempre *)
 327 ndefinition get_c_flag ≝
 328 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 329  match m
 330   return aux_get_type bool with
 331  [ HC05 ⇒ c_flag_HC05
 332  | HC08 ⇒ c_flag_HC08
 333  | HCS08 ⇒ c_flag_HC08
 334  | RS08 ⇒ c_flag_RS08
 335  | IP2022 ⇒ c_flag_IP2022 ]
 336  (alu … s).
 337
 338 (* getter di IRQ, non esiste sempre *)
 339 ndefinition get_irq_flag ≝
 340 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 341  match m
 342   return aux_get_type (option bool) with
 343  [ HC05 ⇒ λalu.Some ? (irq_flag_HC05 alu)
 344  | HC08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
 345  | HCS08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
 346  | RS08 ⇒ λalu.None ?
 347  | IP2022 ⇒ λalu.None ? ]
 348  (alu … s).