helm/software/matita/contribs/ng_assembly/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.ma".
  24
  25 (* **************** *)
  26 (* GETTER SPECIFICI *)
  27 (* **************** *)
  28
  29 (* funzione ausiliaria per il tipaggio dei getter *)
  30 ndefinition aux_get_type ≝ λx:Type.λm:mcu_type.match m with
  31  [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] → x.
  32
  33 (* REGISTRI *)
  34
  35 (* getter di A, esiste sempre *)
  36 ndefinition get_acc_8_low_reg ≝
  37 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  38  match m
  39   return aux_get_type byte8 with
  40  [ HC05 ⇒ acc_low_reg_HC05
  41  | HC08 ⇒ acc_low_reg_HC08
  42  | HCS08 ⇒ acc_low_reg_HC08
  43  | RS08 ⇒ acc_low_reg_RS08 ]
  44  (alu m t 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  (alu m t s).
  56
  57 (* getter di H, non esiste sempre *)
  58 ndefinition get_indX_8_high_reg ≝
  59 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  60  match m
  61   return aux_get_type (option byte8) with
  62  [ HC05 ⇒ λalu.None ?
  63  | HC08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
  64  | HCS08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
  65  | RS08 ⇒ λalu.None ? ]
  66  (alu m t s).
  67
  68 (* getter di H:X, non esiste sempre *)
  69 ndefinition get_indX_16_reg ≝
  70 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  71  match m
  72   return aux_get_type (option word16) with
  73  [ HC05 ⇒ λalu.None ?
  74  | HC08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
  75  | HCS08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
  76  | RS08 ⇒ λalu.None ? ]
  77  (alu m t s).
  78
  79 (* getter di SP, non esiste sempre *)
  80 ndefinition get_sp_reg ≝
  81 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  82  match m
  83   return aux_get_type (option word16) with
  84  [ HC05 ⇒ λalu.Some ? (sp_reg_HC05 alu)
  85  | HC08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
  86  | HCS08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
  87  | RS08 ⇒ λalu.None ? ]
  88  (alu m t s).
  89
  90 (* getter di PC, esiste sempre *)
  91 ndefinition get_pc_reg ≝
  92 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  93  match m
  94   return aux_get_type word16 with
  95  [ HC05 ⇒ pc_reg_HC05
  96  | HC08 ⇒ pc_reg_HC08
  97  | HCS08 ⇒ pc_reg_HC08
  98  | RS08 ⇒ pc_reg_RS08 ]
  99  (alu m t s).
 100
 101 (* getter di SPC, non esiste sempre *)
 102 ndefinition get_spc_reg ≝
 103 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 104  match m
 105   return aux_get_type (option word16) with
 106  [ HC05 ⇒ λalu.None ?
 107  | HC08 ⇒ λalu.None ?
 108  | HCS08 ⇒ λalu.None ?
 109  | RS08 ⇒ λalu.Some ? (spc_reg_RS08 alu) ]
 110  (alu m t s).
 111
 112 (* REGISTRI MEMORY MAPPED *)
 113
 114 (* getter di memory mapped X, non esiste sempre *)
 115 ndefinition get_x_map ≝
 116 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 117  match m
 118   return aux_get_type (option byte8) with
 119  [ HC05 ⇒ λalu.None ?
 120  | HC08 ⇒ λalu.None ?
 121  | HCS08 ⇒ λalu.None ?
 122  | RS08 ⇒ λalu.Some ? (x_map_RS08 alu) ]
 123  (alu m t s).
 124
 125 (* getter di memory mapped PS, non esiste sempre *)
 126 ndefinition get_ps_map ≝
 127 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 128  match m
 129   return aux_get_type (option byte8) with
 130  [ HC05 ⇒ λalu.None ?
 131  | HC08 ⇒ λalu.None ?
 132  | HCS08 ⇒ λalu.None ?
 133  | RS08 ⇒ λalu.Some ? (ps_map_RS08 alu) ]
 134  (alu m t s).
 135
 136 (* FLAG *)
 137
 138 (* getter di V, non esiste sempre *)
 139 ndefinition get_v_flag ≝
 140 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 141  match m
 142   return aux_get_type (option bool) with
 143  [ HC05 ⇒ λalu.None ?
 144  | HC08 ⇒ λalu.Some ? (v_flag_HC08 alu)
 145  | HCS08 ⇒ λalu.Some ? (v_flag_HC08 alu)
 146  | RS08 ⇒ λalu.None ? ]
 147  (alu m t s).
 148
 149 (* getter di H, non esiste sempre *)
 150 ndefinition get_h_flag ≝
 151 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 152  match m
 153   return aux_get_type (option bool) with
 154  [ HC05 ⇒ λalu.Some ? (h_flag_HC05 alu)
 155  | HC08 ⇒ λalu.Some ? (h_flag_HC08 alu)
 156  | HCS08 ⇒ λalu.Some ? (h_flag_HC08 alu)
 157  | RS08 ⇒ λalu.None ? ]
 158  (alu m t s).
 159
 160 (* getter di I, non esiste sempre *)
 161 ndefinition get_i_flag ≝
 162 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 163  match m
 164   return aux_get_type (option bool) with
 165  [ HC05 ⇒ λalu.Some ? (i_flag_HC05 alu)
 166  | HC08 ⇒ λalu.Some ? (i_flag_HC08 alu)
 167  | HCS08 ⇒ λalu.Some ? (i_flag_HC08 alu)
 168  | RS08 ⇒ λalu.None ? ]
 169  (alu m t s).
 170
 171 (* getter di N, non esiste sempre *)
 172 ndefinition get_n_flag ≝
 173 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 174  match m
 175   return aux_get_type (option bool) with
 176  [ HC05 ⇒ λalu.Some ? (n_flag_HC05 alu)
 177  | HC08 ⇒ λalu.Some ? (n_flag_HC08 alu)
 178  | HCS08 ⇒ λalu.Some ? (n_flag_HC08 alu)
 179  | RS08 ⇒ λalu.None ? ]
 180  (alu m t s).
 181
 182 (* getter di Z, esiste sempre *)
 183 ndefinition get_z_flag ≝
 184 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 185  match m
 186   return aux_get_type bool with
 187  [ HC05 ⇒ z_flag_HC05
 188  | HC08 ⇒ z_flag_HC08
 189  | HCS08 ⇒ z_flag_HC08
 190  | RS08 ⇒ z_flag_RS08 ]
 191  (alu m t s).
 192
 193 (* getter di C, esiste sempre *)
 194 ndefinition get_c_flag ≝
 195 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 196  match m
 197   return aux_get_type bool with
 198  [ HC05 ⇒ c_flag_HC05
 199  | HC08 ⇒ c_flag_HC08
 200  | HCS08 ⇒ c_flag_HC08
 201  | RS08 ⇒ c_flag_RS08 ]
 202  (alu m t s).
 203
 204 (* getter di IRQ, non esiste sempre *)
 205 ndefinition get_irq_flag ≝
 206 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 207  match m
 208   return aux_get_type (option bool) with
 209  [ HC05 ⇒ λalu.Some ? (irq_flag_HC05 alu)
 210  | HC08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
 211  | HCS08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
 212  | RS08 ⇒ λalu.None ? ]
 213  (alu m t s).