helm/software/matita/contribs/ng_assembly2/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 (* **************************************** *)
  55 (* raccordo di tutte le possibili scritture *)
  56 (* **************************************** *)
  57
  58 ndefinition multi_mode_writeb ≝
  59 λm.match m
  60     return λm.Πt.any_status m t → word16 → aux_mod_type → aux_im_type m → byte8 →
  61               option (ProdT (any_status m t) word16)
  62    with
  63     [ HC05 ⇒ Freescale_multi_mode_write_auxb HC05
  64     | HC08 ⇒ Freescale_multi_mode_write_auxb HC08
  65     | HCS08 ⇒ Freescale_multi_mode_write_auxb HCS08
  66     | RS08 ⇒ Freescale_multi_mode_write_auxb RS08
  67     | IP2022 ⇒ IP2022_multi_mode_write_auxb
  68   ].
  69
  70 ndefinition multi_mode_writew ≝
  71 λm.match m
  72     return λm.Πt.any_status m t → word16 → aux_im_type m → word16 →
  73               option (ProdT (any_status m t) word16)
  74    with
  75     [ HC05 ⇒ Freescale_multi_mode_write_auxw HC05
  76     | HC08 ⇒ Freescale_multi_mode_write_auxw HC08
  77     | HCS08 ⇒ Freescale_multi_mode_write_auxw HCS08
  78     | RS08 ⇒ Freescale_multi_mode_write_auxw RS08
  79     | IP2022 ⇒ IP2022_multi_mode_write_auxw
  80   ].