1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "emulator/memory/memory_func.ma".
24 include "emulator/memory/memory_trees.ma".
25 include "emulator/memory/memory_bits.ma".
27 (* ********************************************* *)
28 (* ASTRAZIONE DALL'IMPLEMENTAZIONE DELLA MEMORIA *)
29 (* ********************************************* *)
31 (* se si disattiva l'implementazione a funzione
32 la memoria diventa un'oggetto confrontabile! *)
34 (* tipi di implementazione della memoria *)
35 ninductive memory_impl : Type ≝
36 (*MEM_FUNC: memory_impl
37 |*) MEM_TREE: memory_impl
38 | MEM_BITS: memory_impl.
40 (* ausiliario per il tipo della memoria *)
41 ndefinition aux_mem_type ≝
42 λt:memory_impl.match t with
43 [ (*MEM_FUNC ⇒ oct → word16 → byte8
44 |*) MEM_TREE ⇒ aux_20B_type byte8
45 | MEM_BITS ⇒ aux_20B_type (Array8T bool)
48 (* ausiliario per il tipo del checker *)
49 ndefinition aux_chk_type ≝
50 λt:memory_impl.match t with
51 [ (*MEM_FUNC ⇒ oct → word16 → memory_type
52 |*) MEM_TREE ⇒ aux_20B_type memory_type
53 | MEM_BITS ⇒ aux_20B_type (Array8T memory_type)
56 (* unificazione di out_of_bound_memory *)
57 ndefinition out_of_bound_memory ≝
60 return λt.aux_chk_type t
62 [ (*MEM_FUNC ⇒ mf_out_of_bound_memory
63 |*) MEM_TREE ⇒ mt_out_of_bound_memory
64 | MEM_BITS ⇒ mb_out_of_bound_memory
67 (* unificazione di zero_memory *)
68 ndefinition zero_memory ≝
71 return λt.aux_mem_type t
73 [ (*MEM_FUNC ⇒ mf_zero_memory
74 |*) MEM_TREE ⇒ mt_zero_memory
75 | MEM_BITS ⇒ mb_zero_memory
78 (* unificazione della lettura senza chk: mem_read_abs mem addr *)
79 ndefinition mem_read_abs ≝
82 return λt.aux_mem_type t → oct → word16 → byte8
84 [ (*MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
86 |*) MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
88 | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
89 λsel:oct.λaddr:word16.
90 byte8_of_bits (mt_visit ? m sel addr)
93 (* unificazione del chk *)
97 return λt.aux_chk_type t → oct → word16 → Array8T memory_type
99 [ (*MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.λsel:oct.λaddr:word16.
100 match c sel addr with
101 [ MEM_READ_ONLY ⇒ mk_Array8T ? MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY
102 | MEM_READ_WRITE ⇒ mk_Array8T ? MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE
103 | MEM_OUT_OF_BOUND ⇒ mk_Array8T ? MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
105 |*) MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.λsel:oct.λaddr:word16.
106 match mt_visit ? c sel addr with
107 [ MEM_READ_ONLY ⇒ mk_Array8T ? MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY
108 | MEM_READ_WRITE ⇒ mk_Array8T ? MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE
109 | MEM_OUT_OF_BOUND ⇒ mk_Array8T ? MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
111 | MEM_BITS ⇒ mt_visit ?
114 (* unificazione della lettura con chk: mem_read mem chk addr *)
115 ndefinition mem_read ≝
118 return λt.aux_mem_type t → aux_chk_type t → oct → word16 → option byte8
120 [ (*MEM_FUNC ⇒ mf_mem_read
121 |*) MEM_TREE ⇒ mt_mem_read
122 | MEM_BITS ⇒ mb_mem_read
125 (* unificazione della lettura di bit con chk: mem_read mem chk addr sub *)
126 ndefinition mem_read_bit ≝
129 return λt.aux_mem_type t → aux_chk_type t → oct → word16 → oct → option bool
131 [ (*MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
132 λc:aux_chk_type MEM_FUNC.
133 λsel:oct.λaddr:word16.
135 opt_map … (mf_mem_read m c sel addr)
136 (λb.Some ? (getn_array8T o bool (bits_of_byte8 b)))
137 |*) MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
138 λc:aux_chk_type MEM_TREE.
139 λsel:oct.λaddr:word16.
141 opt_map … (mt_mem_read m c sel addr)
142 (λb.Some ? (getn_array8T o bool (bits_of_byte8 b)))
143 | MEM_BITS ⇒ mb_mem_read_bit
146 (* unificazione della scrittura con chk: mem_update mem chk addr val *)
147 ndefinition mem_update ≝
150 return λt.aux_mem_type t → aux_chk_type t → oct → word16 → byte8 → option (aux_mem_type t)
152 [ (*MEM_FUNC ⇒ mf_mem_update
153 |*) MEM_TREE ⇒ mt_mem_update
154 | MEM_BITS ⇒ mb_mem_update
157 (* unificazione della scrittura di bit con chk: mem_update mem chk addr sub val *)
158 ndefinition mem_update_bit ≝
161 return λt.aux_mem_type t → aux_chk_type t → oct → word16 → oct → bool → option (aux_mem_type t)
163 [ (*MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
164 λc:aux_chk_type MEM_FUNC.
165 λsel:oct.λaddr:word16.
168 mf_mem_update m c sel addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 (m addr)) v))
169 |*) MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
170 λc:aux_chk_type MEM_TREE.
171 λsel:oct.λaddr:word16.
174 mt_mem_update m c sel addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 (mt_visit ? m sel addr)) v))
175 | MEM_BITS ⇒ mb_mem_update_bit
178 (* unificazione del caricamento: load_from_source_at old_mem source addr *)
179 ndefinition load_from_source_at ≝
182 return λt.aux_mem_type t → list byte8 → oct → word16 → aux_mem_type t
184 [ (*MEM_FUNC ⇒ mf_load_from_source_at
185 |*) MEM_TREE ⇒ mt_load_from_source_at
186 | MEM_BITS ⇒ mb_load_from_source_at
189 (* unificazione dell'impostazione della memoria: chk_update_ranged chk inf sup v *)
190 ndefinition check_update_ranged ≝
193 return λt.aux_chk_type t → oct → word16 → word16 → memory_type → aux_chk_type t
195 [ (*MEM_FUNC ⇒ mf_check_update_ranged
196 |*) MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.
197 λsel:oct.λaddr:word16.
199 mt_update_ranged ? c sel addr ? (w16_to_recw16 range)
200 | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS.
201 λsel:oct.λaddr:word16.
204 mt_update_ranged ? c sel addr ? (w16_to_recw16 range) (mk_Array8T ? v v v v v v v v)
207 (* unificazione dell'impostazione dei bit: chk_update_bit chk addr sub v *)
208 (* NB: dove non esiste la granularita' del bit, lascio inalterato *)
209 ndefinition check_update_bit ≝
212 return λt.aux_chk_type t → oct → word16 → oct → memory_type → aux_chk_type t
214 [ (*MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.
215 λsel:oct.λaddr:word16.
219 |*) MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.
220 λsel:oct.λaddr:word16.
224 | MEM_BITS ⇒ mb_chk_update_bit
227 ndefinition mem_is_comparable: memory_impl → comparable.
228 #m; @ (aux_mem_type m)
230 ##[ napply mt_zero_memory
231 ##| napply mb_zero_memory ##]
233 ##[ napply (forallc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable byte8_is_comparable))))))
234 ##| napply (forallc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable bool_is_comparable))))))) ##]
236 ##[ napply (eqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable byte8_is_comparable))))))
237 ##| napply (eqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable bool_is_comparable))))))) ##]
239 ##[ napply (eqc_to_eq (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable byte8_is_comparable))))))
240 ##| napply (eqc_to_eq (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable bool_is_comparable))))))) ##]
242 ##[ napply (eq_to_eqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable byte8_is_comparable))))))
243 ##| napply (eq_to_eqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable bool_is_comparable))))))) ##]
245 ##[ napply (neqc_to_neq (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable byte8_is_comparable))))))
246 ##| napply (neqc_to_neq (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable bool_is_comparable))))))) ##]
248 ##[ napply (neq_to_neqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable byte8_is_comparable))))))
249 ##| napply (neq_to_neqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable bool_is_comparable))))))) ##]
251 ##[ napply (decidable_c (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable byte8_is_comparable))))))
252 ##| napply (decidable_c (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable bool_is_comparable))))))) ##]
254 ##[ napply (symmetric_eqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable byte8_is_comparable))))))
255 ##| napply (symmetric_eqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable bool_is_comparable))))))) ##]
259 unification hint 0 ≔ M:memory_impl ⊢ carr (mem_is_comparable M) ≡ aux_mem_type M.
261 ndefinition chk_is_comparable: memory_impl → comparable.
262 #m; @ (aux_chk_type m)
264 ##[ napply mt_out_of_bound_memory
265 ##| napply mb_out_of_bound_memory ##]
267 ##[ napply (forallc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable memorytype_is_comparable))))))
268 ##| napply (forallc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable memorytype_is_comparable))))))) ##]
270 ##[ napply (eqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable memorytype_is_comparable))))))
271 ##| napply (eqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable memorytype_is_comparable))))))) ##]
273 ##[ napply (eqc_to_eq (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable memorytype_is_comparable))))))
274 ##| napply (eqc_to_eq (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable memorytype_is_comparable))))))) ##]
276 ##[ napply (eq_to_eqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable memorytype_is_comparable))))))
277 ##| napply (eq_to_eqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable memorytype_is_comparable))))))) ##]
279 ##[ napply (neqc_to_neq (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable memorytype_is_comparable))))))
280 ##| napply (neqc_to_neq (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable memorytype_is_comparable))))))) ##]
282 ##[ napply (neq_to_neqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable memorytype_is_comparable))))))
283 ##| napply (neq_to_neqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable memorytype_is_comparable))))))) ##]
285 ##[ napply (decidable_c (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable memorytype_is_comparable))))))
286 ##| napply (decidable_c (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable memorytype_is_comparable))))))) ##]
288 ##[ napply (symmetric_eqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable memorytype_is_comparable))))))
289 ##| napply (symmetric_eqc (ar8_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar16_is_comparable (ar8_is_comparable memorytype_is_comparable))))))) ##]
293 unification hint 0 ≔ M:memory_impl ⊢ carr (chk_is_comparable M) ≡ aux_chk_type M.