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 (* Ultima modifica: 05/08/2009 *)
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 ninductive Array16T (T:Type) : Type ≝
42 array_16T : T → T → T → T → T → T → T → T →
43 T → T → T → T → T → T → T → T →
46 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
47 (* posso definire un getter a matrice sull'array *)
48 ndefinition getn_array16T ≝
49 λn:exadecim.λT:Type.λp:Array16T T.
51 [ array_16T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 ⇒
53 [ x0 ⇒ e00 | x1 ⇒ e01 | x2 ⇒ e02 | x3 ⇒ e03 | x4 ⇒ e04 | x5 ⇒ e05 | x6 ⇒ e06 | x7 ⇒ e07
54 | x8 ⇒ e08 | x9 ⇒ e09 | xA ⇒ e10 | xB ⇒ e11 | xC ⇒ e12 | xD ⇒ e13 | xE ⇒ e14 | xF ⇒ e15
57 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
58 (* posso definire un setter a matrice sull'array *)
59 ndefinition setn_array16T ≝
60 λn:exadecim.λT:Type.λp:Array16T T.λv:T.
62 [ array_16T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 ⇒
64 [ x0 ⇒ array_16T T v e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
65 | x1 ⇒ array_16T T e00 v e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
66 | x2 ⇒ array_16T T e00 e01 v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
67 | x3 ⇒ array_16T T e00 e01 e02 v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
68 | x4 ⇒ array_16T T e00 e01 e02 e03 v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
69 | x5 ⇒ array_16T T e00 e01 e02 e03 e04 v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
70 | x6 ⇒ array_16T T e00 e01 e02 e03 e04 e05 v e07 e08 e09 e10 e11 e12 e13 e14 e15
71 | x7 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v e08 e09 e10 e11 e12 e13 e14 e15
72 | x8 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v e09 e10 e11 e12 e13 e14 e15
73 | x9 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v e10 e11 e12 e13 e14 e15
74 | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v e11 e12 e13 e14 e15
75 | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v e12 e13 e14 e15
76 | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v e13 e14 e15
77 | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v e14 e15
78 | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v e15
79 | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 v
82 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
83 (* posso definire un setter multiplo [m,n] a matrice sull'array *)
84 ndefinition setmn_array16T ≝
85 λm,n:exadecim.λT:Type.λp:Array16T T.λv:T.
87 [ array_16T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 ⇒
90 [ x0 ⇒ array_16T T v e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
91 | x1 ⇒ array_16T T v v e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
92 | x2 ⇒ array_16T T v v v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
93 | x3 ⇒ array_16T T v v v v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
94 | x4 ⇒ array_16T T v v v v v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
95 | x5 ⇒ array_16T T v v v v v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
96 | x6 ⇒ array_16T T v v v v v v v e07 e08 e09 e10 e11 e12 e13 e14 e15
97 | x7 ⇒ array_16T T v v v v v v v v e08 e09 e10 e11 e12 e13 e14 e15
98 | x8 ⇒ array_16T T v v v v v v v v v e09 e10 e11 e12 e13 e14 e15
99 | x9 ⇒ array_16T T v v v v v v v v v v e10 e11 e12 e13 e14 e15
100 | xA ⇒ array_16T T v v v v v v v v v v v e11 e12 e13 e14 e15
101 | xB ⇒ array_16T T v v v v v v v v v v v v e12 e13 e14 e15
102 | xC ⇒ array_16T T v v v v v v v v v v v v v e13 e14 e15
103 | xD ⇒ array_16T T v v v v v v v v v v v v v v e14 e15
104 | xE ⇒ array_16T T v v v v v v v v v v v v v v v e15
105 | xF ⇒ array_16T T v v v v v v v v v v v v v v v v ]
108 | x1 ⇒ array_16T T e00 v e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
109 | x2 ⇒ array_16T T e00 v v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
110 | x3 ⇒ array_16T T e00 v v v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
111 | x4 ⇒ array_16T T e00 v v v v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
112 | x5 ⇒ array_16T T e00 v v v v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
113 | x6 ⇒ array_16T T e00 v v v v v v e07 e08 e09 e10 e11 e12 e13 e14 e15
114 | x7 ⇒ array_16T T e00 v v v v v v v e08 e09 e10 e11 e12 e13 e14 e15
115 | x8 ⇒ array_16T T e00 v v v v v v v v e09 e10 e11 e12 e13 e14 e15
116 | x9 ⇒ array_16T T e00 v v v v v v v v v e10 e11 e12 e13 e14 e15
117 | xA ⇒ array_16T T e00 v v v v v v v v v v e11 e12 e13 e14 e15
118 | xB ⇒ array_16T T e00 v v v v v v v v v v v e12 e13 e14 e15
119 | xC ⇒ array_16T T e00 v v v v v v v v v v v v e13 e14 e15
120 | xD ⇒ array_16T T e00 v v v v v v v v v v v v v e14 e15
121 | xE ⇒ array_16T T e00 v v v v v v v v v v v v v v e15
122 | xF ⇒ array_16T T e00 v v v v v v v v v v v v v v v ]
125 | x2 ⇒ array_16T T e00 e01 v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
126 | x3 ⇒ array_16T T e00 e01 v v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
127 | x4 ⇒ array_16T T e00 e01 v v v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
128 | x5 ⇒ array_16T T e00 e01 v v v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
129 | x6 ⇒ array_16T T e00 e01 v v v v v e07 e08 e09 e10 e11 e12 e13 e14 e15
130 | x7 ⇒ array_16T T e00 e01 v v v v v v e08 e09 e10 e11 e12 e13 e14 e15
131 | x8 ⇒ array_16T T e00 e01 v v v v v v v e09 e10 e11 e12 e13 e14 e15
132 | x9 ⇒ array_16T T e00 e01 v v v v v v v v e10 e11 e12 e13 e14 e15
133 | xA ⇒ array_16T T e00 e01 v v v v v v v v v e11 e12 e13 e14 e15
134 | xB ⇒ array_16T T e00 e01 v v v v v v v v v v e12 e13 e14 e15
135 | xC ⇒ array_16T T e00 e01 v v v v v v v v v v v e13 e14 e15
136 | xD ⇒ array_16T T e00 e01 v v v v v v v v v v v v e14 e15
137 | xE ⇒ array_16T T e00 e01 v v v v v v v v v v v v v e15
138 | xF ⇒ array_16T T e00 e01 v v v v v v v v v v v v v v ]
140 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p
141 | x3 ⇒ array_16T T e00 e01 e02 v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
142 | x4 ⇒ array_16T T e00 e01 e02 v v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
143 | x5 ⇒ array_16T T e00 e01 e02 v v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
144 | x6 ⇒ array_16T T e00 e01 e02 v v v v e07 e08 e09 e10 e11 e12 e13 e14 e15
145 | x7 ⇒ array_16T T e00 e01 e02 v v v v v e08 e09 e10 e11 e12 e13 e14 e15
146 | x8 ⇒ array_16T T e00 e01 e02 v v v v v v e09 e10 e11 e12 e13 e14 e15
147 | x9 ⇒ array_16T T e00 e01 e02 v v v v v v v e10 e11 e12 e13 e14 e15
148 | xA ⇒ array_16T T e00 e01 e02 v v v v v v v v e11 e12 e13 e14 e15
149 | xB ⇒ array_16T T e00 e01 e02 v v v v v v v v v e12 e13 e14 e15
150 | xC ⇒ array_16T T e00 e01 e02 v v v v v v v v v v e13 e14 e15
151 | xD ⇒ array_16T T e00 e01 e02 v v v v v v v v v v v e14 e15
152 | xE ⇒ array_16T T e00 e01 e02 v v v v v v v v v v v v e15
153 | xF ⇒ array_16T T e00 e01 e02 v v v v v v v v v v v v v ]
155 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p
156 | x4 ⇒ array_16T T e00 e01 e02 e03 v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
157 | x5 ⇒ array_16T T e00 e01 e02 e03 v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
158 | x6 ⇒ array_16T T e00 e01 e02 e03 v v v e07 e08 e09 e10 e11 e12 e13 e14 e15
159 | x7 ⇒ array_16T T e00 e01 e02 e03 v v v v e08 e09 e10 e11 e12 e13 e14 e15
160 | x8 ⇒ array_16T T e00 e01 e02 e03 v v v v v e09 e10 e11 e12 e13 e14 e15
161 | x9 ⇒ array_16T T e00 e01 e02 e03 v v v v v v e10 e11 e12 e13 e14 e15
162 | xA ⇒ array_16T T e00 e01 e02 e03 v v v v v v v e11 e12 e13 e14 e15
163 | xB ⇒ array_16T T e00 e01 e02 e03 v v v v v v v v e12 e13 e14 e15
164 | xC ⇒ array_16T T e00 e01 e02 e03 v v v v v v v v v e13 e14 e15
165 | xD ⇒ array_16T T e00 e01 e02 e03 v v v v v v v v v v e14 e15
166 | xE ⇒ array_16T T e00 e01 e02 e03 v v v v v v v v v v v e15
167 | xF ⇒ array_16T T e00 e01 e02 e03 v v v v v v v v v v v v ]
169 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p
170 | x5 ⇒ array_16T T e00 e01 e02 e03 e04 v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
171 | x6 ⇒ array_16T T e00 e01 e02 e03 e04 v v e07 e08 e09 e10 e11 e12 e13 e14 e15
172 | x7 ⇒ array_16T T e00 e01 e02 e03 e04 v v v e08 e09 e10 e11 e12 e13 e14 e15
173 | x8 ⇒ array_16T T e00 e01 e02 e03 e04 v v v v e09 e10 e11 e12 e13 e14 e15
174 | x9 ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v e10 e11 e12 e13 e14 e15
175 | xA ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v v e11 e12 e13 e14 e15
176 | xB ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v v v e12 e13 e14 e15
177 | xC ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v v v v e13 e14 e15
178 | xD ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v v v v v e14 e15
179 | xE ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v v v v v v e15
180 | xF ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v v v v v v v ]
182 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p
183 | x6 ⇒ array_16T T e00 e01 e02 e03 e04 e05 v e07 e08 e09 e10 e11 e12 e13 e14 e15
184 | x7 ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v e08 e09 e10 e11 e12 e13 e14 e15
185 | x8 ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v e09 e10 e11 e12 e13 e14 e15
186 | x9 ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v e10 e11 e12 e13 e14 e15
187 | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v v e11 e12 e13 e14 e15
188 | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v v v e12 e13 e14 e15
189 | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v v v v e13 e14 e15
190 | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v v v v v e14 e15
191 | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v v v v v v e15
192 | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v v v v v v v ]
194 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p
195 | x7 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v e08 e09 e10 e11 e12 e13 e14 e15
196 | x8 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v e09 e10 e11 e12 e13 e14 e15
197 | x9 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v e10 e11 e12 e13 e14 e15
198 | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v v e11 e12 e13 e14 e15
199 | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v v v e12 e13 e14 e15
200 | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v v v v e13 e14 e15
201 | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v v v v v e14 e15
202 | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v v v v v v e15
203 | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v v v v v v v ]
205 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
206 | x8 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v e09 e10 e11 e12 e13 e14 e15
207 | x9 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v e10 e11 e12 e13 e14 e15
208 | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v e11 e12 e13 e14 e15
209 | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v e12 e13 e14 e15
210 | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v v e13 e14 e15
211 | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v v v e14 e15
212 | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v v v v e15
213 | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v v v v v ]
215 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
217 | x9 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v e10 e11 e12 e13 e14 e15
218 | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v e11 e12 e13 e14 e15
219 | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v e12 e13 e14 e15
220 | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v v e13 e14 e15
221 | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v v v e14 e15
222 | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v v v v e15
223 | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v v v v v ]
225 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
227 | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v e11 e12 e13 e14 e15
228 | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v e12 e13 e14 e15
229 | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v v e13 e14 e15
230 | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v v v e14 e15
231 | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v v v v e15
232 | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v v v v v ]
234 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
235 | x8 ⇒ p | x9 ⇒ p | xA ⇒ p
236 | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v e12 e13 e14 e15
237 | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v e13 e14 e15
238 | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v v e14 e15
239 | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v v v e15
240 | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v v v v ]
242 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
243 | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p
244 | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v e13 e14 e15
245 | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v e14 e15
246 | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v v e15
247 | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v v v ]
249 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
250 | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p
251 | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v e14 e15
252 | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v v e15
253 | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v v v ]
255 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
256 | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p | xD ⇒ p
257 | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v e15
258 | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v v ]
260 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
261 | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p | xD ⇒ p | xE ⇒ p
262 | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 v ]
265 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
266 (* posso definire un setter composto [m+1,n-1] a matrice sull'array *)
267 (* NB: obbiettivo evitare l'overflow *)
268 ndefinition setmn_array16T_succ_pred ≝
269 λm,n:exadecim.λT:Type.λp:Array16T T.λv:T.
270 match lt_ex m xF with
271 [ true ⇒ match gt_ex n x0 with
272 [ true ⇒ setmn_array16T (succ_ex m) (pred_ex n) T p v
278 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
279 (* posso definire un setter composto [m+1,F] a matrice sull'array *)
280 (* NB: obbiettivo evitare l'overflow *)
281 ndefinition setmn_array16T_succ ≝
282 λm:exadecim.λT:Type.λp:Array16T T.λv:T.
283 match lt_ex m xF with
284 [ true ⇒ setmn_array16T (succ_ex m) xF T p v
288 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
289 (* posso definire un setter composto [0,n-1] a matrice sull'array *)
290 (* NB: obbiettivo evitare l'overflow *)
291 ndefinition setmn_array16T_pred ≝
292 λn:exadecim.λT:Type.λp:Array16T T.λv:T.
293 match gt_ex n x0 with
294 [ true ⇒ setmn_array16T x0 (pred_ex n) T p v
298 (* ************************** *)
299 (* TIPO BYTE COME INSIEME BIT *)
300 (* ************************** *)
302 (* definizione di un byte come 8 bit *)
303 ninductive Array8T (T:Type) : Type ≝
304 array_8T : T → T → T → T → T → T → T → T →
307 (* abbiamo gia' gli ottali come tipo induttivo quindi: *)
308 (* posso definire un getter a matrice sull'array *)
309 ndefinition getn_array8T ≝
310 λn:oct.λT:Type.λp:Array8T T.
312 [ array_8T e07 e06 e05 e04 e03 e02 e01 e00 ⇒
314 [ o0 ⇒ e00 | o1 ⇒ e01 | o2 ⇒ e02 | o3 ⇒ e03 | o4 ⇒ e04 | o5 ⇒ e05 | o6 ⇒ e06 | o7 ⇒ e07 ]].
316 (* abbiamo gia' gli ottali come tipo induttivo quindi: *)
317 (* posso definire un setter a matrice sull'array *)
318 ndefinition setn_array8T ≝
319 λn:oct.λT:Type.λp:Array8T T.λv:T.
321 [ array_8T e07 e06 e05 e04 e03 e02 e01 e00 ⇒
323 [ o0 ⇒ array_8T T e07 e06 e05 e04 e03 e02 e01 v
324 | o1 ⇒ array_8T T e07 e06 e05 e04 e03 e02 v e00
325 | o2 ⇒ array_8T T e07 e06 e05 e04 e03 v e01 e00
326 | o3 ⇒ array_8T T e07 e06 e05 e04 v e02 e01 e00
327 | o4 ⇒ array_8T T e07 e06 e05 v e03 e02 e01 e00
328 | o5 ⇒ array_8T T e07 e06 v e04 e03 e02 e01 e00
329 | o6 ⇒ array_8T T e07 v e05 e04 e03 e02 e01 e00
330 | o7 ⇒ array_8T T v e06 e05 e04 e03 e02 e01 e00
334 ndefinition byte8_of_bits ≝
337 [ array_8T e07 e06 e05 e04 e03 e02 e01 e00 ⇒
339 (or_ex (match e07 with [ true ⇒ x8 | false ⇒ x0 ])
340 (or_ex (match e06 with [ true ⇒ x4 | false ⇒ x0 ])
341 (or_ex (match e05 with [ true ⇒ x2 | false ⇒ x0 ])
342 (match e04 with [ true ⇒ x1 | false ⇒ x0 ]))))
343 (or_ex (match e03 with [ true ⇒ x8 | false ⇒ x0 ])
344 (or_ex (match e02 with [ true ⇒ x4 | false ⇒ x0 ])
345 (or_ex (match e01 with [ true ⇒ x2 | false ⇒ x0 ])
346 (match e00 with [ true ⇒ x1 | false ⇒ x0 ])))) ].
349 ndefinition bits_of_byte8 ≝
352 [ x0 ⇒ match b8l p with
353 [ x0 ⇒ array_8T bool false false false false false false false false
354 | x1 ⇒ array_8T bool false false false false false false false true
355 | x2 ⇒ array_8T bool false false false false false false true false
356 | x3 ⇒ array_8T bool false false false false false false true true
357 | x4 ⇒ array_8T bool false false false false false true false false
358 | x5 ⇒ array_8T bool false false false false false true false true
359 | x6 ⇒ array_8T bool false false false false false true true false
360 | x7 ⇒ array_8T bool false false false false false true true true
361 | x8 ⇒ array_8T bool false false false false true false false false
362 | x9 ⇒ array_8T bool false false false false true false false true
363 | xA ⇒ array_8T bool false false false false true false true false
364 | xB ⇒ array_8T bool false false false false true false true true
365 | xC ⇒ array_8T bool false false false false true true false false
366 | xD ⇒ array_8T bool false false false false true true false true
367 | xE ⇒ array_8T bool false false false false true true true false
368 | xF ⇒ array_8T bool false false false false true true true true ]
369 | x1 ⇒ match b8l p with
370 [ x0 ⇒ array_8T bool false false false true false false false false
371 | x1 ⇒ array_8T bool false false false true false false false true
372 | x2 ⇒ array_8T bool false false false true false false true false
373 | x3 ⇒ array_8T bool false false false true false false true true
374 | x4 ⇒ array_8T bool false false false true false true false false
375 | x5 ⇒ array_8T bool false false false true false true false true
376 | x6 ⇒ array_8T bool false false false true false true true false
377 | x7 ⇒ array_8T bool false false false true false true true true
378 | x8 ⇒ array_8T bool false false false true true false false false
379 | x9 ⇒ array_8T bool false false false true true false false true
380 | xA ⇒ array_8T bool false false false true true false true false
381 | xB ⇒ array_8T bool false false false true true false true true
382 | xC ⇒ array_8T bool false false false true true true false false
383 | xD ⇒ array_8T bool false false false true true true false true
384 | xE ⇒ array_8T bool false false false true true true true false
385 | xF ⇒ array_8T bool false false false true true true true true ]
386 | x2 ⇒ match b8l p with
387 [ x0 ⇒ array_8T bool false false true false false false false false
388 | x1 ⇒ array_8T bool false false true false false false false true
389 | x2 ⇒ array_8T bool false false true false false false true false
390 | x3 ⇒ array_8T bool false false true false false false true true
391 | x4 ⇒ array_8T bool false false true false false true false false
392 | x5 ⇒ array_8T bool false false true false false true false true
393 | x6 ⇒ array_8T bool false false true false false true true false
394 | x7 ⇒ array_8T bool false false true false false true true true
395 | x8 ⇒ array_8T bool false false true false true false false false
396 | x9 ⇒ array_8T bool false false true false true false false true
397 | xA ⇒ array_8T bool false false true false true false true false
398 | xB ⇒ array_8T bool false false true false true false true true
399 | xC ⇒ array_8T bool false false true false true true false false
400 | xD ⇒ array_8T bool false false true false true true false true
401 | xE ⇒ array_8T bool false false true false true true true false
402 | xF ⇒ array_8T bool false false true false true true true true ]
403 | x3 ⇒ match b8l p with
404 [ x0 ⇒ array_8T bool false false true true false false false false
405 | x1 ⇒ array_8T bool false false true true false false false true
406 | x2 ⇒ array_8T bool false false true true false false true false
407 | x3 ⇒ array_8T bool false false true true false false true true
408 | x4 ⇒ array_8T bool false false true true false true false false
409 | x5 ⇒ array_8T bool false false true true false true false true
410 | x6 ⇒ array_8T bool false false true true false true true false
411 | x7 ⇒ array_8T bool false false true true false true true true
412 | x8 ⇒ array_8T bool false false true true true false false false
413 | x9 ⇒ array_8T bool false false true true true false false true
414 | xA ⇒ array_8T bool false false true true true false true false
415 | xB ⇒ array_8T bool false false true true true false true true
416 | xC ⇒ array_8T bool false false true true true true false false
417 | xD ⇒ array_8T bool false false true true true true false true
418 | xE ⇒ array_8T bool false false true true true true true false
419 | xF ⇒ array_8T bool false false true true true true true true ]
420 | x4 ⇒ match b8l p with
421 [ x0 ⇒ array_8T bool false true false false false false false false
422 | x1 ⇒ array_8T bool false true false false false false false true
423 | x2 ⇒ array_8T bool false true false false false false true false
424 | x3 ⇒ array_8T bool false true false false false false true true
425 | x4 ⇒ array_8T bool false true false false false true false false
426 | x5 ⇒ array_8T bool false true false false false true false true
427 | x6 ⇒ array_8T bool false true false false false true true false
428 | x7 ⇒ array_8T bool false true false false false true true true
429 | x8 ⇒ array_8T bool false true false false true false false false
430 | x9 ⇒ array_8T bool false true false false true false false true
431 | xA ⇒ array_8T bool false true false false true false true false
432 | xB ⇒ array_8T bool false true false false true false true true
433 | xC ⇒ array_8T bool false true false false true true false false
434 | xD ⇒ array_8T bool false true false false true true false true
435 | xE ⇒ array_8T bool false true false false true true true false
436 | xF ⇒ array_8T bool false true false false true true true true ]
437 | x5 ⇒ match b8l p with
438 [ x0 ⇒ array_8T bool false true false true false false false false
439 | x1 ⇒ array_8T bool false true false true false false false true
440 | x2 ⇒ array_8T bool false true false true false false true false
441 | x3 ⇒ array_8T bool false true false true false false true true
442 | x4 ⇒ array_8T bool false true false true false true false false
443 | x5 ⇒ array_8T bool false true false true false true false true
444 | x6 ⇒ array_8T bool false true false true false true true false
445 | x7 ⇒ array_8T bool false true false true false true true true
446 | x8 ⇒ array_8T bool false true false true true false false false
447 | x9 ⇒ array_8T bool false true false true true false false true
448 | xA ⇒ array_8T bool false true false true true false true false
449 | xB ⇒ array_8T bool false true false true true false true true
450 | xC ⇒ array_8T bool false true false true true true false false
451 | xD ⇒ array_8T bool false true false true true true false true
452 | xE ⇒ array_8T bool false true false true true true true false
453 | xF ⇒ array_8T bool false true false true true true true true ]
454 | x6 ⇒ match b8l p with
455 [ x0 ⇒ array_8T bool false true true false false false false false
456 | x1 ⇒ array_8T bool false true true false false false false true
457 | x2 ⇒ array_8T bool false true true false false false true false
458 | x3 ⇒ array_8T bool false true true false false false true true
459 | x4 ⇒ array_8T bool false true true false false true false false
460 | x5 ⇒ array_8T bool false true true false false true false true
461 | x6 ⇒ array_8T bool false true true false false true true false
462 | x7 ⇒ array_8T bool false true true false false true true true
463 | x8 ⇒ array_8T bool false true true false true false false false
464 | x9 ⇒ array_8T bool false true true false true false false true
465 | xA ⇒ array_8T bool false true true false true false true false
466 | xB ⇒ array_8T bool false true true false true false true true
467 | xC ⇒ array_8T bool false true true false true true false false
468 | xD ⇒ array_8T bool false true true false true true false true
469 | xE ⇒ array_8T bool false true true false true true true false
470 | xF ⇒ array_8T bool false true true false true true true true ]
471 | x7 ⇒ match b8l p with
472 [ x0 ⇒ array_8T bool false true true true false false false false
473 | x1 ⇒ array_8T bool false true true true false false false true
474 | x2 ⇒ array_8T bool false true true true false false true false
475 | x3 ⇒ array_8T bool false true true true false false true true
476 | x4 ⇒ array_8T bool false true true true false true false false
477 | x5 ⇒ array_8T bool false true true true false true false true
478 | x6 ⇒ array_8T bool false true true true false true true false
479 | x7 ⇒ array_8T bool false true true true false true true true
480 | x8 ⇒ array_8T bool false true true true true false false false
481 | x9 ⇒ array_8T bool false true true true true false false true
482 | xA ⇒ array_8T bool false true true true true false true false
483 | xB ⇒ array_8T bool false true true true true false true true
484 | xC ⇒ array_8T bool false true true true true true false false
485 | xD ⇒ array_8T bool false true true true true true false true
486 | xE ⇒ array_8T bool false true true true true true true false
487 | xF ⇒ array_8T bool false true true true true true true true ]
488 | x8 ⇒ match b8l p with
489 [ x0 ⇒ array_8T bool true false false false false false false false
490 | x1 ⇒ array_8T bool true false false false false false false true
491 | x2 ⇒ array_8T bool true false false false false false true false
492 | x3 ⇒ array_8T bool true false false false false false true true
493 | x4 ⇒ array_8T bool true false false false false true false false
494 | x5 ⇒ array_8T bool true false false false false true false true
495 | x6 ⇒ array_8T bool true false false false false true true false
496 | x7 ⇒ array_8T bool true false false false false true true true
497 | x8 ⇒ array_8T bool true false false false true false false false
498 | x9 ⇒ array_8T bool true false false false true false false true
499 | xA ⇒ array_8T bool true false false false true false true false
500 | xB ⇒ array_8T bool true false false false true false true true
501 | xC ⇒ array_8T bool true false false false true true false false
502 | xD ⇒ array_8T bool true false false false true true false true
503 | xE ⇒ array_8T bool true false false false true true true false
504 | xF ⇒ array_8T bool true false false false true true true true ]
505 | x9 ⇒ match b8l p with
506 [ x0 ⇒ array_8T bool true false false true false false false false
507 | x1 ⇒ array_8T bool true false false true false false false true
508 | x2 ⇒ array_8T bool true false false true false false true false
509 | x3 ⇒ array_8T bool true false false true false false true true
510 | x4 ⇒ array_8T bool true false false true false true false false
511 | x5 ⇒ array_8T bool true false false true false true false true
512 | x6 ⇒ array_8T bool true false false true false true true false
513 | x7 ⇒ array_8T bool true false false true false true true true
514 | x8 ⇒ array_8T bool true false false true true false false false
515 | x9 ⇒ array_8T bool true false false true true false false true
516 | xA ⇒ array_8T bool true false false true true false true false
517 | xB ⇒ array_8T bool true false false true true false true true
518 | xC ⇒ array_8T bool true false false true true true false false
519 | xD ⇒ array_8T bool true false false true true true false true
520 | xE ⇒ array_8T bool true false false true true true true false
521 | xF ⇒ array_8T bool true false false true true true true true ]
522 | xA ⇒ match b8l p with
523 [ x0 ⇒ array_8T bool true false true false false false false false
524 | x1 ⇒ array_8T bool true false true false false false false true
525 | x2 ⇒ array_8T bool true false true false false false true false
526 | x3 ⇒ array_8T bool true false true false false false true true
527 | x4 ⇒ array_8T bool true false true false false true false false
528 | x5 ⇒ array_8T bool true false true false false true false true
529 | x6 ⇒ array_8T bool true false true false false true true false
530 | x7 ⇒ array_8T bool true false true false false true true true
531 | x8 ⇒ array_8T bool true false true false true false false false
532 | x9 ⇒ array_8T bool true false true false true false false true
533 | xA ⇒ array_8T bool true false true false true false true false
534 | xB ⇒ array_8T bool true false true false true false true true
535 | xC ⇒ array_8T bool true false true false true true false false
536 | xD ⇒ array_8T bool true false true false true true false true
537 | xE ⇒ array_8T bool true false true false true true true false
538 | xF ⇒ array_8T bool true false true false true true true true ]
539 | xB ⇒ match b8l p with
540 [ x0 ⇒ array_8T bool true false true true false false false false
541 | x1 ⇒ array_8T bool true false true true false false false true
542 | x2 ⇒ array_8T bool true false true true false false true false
543 | x3 ⇒ array_8T bool true false true true false false true true
544 | x4 ⇒ array_8T bool true false true true false true false false
545 | x5 ⇒ array_8T bool true false true true false true false true
546 | x6 ⇒ array_8T bool true false true true false true true false
547 | x7 ⇒ array_8T bool true false true true false true true true
548 | x8 ⇒ array_8T bool true false true true true false false false
549 | x9 ⇒ array_8T bool true false true true true false false true
550 | xA ⇒ array_8T bool true false true true true false true false
551 | xB ⇒ array_8T bool true false true true true false true true
552 | xC ⇒ array_8T bool true false true true true true false false
553 | xD ⇒ array_8T bool true false true true true true false true
554 | xE ⇒ array_8T bool true false true true true true true false
555 | xF ⇒ array_8T bool true false true true true true true true ]
556 | xC ⇒ match b8l p with
557 [ x0 ⇒ array_8T bool true true false false false false false false
558 | x1 ⇒ array_8T bool true true false false false false false true
559 | x2 ⇒ array_8T bool true true false false false false true false
560 | x3 ⇒ array_8T bool true true false false false false true true
561 | x4 ⇒ array_8T bool true true false false false true false false
562 | x5 ⇒ array_8T bool true true false false false true false true
563 | x6 ⇒ array_8T bool true true false false false true true false
564 | x7 ⇒ array_8T bool true true false false false true true true
565 | x8 ⇒ array_8T bool true true false false true false false false
566 | x9 ⇒ array_8T bool true true false false true false false true
567 | xA ⇒ array_8T bool true true false false true false true false
568 | xB ⇒ array_8T bool true true false false true false true true
569 | xC ⇒ array_8T bool true true false false true true false false
570 | xD ⇒ array_8T bool true true false false true true false true
571 | xE ⇒ array_8T bool true true false false true true true false
572 | xF ⇒ array_8T bool true true false false true true true true ]
573 | xD ⇒ match b8l p with
574 [ x0 ⇒ array_8T bool true true false true false false false false
575 | x1 ⇒ array_8T bool true true false true false false false true
576 | x2 ⇒ array_8T bool true true false true false false true false
577 | x3 ⇒ array_8T bool true true false true false false true true
578 | x4 ⇒ array_8T bool true true false true false true false false
579 | x5 ⇒ array_8T bool true true false true false true false true
580 | x6 ⇒ array_8T bool true true false true false true true false
581 | x7 ⇒ array_8T bool true true false true false true true true
582 | x8 ⇒ array_8T bool true true false true true false false false
583 | x9 ⇒ array_8T bool true true false true true false false true
584 | xA ⇒ array_8T bool true true false true true false true false
585 | xB ⇒ array_8T bool true true false true true false true true
586 | xC ⇒ array_8T bool true true false true true true false false
587 | xD ⇒ array_8T bool true true false true true true false true
588 | xE ⇒ array_8T bool true true false true true true true false
589 | xF ⇒ array_8T bool true true false true true true true true ]
590 | xE ⇒ match b8l p with
591 [ x0 ⇒ array_8T bool true true true false false false false false
592 | x1 ⇒ array_8T bool true true true false false false false true
593 | x2 ⇒ array_8T bool true true true false false false true false
594 | x3 ⇒ array_8T bool true true true false false false true true
595 | x4 ⇒ array_8T bool true true true false false true false false
596 | x5 ⇒ array_8T bool true true true false false true false true
597 | x6 ⇒ array_8T bool true true true false false true true false
598 | x7 ⇒ array_8T bool true true true false false true true true
599 | x8 ⇒ array_8T bool true true true false true false false false
600 | x9 ⇒ array_8T bool true true true false true false false true
601 | xA ⇒ array_8T bool true true true false true false true false
602 | xB ⇒ array_8T bool true true true false true false true true
603 | xC ⇒ array_8T bool true true true false true true false false
604 | xD ⇒ array_8T bool true true true false true true false true
605 | xE ⇒ array_8T bool true true true false true true true false
606 | xF ⇒ array_8T bool true true true false true true true true ]
607 | xF ⇒ match b8l p with
608 [ x0 ⇒ array_8T bool true true true true false false false false
609 | x1 ⇒ array_8T bool true true true true false false false true
610 | x2 ⇒ array_8T bool true true true true false false true false
611 | x3 ⇒ array_8T bool true true true true false false true true
612 | x4 ⇒ array_8T bool true true true true false true false false
613 | x5 ⇒ array_8T bool true true true true false true false true
614 | x6 ⇒ array_8T bool true true true true false true true false
615 | x7 ⇒ array_8T bool true true true true false true true true
616 | x8 ⇒ array_8T bool true true true true true false false false
617 | x9 ⇒ array_8T bool true true true true true false false true
618 | xA ⇒ array_8T bool true true true true true false true false
619 | xB ⇒ array_8T bool true true true true true false true true
620 | xC ⇒ array_8T bool true true true true true true false false
621 | xD ⇒ array_8T bool true true true true true true false true
622 | xE ⇒ array_8T bool true true true true true true true false
623 | xF ⇒ array_8T bool true true true true true true true true ]