helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write.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/read_write/Freescale_load_write.ma".
  24 include "emulator/read_write/IP2022_load_write.ma".
  25
  26 (* ************************************** *)
  27 (* raccordo di tutte le possibili letture *)
  28 (* ************************************** *)
  29
  30 ndefinition multi_mode_loadb ≝
  31 λm.match m
  32     return λm.Πt.any_status m t → word16 → aux_im_type m →
  33               option (Prod3T (any_status m t) byte8 word16)
  34    with
  35     [ HC05 ⇒ Freescale_multi_mode_load_auxb HC05
  36     | HC08 ⇒ Freescale_multi_mode_load_auxb HC08
  37     | HCS08 ⇒ Freescale_multi_mode_load_auxb HCS08
  38     | RS08 ⇒ Freescale_multi_mode_load_auxb RS08
  39     | IP2022 ⇒ IP2022_multi_mode_load_auxb
  40   ].
  41
  42 ndefinition multi_mode_loadw ≝
  43 λm.match m
  44     return λm.Πt.any_status m t → word16 → aux_im_type m →
  45                  option (Prod3T (any_status m t) word16 word16)
  46    with
  47     [ HC05 ⇒ Freescale_multi_mode_load_auxw HC05
  48     | HC08 ⇒ Freescale_multi_mode_load_auxw HC08
  49     | HCS08 ⇒ Freescale_multi_mode_load_auxw HCS08
  50     | RS08 ⇒ Freescale_multi_mode_load_auxw RS08
  51     | IP2022 ⇒ IP2022_multi_mode_load_auxw
  52   ].
  53
  54 (* tutte le modalita' di lettura: false=loadb true=loadw *)
  55
  56 (* **************************************** *)
  57 (* raccordo di tutte le possibili scritture *)
  58 (* **************************************** *)
  59
  60 ndefinition multi_mode_writeb ≝
  61 λm.match m
  62     return λm.Πt.any_status m t → word16 → aux_im_type m → byte8 →
  63               option (ProdT (any_status m t) word16)
  64    with
  65     [ HC05 ⇒ Freescale_multi_mode_write_auxb HC05
  66     | HC08 ⇒ Freescale_multi_mode_write_auxb HC08
  67     | HCS08 ⇒ Freescale_multi_mode_write_auxb HCS08
  68     | RS08 ⇒ Freescale_multi_mode_write_auxb RS08
  69     | IP2022 ⇒ IP2022_multi_mode_write_auxb
  70   ].
  71
  72 ndefinition multi_mode_writew ≝
  73 λm.match m
  74     return λm.Πt.any_status m t → word16 → aux_im_type m → word16 →
  75               option (ProdT (any_status m t) word16)
  76    with
  77     [ HC05 ⇒ Freescale_multi_mode_write_auxw HC05
  78     | HC08 ⇒ Freescale_multi_mode_write_auxw HC08
  79     | HCS08 ⇒ Freescale_multi_mode_write_auxw HCS08
  80     | RS08 ⇒ Freescale_multi_mode_write_auxw RS08
  81     | IP2022 ⇒ IP2022_multi_mode_write_auxw
  82   ].