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 (* ********************************************************************** *)
24 include "num/byte8.ma".
26 (* **************************** *)
27 (* TIPI PER I MODULI DI MEMORIA *)
28 (* **************************** *)
30 (* tipi di memoria:RAM/ROM/non installata *)
31 ninductive memory_type : Type ≝
32 MEM_READ_ONLY: memory_type
33 | MEM_READ_WRITE: memory_type
34 | MEM_OUT_OF_BOUND: memory_type.
36 (* **************** *)
37 (* TIPO ARRAY DA 16 *)
38 (* **************** *)
40 (* definizione di un array omogeneo di dimensione 16 *)
41 nrecord Array16T (T:Type) : Type ≝
42 { a16_1 : T ; a16_2 : T ; a16_3 : T ; a16_4 : T
43 ; a16_5 : T ; a16_6 : T ; a16_7 : T ; a16_8 : T
44 ; a16_9 : T ; a16_10 : T ; a16_11 : T ; a16_12 : T
45 ; a16_13 : T ; a16_14 : T ; a16_15 : T ; a16_16 : T }.
47 (* operatore uguaglianza *)
49 λT.λf:T → T → bool.λa1,a2:Array16T T.
50 (f (a16_1 ? a1) (a16_1 ? a2)) ⊗ (f (a16_2 ? a1) (a16_2 ? a2)) ⊗
51 (f (a16_3 ? a1) (a16_3 ? a2)) ⊗ (f (a16_4 ? a1) (a16_4 ? a2)) ⊗
52 (f (a16_5 ? a1) (a16_5 ? a2)) ⊗ (f (a16_6 ? a1) (a16_6 ? a2)) ⊗
53 (f (a16_7 ? a1) (a16_7 ? a2)) ⊗ (f (a16_8 ? a1) (a16_8 ? a2)) ⊗
54 (f (a16_9 ? a1) (a16_9 ? a2)) ⊗ (f (a16_10 ? a1) (a16_10 ? a2)) ⊗
55 (f (a16_11 ? a1) (a16_11 ? a2)) ⊗ (f (a16_12 ? a1) (a16_12 ? a2)) ⊗
56 (f (a16_13 ? a1) (a16_13 ? a2)) ⊗ (f (a16_14 ? a1) (a16_14 ? a2)) ⊗
57 (f (a16_15 ? a1) (a16_15 ? a2)) ⊗ (f (a16_16 ? a1) (a16_16 ? a2)).
59 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
60 (* posso definire un getter a matrice sull'array *)
62 ndefinition getn_array16T ≝
63 λn:exadecim.λT:Type.λp:Array16T T.
64 match n return λn.(Array16T T) → T with
65 [ x0 ⇒ a16_1 T | x1 ⇒ a16_2 T | x2 ⇒ a16_3 T | x3 ⇒ a16_4 T
66 | x4 ⇒ a16_5 T | x5 ⇒ a16_6 T | x6 ⇒ a16_7 T | x7 ⇒ a16_8 T
67 | x8 ⇒ a16_9 T | x9 ⇒ a16_10 T | xA ⇒ a16_11 T | xB ⇒ a16_12 T
68 | xC ⇒ a16_13 T | xD ⇒ a16_14 T | xE ⇒ a16_15 T | xF ⇒ a16_16 T
71 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
72 (* posso definire un setter a matrice sull'array *)
73 ndefinition setn_array16T ≝
74 λn:exadecim.λT:Type.λp:Array16T T.λv:T.
75 let e00 ≝ (a16_1 T p) in
76 let e01 ≝ (a16_2 T p) in
77 let e02 ≝ (a16_3 T p) in
78 let e03 ≝ (a16_4 T p) in
79 let e04 ≝ (a16_5 T p) in
80 let e05 ≝ (a16_6 T p) in
81 let e06 ≝ (a16_7 T p) in
82 let e07 ≝ (a16_8 T p) in
83 let e08 ≝ (a16_9 T p) in
84 let e09 ≝ (a16_10 T p) in
85 let e10 ≝ (a16_11 T p) in
86 let e11 ≝ (a16_12 T p) in
87 let e12 ≝ (a16_13 T p) in
88 let e13 ≝ (a16_14 T p) in
89 let e14 ≝ (a16_15 T p) in
90 let e15 ≝ (a16_16 T p) in
92 [ x0 ⇒ mk_Array16T T v e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
93 | x1 ⇒ mk_Array16T T e00 v e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
94 | x2 ⇒ mk_Array16T T e00 e01 v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
95 | x3 ⇒ mk_Array16T T e00 e01 e02 v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
96 | x4 ⇒ mk_Array16T T e00 e01 e02 e03 v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
97 | x5 ⇒ mk_Array16T T e00 e01 e02 e03 e04 v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
98 | x6 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v e07 e08 e09 e10 e11 e12 e13 e14 e15
99 | x7 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v e08 e09 e10 e11 e12 e13 e14 e15
100 | x8 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v e09 e10 e11 e12 e13 e14 e15
101 | x9 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v e10 e11 e12 e13 e14 e15
102 | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v e11 e12 e13 e14 e15
103 | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v e12 e13 e14 e15
104 | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v e13 e14 e15
105 | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v e14 e15
106 | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v e15
107 | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 v
110 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
111 (* posso definire un setter multiplo [m,n] a matrice sull'array *)
113 ndefinition setmn_array16T ≝
114 λm,n:exadecim.λT:Type.λp:Array16T T.λv:T.
115 let e00 ≝ (a16_1 T p) in
116 let e01 ≝ (a16_2 T p) in
117 let e02 ≝ (a16_3 T p) in
118 let e03 ≝ (a16_4 T p) in
119 let e04 ≝ (a16_5 T p) in
120 let e05 ≝ (a16_6 T p) in
121 let e06 ≝ (a16_7 T p) in
122 let e07 ≝ (a16_8 T p) in
123 let e08 ≝ (a16_9 T p) in
124 let e09 ≝ (a16_10 T p) in
125 let e10 ≝ (a16_11 T p) in
126 let e11 ≝ (a16_12 T p) in
127 let e12 ≝ (a16_13 T p) in
128 let e13 ≝ (a16_14 T p) in
129 let e14 ≝ (a16_15 T p) in
130 let e15 ≝ (a16_16 T p) in
133 [ x0 ⇒ mk_Array16T T v e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
134 | x1 ⇒ mk_Array16T T v v e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
135 | x2 ⇒ mk_Array16T T v v v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
136 | x3 ⇒ mk_Array16T T v v v v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
137 | x4 ⇒ mk_Array16T T v v v v v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
138 | x5 ⇒ mk_Array16T T v v v v v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
139 | x6 ⇒ mk_Array16T T v v v v v v v e07 e08 e09 e10 e11 e12 e13 e14 e15
140 | x7 ⇒ mk_Array16T T v v v v v v v v e08 e09 e10 e11 e12 e13 e14 e15
141 | x8 ⇒ mk_Array16T T v v v v v v v v v e09 e10 e11 e12 e13 e14 e15
142 | x9 ⇒ mk_Array16T T v v v v v v v v v v e10 e11 e12 e13 e14 e15
143 | xA ⇒ mk_Array16T T v v v v v v v v v v v e11 e12 e13 e14 e15
144 | xB ⇒ mk_Array16T T v v v v v v v v v v v v e12 e13 e14 e15
145 | xC ⇒ mk_Array16T T v v v v v v v v v v v v v e13 e14 e15
146 | xD ⇒ mk_Array16T T v v v v v v v v v v v v v v e14 e15
147 | xE ⇒ mk_Array16T T v v v v v v v v v v v v v v v e15
148 | xF ⇒ mk_Array16T T v v v v v v v v v v v v v v v v ]
151 | x1 ⇒ mk_Array16T T e00 v e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
152 | x2 ⇒ mk_Array16T T e00 v v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
153 | x3 ⇒ mk_Array16T T e00 v v v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
154 | x4 ⇒ mk_Array16T T e00 v v v v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
155 | x5 ⇒ mk_Array16T T e00 v v v v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
156 | x6 ⇒ mk_Array16T T e00 v v v v v v e07 e08 e09 e10 e11 e12 e13 e14 e15
157 | x7 ⇒ mk_Array16T T e00 v v v v v v v e08 e09 e10 e11 e12 e13 e14 e15
158 | x8 ⇒ mk_Array16T T e00 v v v v v v v v e09 e10 e11 e12 e13 e14 e15
159 | x9 ⇒ mk_Array16T T e00 v v v v v v v v v e10 e11 e12 e13 e14 e15
160 | xA ⇒ mk_Array16T T e00 v v v v v v v v v v e11 e12 e13 e14 e15
161 | xB ⇒ mk_Array16T T e00 v v v v v v v v v v v e12 e13 e14 e15
162 | xC ⇒ mk_Array16T T e00 v v v v v v v v v v v v e13 e14 e15
163 | xD ⇒ mk_Array16T T e00 v v v v v v v v v v v v v e14 e15
164 | xE ⇒ mk_Array16T T e00 v v v v v v v v v v v v v v e15
165 | xF ⇒ mk_Array16T T e00 v v v v v v v v v v v v v v v ]
168 | x2 ⇒ mk_Array16T T e00 e01 v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
169 | x3 ⇒ mk_Array16T T e00 e01 v v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
170 | x4 ⇒ mk_Array16T T e00 e01 v v v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
171 | x5 ⇒ mk_Array16T T e00 e01 v v v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
172 | x6 ⇒ mk_Array16T T e00 e01 v v v v v e07 e08 e09 e10 e11 e12 e13 e14 e15
173 | x7 ⇒ mk_Array16T T e00 e01 v v v v v v e08 e09 e10 e11 e12 e13 e14 e15
174 | x8 ⇒ mk_Array16T T e00 e01 v v v v v v v e09 e10 e11 e12 e13 e14 e15
175 | x9 ⇒ mk_Array16T T e00 e01 v v v v v v v v e10 e11 e12 e13 e14 e15
176 | xA ⇒ mk_Array16T T e00 e01 v v v v v v v v v e11 e12 e13 e14 e15
177 | xB ⇒ mk_Array16T T e00 e01 v v v v v v v v v v e12 e13 e14 e15
178 | xC ⇒ mk_Array16T T e00 e01 v v v v v v v v v v v e13 e14 e15
179 | xD ⇒ mk_Array16T T e00 e01 v v v v v v v v v v v v e14 e15
180 | xE ⇒ mk_Array16T T e00 e01 v v v v v v v v v v v v v e15
181 | xF ⇒ mk_Array16T T e00 e01 v v v v v v v v v v v v v v ]
183 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p
184 | x3 ⇒ mk_Array16T T e00 e01 e02 v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
185 | x4 ⇒ mk_Array16T T e00 e01 e02 v v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
186 | x5 ⇒ mk_Array16T T e00 e01 e02 v v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
187 | x6 ⇒ mk_Array16T T e00 e01 e02 v v v v e07 e08 e09 e10 e11 e12 e13 e14 e15
188 | x7 ⇒ mk_Array16T T e00 e01 e02 v v v v v e08 e09 e10 e11 e12 e13 e14 e15
189 | x8 ⇒ mk_Array16T T e00 e01 e02 v v v v v v e09 e10 e11 e12 e13 e14 e15
190 | x9 ⇒ mk_Array16T T e00 e01 e02 v v v v v v v e10 e11 e12 e13 e14 e15
191 | xA ⇒ mk_Array16T T e00 e01 e02 v v v v v v v v e11 e12 e13 e14 e15
192 | xB ⇒ mk_Array16T T e00 e01 e02 v v v v v v v v v e12 e13 e14 e15
193 | xC ⇒ mk_Array16T T e00 e01 e02 v v v v v v v v v v e13 e14 e15
194 | xD ⇒ mk_Array16T T e00 e01 e02 v v v v v v v v v v v e14 e15
195 | xE ⇒ mk_Array16T T e00 e01 e02 v v v v v v v v v v v v e15
196 | xF ⇒ mk_Array16T T e00 e01 e02 v v v v v v v v v v v v v ]
198 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p
199 | x4 ⇒ mk_Array16T T e00 e01 e02 e03 v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
200 | x5 ⇒ mk_Array16T T e00 e01 e02 e03 v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
201 | x6 ⇒ mk_Array16T T e00 e01 e02 e03 v v v e07 e08 e09 e10 e11 e12 e13 e14 e15
202 | x7 ⇒ mk_Array16T T e00 e01 e02 e03 v v v v e08 e09 e10 e11 e12 e13 e14 e15
203 | x8 ⇒ mk_Array16T T e00 e01 e02 e03 v v v v v e09 e10 e11 e12 e13 e14 e15
204 | x9 ⇒ mk_Array16T T e00 e01 e02 e03 v v v v v v e10 e11 e12 e13 e14 e15
205 | xA ⇒ mk_Array16T T e00 e01 e02 e03 v v v v v v v e11 e12 e13 e14 e15
206 | xB ⇒ mk_Array16T T e00 e01 e02 e03 v v v v v v v v e12 e13 e14 e15
207 | xC ⇒ mk_Array16T T e00 e01 e02 e03 v v v v v v v v v e13 e14 e15
208 | xD ⇒ mk_Array16T T e00 e01 e02 e03 v v v v v v v v v v e14 e15
209 | xE ⇒ mk_Array16T T e00 e01 e02 e03 v v v v v v v v v v v e15
210 | xF ⇒ mk_Array16T T e00 e01 e02 e03 v v v v v v v v v v v v ]
212 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p
213 | x5 ⇒ mk_Array16T T e00 e01 e02 e03 e04 v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
214 | x6 ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v e07 e08 e09 e10 e11 e12 e13 e14 e15
215 | x7 ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v v e08 e09 e10 e11 e12 e13 e14 e15
216 | x8 ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v v v e09 e10 e11 e12 e13 e14 e15
217 | x9 ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v v v v e10 e11 e12 e13 e14 e15
218 | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v v v v v e11 e12 e13 e14 e15
219 | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v v v v v v e12 e13 e14 e15
220 | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v v v v v v v e13 e14 e15
221 | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v v v v v v v v e14 e15
222 | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v v v v v v v v v e15
223 | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v v v v v v v v v v ]
225 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p
226 | x6 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v e07 e08 e09 e10 e11 e12 e13 e14 e15
227 | x7 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v e08 e09 e10 e11 e12 e13 e14 e15
228 | x8 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v v e09 e10 e11 e12 e13 e14 e15
229 | x9 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v v v e10 e11 e12 e13 e14 e15
230 | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v v v v e11 e12 e13 e14 e15
231 | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v v v v v e12 e13 e14 e15
232 | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v v v v v v e13 e14 e15
233 | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v v v v v v v e14 e15
234 | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v v v v v v v v e15
235 | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v v v v v v v v v ]
237 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p
238 | x7 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v e08 e09 e10 e11 e12 e13 e14 e15
239 | x8 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v e09 e10 e11 e12 e13 e14 e15
240 | x9 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v v e10 e11 e12 e13 e14 e15
241 | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v v v e11 e12 e13 e14 e15
242 | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v v v v e12 e13 e14 e15
243 | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v v v v v e13 e14 e15
244 | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v v v v v v e14 e15
245 | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v v v v v v v e15
246 | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v v v v v v v v ]
248 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
249 | x8 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v e09 e10 e11 e12 e13 e14 e15
250 | x9 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v e10 e11 e12 e13 e14 e15
251 | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v e11 e12 e13 e14 e15
252 | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v e12 e13 e14 e15
253 | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v v e13 e14 e15
254 | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v v v e14 e15
255 | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v v v v e15
256 | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v v v v v ]
258 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
260 | x9 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v e10 e11 e12 e13 e14 e15
261 | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v e11 e12 e13 e14 e15
262 | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v e12 e13 e14 e15
263 | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v v e13 e14 e15
264 | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v v v e14 e15
265 | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v v v v e15
266 | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v v v v v ]
268 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
270 | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v e11 e12 e13 e14 e15
271 | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v e12 e13 e14 e15
272 | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v v e13 e14 e15
273 | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v v v e14 e15
274 | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v v v v e15
275 | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v v v v v ]
277 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
278 | x8 ⇒ p | x9 ⇒ p | xA ⇒ p
279 | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v e12 e13 e14 e15
280 | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v e13 e14 e15
281 | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v v e14 e15
282 | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v v v e15
283 | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v v v v ]
285 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
286 | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p
287 | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v e13 e14 e15
288 | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v e14 e15
289 | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v v e15
290 | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v v v ]
292 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
293 | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p
294 | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v e14 e15
295 | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v v e15
296 | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v v v ]
298 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
299 | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p | xD ⇒ p
300 | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v e15
301 | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v v ]
303 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
304 | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p | xD ⇒ p | xE ⇒ p
305 | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 v ]
308 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
309 (* posso definire un setter composto [m+1,n-1] a matrice sull'array *)
310 (* NB: obbiettivo evitare l'overflow *)
311 ndefinition setmn_array16T_succ_pred ≝
312 λm,n:exadecim.λT:Type.λp:Array16T T.λv:T.
313 match lt_ex m xF with
314 [ true ⇒ match gt_ex n x0 with
315 [ true ⇒ setmn_array16T (succ_ex m) (pred_ex n) T p v
321 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
322 (* posso definire un setter composto [m+1,F] a matrice sull'array *)
323 (* NB: obbiettivo evitare l'overflow *)
324 ndefinition setmn_array16T_succ ≝
325 λm:exadecim.λT:Type.λp:Array16T T.λv:T.
326 match lt_ex m xF with
327 [ true ⇒ setmn_array16T (succ_ex m) xF T p v
331 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
332 (* posso definire un setter composto [0,n-1] a matrice sull'array *)
333 (* NB: obbiettivo evitare l'overflow *)
334 ndefinition setmn_array16T_pred ≝
335 λn:exadecim.λT:Type.λp:Array16T T.λv:T.
336 match gt_ex n x0 with
337 [ true ⇒ setmn_array16T x0 (pred_ex n) T p v
341 (* ************************** *)
342 (* TIPO BYTE COME INSIEME BIT *)
343 (* ************************** *)
345 (* definizione di un byte come 8 bit *)
346 nrecord Array8T (T:Type) : Type ≝
347 { a8_1 : T ; a8_2 : T ; a8_3 : T ; a8_4 : T
348 ; a8_5 : T ; a8_6 : T ; a8_7 : T ; a8_8 : T }.
350 (* operatore uguaglianza *)
352 λT.λf:T → T → bool.λa1,a2:Array8T T.
353 (f (a8_1 ? a1) (a8_1 ? a2)) ⊗ (f (a8_2 ? a1) (a8_2 ? a2)) ⊗
354 (f (a8_3 ? a1) (a8_3 ? a2)) ⊗ (f (a8_4 ? a1) (a8_4 ? a2)) ⊗
355 (f (a8_5 ? a1) (a8_5 ? a2)) ⊗ (f (a8_6 ? a1) (a8_6 ? a2)) ⊗
356 (f (a8_7 ? a1) (a8_7 ? a2)) ⊗ (f (a8_8 ? a1) (a8_8 ? a2)).
358 (* abbiamo gia' gli ottali come tipo induttivo quindi: *)
359 (* posso definire un getter a matrice sull'array *)
360 ndefinition getn_array8T ≝
361 λn:oct.λT:Type.λp:Array8T T.
362 match n return λn.(Array8T T) → T with
363 [ o0 ⇒ a8_1 T | o1 ⇒ a8_2 T | o2 ⇒ a8_3 T | o3 ⇒ a8_4 T
364 | o4 ⇒ a8_5 T | o5 ⇒ a8_6 T | o6 ⇒ a8_7 T | o7 ⇒ a8_8 T
367 (* abbiamo gia' gli ottali come tipo induttivo quindi: *)
368 (* posso definire un setter a matrice sull'array *)
369 ndefinition setn_array8T ≝
370 λn:oct.λT:Type.λp:Array8T T.λv:T.
371 let e00 ≝ (a8_1 T p) in
372 let e01 ≝ (a8_2 T p) in
373 let e02 ≝ (a8_3 T p) in
374 let e03 ≝ (a8_4 T p) in
375 let e04 ≝ (a8_5 T p) in
376 let e05 ≝ (a8_6 T p) in
377 let e06 ≝ (a8_7 T p) in
378 let e07 ≝ (a8_8 T p) in
380 [ o0 ⇒ mk_Array8T T v e01 e02 e03 e04 e05 e06 e07
381 | o1 ⇒ mk_Array8T T e00 v e02 e03 e04 e05 e06 e07
382 | o2 ⇒ mk_Array8T T e00 e01 v e03 e04 e05 e06 e07
383 | o3 ⇒ mk_Array8T T e00 e01 e02 v e04 e05 e06 e07
384 | o4 ⇒ mk_Array8T T e00 e01 e02 e03 v e05 e06 e07
385 | o5 ⇒ mk_Array8T T e00 e01 e02 e03 e04 v e06 e07
386 | o6 ⇒ mk_Array8T T e00 e01 e02 e03 e04 e05 v e07
387 | o7 ⇒ mk_Array8T T e00 e01 e02 e03 e04 e05 e06 v
391 ndefinition byte8_of_bits ≝
394 (or_ex (match a8_1 ? p with [ true ⇒ x8 | false ⇒ x0 ])
395 (or_ex (match a8_2 ? p with [ true ⇒ x4 | false ⇒ x0 ])
396 (or_ex (match a8_3 ? p with [ true ⇒ x2 | false ⇒ x0 ])
397 (match a8_4 ? p with [ true ⇒ x1 | false ⇒ x0 ]))))
398 (or_ex (match a8_5 ? p with [ true ⇒ x8 | false ⇒ x0 ])
399 (or_ex (match a8_6 ? p with [ true ⇒ x4 | false ⇒ x0 ])
400 (or_ex (match a8_7 ? p with [ true ⇒ x2 | false ⇒ x0 ])
401 (match a8_8 ? p with [ true ⇒ x1 | false ⇒ x0 ])))).
404 ndefinition bits_of_exadecim ≝
405 λe:exadecim.match e with
406 [ x0 ⇒ quadruple … false false false false
407 | x1 ⇒ quadruple … false false false true
408 | x2 ⇒ quadruple … false false true false
409 | x3 ⇒ quadruple … false false true true
410 | x4 ⇒ quadruple … false true false false
411 | x5 ⇒ quadruple … false true false true
412 | x6 ⇒ quadruple … false true true false
413 | x7 ⇒ quadruple … false true true true
414 | x8 ⇒ quadruple … true false false false
415 | x9 ⇒ quadruple … true false false true
416 | xA ⇒ quadruple … true false true false
417 | xB ⇒ quadruple … true false true true
418 | xC ⇒ quadruple … true true false false
419 | xD ⇒ quadruple … true true false true
420 | xE ⇒ quadruple … true true true false
421 | xF ⇒ quadruple … true true true true
424 ndefinition bits_of_byte8 ≝
426 mk_Array8T ? (fst4T … (bits_of_exadecim (cnH ? b)))
427 (snd4T … (bits_of_exadecim (cnH ? b)))
428 (thd4T … (bits_of_exadecim (cnH ? b)))
429 (fth4T … (bits_of_exadecim (cnH ? b)))
430 (fst4T … (bits_of_exadecim (cnL ? b)))
431 (snd4T … (bits_of_exadecim (cnL ? b)))
432 (thd4T … (bits_of_exadecim (cnL ? b)))
433 (fth4T … (bits_of_exadecim (cnL ? b))).