]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/ng_assembly/emulator/memory/memory_trees.ma
mod change (-x)
[helm.git] / matita / matita / contribs / ng_assembly / emulator / memory / memory_trees.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_struct.ma".
24 include "num/word32.ma".
25 include "common/option.ma".
26 include "common/list.ma".
27
28 (* ********************* *)
29 (* MEMORIA E DESCRITTORE *)
30 (* ********************* *)
31
32 ndefinition aux_32B_filler ≝
33 λT:Type.λel:T.
34 let lev8 ≝ mk_Array16T T el el el el el el el el el el el el el el el el in
35 let lev7 ≝ mk_Array16T ?
36            lev8 lev8 lev8 lev8 lev8 lev8 lev8 lev8
37            lev8 lev8 lev8 lev8 lev8 lev8 lev8 lev8
38            in
39 let lev6 ≝ mk_Array16T ?
40            lev7 lev7 lev7 lev7 lev7 lev7 lev7 lev7
41            lev7 lev7 lev7 lev7 lev7 lev7 lev7 lev7
42            in
43 let lev5 ≝ mk_Array16T ?
44            lev6 lev6 lev6 lev6 lev6 lev6 lev6 lev6
45            lev6 lev6 lev6 lev6 lev6 lev6 lev6 lev6
46            in
47 let lev4 ≝ mk_Array16T ?
48            lev5 lev5 lev5 lev5 lev5 lev5 lev5 lev5
49            lev5 lev5 lev5 lev5 lev5 lev5 lev5 lev5
50            in
51 let lev3 ≝ mk_Array16T ?
52            lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
53            lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
54            in
55 let lev2 ≝ mk_Array16T ?
56            lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
57            lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
58            in
59 let lev1 ≝ mk_Array16T ?
60            lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
61            lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
62            in
63 lev1.
64
65 ndefinition aux_32B_type ≝
66 λT:Type.Array16T (Array16T (Array16T (Array16T (Array16T (Array16T (Array16T (Array16T T))))))).
67
68 (* tutta la memoria non installata *)
69 ndefinition mt_out_of_bound_memory ≝ aux_32B_filler ? MEM_OUT_OF_BOUND.
70
71 (* tutta la memoria a 0 *)
72 ndefinition mt_zero_memory ≝ aux_32B_filler ? 〈x0,x0〉.
73
74 (* visita di un albero da 4GB di elementi: ln16(4GB)=8 passaggi *)
75 ndefinition mt_visit ≝
76 λT:Type.λdata:aux_32B_type T.λaddr:word32.
77  getn_array16T (cnL ? (cnL ? (cnL ? addr))) ?
78   (getn_array16T (cnH ? (cnL ? (cnL ? addr))) ?
79    (getn_array16T (cnL ? (cnH ? (cnL ? addr))) ?
80     (getn_array16T (cnH ? (cnH ? (cnL ? addr))) ?
81      (getn_array16T (cnL ? (cnL ? (cnH ? addr))) ?
82       (getn_array16T (cnH ? (cnL ? (cnH ? addr))) ?
83        (getn_array16T (cnL ? (cnH ? (cnH ? addr))) ?
84         (getn_array16T (cnH ? (cnH ? (cnH ? addr))) ? data))))))).
85
86 (* scrittura di un elemento in un albero da 4GB *)
87 ndefinition mt_update ≝
88 λT:Type.λdata:aux_32B_type T.λaddr:word32.λv:T.
89  let lev2 ≝ getn_array16T (cnH ? (cnH ? (cnH ? addr))) ? data in
90  let lev3 ≝ getn_array16T (cnL ? (cnH ? (cnH ? addr))) ? lev2 in
91  let lev4 ≝ getn_array16T (cnH ? (cnL ? (cnH ? addr))) ? lev3 in
92  let lev5 ≝ getn_array16T (cnL ? (cnL ? (cnH ? addr))) ? lev4 in
93  let lev6 ≝ getn_array16T (cnH ? (cnH ? (cnL ? addr))) ? lev5 in
94  let lev7 ≝ getn_array16T (cnL ? (cnH ? (cnL ? addr))) ? lev6 in
95  let lev8 ≝ getn_array16T (cnH ? (cnL ? (cnL ? addr))) ? lev7 in
96
97  setn_array16T (cnH ? (cnH ? (cnH ? addr))) ? data
98   (setn_array16T (cnL ? (cnH ? (cnH ? addr))) ? lev2
99    (setn_array16T (cnH ? (cnL ? (cnH ? addr))) ? lev3
100     (setn_array16T (cnL ? (cnL ? (cnH ? addr))) ? lev4
101      (setn_array16T (cnH ? (cnH ? (cnL ? addr))) ? lev5
102       (setn_array16T (cnL ? (cnH ? (cnL ? addr))) ? lev6
103        (setn_array16T (cnH ? (cnL ? (cnL ? addr))) ? lev7
104         (setn_array16T (cnL ? (cnL ? (cnL ? addr))) T lev8 v))))))).
105
106 (* scrittura di un range (max 64KB) in un albero da 4GB *)
107 nlet rec mt_update_ranged (T:Type) (data:aux_32B_type T) (addr:word32) (w:word16) (rw:rec_word16 w) (v:T) on rw ≝
108  match rw with
109   [ w16_O ⇒ data
110   | w16_S w' rw' ⇒ mt_update_ranged T (mt_update T data addr v)
111                                     (succ_w32 addr) w' rw' v
112   ].
113
114 (* scrivi controllando il tipo di memoria *)
115 ndefinition mt_mem_update ≝
116 λmem:aux_32B_type byte8.
117 λchk:aux_32B_type memory_type.
118 λaddr:word32.λv:byte8.
119  match mt_visit ? chk addr with
120   (* ROM? ok, ma il valore viene perso *)
121   [ MEM_READ_ONLY ⇒ Some ? mem
122   (* RAM? ok *)
123   | MEM_READ_WRITE ⇒ Some ? (mt_update ? mem addr v)
124   (* NON INSTALLATA? no *)
125   | MEM_OUT_OF_BOUND ⇒ None ? ].  
126
127 (* leggi controllando il tipo di memoria *)
128 ndefinition mt_mem_read ≝
129 λmem:aux_32B_type byte8.
130 λchk:aux_32B_type memory_type.
131 λaddr:word32.
132  match mt_visit ? chk addr with
133   [ MEM_READ_ONLY ⇒ Some ? (mt_visit ? mem addr)
134   | MEM_READ_WRITE ⇒ Some ? (mt_visit ? mem addr)
135   | MEM_OUT_OF_BOUND ⇒ None ? ].
136
137 (* ************************** *)
138 (* CARICAMENTO PROGRAMMA/DATI *)
139 (* ************************** *)
140
141 (* carica a paratire da addr, overflow se si supera 0xFFFF... *)
142 nlet rec mt_load_from_source_at (old_mem:aux_32B_type byte8)
143                                 (src:list byte8) (addr:word32) on src ≝
144  match src with
145   (* fine di source: carica da old_mem *)
146   [ nil ⇒ old_mem
147   | cons hd tl ⇒ mt_load_from_source_at (mt_update ? old_mem addr hd) tl (succ_w32 addr)
148   ].