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

Last change on this file since 688 was 475, checked in by mulligan, 9 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.