]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/ng_assembly2/emulator/memory/memory_bits.ma
wip ....
[helm.git] / matita / matita / contribs / ng_assembly2 / emulator / memory / memory_bits.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/memory/memory_trees.ma".
24
25 (* ********************* *)
26 (* MEMORIA E DESCRITTORE *)
27 (* ********************* *)
28
29 (* tutta la memoria non installata *)
30 ndefinition mb_out_of_bound_memory ≝
31  aux_20B_filler ?
32   (mk_Array8T ? MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
33                 MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND).
34
35 (* tutta la memoria a 0 *)
36 ndefinition mb_zero_memory ≝
37  aux_20B_filler ? (mk_Array8T ? false false false false false false false false).
38
39 (* scrivi bit controllando il tipo di memoria *)
40 ndefinition mb_mem_update_bit ≝
41 λmem:aux_20B_type (Array8T bool).
42 λchk:aux_20B_type (Array8T memory_type).
43 λsel:oct.λaddr:word16.λsub:oct.λv:bool.
44  match getn_array8T sub ? (mt_visit ? chk sel addr) with
45   (* ROM? ok, ma il valore viene perso *)
46   [ MEM_READ_ONLY ⇒ Some ? mem
47   (* RAM? ok *)
48   | MEM_READ_WRITE ⇒ Some ? (mt_update ? mem sel addr (setn_array8T sub ? (mt_visit ? mem sel addr) v))
49   (* NON INSTALLATA? no *)
50   | MEM_OUT_OF_BOUND ⇒ None ? ].
51
52 ndefinition mb_mem_update ≝
53 λmem:aux_20B_type (Array8T bool).
54 λchk:aux_20B_type (Array8T memory_type).
55 λsel:oct.λaddr:word16.λv:byte8.
56 let old_value ≝ mt_visit (Array8T bool) mem sel addr in
57 let new_value ≝ bits_of_byte8 v in
58 let memtypes ≝ mt_visit (Array8T memory_type) chk sel addr in
59 let newbit0 ≝ match getn_array8T o0 memory_type memtypes with
60  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o0 bool old_value)
61  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o0 bool new_value)
62  | MEM_OUT_OF_BOUND ⇒ None bool ] in
63 let newbit1 ≝ match getn_array8T o1 memory_type memtypes with
64  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o1 bool old_value)
65  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o1 bool new_value)
66  | MEM_OUT_OF_BOUND ⇒ None bool ] in
67 let newbit2 ≝ match getn_array8T o2 memory_type memtypes with
68  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o2 bool old_value)
69  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o2 bool new_value)
70  | MEM_OUT_OF_BOUND ⇒ None bool ] in
71 let newbit3 ≝ match getn_array8T o3 memory_type memtypes with
72  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o3 bool old_value)
73  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o3 bool new_value)
74  | MEM_OUT_OF_BOUND ⇒ None bool ] in
75 let newbit4 ≝ match getn_array8T o4 memory_type memtypes with
76  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o4 bool old_value)
77  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o4 bool new_value)
78  | MEM_OUT_OF_BOUND ⇒ None bool ] in
79 let newbit5 ≝ match getn_array8T o5 memory_type memtypes with
80  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o5 bool old_value)
81  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o5 bool new_value)
82  | MEM_OUT_OF_BOUND ⇒ None bool ] in
83 let newbit6 ≝ match getn_array8T o6 memory_type memtypes with
84  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o6 bool old_value)
85  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o6 bool new_value)
86  | MEM_OUT_OF_BOUND ⇒ None bool ] in
87 let newbit7 ≝ match getn_array8T o7 memory_type memtypes with
88  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o7 bool old_value)
89  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o7 bool new_value)
90  | MEM_OUT_OF_BOUND ⇒ None bool ] in
91        opt_map … newbit0
92  (λnb0.opt_map … newbit1
93  (λnb1.opt_map … newbit2
94  (λnb2.opt_map … newbit3
95  (λnb3.opt_map … newbit4
96  (λnb4.opt_map … newbit5
97  (λnb5.opt_map … newbit6
98  (λnb6.opt_map … newbit7
99  (λnb7.Some ? (mt_update ? mem sel addr (mk_Array8T bool nb7 nb6 nb5 nb4 nb3 nb2 nb1 nb0)))))))))).
100
101 (* scrivi tipo di bit *)
102 ndefinition mb_chk_update_bit ≝
103 λchk:aux_20B_type (Array8T memory_type).
104 λsel:oct.λaddr:word16.λsub:oct.λv:memory_type.
105  mt_update ? chk sel addr (setn_array8T sub ? (mt_visit ? chk sel addr) v).
106
107 (* leggi bit controllando il tipo di memoria *)
108 ndefinition mb_mem_read_bit ≝
109 λmem:aux_20B_type (Array8T bool).
110 λchk:aux_20B_type (Array8T memory_type).
111 λsel:oct.λaddr:word16.λsub:oct.
112  match getn_array8T sub ? (mt_visit ? chk sel addr) with
113   (* ROM? ok, ma il valore viene perso *)
114   [ MEM_READ_ONLY ⇒ Some ? (getn_array8T sub ? (mt_visit ? mem sel addr))
115   (* RAM? ok *)
116   | MEM_READ_WRITE ⇒ Some ? (getn_array8T sub ? (mt_visit ? mem sel addr))
117   (* NON INSTALLATA? no *)
118   | MEM_OUT_OF_BOUND ⇒ None ? ]. 
119
120 (* leggi controllando il tipo di memoria *)
121 (* NB: devono esistere tutti i bit *)
122 ndefinition mb_mem_read ≝
123 λmem:aux_20B_type (Array8T bool).
124 λchk:aux_20B_type (Array8T memory_type).
125 λsel:oct.λaddr:word16.
126 let value ≝ mt_visit (Array8T bool) mem sel addr in
127 let memtypes ≝ mt_visit (Array8T memory_type) chk sel addr in
128 let newbit0 ≝ match getn_array8T o0 memory_type memtypes with
129  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o0 bool value)
130  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o0 bool value)
131  | MEM_OUT_OF_BOUND ⇒ None bool ] in
132 let newbit1 ≝ match getn_array8T o1 memory_type memtypes with
133  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o1 bool value)
134  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o1 bool value)
135  | MEM_OUT_OF_BOUND ⇒ None bool ] in
136 let newbit2 ≝ match getn_array8T o2 memory_type memtypes with
137  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o2 bool value)
138  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o2 bool value)
139  | MEM_OUT_OF_BOUND ⇒ None bool ] in
140 let newbit3 ≝ match getn_array8T o3 memory_type memtypes with
141  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o3 bool value)
142  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o3 bool value)
143  | MEM_OUT_OF_BOUND ⇒ None bool ] in
144 let newbit4 ≝ match getn_array8T o4 memory_type memtypes with
145  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o4 bool value)
146  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o4 bool value)
147  | MEM_OUT_OF_BOUND ⇒ None bool ] in
148 let newbit5 ≝ match getn_array8T o5 memory_type memtypes with
149  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o5 bool value)
150  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o5 bool value)
151  | MEM_OUT_OF_BOUND ⇒ None bool ] in
152 let newbit6 ≝ match getn_array8T o6 memory_type memtypes with
153  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o6 bool value)
154  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o6 bool value)
155  | MEM_OUT_OF_BOUND ⇒ None bool ] in
156 let newbit7 ≝ match getn_array8T o7 memory_type memtypes with
157  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o7 bool value)
158  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o7 bool value)
159  | MEM_OUT_OF_BOUND ⇒ None bool ] in
160        opt_map … newbit0
161  (λnb0.opt_map … newbit1
162  (λnb1.opt_map … newbit2
163  (λnb2.opt_map … newbit3
164  (λnb3.opt_map … newbit4
165  (λnb4.opt_map … newbit5
166  (λnb5.opt_map … newbit6
167  (λnb6.opt_map … newbit7
168  (λnb7.Some ? (byte8_of_bits (mk_Array8T bool nb7 nb6 nb5 nb4 nb3 nb2 nb1 nb0)))))))))).
169
170 (* ************************** *)
171 (* CARICAMENTO PROGRAMMA/DATI *)
172 (* ************************** *)
173
174 (* carica a paratire da addr, scartando source (pescando da old_mem) se si supera 0xFFFF... *)
175 nlet rec mb_load_from_source_at (old_mem:aux_20B_type (Array8T bool))
176                                 (src:list byte8) (sel:oct) (addr:word16) on src ≝
177  match src with
178   (* fine di source: carica da old_mem *)
179   [ nil ⇒ old_mem
180   | cons hd tl ⇒ mb_load_from_source_at (mt_update ? old_mem sel addr (bits_of_byte8 hd))
181                                         tl sel (succc ? addr)
182   ].