]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/assembly/freescale/memory_bits.ma
- lambda: some parts commented out, some refactoring
[helm.git] / matita / matita / contribs / assembly / freescale / 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:                                                         *)
19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
20 (*                                                                        *)
21 (* Questo materiale fa parte della tesi:                                  *)
22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
23 (*                                                                        *)
24 (*                    data ultima modifica 15/11/2007                     *)
25 (* ********************************************************************** *)
26
27 include "freescale/memory_trees.ma".
28
29 (* ********************* *)
30 (* MEMORIA E DESCRITTORE *)
31 (* ********************* *)
32
33 (* tutta la memoria non installata *)
34 definition mb_out_of_bound_memory ≝
35 let base ≝ array_8T memory_type MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
36                                 MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND in
37 let lev4 ≝ array_16T ? 
38            base base base base base base base base
39            base base base base base base base base
40            in
41 let lev3 ≝ array_16T ?
42            lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
43            lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
44            in
45 let lev2 ≝ array_16T ?
46            lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
47            lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
48            in
49 let lev1 ≝ array_16T ?
50            lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
51            lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
52            in
53 lev1.
54
55 (* tutta la memoria a 0 *)
56 definition mb_zero_memory ≝
57 let base ≝ array_8T bool false false false false false false false false in
58 let lev4 ≝ array_16T ? 
59            base base base base base base base base
60            base base base base base base base base
61            in
62 let lev3 ≝ array_16T ?
63            lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
64            lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
65            in
66 let lev2 ≝ array_16T ?
67            lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
68            lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
69            in
70 let lev1 ≝ array_16T ?
71            lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
72            lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
73            in
74 lev1.
75
76 (* scrivi bit controllando il tipo di memoria *)
77 definition mb_mem_update_bit ≝
78 λmem:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T bool)))).
79 λchk:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T memory_type)))).
80 λaddr:word16.λsub:oct.λv:bool.
81  match getn_array8T sub memory_type (mt_visit (Prod8T memory_type) chk addr) with
82   (* ROM? ok, ma il valore viene perso *)
83   [ MEM_READ_ONLY ⇒ Some ? mem
84   (* RAM? ok *)
85   | MEM_READ_WRITE ⇒ Some ? (mt_update (Prod8T bool) mem addr (setn_array8T sub bool (mt_visit (Prod8T bool) mem addr) v))
86   (* NON INSTALLATA? no *)
87   | MEM_OUT_OF_BOUND ⇒ None ? ].
88
89 (* scrivi tipo di bit *)
90 definition mb_chk_update_bit ≝
91 λchk:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T memory_type)))).
92 λaddr:word16.λsub:oct.λv:memory_type.
93  mt_update (Prod8T memory_type) chk addr (setn_array8T sub memory_type (mt_visit (Prod8T memory_type) chk addr) v).
94
95 (* leggi bit controllando il tipo di memoria *)
96 definition mb_mem_read_bit ≝
97 λmem:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T bool)))).
98 λchk:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T memory_type)))).
99 λaddr:word16.λsub:oct.
100  match getn_array8T sub memory_type (mt_visit (Prod8T memory_type) chk addr) with
101   (* ROM? ok, ma il valore viene perso *)
102   [ MEM_READ_ONLY ⇒ Some ? (getn_array8T sub bool (mt_visit (Prod8T bool) mem addr))
103   (* RAM? ok *)
104   | MEM_READ_WRITE ⇒ Some ? (getn_array8T sub bool (mt_visit (Prod8T bool) mem addr))
105   (* NON INSTALLATA? no *)
106   | MEM_OUT_OF_BOUND ⇒ None ? ]. 
107
108 definition mb_chk_get ≝
109 λchk:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T memory_type)))).λaddr:word16.
110 let c ≝ mt_visit (Prod8T memory_type) chk addr in
111 array_8T ? (getn_array8T o7 ? c) (getn_array8T o6 ? c)
112            (getn_array8T o5 ? c) (getn_array8T o4 ? c)
113            (getn_array8T o3 ? c) (getn_array8T o2 ? c)
114            (getn_array8T o1 ? c) (getn_array8T o0 ? c).
115
116 (* scrivi controllando il tipo di memoria *)
117 (* NB: devono esistere tutti i bit *)
118 definition mb_mem_update ≝
119 λmem:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T bool)))).
120 λchk:Prod8T memory_type.
121 λaddr:word16.λv:byte8.
122 let old_value ≝ mt_visit (Prod8T bool) mem addr in
123 let new_value ≝ bits_of_byte8 v in
124 let newbit0 ≝ match getn_array8T o0 memory_type chk with
125  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o0 bool old_value)
126  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o0 bool new_value)
127  | MEM_OUT_OF_BOUND ⇒ None bool ] in
128 let newbit1 ≝ match getn_array8T o1 memory_type chk with
129  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o1 bool old_value)
130  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o1 bool new_value)
131  | MEM_OUT_OF_BOUND ⇒ None bool ] in
132 let newbit2 ≝ match getn_array8T o2 memory_type chk with
133  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o2 bool old_value)
134  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o2 bool new_value)
135  | MEM_OUT_OF_BOUND ⇒ None bool ] in
136 let newbit3 ≝ match getn_array8T o3 memory_type chk with
137  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o3 bool old_value)
138  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o3 bool new_value)
139  | MEM_OUT_OF_BOUND ⇒ None bool ] in
140 let newbit4 ≝ match getn_array8T o4 memory_type chk with
141  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o4 bool old_value)
142  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o4 bool new_value)
143  | MEM_OUT_OF_BOUND ⇒ None bool ] in
144 let newbit5 ≝ match getn_array8T o5 memory_type chk with
145  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o5 bool old_value)
146  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o5 bool new_value)
147  | MEM_OUT_OF_BOUND ⇒ None bool ] in
148 let newbit6 ≝ match getn_array8T o6 memory_type chk with
149  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o6 bool old_value)
150  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o6 bool new_value)
151  | MEM_OUT_OF_BOUND ⇒ None bool ] in
152 let newbit7 ≝ match getn_array8T o7 memory_type chk with
153  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o7 bool old_value)
154  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o7 bool new_value)
155  | MEM_OUT_OF_BOUND ⇒ None bool ] in
156        opt_map ?? newbit0
157  (λnb0.opt_map ?? newbit1
158  (λnb1.opt_map ?? newbit2
159  (λnb2.opt_map ?? newbit3
160  (λnb3.opt_map ?? newbit4
161  (λnb4.opt_map ?? newbit5
162  (λnb5.opt_map ?? newbit6
163  (λnb6.opt_map ?? newbit7
164  (λnb7.Some ? (mt_update (Prod8T bool) mem addr (array_8T bool nb7 nb6 nb5 nb4 nb3 nb2 nb1 nb0)))))))))).
165
166 (* leggi controllando il tipo di memoria *)
167 (* NB: devono esistere tutti i bit *)
168 definition mb_mem_read ≝
169 λmem:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T bool)))).
170 λchk:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T memory_type)))).
171 λaddr:word16.
172 let bit_types ≝ mt_visit (Prod8T memory_type) chk addr in
173 let value ≝ mt_visit (Prod8T bool) mem addr in
174 let newbit0 ≝ match getn_array8T o0 memory_type bit_types with
175  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o0 bool value)
176  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o0 bool value)
177  | MEM_OUT_OF_BOUND ⇒ None bool ] in
178 let newbit1 ≝ match getn_array8T o1 memory_type bit_types with
179  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o1 bool value)
180  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o1 bool value)
181  | MEM_OUT_OF_BOUND ⇒ None bool ] in
182 let newbit2 ≝ match getn_array8T o2 memory_type bit_types with
183  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o2 bool value)
184  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o2 bool value)
185  | MEM_OUT_OF_BOUND ⇒ None bool ] in
186 let newbit3 ≝ match getn_array8T o3 memory_type bit_types with
187  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o3 bool value)
188  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o3 bool value)
189  | MEM_OUT_OF_BOUND ⇒ None bool ] in
190 let newbit4 ≝ match getn_array8T o4 memory_type bit_types with
191  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o4 bool value)
192  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o4 bool value)
193  | MEM_OUT_OF_BOUND ⇒ None bool ] in
194 let newbit5 ≝ match getn_array8T o5 memory_type bit_types with
195  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o5 bool value)
196  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o5 bool value)
197  | MEM_OUT_OF_BOUND ⇒ None bool ] in
198 let newbit6 ≝ match getn_array8T o6 memory_type bit_types with
199  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o6 bool value)
200  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o6 bool value)
201  | MEM_OUT_OF_BOUND ⇒ None bool ] in
202 let newbit7 ≝ match getn_array8T o7 memory_type bit_types with
203  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o7 bool value)
204  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o7 bool value)
205  | MEM_OUT_OF_BOUND ⇒ None bool ] in
206        opt_map ?? newbit0
207  (λnb0.opt_map ?? newbit1
208  (λnb1.opt_map ?? newbit2
209  (λnb2.opt_map ?? newbit3
210  (λnb3.opt_map ?? newbit4
211  (λnb4.opt_map ?? newbit5
212  (λnb5.opt_map ?? newbit6
213  (λnb6.opt_map ?? newbit7
214  (λnb7.Some ? (byte8_of_bits (array_8T bool nb7 nb6 nb5 nb4 nb3 nb2 nb1 nb0)))))))))).
215
216 (* ************************** *)
217 (* CARICAMENTO PROGRAMMA/DATI *)
218 (* ************************** *)
219
220 (* carica a paratire da addr, scartando source (pescando da old_mem) se si supera 0xFFFF... *)
221 let rec mb_load_from_source_at (old_mem:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T bool)))))
222                                (source:list byte8) (addr:word16) on source ≝
223 match source with
224  (* fine di source: carica da old_mem *)
225  [ nil ⇒ old_mem
226  | cons hd tl ⇒ match lt_w16 addr 〈〈xF,xF〉:〈xF,xF〉〉 with
227   (* non supera 0xFFFF, ricorsione *)
228   [ true ⇒ mb_load_from_source_at (mt_update ? old_mem addr (bits_of_byte8 hd)) tl (plus_w16nc addr 〈〈x0,x0〉:〈x0,x1〉〉)
229   (* supera 0xFFFF, niente ricorsione *)
230   | false ⇒ mt_update ? old_mem addr (bits_of_byte8 hd)
231   ]].