source: src/ASM/new-matita-development/Fetch.ma @ 688

Last change on this file since 688 was 475, checked in by mulligan, 10 years ago

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