]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/ng_assembly/emulator/memory/memory_struct.ma
Stuff moved from old Matita.
[helm.git] / matita / matita / contribs / ng_assembly / emulator / memory / memory_struct.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 "num/oct.ma".
24 include "num/byte8.ma".
25
26 (* **************************** *)
27 (* TIPI PER I MODULI DI MEMORIA *)
28 (* **************************** *)
29
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.
35
36 (* **************** *)
37 (* TIPO ARRAY DA 16 *)
38 (* **************** *)
39
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 }.
46
47 (* operatore uguaglianza *)
48 ndefinition eq_ar16 ≝
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)).
58
59 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
60 (* posso definire un getter a matrice sull'array *)
61
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
69   ] p.
70
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
91  match n with
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
108   ].
109
110 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
111 (* posso definire un setter multiplo [m,n] a matrice sull'array *)
112 (* m ≤ n *)
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
131  match m with
132   [ x0 ⇒ match n with
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 ]
149   | x1 ⇒ match n with
150    [ x0 ⇒ p
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 ]
166   | x2 ⇒ match n with
167    [ x0 ⇒ p | x1 ⇒ p
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 ]
182   | x3 ⇒ match n with
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 ]
197   | x4 ⇒ match n with
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 ]
211   | x5 ⇒ match n with
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 ]
224   | x6 ⇒ match n with
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 ]
236   | x7 ⇒ match n with
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 ]
247   | x8 ⇒ match n with
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 ]
257   | x9 ⇒ match n with
258    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p  | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
259    | x8 ⇒ 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 ]
267   | xA ⇒ match n with
268    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
269    | x8 ⇒ p | x9 ⇒ 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 ]
276   | xB ⇒ match n with
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 ]
284   | xC ⇒ match n with
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 ]
291   | xD ⇒ match n with
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 ]
297   | xE ⇒ match n with
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 ]
302   | xF ⇒ match n with
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 ]
306   ].
307
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
316    | false ⇒ p
317    ]
318   | false ⇒ p
319   ].
320
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
328   | false ⇒ p
329   ].
330
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
338   | false ⇒ p
339   ].
340
341 (* ************************** *)
342 (* TIPO BYTE COME INSIEME BIT *)
343 (* ************************** *)
344
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 }.
349
350 (* operatore uguaglianza *)
351 ndefinition eq_ar8 ≝
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)).
357
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
365   ] p.
366
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
379  match n with
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
388   ].
389
390 (* lettura byte *)
391 ndefinition byte8_of_bits ≝
392 λp:Array8T bool.
393    mk_byte8
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 ])))).
402
403 (* scrittura byte *)
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
422  ].
423
424 ndefinition bits_of_byte8 ≝
425 λb: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))).