]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/contribs/ng_assembly2/emulator/read_write/load_write.ma
wip ....
[helm.git] / matitaB / 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   ].