1 | include "ASM.ma". |
---|
2 | |
---|
3 | ndefinition assembly1 ≝ |
---|
4 | λi: instruction.match i with |
---|
5 | [ ACALL addr ⇒ |
---|
6 | match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with |
---|
7 | [ ADDR11 w ⇒ λ_. |
---|
8 | let 〈v1,v2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S Z))) w in |
---|
9 | [ (v1 @@ [[true; false; false; false; true]]) ; v2 ] |
---|
10 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) |
---|
11 | | ADD addr1 addr2 ⇒ |
---|
12 | match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with |
---|
13 | [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[false;false;true;false;true;r1;r2;r2]]) ] |
---|
14 | | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ] |
---|
15 | | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;false;false;true;true;i1]]) ] |
---|
16 | | DATA b1 ⇒ λ_. [ ([[false;false;true;false;false;true;false;false]]) ; b1 ] |
---|
17 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) |
---|
18 | | ADDC addr1 addr2 ⇒ |
---|
19 | match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with |
---|
20 | [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[false;false;true;true;true;r1;r2;r2]]) ] |
---|
21 | | DIRECT b1 ⇒ λ_.[ ([[false;false;true;true;false;true;false;true]]); b1 ] |
---|
22 | | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;true;false;true;true;i1]]) ] |
---|
23 | | DATA b1 ⇒ λ_. [ ([[false;false;true;true;false;true;false;false]]) ; b1 ] |
---|
24 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) |
---|
25 | | AJMP addr ⇒ |
---|
26 | match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with |
---|
27 | [ ADDR11 w ⇒ λ_. |
---|
28 | let 〈v1,v2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S Z))) w in |
---|
29 | [ (v1 @@ [[false; false; false; false; true]]) ; v2 ] |
---|
30 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) |
---|
31 | | ANL addrs ⇒ |
---|
32 | match addrs with |
---|
33 | [ Left addrs ⇒ match addrs with |
---|
34 | [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in |
---|
35 | match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with |
---|
36 | [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[false;true;false;true;true;r1;r2;r2]]) ] |
---|
37 | | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ] |
---|
38 | | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;true;false;true;true;i1]]) ] |
---|
39 | | DATA b1 ⇒ λ_. [ ([[false;true;false;true;false;true;false;false]]) ; b1 ] |
---|
40 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) |
---|
41 | | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in |
---|
42 | let b1 ≝ |
---|
43 | match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with |
---|
44 | [ DIRECT b1 ⇒ λ_.b1 |
---|
45 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in |
---|
46 | match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with |
---|
47 | [ ACC_A ⇒ λ_.[ ([[false;true;false;true;false;false;true;false]]) ; b1 ] |
---|
48 | | DATA b2 ⇒ λ_. [ ([[false;true;false;true;false;false;true;true]]) ; b1 ; b2 ] |
---|
49 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) |
---|
50 | ] |
---|
51 | | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in |
---|
52 | match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with |
---|
53 | [ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ] |
---|
54 | | N_BIT_ADDR b1 ⇒ λ_. [ ([[true;false;true;true;false;false;false;false]]) ; b1 ] |
---|
55 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] |
---|
56 | | CLR addr ⇒ |
---|
57 | match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with |
---|
58 | [ ACC_A ⇒ λ_. |
---|
59 | [ ([[true; true; true; false; false; true; false; false]]) ] |
---|
60 | | CARRY ⇒ λ_. |
---|
61 | [ ([[true; true; false; false; false; false; true; true]]) ] |
---|
62 | | BIT_ADDR b1 ⇒ λ_. |
---|
63 | [ ([[true; true; false; false; false; false; true; false]]) ; b1 ] |
---|
64 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) |
---|
65 | | CPL addr ⇒ |
---|
66 | match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with |
---|
67 | [ ACC_A ⇒ λ_. |
---|
68 | [ ([[true; true; true; true; false; true; false; false]]) ] |
---|
69 | | CARRY ⇒ λ_. |
---|
70 | [ ([[true; false; true; true; false; false; true; true]]) ] |
---|
71 | | BIT_ADDR b1 ⇒ λ_. |
---|
72 | [ ([[true; false; true; true; false; false; true; false]]) ; b1 ] |
---|
73 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) |
---|
74 | | DA addr ⇒ |
---|
75 | [ ([[true; true; false; true; false; true; false; false]]) ] |
---|
76 | | DEC addr ⇒ |
---|
77 | match addr return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect]] x) → ? with |
---|
78 | [ ACC_A ⇒ λ_. |
---|
79 | [ ([[false; false; false; true; false; true; false; false]]) ] |
---|
80 | | REGISTER r1 r2 r3 ⇒ λ_. |
---|
81 | [ ([[false; false; false; true; true; r1; r2; r3]]) ] |
---|
82 | | DIRECT b1 ⇒ λ_. |
---|
83 | [ ([[false; false; false; true; false; true; false; true]]); b1 ] |
---|
84 | | INDIRECT i1 ⇒ λ_. |
---|
85 | [ ([[false; false; false; true; false; true; true; i1]]) ] |
---|
86 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) |
---|
87 | | DIV addr1 addr2 ⇒ |
---|
88 | [ ([[true;false;false;false;false;true;false;false]]) ] |
---|
89 | | Jump j ⇒ |
---|
90 | match j with |
---|
91 | [ DJNZ addr1 addr2 ⇒ |
---|
92 | let b2 ≝ |
---|
93 | match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with |
---|
94 | [ RELATIVE b2 ⇒ λ_. b2 |
---|
95 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in |
---|
96 | match addr1 return λx. bool_to_Prop (is_in ? [[register;direct]] x) → ? with |
---|
97 | [ REGISTER r1 r2 r3 ⇒ λ_. |
---|
98 | [ ([[true; true; false; true; true; r1; r2; r3]]) ; b2 ] |
---|
99 | | DIRECT b1 ⇒ λ_. |
---|
100 | [ ([[true; true; false; true; false; true; false; true]]); b1; b2 ] |
---|
101 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) |
---|
102 | | JC addr ⇒ |
---|
103 | match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with |
---|
104 | [ RELATIVE b1 ⇒ λ_. |
---|
105 | [ ([[false; true; false; false; false; false; false; false]]); b1 ] |
---|
106 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) |
---|
107 | | JNC addr ⇒ |
---|
108 | match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with |
---|
109 | [ RELATIVE b1 ⇒ λ_. |
---|
110 | [ ([[false; true; false; true; false; false; false; false]]); b1 ] |
---|
111 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) |
---|
112 | | JZ addr ⇒ |
---|
113 | match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with |
---|
114 | [ RELATIVE b1 ⇒ λ_. |
---|
115 | [ ([[false; true; true; false; false; false; false; false]]); b1 ] |
---|
116 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) |
---|
117 | | JNZ addr ⇒ |
---|
118 | match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with |
---|
119 | [ RELATIVE b1 ⇒ λ_. |
---|
120 | [ ([[false; true; true; true; false; false; false; false]]); b1 ] |
---|
121 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) |
---|
122 | | JB addr1 addr2 ⇒ |
---|
123 | let b2 ≝ |
---|
124 | match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with |
---|
125 | [ RELATIVE b2 ⇒ λ_. b2 |
---|
126 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in |
---|
127 | match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with |
---|
128 | [ BIT_ADDR b1 ⇒ λ_. |
---|
129 | [ ([[false; false; true; false; false; false; false; false]]); b1; b2 ] |
---|
130 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) |
---|
131 | | JNB addr1 addr2 ⇒ |
---|
132 | let b2 ≝ |
---|
133 | match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with |
---|
134 | [ RELATIVE b2 ⇒ λ_. b2 |
---|
135 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in |
---|
136 | match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with |
---|
137 | [ BIT_ADDR b1 ⇒ λ_. |
---|
138 | [ ([[false; false; true; true; false; false; false; false]]); b1; b2 ] |
---|
139 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) |
---|
140 | | JBC addr1 addr2 ⇒ |
---|
141 | let b2 ≝ |
---|
142 | match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with |
---|
143 | [ RELATIVE b2 ⇒ λ_. b2 |
---|
144 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in |
---|
145 | match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with |
---|
146 | [ BIT_ADDR b1 ⇒ λ_. |
---|
147 | [ ([[false; false; false; true; false; false; false; false]]); b1; b2 ] |
---|
148 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) |
---|
149 | | CJNE addrs addr3 ⇒ |
---|
150 | let b3 ≝ |
---|
151 | match addr3 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with |
---|
152 | [ RELATIVE b3 ⇒ λ_. b3 |
---|
153 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr3) in |
---|
154 | match addrs with |
---|
155 | [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in |
---|
156 | match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with |
---|
157 | [ DIRECT b1 ⇒ λ_. |
---|
158 | [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ] |
---|
159 | [ DATA b1 ⇒ λ_. |
---|
160 | [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ] |
---|
161 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) |
---|
162 | | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in |
---|
163 | let b2 ≝ |
---|
164 | match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with |
---|
165 | [ DATA b2 ⇒ λ_. b2 |
---|
166 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in |
---|
167 | match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with |
---|
168 | [ DIRECT b1 ⇒ λ_. |
---|
169 | [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ] |
---|
170 | [ DATA b1 ⇒ λ_. |
---|
171 | [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ] |
---|
172 | | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) |
---|
173 | |
---|
174 | ] |
---|
175 | | _ ⇒ [ ] |
---|
176 | ] |
---|
177 | | _ ⇒ [ ]]. |
---|
178 | |
---|
179 | (* |
---|
180 | | `CJNE (`U2 (`REG(r1,r2,r3), `DATA b1), `REL b2) -> |
---|
181 | [mk_byte_from_bits ((true,false,true,true),(true,r1,r2,r3)); b1; b2] |
---|
182 | | `CJNE (`U2 (`INDIRECT i1, `DATA b1), `REL b2) -> |
---|
183 | [mk_byte_from_bits ((true,false,true,true),(false,true,true,i1)); b1; b2] |
---|
184 | |
---|
185 | |
---|
186 | | `INC `A -> |
---|
187 | [mk_byte_from_bits ((false,false,false,false),(false,true,false,false))] |
---|
188 | | `INC (`REG(r1,r2,r3)) -> |
---|
189 | [mk_byte_from_bits ((false,false,false,false),(true,r1,r2,r3))] |
---|
190 | | `INC (`DIRECT b1) -> |
---|
191 | [mk_byte_from_bits ((false,false,false,false),(false,true,false,true)); b1] |
---|
192 | | `INC (`INDIRECT i1) -> |
---|
193 | [mk_byte_from_bits ((false,false,false,false),(false,true,true,i1))] |
---|
194 | | `INC `DPTR -> |
---|
195 | [mk_byte_from_bits ((true,false,true,false),(false,false,true,true))] |
---|
196 | | `JMP `IND_DPTR -> |
---|
197 | [mk_byte_from_bits ((false,true,true,true),(false,false,true,true))] |
---|
198 | | `LCALL (`ADDR16 w) -> |
---|
199 | let (b1,b2) = from_word w in |
---|
200 | [mk_byte_from_bits ((false,false,false,true),(false,false,true,false)); b1; b2] |
---|
201 | | `LJMP (`ADDR16 w) -> |
---|
202 | let (b1,b2) = from_word w in |
---|
203 | [mk_byte_from_bits ((false,false,false,false),(false,false,true,false)); b1; b2] |
---|
204 | | `MOV (`U1 (`A, `REG(r1,r2,r3))) -> |
---|
205 | [mk_byte_from_bits ((true,true,true,false),(true,r1,r2,r3))] |
---|
206 | | `MOV (`U1 (`A, `DIRECT b1)) -> |
---|
207 | [mk_byte_from_bits ((true,true,true,false),(false,true,false,true)); b1] |
---|
208 | | `MOV (`U1 (`A, `INDIRECT i1)) -> |
---|
209 | [mk_byte_from_bits ((true,true,true,false),(false,true,true,i1))] |
---|
210 | | `MOV (`U1 (`A, `DATA b1)) -> |
---|
211 | [mk_byte_from_bits ((false,true,true,true),(false,true,false,false)); b1] |
---|
212 | | `MOV (`U2 (`REG(r1,r2,r3), `A)) -> |
---|
213 | [mk_byte_from_bits ((true,true,true,true),(true,r1,r2,r3))] |
---|
214 | | `MOV (`U2 (`REG(r1,r2,r3), (`DIRECT b1))) -> |
---|
215 | [mk_byte_from_bits ((true,false,true,false),(true,r1,r2,r3)); b1] |
---|
216 | | `MOV (`U2 (`REG(r1,r2,r3), (`DATA b1))) -> |
---|
217 | [mk_byte_from_bits ((false,true,true,true),(true,r1,r2,r3)); b1] |
---|
218 | | `MOV (`U3 (`DIRECT b1, `A)) -> |
---|
219 | [mk_byte_from_bits ((true,true,true,true),(false,true,false,true)); b1] |
---|
220 | | `MOV (`U3 (`DIRECT b1, `REG(r1,r2,r3))) -> |
---|
221 | [mk_byte_from_bits ((true,false,false,false),(true,r1,r2,r3)); b1] |
---|
222 | | `MOV (`U3 (`DIRECT b1, `DIRECT b2)) -> |
---|
223 | [mk_byte_from_bits ((true,false,false,false),(false,true,false,true)); b1; b2] |
---|
224 | | `MOV (`U3 (`DIRECT b1, `INDIRECT i1)) -> |
---|
225 | [mk_byte_from_bits ((true,false,false,false),(false,true,true,i1)); b1] |
---|
226 | | `MOV (`U3 (`DIRECT b1, `DATA b2)) -> |
---|
227 | [mk_byte_from_bits ((false,true,true,true),(false,true,false,true)); b1; b2] |
---|
228 | | `MOV (`U2 (`INDIRECT i1, `A)) -> |
---|
229 | [mk_byte_from_bits ((true,true,true,true),(false,true,true,i1))] |
---|
230 | | `MOV (`U2 (`INDIRECT i1, `DIRECT b1)) -> |
---|
231 | [mk_byte_from_bits ((true,false,true,false),(false,true,true,i1)); b1] |
---|
232 | | `MOV (`U2 (`INDIRECT i1, `DATA b1)) -> |
---|
233 | [mk_byte_from_bits ((false,true,true,true),(false,true,true,i1)); b1] |
---|
234 | | `MOV (`U5 (`C, `BIT b1)) -> |
---|
235 | [mk_byte_from_bits ((true,false,true,false),(false,false,true,false)); b1] |
---|
236 | | `MOV (`U6 (`BIT b1, `C)) -> |
---|
237 | [mk_byte_from_bits ((true,false,false,true),(false,false,true,false)); b1] |
---|
238 | | `MOV (`U4 (`DPTR, `DATA16 w)) -> |
---|
239 | let (b1,b2) = from_word w in |
---|
240 | [mk_byte_from_bits ((true,false,false,true),(false,false,false,false)); b1; b2] |
---|
241 | | `MOVC (`A, `A_DPTR) -> |
---|
242 | [mk_byte_from_bits ((true,false,false,true),(false,false,true,true))] |
---|
243 | | `MOVC (`A, `A_PC) -> |
---|
244 | [mk_byte_from_bits ((true,false,false,false),(false,false,true,true))] |
---|
245 | | `MOVX (`U1 (`A, `EXT_INDIRECT i1)) -> |
---|
246 | [mk_byte_from_bits ((true,true,true,false),(false,false,true,i1))] |
---|
247 | | `MOVX (`U1 (`A, `EXT_IND_DPTR)) -> |
---|
248 | [mk_byte_from_bits ((true,true,true,false),(false,false,false,false))] |
---|
249 | | `MOVX (`U2 (`EXT_INDIRECT i1, `A)) -> |
---|
250 | [mk_byte_from_bits ((true,true,true,true),(false,false,true,i1))] |
---|
251 | | `MOVX (`U2 (`EXT_IND_DPTR, `A)) -> |
---|
252 | [mk_byte_from_bits ((true,true,true,true),(false,false,false,false))] |
---|
253 | | `MUL(`A, `B) -> |
---|
254 | [mk_byte_from_bits ((true,false,true,false),(false,true,false,false))] |
---|
255 | | `NOP -> |
---|
256 | [mk_byte_from_bits ((false,false,false,false),(false,false,false,false))] |
---|
257 | | `ORL (`U1(`A, `REG(r1,r2,r3))) -> |
---|
258 | [mk_byte_from_bits ((false,true,false,false),(true,r1,r2,r3))] |
---|
259 | | `ORL (`U1(`A, `DIRECT b1)) -> |
---|
260 | [mk_byte_from_bits ((false,true,false,false),(false,true,false,true)); b1] |
---|
261 | | `ORL (`U1(`A, `INDIRECT i1)) -> |
---|
262 | [mk_byte_from_bits ((false,true,false,false),(false,true,true,i1))] |
---|
263 | | `ORL (`U1(`A, `DATA b1)) -> |
---|
264 | [mk_byte_from_bits ((false,true,false,false),(false,true,false,false)); b1] |
---|
265 | | `ORL (`U2(`DIRECT b1, `A)) -> |
---|
266 | [mk_byte_from_bits ((false,true,false,false),(false,false,true,false)); b1] |
---|
267 | | `ORL (`U2 (`DIRECT b1, `DATA b2)) -> |
---|
268 | [mk_byte_from_bits ((false,true,false,false),(false,false,true,true)); b1; b2] |
---|
269 | | `ORL (`U3 (`C, `BIT b1)) -> |
---|
270 | [mk_byte_from_bits ((false,true,true,true),(false,false,true,false)); b1] |
---|
271 | | `ORL (`U3 (`C, `NBIT b1)) -> |
---|
272 | [mk_byte_from_bits ((true,false,true,false),(false,false,false,false)); b1] |
---|
273 | | `POP (`DIRECT b1) -> |
---|
274 | [mk_byte_from_bits ((true,true,false,true),(false,false,false,false)); b1] |
---|
275 | | `PUSH (`DIRECT b1) -> |
---|
276 | [mk_byte_from_bits ((true,true,false,false),(false,false,false,false)); b1] |
---|
277 | | `RET -> |
---|
278 | [mk_byte_from_bits ((false,false,true,false),(false,false,true,false))] |
---|
279 | | `RETI -> |
---|
280 | [mk_byte_from_bits ((false,false,true,true),(false,false,true,false))] |
---|
281 | | `RL `A -> |
---|
282 | [mk_byte_from_bits ((false,false,true,false),(false,false,true,true))] |
---|
283 | | `RLC `A -> |
---|
284 | [mk_byte_from_bits ((false,false,true,true),(false,false,true,true))] |
---|
285 | | `RR `A -> |
---|
286 | [mk_byte_from_bits ((false,false,false,false),(false,false,true,true))] |
---|
287 | | `RRC `A -> |
---|
288 | [mk_byte_from_bits ((false,false,false,true),(false,false,true,true))] |
---|
289 | | `SETB `C -> |
---|
290 | [mk_byte_from_bits ((true,true,false,true),(false,false,true,true))] |
---|
291 | | `SETB (`BIT b1) -> |
---|
292 | [mk_byte_from_bits ((true,true,false,true),(false,false,true,false)); b1] |
---|
293 | | `SJMP (`REL b1) -> |
---|
294 | [mk_byte_from_bits ((true,false,false,false),(false,false,false,false)); b1] |
---|
295 | | `SUBB (`A, `REG(r1,r2,r3)) -> |
---|
296 | [mk_byte_from_bits ((true,false,false,true),(true,r1,r2,r3))] |
---|
297 | | `SUBB (`A, `DIRECT b1) -> |
---|
298 | [mk_byte_from_bits ((true,false,false,true),(false,true,false,true)); b1] |
---|
299 | | `SUBB (`A, `INDIRECT i1) -> |
---|
300 | [mk_byte_from_bits ((true,false,false,true),(false,true,true,i1))] |
---|
301 | | `SUBB (`A, `DATA b1) -> |
---|
302 | [mk_byte_from_bits ((true,false,false,true),(false,true,false,false)); b1] |
---|
303 | | `SWAP `A -> |
---|
304 | [mk_byte_from_bits ((true,true,false,false),(false,true,false,false))] |
---|
305 | | `XCH (`A, `REG(r1,r2,r3)) -> |
---|
306 | [mk_byte_from_bits ((true,true,false,false),(true,r1,r2,r3))] |
---|
307 | | `XCH (`A, `DIRECT b1) -> |
---|
308 | [mk_byte_from_bits ((true,true,false,false),(false,true,false,true)); b1] |
---|
309 | | `XCH (`A, `INDIRECT i1) -> |
---|
310 | [mk_byte_from_bits ((true,true,false,false),(false,true,true,i1))] |
---|
311 | | `XCHD(`A, `INDIRECT i1) -> |
---|
312 | [mk_byte_from_bits ((true,true,false,true),(false,true,true,i1))] |
---|
313 | | `XRL(`U1(`A, `REG(r1,r2,r3))) -> |
---|
314 | [mk_byte_from_bits ((false,true,true,false),(true,r1,r2,r3))] |
---|
315 | | `XRL(`U1(`A, `DIRECT b1)) -> |
---|
316 | [mk_byte_from_bits ((false,true,true,false),(false,true,false,true)); b1] |
---|
317 | | `XRL(`U1(`A, `INDIRECT i1)) -> |
---|
318 | [mk_byte_from_bits ((false,true,true,false),(false,true,true,i1))] |
---|
319 | | `XRL(`U1(`A, `DATA b1)) -> |
---|
320 | [mk_byte_from_bits ((false,true,true,false),(false,true,false,false)); b1] |
---|
321 | | `XRL(`U2(`DIRECT b1, `A)) -> |
---|
322 | [mk_byte_from_bits ((false,true,true,false),(false,false,true,false)); b1] |
---|
323 | | `XRL(`U2(`DIRECT b1, `DATA b2)) -> |
---|
324 | [mk_byte_from_bits ((false,true,true,false),(false,false,true,true)); b1; b2] |
---|
325 | ;; |
---|
326 | |
---|
327 | |
---|
328 | |
---|
329 | nrecord Sigma (A: Type[0]) (T: A → Type[0]) : Type[0] ≝ { |
---|
330 | elem:> A; |
---|
331 | witness: T elem |
---|
332 | }. |
---|
333 | |
---|
334 | interpretation "Sigma" 'sigma T = (Sigma ? T). |
---|
335 | |
---|
336 | naxiom daemon: False. |
---|
337 | |
---|
338 | naxiom decode_register: Vector Bool (S (S (S Z))) → [reg]. |
---|
339 | naxiom decode_direct: Vector Bool (S (S (S Z))) → [direct]. |
---|
340 | |
---|
341 | ndefinition decode_tbl0: List ((Σn.Vector Bool n) × (Vector Bool (S (S (S Z))) → Instruction)) |
---|
342 | ≝ |
---|
343 | [mk_Cartesian ?? |
---|
344 | (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true]) |
---|
345 | (λl. |
---|
346 | ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) |
---|
347 | (mk_subaddressing_mode ? ? (decode_register l) ?)); |
---|
348 | mk_Cartesian ?? |
---|
349 | (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true]) |
---|
350 | (λl. |
---|
351 | ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) |
---|
352 | (mk_subaddressing_mode ? ? (decode_direct l) ?)) ]. |
---|
353 | ncases daemon. |
---|
354 | nqed. |
---|
355 | |
---|
356 | |
---|
357 | naxiom decode_register: List Bool → [reg]. |
---|
358 | naxiom decode_direct: List Bool → [direct]. |
---|
359 | |
---|
360 | ndefinition decode_tbl0: List (List Bool × (List Bool → Instruction)) |
---|
361 | ≝ |
---|
362 | [mk_Cartesian ?? |
---|
363 | [ false; false; true; false; true] |
---|
364 | (λl. |
---|
365 | ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) |
---|
366 | (mk_subaddressing_mode ? ? (decode_register l) ?)); |
---|
367 | mk_Cartesian ?? |
---|
368 | [ false; false; true; false; true] |
---|
369 | (λl. |
---|
370 | ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) |
---|
371 | (mk_subaddressing_mode ? ? (decode_direct l) ?)) ]. |
---|
372 | ncases daemon. |
---|
373 | nqed. |
---|
374 | |
---|
375 | |
---|
376 | ndefinition decode_tbl1: |
---|
377 | List (List Bool × Σaddr:all_types. [addr] → Instruction) |
---|
378 | ≝ |
---|
379 | [mk_Cartesian ?? |
---|
380 | [ false; false; true; false; true] |
---|
381 | (mk_Sigma ? (λaddr:all_types. [addr] → Instruction) |
---|
382 | reg |
---|
383 | (λa. |
---|
384 | ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) |
---|
385 | (mk_subaddressing_mode ? ? a ?))) ]. |
---|
386 | ncases daemon. |
---|
387 | nqed. |
---|
388 | |
---|
389 | ndefinition decode_tbl2: |
---|
390 | List (List Bool × Σaddr:all_types. [addr] → Instruction) |
---|
391 | ≝ |
---|
392 | [mk_Cartesian ?? |
---|
393 | [ false; false; true; false; false; true; false; true] |
---|
394 | (mk_Sigma ? (λaddr:all_types. [addr] → Instruction) |
---|
395 | direct |
---|
396 | (λa. |
---|
397 | ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) |
---|
398 | (mk_subaddressing_mode ? ? a ?))) ]. |
---|
399 | ncases daemon. |
---|
400 | nqed. |
---|
401 | |
---|
402 | ndefinition decode_tbl ≝ decode_tbl1 @ decode_tbl2. |
---|
403 | |
---|
404 | decode_addr_mode; ∀addr:all_types. List Bool → [addr]. |
---|
405 | |
---|
406 | decode ≝ |
---|
407 | λl:List Bit. |
---|
408 | List.iter |
---|
409 | (fun l0 addr mk_f → |
---|
410 | match split_prefix l l0 with |
---|
411 | [ None ⇒ ... |
---|
412 | | Some r ⇒ mk_f (decode_addr_mode r) ] |
---|
413 | |
---|
414 | ) decode_tbl |
---|
415 | |
---|
416 | encode ≝ |
---|
417 | |
---|
418 | ndefinition decode_tbl: |
---|
419 | List (List Bool × Σaddr:all_types. [addr] → Instruction) |
---|
420 | ≝ |
---|
421 | [mk_Cartesian ?? |
---|
422 | [ False; False; True; False; True] |
---|
423 | (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction) |
---|
424 | reg |
---|
425 | (λa:subaddressing_mode ? [reg]. |
---|
426 | ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) |
---|
427 | (mk_subaddressing_mode ? ? a ?))); |
---|
428 | mk_Cartesian ?? |
---|
429 | [ False; False; True; False; False; True; False; True] |
---|
430 | (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction) |
---|
431 | direct |
---|
432 | (λa:subaddressing_mode ? [direct]. |
---|
433 | ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) |
---|
434 | (mk_subaddressing_mode ? ? a ?))) |
---|
435 | ]. |
---|
436 | nnormalize; |
---|
437 | |
---|
438 | ]. |
---|
439 | *) |
---|