source: Deliverables/D4.1/Matita/Fetch.ma @ 465

Last change on this file since 465 was 465, checked in by mulligan, 9 years ago

Moved over to standard library.

File size: 20.3 KB
Line 
1include "BitVectorTrie.ma".
2include "Arithmetic.ma".
3include "ASM.ma".
4
5ndefinition next: BitVectorTrie Byte 16 → Word → Word × Byte ≝
6 λpmem,pc.
7  let 〈x,res〉 ≝ half_add … pc (bitvector_of_nat 16 (S O)) in
8   〈res, lookup … pc pmem (zero 8)〉.
9
10(* timings taken from SIEMENS *)
11
12ndefinition fetch: BitVectorTrie Byte 16 → Word → instruction × Word × nat ≝
13 λpmem,pc.
14  let 〈pc,v〉 ≝ next pmem pc in
15   let 〈b,v〉≝  head … v in if b then
16    let 〈b,v〉≝  head … v in if b then
17     let 〈b,v〉≝  head … v in if b then
18      let 〈b,v〉≝  head … v in if b then
19       let 〈b,v〉≝  head … v in if b then
20        〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,ACC_A〉))))), pc〉, 1〉
21       else
22        let 〈b,v〉≝  head … v in if b then
23         let 〈b,v〉≝  head … v in if b then
24          〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),ACC_A〉))))), pc〉, 1〉
25         else
26          let 〈b,v〉≝  head … v in if b then
27           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉)))), pc〉, 1〉
28          else
29           〈〈CPL … ACC_A, pc〉, 1〉
30        else
31         let 〈b,v〉≝  head … v in if b then
32          〈〈MOVX … (inr … 〈EXT_INDIRECT (from_singl … v),ACC_A〉), pc〉, 2〉
33         else
34          let 〈b,v〉≝  head … v in if b then
35           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
36          else
37           〈〈MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉), pc〉, 2〉
38      else
39       let 〈b,v〉≝  head … v in if b then
40        〈〈MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,REGISTER v〉))))), pc〉, 1〉
41       else
42        let 〈b,v〉≝  head … v in if b then
43         let 〈b,v〉≝  head … v in if b then
44          〈〈MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))))), pc〉, 1〉
45         else
46          let 〈b,v〉≝  head … v in if b then
47           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉))))), pc〉, 1〉
48          else
49           〈〈CLR … ACC_A, pc〉, 1〉
50        else
51         let 〈b,v〉≝  head … v in if b then
52          〈〈MOVX … (inl … 〈ACC_A,EXT_INDIRECT (from_singl … v)〉), pc〉, 2〉
53         else
54          let 〈b,v〉≝  head … v in if b then
55           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
56          else
57           〈〈MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉), pc〉, 2〉
58     else
59      let 〈b,v〉≝  head … v in if b then
60       let 〈b,v〉≝  head … v in if b then
61        let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉
62       else
63        let 〈b,v〉≝  head … v in if b then
64         let 〈b,v〉≝  head … v in if b then
65          〈〈XCHD … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉
66         else
67          let 〈b,v〉≝  head … v in if b then
68           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉
69          else
70           〈〈DA … ACC_A, pc〉, 1〉
71        else
72         let 〈b,v〉≝  head … v in if b then
73          let 〈b,v〉≝  head … v in if b then
74           〈〈SETB … CARRY, pc〉, 1〉
75          else
76           let 〈pc,b1〉≝ next pmem pc in 〈〈SETB … (BIT_ADDR b1), pc〉, 1〉
77         else
78          let 〈b,v〉≝  head … v in if b then
79           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
80          else
81           let 〈pc,b1〉≝ next pmem pc in 〈〈POP … (DIRECT b1), pc〉, 2〉
82      else
83       let 〈b,v〉≝  head … v in if b then
84        〈〈XCH … ACC_A (REGISTER v), pc〉, 1〉
85       else
86        let 〈b,v〉≝  head … v in if b then
87         let 〈b,v〉≝  head … v in if b then
88          〈〈XCH … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉
89         else
90          let 〈b,v〉≝  head … v in if b then
91           let 〈pc,b1〉≝ next pmem pc in 〈〈XCH … ACC_A (DIRECT b1), pc〉, 1〉
92          else
93           〈〈SWAP … ACC_A, pc〉, 1〉
94        else
95         let 〈b,v〉≝  head … v in if b then
96          let 〈b,v〉≝  head … v in if b then
97           〈〈CLR … CARRY, pc〉, 1〉
98          else
99           let 〈pc,b1〉≝ next pmem pc in 〈〈CLR … (BIT_ADDR b1), pc〉, 1〉
100         else
101          let 〈b,v〉≝  head … v in if b then
102           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
103          else
104           let 〈pc,b1〉≝ next pmem pc in 〈〈PUSH … (DIRECT b1), pc〉, 2〉
105    else
106     let 〈b,v〉≝  head … v in if b then
107      let 〈b,v〉≝  head … v in if b then
108       let 〈b,v〉≝  head … v in if b then
109        let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE …  (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
110       else
111        let 〈b,v〉≝  head … v in if b then
112         let 〈b,v〉≝  head … v in if b then
113          let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉
114         else
115          let 〈b,v〉≝  head … v in if b then
116           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE …  (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉
117          else
118           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
119        else
120         let 〈b,v〉≝  head … v in if b then
121          let 〈b,v〉≝  head … v in if b then
122           〈〈CPL … CARRY, pc〉, 1〉
123          else
124           let 〈pc,b1〉≝ next pmem pc in 〈〈CPL … (BIT_ADDR b1), pc〉, 1〉
125         else
126          let 〈b,v〉≝  head … v in if b then
127           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
128          else
129           let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉), pc〉, 2〉
130      else
131       let 〈b,v〉≝  head … v in if b then
132        let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉))))), pc〉, 2〉
133       else
134        let 〈b,v〉≝  head … v in if b then
135         let 〈b,v〉≝  head … v in if b then
136          let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉))))), pc〉, 2〉
137         else
138          〈〈MUL … ACC_A ACC_B, pc〉, 4〉
139        else
140         let 〈b,v〉≝  head … v in if b then
141          let 〈b,v〉≝  head … v in if b then
142           〈〈INC … DPTR, pc〉, 2〉
143          else
144           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 1〉
145         else
146          let 〈b,v〉≝  head … v in if b then
147           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
148          else
149           let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉), pc〉, 2〉
150     else
151      let 〈b,v〉≝  head … v in if b then
152       let 〈b,v〉≝  head … v in if b then
153        〈〈SUBB … ACC_A (REGISTER v), pc〉, 1〉
154       else
155        let 〈b,v〉≝  head … v in if b then
156         let 〈b,v〉≝  head … v in if b then
157          〈〈SUBB … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉
158         else
159          let 〈b,v〉≝  head … v in if b then
160           let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB … ACC_A (DIRECT b1), pc〉, 1〉
161          else
162           let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB … ACC_A (DATA b1), pc〉, 1〉
163        else
164         let 〈b,v〉≝  head … v in if b then
165          let 〈b,v〉≝  head … v in if b then
166           〈〈MOVC … ACC_A (ACC_DPTR), pc〉, 2〉
167          else
168           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inr … 〈BIT_ADDR b1,CARRY〉), pc〉, 2〉
169         else
170          let 〈b,v〉≝  head … v in if b then
171           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
172          else
173           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉))), pc〉, 2〉
174      else
175       let 〈b,v〉≝  head … v in if b then
176        let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉)))), pc〉, 2〉
177       else
178        let 〈b,v〉≝  head … v in if b then
179         let 〈b,v〉≝  head … v in if b then
180          let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉)))), pc〉, 2〉
181         else
182          let 〈b,v〉≝  head … v in if b then
183           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉)))), pc〉, 2〉
184          else
185           〈〈DIV … ACC_A ACC_B, pc〉, 4〉
186        else
187         let 〈b,v〉≝  head … v in if b then
188          let 〈b,v〉≝  head … v in if b then
189           〈〈MOVC … ACC_A (ACC_PC), pc〉, 2〉
190          else
191           let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inr … 〈CARRY,BIT_ADDR b1〉), pc〉, 2〉
192         else
193          let 〈b,v〉≝  head … v in if b then
194           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
195          else
196           let 〈pc,b1〉≝ next pmem pc in 〈〈SJMP … (RELATIVE b1), pc〉, 2〉
197   else
198    let 〈b,v〉≝  head … v in if b then
199     let 〈b,v〉≝  head … v in if b then
200      let 〈b,v〉≝  head … v in if b then
201       let 〈b,v〉≝  head … v in if b then
202        let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉))))), pc〉, 1〉
203       else
204        let 〈b,v〉≝  head … v in if b then
205         let 〈b,v〉≝  head … v in if b then
206          let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉))))), pc〉, 1〉
207         else
208          let 〈b,v〉≝  head … v in if b then
209           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉)))), pc〉, 3〉
210          else
211           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉))))), pc〉, 1〉
212        else
213         let 〈b,v〉≝  head … v in if b then
214          let 〈b,v〉≝  head … v in if b then
215           〈〈JMP … INDIRECT_DPTR, pc〉, 2〉
216          else
217           let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inr … 〈CARRY,BIT_ADDR b1〉), pc〉, 2〉
218         else
219          let 〈b,v〉≝  head … v in if b then
220           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
221          else
222           let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JNZ … (RELATIVE b1)), pc〉, 2〉
223      else
224       let 〈b,v〉≝  head … v in if b then
225        〈〈XRL … (inl … 〈ACC_A,REGISTER v〉), pc〉, 1〉
226       else
227        let 〈b,v〉≝  head … v in if b then
228         let 〈b,v〉≝  head … v in if b then
229          〈〈XRL … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉), pc〉, 1〉
230         else
231          let 〈b,v〉≝  head … v in if b then
232           let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (inl … 〈ACC_A,DIRECT b1〉), pc〉, 1〉
233          else
234           let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (inl … 〈ACC_A,DATA b1〉), pc〉, 1〉
235        else
236         let 〈b,v〉≝  head … v in if b then
237          let 〈b,v〉≝  head … v in if b then
238           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈XRL … (inr … 〈DIRECT b1,DATA b2〉), pc〉, 2〉
239          else
240           let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (inr … 〈DIRECT b1,ACC_A〉), pc〉, 1〉
241         else
242          let 〈b,v〉≝  head … v in if b then
243           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
244          else
245           let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JZ … (RELATIVE b1)), pc〉, 2〉
246     else
247      let 〈b,v〉≝  head … v in if b then
248       let 〈b,v〉≝  head … v in if b then
249        〈〈ANL … (inl … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉
250       else
251        let 〈b,v〉≝  head … v in if b then
252         let 〈b,v〉≝  head … v in if b then
253          〈〈ANL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉
254         else
255          let 〈b,v〉≝  head … v in if b then
256           let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉
257          else
258           let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inl … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉
259        else
260         let 〈b,v〉≝  head … v in if b then
261          let 〈b,v〉≝  head … v in if b then
262           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉
263          else
264           let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
265         else
266          let 〈b,v〉≝  head … v in if b then
267           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
268          else
269           let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JNC … (RELATIVE b1)), pc〉, 2〉
270      else
271       let 〈b,v〉≝  head … v in if b then
272        〈〈ORL … (inl … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉
273       else
274        let 〈b,v〉≝  head … v in if b then
275         let 〈b,v〉≝  head … v in if b then
276          〈〈ORL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉
277         else
278          let 〈b,v〉≝  head … v in if b then
279           let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉
280          else
281           let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inl … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉
282        else
283         let 〈b,v〉≝  head … v in if b then
284          let 〈b,v〉≝  head … v in if b then
285           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉
286          else
287           let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
288         else
289          let 〈b,v〉≝  head … v in if b then
290           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
291          else
292           let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JC … (RELATIVE b1)), pc〉, 2〉
293    else
294     let 〈b,v〉≝  head … v in if b then
295      let 〈b,v〉≝  head … v in if b then
296       let 〈b,v〉≝  head … v in if b then
297        〈〈ADDC … ACC_A (REGISTER v), pc〉, 1〉
298       else
299        let 〈b,v〉≝  head … v in if b then
300         let 〈b,v〉≝  head … v in if b then
301          〈〈ADDC … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉
302         else
303          let 〈b,v〉≝  head … v in if b then
304           let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC … ACC_A (DIRECT b1), pc〉, 1〉
305          else
306           let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC … ACC_A (DATA b1), pc〉, 1〉
307        else
308         let 〈b,v〉≝  head … v in if b then
309          let 〈b,v〉≝  head … v in if b then
310           〈〈RLC … ACC_A, pc〉, 1〉
311          else
312           〈〈RETI …, pc〉, 2〉
313         else
314          let 〈b,v〉≝  head … v in if b then
315           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
316          else
317           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
318      else
319       let 〈b,v〉≝  head … v in if b then
320        〈〈ADD … ACC_A (REGISTER v), pc〉, 1〉
321       else
322        let 〈b,v〉≝  head … v in if b then
323         let 〈b,v〉≝  head … v in if b then
324          〈〈ADD … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉
325         else
326          let 〈b,v〉≝  head … v in if b then
327           let 〈pc,b1〉≝ next pmem pc in 〈〈ADD … ACC_A (DIRECT b1), pc〉, 1〉
328          else
329           let 〈pc,b1〉≝ next pmem pc in 〈〈ADD … ACC_A (DATA b1), pc〉, 1〉
330        else
331         let 〈b,v〉≝  head … v in if b then
332          let 〈b,v〉≝  head … v in if b then
333           〈〈RL … ACC_A, pc〉, 1〉
334          else
335           〈〈RET …, pc〉, 2〉
336         else
337          let 〈b,v〉≝  head … v in if b then
338           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
339          else
340           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
341     else
342      let 〈b,v〉≝  head … v in if b then
343       let 〈b,v〉≝  head … v in if b then
344        〈〈DEC … (REGISTER v), pc〉, 1〉
345       else
346        let 〈b,v〉≝  head … v in if b then
347         let 〈b,v〉≝  head … v in if b then
348          〈〈DEC … (INDIRECT (from_singl … v)), pc〉, 1〉
349         else
350          let 〈b,v〉≝  head … v in if b then
351           let 〈pc,b1〉≝ next pmem pc in 〈〈DEC … (DIRECT b1), pc〉, 1〉
352          else
353           〈〈DEC … ACC_A, pc〉, 1〉
354        else
355         let 〈b,v〉≝  head … v in if b then
356          let 〈b,v〉≝  head … v in if b then
357           〈〈RRC … ACC_A, pc〉, 1〉
358          else
359           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉
360         else
361          let 〈b,v〉≝  head … v in if b then
362           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
363          else
364           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
365      else
366       let 〈b,v〉≝  head … v in if b then
367        〈〈INC … (REGISTER v), pc〉, 1〉
368       else
369        let 〈b,v〉≝  head … v in if b then
370         let 〈b,v〉≝  head … v in if b then
371          〈〈INC … (INDIRECT (from_singl … v)), pc〉, 1〉
372         else
373          let 〈b,v〉≝  head … v in if b then
374           let 〈pc,b1〉≝ next pmem pc in 〈〈INC … (DIRECT b1), pc〉, 1〉
375          else
376           〈〈INC … ACC_A, pc〉, 1〉
377        else
378         let 〈b,v〉≝  head … v in if b then
379          let 〈b,v〉≝  head … v in if b then
380           〈〈RR … ACC_A, pc〉, 1〉
381          else
382           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉
383         else
384          let 〈b,v〉≝  head … v in if b then
385           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
386          else
387           〈〈NOP …, pc〉, 1〉.
388 @.
389nqed.
Note: See TracBrowser for help on using the repository browser.