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 "num/byte8.ma".
25 (* **************** *)
26 (* TIPO ARRAY DA 16 *)
27 (* **************** *)
29 (* definizione di un array omogeneo di dimensione 16 *)
30 nrecord Array16T (T:Type) : Type ≝
31 { a16_1 : T ; a16_2 : T ; a16_3 : T ; a16_4 : T
32 ; a16_5 : T ; a16_6 : T ; a16_7 : T ; a16_8 : T
33 ; a16_9 : T ; a16_10 : T ; a16_11 : T ; a16_12 : T
34 ; a16_13 : T ; a16_14 : T ; a16_15 : T ; a16_16 : T }.
36 (* operatore uguaglianza *)
38 λT.λf:T → T → bool.λa1,a2:Array16T T.
39 (f (a16_1 ? a1) (a16_1 ? a2)) ⊗ (f (a16_2 ? a1) (a16_2 ? a2)) ⊗
40 (f (a16_3 ? a1) (a16_3 ? a2)) ⊗ (f (a16_4 ? a1) (a16_4 ? a2)) ⊗
41 (f (a16_5 ? a1) (a16_5 ? a2)) ⊗ (f (a16_6 ? a1) (a16_6 ? a2)) ⊗
42 (f (a16_7 ? a1) (a16_7 ? a2)) ⊗ (f (a16_8 ? a1) (a16_8 ? a2)) ⊗
43 (f (a16_9 ? a1) (a16_9 ? a2)) ⊗ (f (a16_10 ? a1) (a16_10 ? a2)) ⊗
44 (f (a16_11 ? a1) (a16_11 ? a2)) ⊗ (f (a16_12 ? a1) (a16_12 ? a2)) ⊗
45 (f (a16_13 ? a1) (a16_13 ? a2)) ⊗ (f (a16_14 ? a1) (a16_14 ? a2)) ⊗
46 (f (a16_15 ? a1) (a16_15 ? a2)) ⊗ (f (a16_16 ? a1) (a16_16 ? a2)).
48 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
49 (* posso definire un getter a matrice sull'array *)
51 ndefinition getn_array16T ≝
52 λn:exadecim.λT:Type.λp:Array16T T.
53 match n return λn.(Array16T T) → T with
54 [ x0 ⇒ a16_1 T | x1 ⇒ a16_2 T | x2 ⇒ a16_3 T | x3 ⇒ a16_4 T
55 | x4 ⇒ a16_5 T | x5 ⇒ a16_6 T | x6 ⇒ a16_7 T | x7 ⇒ a16_8 T
56 | x8 ⇒ a16_9 T | x9 ⇒ a16_10 T | xA ⇒ a16_11 T | xB ⇒ a16_12 T
57 | xC ⇒ a16_13 T | xD ⇒ a16_14 T | xE ⇒ a16_15 T | xF ⇒ a16_16 T
60 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
61 (* posso definire un setter a matrice sull'array *)
62 ndefinition setn_array16T ≝
63 λn:exadecim.λT:Type.λp:Array16T T.λv:T.
64 let e00 ≝ (a16_1 T p) in
65 let e01 ≝ (a16_2 T p) in
66 let e02 ≝ (a16_3 T p) in
67 let e03 ≝ (a16_4 T p) in
68 let e04 ≝ (a16_5 T p) in
69 let e05 ≝ (a16_6 T p) in
70 let e06 ≝ (a16_7 T p) in
71 let e07 ≝ (a16_8 T p) in
72 let e08 ≝ (a16_9 T p) in
73 let e09 ≝ (a16_10 T p) in
74 let e10 ≝ (a16_11 T p) in
75 let e11 ≝ (a16_12 T p) in
76 let e12 ≝ (a16_13 T p) in
77 let e13 ≝ (a16_14 T p) in
78 let e14 ≝ (a16_15 T p) in
79 let e15 ≝ (a16_16 T p) in
81 [ x0 ⇒ mk_Array16T T v e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
82 | x1 ⇒ mk_Array16T T e00 v e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
83 | x2 ⇒ mk_Array16T T e00 e01 v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
84 | x3 ⇒ mk_Array16T T e00 e01 e02 v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
85 | x4 ⇒ mk_Array16T T e00 e01 e02 e03 v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
86 | x5 ⇒ mk_Array16T T e00 e01 e02 e03 e04 v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
87 | x6 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v e07 e08 e09 e10 e11 e12 e13 e14 e15
88 | x7 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v e08 e09 e10 e11 e12 e13 e14 e15
89 | x8 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v e09 e10 e11 e12 e13 e14 e15
90 | x9 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v e10 e11 e12 e13 e14 e15
91 | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v e11 e12 e13 e14 e15
92 | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v e12 e13 e14 e15
93 | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v e13 e14 e15
94 | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v e14 e15
95 | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v e15
96 | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 v
99 (* ************************** *)
100 (* TIPO BYTE COME INSIEME BIT *)
101 (* ************************** *)
103 (* definizione di un byte come 8 bit *)
104 nrecord Array8T (T:Type) : Type ≝
105 { a8_1 : T ; a8_2 : T ; a8_3 : T ; a8_4 : T
106 ; a8_5 : T ; a8_6 : T ; a8_7 : T ; a8_8 : T }.
108 (* operatore uguaglianza *)
110 λT.λf:T → T → bool.λa1,a2:Array8T T.
111 (f (a8_1 ? a1) (a8_1 ? a2)) ⊗ (f (a8_2 ? a1) (a8_2 ? a2)) ⊗
112 (f (a8_3 ? a1) (a8_3 ? a2)) ⊗ (f (a8_4 ? a1) (a8_4 ? a2)) ⊗
113 (f (a8_5 ? a1) (a8_5 ? a2)) ⊗ (f (a8_6 ? a1) (a8_6 ? a2)) ⊗
114 (f (a8_7 ? a1) (a8_7 ? a2)) ⊗ (f (a8_8 ? a1) (a8_8 ? a2)).
116 (* abbiamo gia' gli ottali come tipo induttivo quindi: *)
117 (* posso definire un getter a matrice sull'array *)
118 ndefinition getn_array8T ≝
119 λn:oct.λT:Type.λp:Array8T T.
120 match n return λn.(Array8T T) → T with
121 [ o0 ⇒ a8_1 T | o1 ⇒ a8_2 T | o2 ⇒ a8_3 T | o3 ⇒ a8_4 T
122 | o4 ⇒ a8_5 T | o5 ⇒ a8_6 T | o6 ⇒ a8_7 T | o7 ⇒ a8_8 T
125 (* abbiamo gia' gli ottali come tipo induttivo quindi: *)
126 (* posso definire un setter a matrice sull'array *)
127 ndefinition setn_array8T ≝
128 λn:oct.λT:Type.λp:Array8T T.λv:T.
129 let e00 ≝ (a8_1 T p) in
130 let e01 ≝ (a8_2 T p) in
131 let e02 ≝ (a8_3 T p) in
132 let e03 ≝ (a8_4 T p) in
133 let e04 ≝ (a8_5 T p) in
134 let e05 ≝ (a8_6 T p) in
135 let e06 ≝ (a8_7 T p) in
136 let e07 ≝ (a8_8 T p) in
138 [ o0 ⇒ mk_Array8T T v e01 e02 e03 e04 e05 e06 e07
139 | o1 ⇒ mk_Array8T T e00 v e02 e03 e04 e05 e06 e07
140 | o2 ⇒ mk_Array8T T e00 e01 v e03 e04 e05 e06 e07
141 | o3 ⇒ mk_Array8T T e00 e01 e02 v e04 e05 e06 e07
142 | o4 ⇒ mk_Array8T T e00 e01 e02 e03 v e05 e06 e07
143 | o5 ⇒ mk_Array8T T e00 e01 e02 e03 e04 v e06 e07
144 | o6 ⇒ mk_Array8T T e00 e01 e02 e03 e04 e05 v e07
145 | o7 ⇒ mk_Array8T T e00 e01 e02 e03 e04 e05 e06 v
149 ndefinition byte8_of_bits ≝
152 (orc ? (match a8_1 ? p with [ true ⇒ x8 | false ⇒ x0 ])
153 (orc ? (match a8_2 ? p with [ true ⇒ x4 | false ⇒ x0 ])
154 (orc ? (match a8_3 ? p with [ true ⇒ x2 | false ⇒ x0 ])
155 (match a8_4 ? p with [ true ⇒ x1 | false ⇒ x0 ]))))
156 (orc ? (match a8_5 ? p with [ true ⇒ x8 | false ⇒ x0 ])
157 (orc ? (match a8_6 ? p with [ true ⇒ x4 | false ⇒ x0 ])
158 (orc ? (match a8_7 ? p with [ true ⇒ x2 | false ⇒ x0 ])
159 (match a8_8 ? p with [ true ⇒ x1 | false ⇒ x0 ])))).
162 ndefinition bits_of_exadecim ≝
163 λe:exadecim.match e with
164 [ x0 ⇒ quadruple … false false false false
165 | x1 ⇒ quadruple … false false false true
166 | x2 ⇒ quadruple … false false true false
167 | x3 ⇒ quadruple … false false true true
168 | x4 ⇒ quadruple … false true false false
169 | x5 ⇒ quadruple … false true false true
170 | x6 ⇒ quadruple … false true true false
171 | x7 ⇒ quadruple … false true true true
172 | x8 ⇒ quadruple … true false false false
173 | x9 ⇒ quadruple … true false false true
174 | xA ⇒ quadruple … true false true false
175 | xB ⇒ quadruple … true false true true
176 | xC ⇒ quadruple … true true false false
177 | xD ⇒ quadruple … true true false true
178 | xE ⇒ quadruple … true true true false
179 | xF ⇒ quadruple … true true true true
182 ndefinition bits_of_byte8 ≝
184 mk_Array8T ? (fst4T … (bits_of_exadecim (cnH ? b)))
185 (snd4T … (bits_of_exadecim (cnH ? b)))
186 (thd4T … (bits_of_exadecim (cnH ? b)))
187 (fth4T … (bits_of_exadecim (cnH ? b)))
188 (fst4T … (bits_of_exadecim (cnL ? b)))
189 (snd4T … (bits_of_exadecim (cnL ? b)))
190 (thd4T … (bits_of_exadecim (cnL ? b)))
191 (fth4T … (bits_of_exadecim (cnL ? b))).