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/comp_num.ma".
24 include "num/exadecim.ma".
25 include "num/bitrigesim.ma".
31 ndefinition byte8 ≝ comp_num exadecim.
32 ndefinition mk_byte8 ≝ λe1,e2.mk_comp_num exadecim e1 e2.
35 notation "〈x,y〉" non associative with precedence 80
36 for @{ mk_comp_num exadecim $x $y }.
38 ndefinition byte8_is_comparable_ext ≝ cn_is_comparable_ext exadecim_is_comparable_ext.
39 unification hint 0 ≔ ⊢ carr (comp_base byte8_is_comparable_ext) ≡ comp_num exadecim.
40 unification hint 0 ≔ ⊢ carr (comp_base byte8_is_comparable_ext) ≡ byte8.
42 (* operatore estensione unsigned *)
43 ndefinition extu_b8 ≝ λe2.〈zeroc ?,e2〉.
45 (* operatore estensione signed *)
47 λe2.〈(match getMSBc ? e2 with
48 [ true ⇒ predc ? (zeroc ?) | false ⇒ zeroc ? ]),e2〉.
50 (* operatore moltiplicazione senza segno: e*e=[0x00,0xE1] *)
52 λe1,e2:exadecim.match e1 with
54 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x0〉 | x2 ⇒ 〈x0,x0〉 | x3 ⇒ 〈x0,x0〉
55 | x4 ⇒ 〈x0,x0〉 | x5 ⇒ 〈x0,x0〉 | x6 ⇒ 〈x0,x0〉 | x7 ⇒ 〈x0,x0〉
56 | x8 ⇒ 〈x0,x0〉 | x9 ⇒ 〈x0,x0〉 | xA ⇒ 〈x0,x0〉 | xB ⇒ 〈x0,x0〉
57 | xC ⇒ 〈x0,x0〉 | xD ⇒ 〈x0,x0〉 | xE ⇒ 〈x0,x0〉 | xF ⇒ 〈x0,x0〉 ]
59 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x1〉 | x2 ⇒ 〈x0,x2〉 | x3 ⇒ 〈x0,x3〉
60 | x4 ⇒ 〈x0,x4〉 | x5 ⇒ 〈x0,x5〉 | x6 ⇒ 〈x0,x6〉 | x7 ⇒ 〈x0,x7〉
61 | x8 ⇒ 〈x0,x8〉 | x9 ⇒ 〈x0,x9〉 | xA ⇒ 〈x0,xA〉 | xB ⇒ 〈x0,xB〉
62 | xC ⇒ 〈x0,xC〉 | xD ⇒ 〈x0,xD〉 | xE ⇒ 〈x0,xE〉 | xF ⇒ 〈x0,xF〉 ]
64 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x2〉 | x2 ⇒ 〈x0,x4〉 | x3 ⇒ 〈x0,x6〉
65 | x4 ⇒ 〈x0,x8〉 | x5 ⇒ 〈x0,xA〉 | x6 ⇒ 〈x0,xC〉 | x7 ⇒ 〈x0,xE〉
66 | x8 ⇒ 〈x1,x0〉 | x9 ⇒ 〈x1,x2〉 | xA ⇒ 〈x1,x4〉 | xB ⇒ 〈x1,x6〉
67 | xC ⇒ 〈x1,x8〉 | xD ⇒ 〈x1,xA〉 | xE ⇒ 〈x1,xC〉 | xF ⇒ 〈x1,xE〉 ]
69 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x3〉 | x2 ⇒ 〈x0,x6〉 | x3 ⇒ 〈x0,x9〉
70 | x4 ⇒ 〈x0,xC〉 | x5 ⇒ 〈x0,xF〉 | x6 ⇒ 〈x1,x2〉 | x7 ⇒ 〈x1,x5〉
71 | x8 ⇒ 〈x1,x8〉 | x9 ⇒ 〈x1,xB〉 | xA ⇒ 〈x1,xE〉 | xB ⇒ 〈x2,x1〉
72 | xC ⇒ 〈x2,x4〉 | xD ⇒ 〈x2,x7〉 | xE ⇒ 〈x2,xA〉 | xF ⇒ 〈x2,xD〉 ]
74 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x4〉 | x2 ⇒ 〈x0,x8〉 | x3 ⇒ 〈x0,xC〉
75 | x4 ⇒ 〈x1,x0〉 | x5 ⇒ 〈x1,x4〉 | x6 ⇒ 〈x1,x8〉 | x7 ⇒ 〈x1,xC〉
76 | x8 ⇒ 〈x2,x0〉 | x9 ⇒ 〈x2,x4〉 | xA ⇒ 〈x2,x8〉 | xB ⇒ 〈x2,xC〉
77 | xC ⇒ 〈x3,x0〉 | xD ⇒ 〈x3,x4〉 | xE ⇒ 〈x3,x8〉 | xF ⇒ 〈x3,xC〉 ]
79 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x5〉 | x2 ⇒ 〈x0,xA〉 | x3 ⇒ 〈x0,xF〉
80 | x4 ⇒ 〈x1,x4〉 | x5 ⇒ 〈x1,x9〉 | x6 ⇒ 〈x1,xE〉 | x7 ⇒ 〈x2,x3〉
81 | x8 ⇒ 〈x2,x8〉 | x9 ⇒ 〈x2,xD〉 | xA ⇒ 〈x3,x2〉 | xB ⇒ 〈x3,x7〉
82 | xC ⇒ 〈x3,xC〉 | xD ⇒ 〈x4,x1〉 | xE ⇒ 〈x4,x6〉 | xF ⇒ 〈x4,xB〉 ]
84 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x6〉 | x2 ⇒ 〈x0,xC〉 | x3 ⇒ 〈x1,x2〉
85 | x4 ⇒ 〈x1,x8〉 | x5 ⇒ 〈x1,xE〉 | x6 ⇒ 〈x2,x4〉 | x7 ⇒ 〈x2,xA〉
86 | x8 ⇒ 〈x3,x0〉 | x9 ⇒ 〈x3,x6〉 | xA ⇒ 〈x3,xC〉 | xB ⇒ 〈x4,x2〉
87 | xC ⇒ 〈x4,x8〉 | xD ⇒ 〈x4,xE〉 | xE ⇒ 〈x5,x4〉 | xF ⇒ 〈x5,xA〉 ]
89 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x7〉 | x2 ⇒ 〈x0,xE〉 | x3 ⇒ 〈x1,x5〉
90 | x4 ⇒ 〈x1,xC〉 | x5 ⇒ 〈x2,x3〉 | x6 ⇒ 〈x2,xA〉 | x7 ⇒ 〈x3,x1〉
91 | x8 ⇒ 〈x3,x8〉 | x9 ⇒ 〈x3,xF〉 | xA ⇒ 〈x4,x6〉 | xB ⇒ 〈x4,xD〉
92 | xC ⇒ 〈x5,x4〉 | xD ⇒ 〈x5,xB〉 | xE ⇒ 〈x6,x2〉 | xF ⇒ 〈x6,x9〉 ]
94 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x8〉 | x2 ⇒ 〈x1,x0〉 | x3 ⇒ 〈x1,x8〉
95 | x4 ⇒ 〈x2,x0〉 | x5 ⇒ 〈x2,x8〉 | x6 ⇒ 〈x3,x0〉 | x7 ⇒ 〈x3,x8〉
96 | x8 ⇒ 〈x4,x0〉 | x9 ⇒ 〈x4,x8〉 | xA ⇒ 〈x5,x0〉 | xB ⇒ 〈x5,x8〉
97 | xC ⇒ 〈x6,x0〉 | xD ⇒ 〈x6,x8〉 | xE ⇒ 〈x7,x0〉 | xF ⇒ 〈x7,x8〉 ]
99 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x9〉 | x2 ⇒ 〈x1,x2〉 | x3 ⇒ 〈x1,xB〉
100 | x4 ⇒ 〈x2,x4〉 | x5 ⇒ 〈x2,xD〉 | x6 ⇒ 〈x3,x6〉 | x7 ⇒ 〈x3,xF〉
101 | x8 ⇒ 〈x4,x8〉 | x9 ⇒ 〈x5,x1〉 | xA ⇒ 〈x5,xA〉 | xB ⇒ 〈x6,x3〉
102 | xC ⇒ 〈x6,xC〉 | xD ⇒ 〈x7,x5〉 | xE ⇒ 〈x7,xE〉 | xF ⇒ 〈x8,x7〉 ]
104 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xA〉 | x2 ⇒ 〈x1,x4〉 | x3 ⇒ 〈x1,xE〉
105 | x4 ⇒ 〈x2,x8〉 | x5 ⇒ 〈x3,x2〉 | x6 ⇒ 〈x3,xC〉 | x7 ⇒ 〈x4,x6〉
106 | x8 ⇒ 〈x5,x0〉 | x9 ⇒ 〈x5,xA〉 | xA ⇒ 〈x6,x4〉 | xB ⇒ 〈x6,xE〉
107 | xC ⇒ 〈x7,x8〉 | xD ⇒ 〈x8,x2〉 | xE ⇒ 〈x8,xC〉 | xF ⇒ 〈x9,x6〉 ]
109 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xB〉 | x2 ⇒ 〈x1,x6〉 | x3 ⇒ 〈x2,x1〉
110 | x4 ⇒ 〈x2,xC〉 | x5 ⇒ 〈x3,x7〉 | x6 ⇒ 〈x4,x2〉 | x7 ⇒ 〈x4,xD〉
111 | x8 ⇒ 〈x5,x8〉 | x9 ⇒ 〈x6,x3〉 | xA ⇒ 〈x6,xE〉 | xB ⇒ 〈x7,x9〉
112 | xC ⇒ 〈x8,x4〉 | xD ⇒ 〈x8,xF〉 | xE ⇒ 〈x9,xA〉 | xF ⇒ 〈xA,x5〉 ]
114 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xC〉 | x2 ⇒ 〈x1,x8〉 | x3 ⇒ 〈x2,x4〉
115 | x4 ⇒ 〈x3,x0〉 | x5 ⇒ 〈x3,xC〉 | x6 ⇒ 〈x4,x8〉 | x7 ⇒ 〈x5,x4〉
116 | x8 ⇒ 〈x6,x0〉 | x9 ⇒ 〈x6,xC〉 | xA ⇒ 〈x7,x8〉 | xB ⇒ 〈x8,x4〉
117 | xC ⇒ 〈x9,x0〉 | xD ⇒ 〈x9,xC〉 | xE ⇒ 〈xA,x8〉 | xF ⇒ 〈xB,x4〉 ]
119 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xD〉 | x2 ⇒ 〈x1,xA〉 | x3 ⇒ 〈x2,x7〉
120 | x4 ⇒ 〈x3,x4〉 | x5 ⇒ 〈x4,x1〉 | x6 ⇒ 〈x4,xE〉 | x7 ⇒ 〈x5,xB〉
121 | x8 ⇒ 〈x6,x8〉 | x9 ⇒ 〈x7,x5〉 | xA ⇒ 〈x8,x2〉 | xB ⇒ 〈x8,xF〉
122 | xC ⇒ 〈x9,xC〉 | xD ⇒ 〈xA,x9〉 | xE ⇒ 〈xB,x6〉 | xF ⇒ 〈xC,x3〉 ]
124 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xE〉 | x2 ⇒ 〈x1,xC〉 | x3 ⇒ 〈x2,xA〉
125 | x4 ⇒ 〈x3,x8〉 | x5 ⇒ 〈x4,x6〉 | x6 ⇒ 〈x5,x4〉 | x7 ⇒ 〈x6,x2〉
126 | x8 ⇒ 〈x7,x0〉 | x9 ⇒ 〈x7,xE〉 | xA ⇒ 〈x8,xC〉 | xB ⇒ 〈x9,xA〉
127 | xC ⇒ 〈xA,x8〉 | xD ⇒ 〈xB,x6〉 | xE ⇒ 〈xC,x4〉 | xF ⇒ 〈xD,x2〉 ]
129 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xF〉 | x2 ⇒ 〈x1,xE〉 | x3 ⇒ 〈x2,xD〉
130 | x4 ⇒ 〈x3,xC〉 | x5 ⇒ 〈x4,xB〉 | x6 ⇒ 〈x5,xA〉 | x7 ⇒ 〈x6,x9〉
131 | x8 ⇒ 〈x7,x8〉 | x9 ⇒ 〈x8,x7〉 | xA ⇒ 〈x9,x6〉 | xB ⇒ 〈xA,x5〉
132 | xC ⇒ 〈xB,x4〉 | xD ⇒ 〈xC,x3〉 | xE ⇒ 〈xD,x2〉 | xF ⇒ 〈xE,x1〉 ]
135 (* operatore moltiplicazione con segno *)
136 ndefinition muls_ex ≝
137 λe1,e2:exadecim.match e1 with
139 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x0〉 | x2 ⇒ 〈x0,x0〉 | x3 ⇒ 〈x0,x0〉
140 | x4 ⇒ 〈x0,x0〉 | x5 ⇒ 〈x0,x0〉 | x6 ⇒ 〈x0,x0〉 | x7 ⇒ 〈x0,x0〉
141 | x8 ⇒ 〈x0,x0〉 | x9 ⇒ 〈x0,x0〉 | xA ⇒ 〈x0,x0〉 | xB ⇒ 〈x0,x0〉
142 | xC ⇒ 〈x0,x0〉 | xD ⇒ 〈x0,x0〉 | xE ⇒ 〈x0,x0〉 | xF ⇒ 〈x0,x0〉 ]
144 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x1〉 | x2 ⇒ 〈x0,x2〉 | x3 ⇒ 〈x0,x3〉
145 | x4 ⇒ 〈x0,x4〉 | x5 ⇒ 〈x0,x5〉 | x6 ⇒ 〈x0,x6〉 | x7 ⇒ 〈x0,x7〉
146 | x8 ⇒ 〈xF,x8〉 | x9 ⇒ 〈xF,x9〉 | xA ⇒ 〈xF,xA〉 | xB ⇒ 〈xF,xB〉
147 | xC ⇒ 〈xF,xC〉 | xD ⇒ 〈xF,xD〉 | xE ⇒ 〈xF,xE〉 | xF ⇒ 〈xF,xF〉 ]
149 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x2〉 | x2 ⇒ 〈x0,x4〉 | x3 ⇒ 〈x0,x6〉
150 | x4 ⇒ 〈x0,x8〉 | x5 ⇒ 〈x0,xA〉 | x6 ⇒ 〈x0,xC〉 | x7 ⇒ 〈x0,xE〉
151 | x8 ⇒ 〈xF,x0〉 | x9 ⇒ 〈xF,x2〉 | xA ⇒ 〈xF,x4〉 | xB ⇒ 〈xF,x6〉
152 | xC ⇒ 〈xF,x8〉 | xD ⇒ 〈xF,xA〉 | xE ⇒ 〈xF,xC〉 | xF ⇒ 〈xF,xE〉 ]
154 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x3〉 | x2 ⇒ 〈x0,x6〉 | x3 ⇒ 〈x0,x9〉
155 | x4 ⇒ 〈x0,xC〉 | x5 ⇒ 〈x0,xF〉 | x6 ⇒ 〈x1,x2〉 | x7 ⇒ 〈x1,x5〉
156 | x8 ⇒ 〈xE,x8〉 | x9 ⇒ 〈xE,xB〉 | xA ⇒ 〈xE,xE〉 | xB ⇒ 〈xF,x1〉
157 | xC ⇒ 〈xF,x4〉 | xD ⇒ 〈xF,x7〉 | xE ⇒ 〈xF,xA〉 | xF ⇒ 〈xF,xD〉 ]
159 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x4〉 | x2 ⇒ 〈x0,x8〉 | x3 ⇒ 〈x0,xC〉
160 | x4 ⇒ 〈x1,x0〉 | x5 ⇒ 〈x1,x4〉 | x6 ⇒ 〈x1,x8〉 | x7 ⇒ 〈x1,xC〉
161 | x8 ⇒ 〈xE,x0〉 | x9 ⇒ 〈xE,x4〉 | xA ⇒ 〈xE,x8〉 | xB ⇒ 〈xE,xC〉
162 | xC ⇒ 〈xF,x0〉 | xD ⇒ 〈xF,x4〉 | xE ⇒ 〈xF,x8〉 | xF ⇒ 〈xF,xC〉 ]
164 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x5〉 | x2 ⇒ 〈x0,xA〉 | x3 ⇒ 〈x0,xF〉
165 | x4 ⇒ 〈x1,x4〉 | x5 ⇒ 〈x1,x9〉 | x6 ⇒ 〈x1,xE〉 | x7 ⇒ 〈x2,x3〉
166 | x8 ⇒ 〈xD,x8〉 | x9 ⇒ 〈xD,xD〉 | xA ⇒ 〈xE,x2〉 | xB ⇒ 〈xE,x7〉
167 | xC ⇒ 〈xE,xC〉 | xD ⇒ 〈xF,x1〉 | xE ⇒ 〈xF,x6〉 | xF ⇒ 〈xF,xB〉 ]
169 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x6〉 | x2 ⇒ 〈x0,xC〉 | x3 ⇒ 〈x1,x2〉
170 | x4 ⇒ 〈x1,x8〉 | x5 ⇒ 〈x1,xE〉 | x6 ⇒ 〈x2,x4〉 | x7 ⇒ 〈x2,xA〉
171 | x8 ⇒ 〈xD,x0〉 | x9 ⇒ 〈xD,x6〉 | xA ⇒ 〈xD,xC〉 | xB ⇒ 〈xE,x2〉
172 | xC ⇒ 〈xE,x8〉 | xD ⇒ 〈xE,xE〉 | xE ⇒ 〈xF,x4〉 | xF ⇒ 〈xF,xA〉 ]
174 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x7〉 | x2 ⇒ 〈x0,xE〉 | x3 ⇒ 〈x1,x5〉
175 | x4 ⇒ 〈x1,xC〉 | x5 ⇒ 〈x2,x3〉 | x6 ⇒ 〈x2,xA〉 | x7 ⇒ 〈x3,x1〉
176 | x8 ⇒ 〈xC,x8〉 | x9 ⇒ 〈xC,xF〉 | xA ⇒ 〈xD,x6〉 | xB ⇒ 〈xD,xD〉
177 | xC ⇒ 〈xE,x4〉 | xD ⇒ 〈xE,xB〉 | xE ⇒ 〈xF,x2〉 | xF ⇒ 〈xF,x9〉 ]
179 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈xF,x8〉 | x2 ⇒ 〈xF,x0〉 | x3 ⇒ 〈xE,x8〉
180 | x4 ⇒ 〈xE,x0〉 | x5 ⇒ 〈xD,x8〉 | x6 ⇒ 〈xD,x0〉 | x7 ⇒ 〈xC,x8〉
181 | x8 ⇒ 〈x4,x0〉 | x9 ⇒ 〈x3,x8〉 | xA ⇒ 〈x3,x0〉 | xB ⇒ 〈x2,x8〉
182 | xC ⇒ 〈x2,x0〉 | xD ⇒ 〈x1,x8〉 | xE ⇒ 〈x1,x0〉 | xF ⇒ 〈x0,x8〉 ]
184 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈xF,x9〉 | x2 ⇒ 〈xF,x2〉 | x3 ⇒ 〈xE,xB〉
185 | x4 ⇒ 〈xE,x4〉 | x5 ⇒ 〈xD,xD〉 | x6 ⇒ 〈xD,x6〉 | x7 ⇒ 〈xC,xF〉
186 | x8 ⇒ 〈x3,x8〉 | x9 ⇒ 〈x3,x1〉 | xA ⇒ 〈x2,xA〉 | xB ⇒ 〈x2,x3〉
187 | xC ⇒ 〈x1,xC〉 | xD ⇒ 〈x1,x5〉 | xE ⇒ 〈x0,xE〉 | xF ⇒ 〈x0,x7〉 ]
189 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈xF,xA〉 | x2 ⇒ 〈xF,x4〉 | x3 ⇒ 〈xE,xE〉
190 | x4 ⇒ 〈xE,x8〉 | x5 ⇒ 〈xE,x2〉 | x6 ⇒ 〈xD,xC〉 | x7 ⇒ 〈xD,x6〉
191 | x8 ⇒ 〈x3,x0〉 | x9 ⇒ 〈x2,xA〉 | xA ⇒ 〈x2,x4〉 | xB ⇒ 〈x1,xE〉
192 | xC ⇒ 〈x1,x8〉 | xD ⇒ 〈x1,x2〉 | xE ⇒ 〈x0,xC〉 | xF ⇒ 〈x0,x6〉 ]
194 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈xF,xB〉 | x2 ⇒ 〈xF,x6〉 | x3 ⇒ 〈xF,x1〉
195 | x4 ⇒ 〈xE,xC〉 | x5 ⇒ 〈xE,x7〉 | x6 ⇒ 〈xE,x2〉 | x7 ⇒ 〈xD,xD〉
196 | x8 ⇒ 〈x2,x8〉 | x9 ⇒ 〈x2,x3〉 | xA ⇒ 〈x1,xE〉 | xB ⇒ 〈x1,x9〉
197 | xC ⇒ 〈x1,x4〉 | xD ⇒ 〈x0,xF〉 | xE ⇒ 〈x0,xA〉 | xF ⇒ 〈x0,x5〉 ]
199 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈xF,xC〉 | x2 ⇒ 〈xF,x8〉 | x3 ⇒ 〈xF,x4〉
200 | x4 ⇒ 〈xF,x0〉 | x5 ⇒ 〈xE,xC〉 | x6 ⇒ 〈xE,x8〉 | x7 ⇒ 〈xE,x4〉
201 | x8 ⇒ 〈x2,x0〉 | x9 ⇒ 〈x1,xC〉 | xA ⇒ 〈x1,x8〉 | xB ⇒ 〈x1,x4〉
202 | xC ⇒ 〈x1,x0〉 | xD ⇒ 〈x0,xC〉 | xE ⇒ 〈x0,x8〉 | xF ⇒ 〈x0,x4〉 ]
204 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈xF,xD〉 | x2 ⇒ 〈xF,xA〉 | x3 ⇒ 〈xF,x7〉
205 | x4 ⇒ 〈xF,x4〉 | x5 ⇒ 〈xF,x1〉 | x6 ⇒ 〈xE,xE〉 | x7 ⇒ 〈xE,xB〉
206 | x8 ⇒ 〈x1,x8〉 | x9 ⇒ 〈x1,x5〉 | xA ⇒ 〈x1,x2〉 | xB ⇒ 〈x0,xF〉
207 | xC ⇒ 〈x0,xC〉 | xD ⇒ 〈x0,x9〉 | xE ⇒ 〈x0,x6〉 | xF ⇒ 〈x0,x3〉 ]
209 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈xF,xE〉 | x2 ⇒ 〈xF,xC〉 | x3 ⇒ 〈xF,xA〉
210 | x4 ⇒ 〈xF,x8〉 | x5 ⇒ 〈xF,x6〉 | x6 ⇒ 〈xF,x4〉 | x7 ⇒ 〈xF,x2〉
211 | x8 ⇒ 〈x1,x0〉 | x9 ⇒ 〈x0,xE〉 | xA ⇒ 〈x0,xC〉 | xB ⇒ 〈x0,xA〉
212 | xC ⇒ 〈x0,x8〉 | xD ⇒ 〈x0,x6〉 | xE ⇒ 〈x0,x4〉 | xF ⇒ 〈x0,x2〉 ]
214 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈xF,xF〉 | x2 ⇒ 〈xF,xE〉 | x3 ⇒ 〈xF,xD〉
215 | x4 ⇒ 〈xF,xC〉 | x5 ⇒ 〈xF,xB〉 | x6 ⇒ 〈xF,xA〉 | x7 ⇒ 〈xF,x9〉
216 | x8 ⇒ 〈x0,x8〉 | x9 ⇒ 〈x0,x7〉 | xA ⇒ 〈x0,x6〉 | xB ⇒ 〈x0,x5〉
217 | xC ⇒ 〈x0,x4〉 | xD ⇒ 〈x0,x3〉 | xE ⇒ 〈x0,x2〉 | xF ⇒ 〈x0,x1〉 ]
220 (* correzione per somma su BCD *)
221 (* input: halfcarry,carry,X(BCD+BCD) *)
222 (* output: X',carry' *)
225 match ltc ? X 〈x9,xA〉 with
228 (* X' = [(b16l X):0x0-0x9] X + [h=1 ? 0x06 : 0x00] + [c=1 ? 0x60 : 0x00]
229 [(b16l X):0xA-0xF] X + 0x06 + [c=1 ? 0x60 : 0x00] *)
231 let X' ≝ match (ltc ? (cnL ? X) xA) ⊗ (⊖h) with
233 | false ⇒ plusc_d_d ? X 〈x0,x6〉 ] in
234 let X'' ≝ match c with
235 [ true ⇒ plusc_d_d ? X' 〈x6,x0〉
240 (* X' = [X:0x9A-0xFF]
241 [(b16l X):0x0-0x9] X + [h=1 ? 0x06 : 0x00] + 0x60
242 [(b16l X):0xA-0xF] X + 0x6 + 0x60 *)
244 let X' ≝ match (ltc ? (cnL ? X) xA) ⊗ (⊖h) with
246 | false ⇒ plusc_d_d ? X 〈x0,x6〉 ] in
247 let X'' ≝ plusc_d_d ? X' 〈x6,x0〉 in
252 ninductive rec_byte8 : byte8 → Type ≝
253 b8_O : rec_byte8 (zeroc ?)
254 | b8_S : ∀n.rec_byte8 n → rec_byte8 (succc ? n).
256 (* byte → byte ricorsivi *)
257 ndefinition b8_to_recb8_aux1 : Πn.rec_byte8 〈n,x0〉 → rec_byte8 〈succc ? n,x0〉 ≝
258 λn.λrecb:rec_byte8 〈n,x0〉.
259 b8_S 〈n,xF〉 (b8_S 〈n,xE〉 (b8_S 〈n,xD〉 (b8_S 〈n,xC〉 (
260 b8_S 〈n,xB〉 (b8_S 〈n,xA〉 (b8_S 〈n,x9〉 (b8_S 〈n,x8〉 (
261 b8_S 〈n,x7〉 (b8_S 〈n,x6〉 (b8_S 〈n,x5〉 (b8_S 〈n,x4〉 (
262 b8_S 〈n,x3〉 (b8_S 〈n,x2〉 (b8_S 〈n,x1〉 (b8_S 〈n,x0〉 recb))))))))))))))).
264 (* ... cifra esadecimale superiore *)
265 nlet rec b8_to_recb8_aux2 (n:exadecim) (r:rec_exadecim n) on r ≝
266 match r return λx.λy:rec_exadecim x.rec_byte8 〈x,x0〉 with
268 | ex_S t n' ⇒ b8_to_recb8_aux1 ? (b8_to_recb8_aux2 t n')
271 (* ... cifra esadecimale inferiore *)
272 ndefinition b8_to_recb8_aux3 : Πn1,n2.rec_byte8 〈n1,x0〉 → rec_byte8 〈n1,n2〉 ≝
273 λn1,n2.λrecb:rec_byte8 〈n1,x0〉.
274 match n2 return λx.rec_byte8 〈n1,x〉 with
276 | x1 ⇒ b8_S 〈n1,x0〉 recb
277 | x2 ⇒ b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)
278 | x3 ⇒ b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb))
279 | x4 ⇒ b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))
280 | x5 ⇒ b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (
281 b8_S 〈n1,x0〉 recb))))
282 | x6 ⇒ b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (
283 b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))
284 | x7 ⇒ b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (
285 b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb))))))
286 | x8 ⇒ b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (
287 b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))))
288 | x9 ⇒ b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (
289 b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (
290 b8_S 〈n1,x0〉 recb))))))))
291 | xA ⇒ b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (
292 b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (
293 b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))))))
294 | xB ⇒ b8_S 〈n1,xA〉 (b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (
295 b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (
296 b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb))))))))))
297 | xC ⇒ b8_S 〈n1,xB〉 (b8_S 〈n1,xA〉 (b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (
298 b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (
299 b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))))))))
300 | xD ⇒ b8_S 〈n1,xC〉 (b8_S 〈n1,xB〉 (b8_S 〈n1,xA〉 (b8_S 〈n1,x9〉 (
301 b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (
302 b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (
303 b8_S 〈n1,x0〉 recb))))))))))))
304 | xE ⇒ b8_S 〈n1,xD〉 (b8_S 〈n1,xC〉 (b8_S 〈n1,xB〉 (b8_S 〈n1,xA〉 (
305 b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (
306 b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (
307 b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))))))))))
308 | xF ⇒ b8_S 〈n1,xE〉 (b8_S 〈n1,xD〉 (b8_S 〈n1,xC〉 (b8_S 〈n1,xB〉 (
309 b8_S 〈n1,xA〉 (b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (
310 b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (
311 b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb))))))))))))))
315 nlemma b8_to_recb8 : Πb.rec_byte8 b.
316 #b; nletin K ≝ (b8_to_recb8_aux3
317 (b8h b) (b8l b) (b8_to_recb8_aux2 (b8h b) (ex_to_recex (b8h b))));
318 ncases b in K; #e1; #e2; #K; napply K;
322 ndefinition b8_to_recb8 : Πb.rec_byte8 b ≝
324 [ mk_comp_num h l ⇒ b8_to_recb8_aux3 h l (b8_to_recb8_aux2 h (ex_to_recex h)) ].
326 (* ottali → esadecimali *)
327 ndefinition b8_of_bit ≝
329 [ t00 ⇒ 〈x0,x0〉 | t01 ⇒ 〈x0,x1〉 | t02 ⇒ 〈x0,x2〉 | t03 ⇒ 〈x0,x3〉
330 | t04 ⇒ 〈x0,x4〉 | t05 ⇒ 〈x0,x5〉 | t06 ⇒ 〈x0,x6〉 | t07 ⇒ 〈x0,x7〉
331 | t08 ⇒ 〈x0,x8〉 | t09 ⇒ 〈x0,x9〉 | t0A ⇒ 〈x0,xA〉 | t0B ⇒ 〈x0,xB〉
332 | t0C ⇒ 〈x0,xC〉 | t0D ⇒ 〈x0,xD〉 | t0E ⇒ 〈x0,xE〉 | t0F ⇒ 〈x0,xF〉
333 | t10 ⇒ 〈x1,x0〉 | t11 ⇒ 〈x1,x1〉 | t12 ⇒ 〈x1,x2〉 | t13 ⇒ 〈x1,x3〉
334 | t14 ⇒ 〈x1,x4〉 | t15 ⇒ 〈x1,x5〉 | t16 ⇒ 〈x1,x6〉 | t17 ⇒ 〈x1,x7〉
335 | t18 ⇒ 〈x1,x8〉 | t19 ⇒ 〈x1,x9〉 | t1A ⇒ 〈x1,xA〉 | t1B ⇒ 〈x1,xB〉
336 | t1C ⇒ 〈x1,xC〉 | t1D ⇒ 〈x1,xD〉 | t1E ⇒ 〈x1,xE〉 | t1F ⇒ 〈x1,xF〉