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

Last change on this file since 323 was 323, checked in by sacerdot, 9 years ago

...

File size: 19.5 KB
Line 
1include "BitVectorTrie.ma".
2include "Arithmetic.ma".
3include "ASM.ma".
4
5ndefinition next: BitVectorTrie Byte sixteen → Word → Word × Byte ≝
6 λpmem,pc.
7  let 〈x,res〉 ≝ half_add ? pc (bitvector_of_nat sixteen (S Z)) in
8   〈res, lookup … pc pmem (zero eight)〉.
9
10(* timings taken from SIEMENS *)
11
12ndefinition fetch: BitVectorTrie Byte sixteen → 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 ? ((Left ?? (Left ?? (Left ?? (Left ?? (Right ?? (? 〈REGISTER v,ACC_A〉))))))), pc〉, one〉
21       else
22        let 〈b,v〉≝  head … v in if b then
23         let 〈b,v〉≝  head … v in if b then
24          ?(*〈〈MOV (U2 (INDIRECT (from_singl … v)) ACC_A), pc〉, one〉*)
25         else
26          let 〈b,v〉≝  head … v in if b then
27           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈MOV (U3 (DIRECT b1) ACC_A), pc〉, one〉*)
28          else
29           〈〈CPL … ACC_A, pc〉, one〉
30        else
31         let 〈b,v〉≝  head … v in if b then
32          ?(*〈〈MOVX (U2 (EXT_INDIRECT (from_singl … v)) ACC_A), pc〉, two〉*)
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〉, two〉
36          else
37           ?(*〈〈MOVX (U2 (EXT_IND_DPTR) ACC_A), pc〉, two〉*)
38      else
39       let 〈b,v〉≝  head … v in if b then
40        〈〈MOV ? (Left ?? (Left ?? (Left ?? (Left ?? (Left ?? (? 〈ACC_A,REGISTER v〉)))))), pc〉, one〉
41       else
42        let 〈b,v〉≝  head … v in if b then
43         let 〈b,v〉≝  head … v in if b then
44          ?(*〈〈MOV (U1 ACC_A (INDIRECT (from_singl … v))), pc〉, one〉*)
45         else
46          let 〈b,v〉≝  head … v in if b then
47           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈MOV (U1 ACC_A (DIRECT b1)), pc〉, one〉*)
48          else
49           〈〈CLR … ACC_A, pc〉, one〉
50        else
51         let 〈b,v〉≝  head … v in if b then
52          ?(*〈〈MOVX (U1 ACC_A (EXT_INDIRECT (from_singl … v))), pc〉, two〉*)
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〉, two〉
56          else
57           ?(*〈〈MOVX (U1 ACC_A EXT_IND_DPTR), pc〉, two〉*)
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 … (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, two〉
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〉, one〉
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 … (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, two〉
69          else
70           〈〈DA … ACC_A, pc〉, one〉
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〉, one〉
75          else
76           let 〈pc,b1〉≝ next pmem pc in 〈〈SETB … (BIT_ADDR (from_singl … b1)), pc〉, one〉
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〉, two〉
80          else
81           let 〈pc,b1〉≝ next pmem pc in 〈〈POP … (DIRECT b1), pc〉, two〉
82      else
83       let 〈b,v〉≝  head … v in if b then
84        〈〈XCH … ACC_A (REGISTER v), pc〉, one〉
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〉, one〉
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〉, one〉
92          else
93           〈〈SWAP … ACC_A, pc〉, one〉
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〉, one〉
98          else
99           let 〈pc,b1〉≝ next pmem pc in 〈〈CLR … (BIT_ADDR b1), pc〉, one〉
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〉, two〉
103          else
104           let 〈pc,b1〉≝ next pmem pc in 〈〈PUSH … (DIRECT b1), pc〉, two〉
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 … (CJNE …  (U2 (REGISTER v) DATA b1) (RELATIVE b2)), pc〉, two〉*)
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 … (CJNE … (U2 (INDIRECT (from_singl … v)) (DATA b1)) (RELATIVE b2)), pc〉, two〉*)
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 … (CJNE …  (U1 ACC_A (DIRECT b1)) (RELATIVE b2)), pc〉, two〉*)
117          else
118           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in ?(*〈〈Jump … (CJNE … (U1 ACC_A (DATA b1)) (RELATIVE b2)), pc〉, two〉*)
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〉, one〉
123          else
124           let 〈pc,b1〉≝ next pmem pc in 〈〈CPL … (BIT_ADDR b1), pc〉, one〉
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〉, two〉
128          else
129           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ANL (U3 C (N_BIT_ADDR b1)), pc〉, two〉*)
130      else
131       let 〈b,v〉≝  head … v in if b then
132        let 〈pc,b1〉≝ next pmem pc in ?(*〈〈MOV (U2 (REGISTER v) (DIRECT b1)), pc〉, two〉*)
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 (U2 (INDIRECT (from_singl … v)) (DIRECT b1)), pc〉, two〉*)
137         else
138          〈〈MUL … ACC_A ACC_B, pc〉, four〉
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〉, two〉
143          else
144           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈MOV (U5 C (BIT_ADDR b1)), pc〉, one〉*)
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〉, two〉
148          else
149           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ORL (U3 C (N_BIT_ADDR b1)), pc〉, two〉*)
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〉, one〉
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_singg … v)), pc〉, one〉
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〉, one〉
161          else
162           let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB … ACC_A (DATA b1), pc〉, one〉
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_A_DPTR), pc〉, two〉
167          else
168           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈MOV (U6 (BIT_ADDR b1) C), pc〉, two〉*)
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〉, two〉
172          else
173           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in ?(*〈〈MOV (U4 DPTR (DATA16 (mk_word b1 b2))), pc〉, two〉*)
174      else
175       let 〈b,v〉≝  head … v in if b then
176        let 〈pc,b1〉≝ next pmem pc in ?(*〈〈MOV (U3 (DIRECT b1) (REGISTER v)), pc〉, two〉*)
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 (U3 (DIRECT b1) (INDIRECT (from_singl … v))), pc〉, two〉*)
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 (U3 (DIRECT b1) (DIRECT b2)), pc〉, two〉*)
184          else
185           〈〈DIV … ACC_A ACC_B, pc〉, four〉
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_A_PC), pc〉, two〉
190          else
191           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ANL (U3 C (BIT_ADDR b1)), pc〉, two〉*)
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〉, two〉
195          else
196           let 〈pc,b1〉≝ next pmem pc in 〈〈SJMP … (RELATIVE b1), pc〉, two〉
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 (U2 (REGISTER v) (DATA b1)), pc〉, one〉*)
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 (U2 (INDIRECT (from_singl … v)) (DATA b1)), pc〉, one〉*)
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 (U3 (DIRECT b1) (DATA b2)), pc〉, three〉*)
210          else
211           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈MOV (U1 ACC_A (DATA b1)), pc〉, one〉*)
212        else
213         let 〈b,v〉≝  head … v in if b then
214          let 〈b,v〉≝  head … v in if b then
215           〈〈JMP … IND_DPTR, pc〉, two〉
216          else
217           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ORL (U3 C (BIT_ADDR b1)), pc〉, two〉*)
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〉, two〉
221          else
222           let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JNZ … (RELATIVE b1)), pc〉, two〉
223      else
224       let 〈b,v〉≝  head … v in if b then
225        ?(*〈〈XRL(U1 ACC_A (REGISTER v)), pc〉, one〉*)
226       else
227        let 〈b,v〉≝  head … v in if b then
228         let 〈b,v〉≝  head … v in if b then
229          ?(*〈〈XRL(U1 ACC_A (INDIRECT (from_singl … v))), pc〉, one〉*)
230         else
231          let 〈b,v〉≝  head … v in if b then
232           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈XRL(U1 ACC_A (DIRECT b1)), pc〉, one〉*)
233          else
234           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈XRL(U1 ACC_A (DATA b1)), pc〉, one〉*)
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(U2 (DIRECT b1) (DATA b2)), pc〉, two〉*)
239          else
240           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈XRL(U2 (DIRECT b1) ACC_A), pc〉, one〉*)
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〉, two〉
244          else
245           let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JZ … (RELATIVE b1)), pc〉, two〉
246     else
247      let 〈b,v〉≝  head … v in if b then
248       let 〈b,v〉≝  head … v in if b then
249        ?(*〈〈ANL (U1 ACC_A (REGISTER v)), pc〉, one〉*)
250       else
251        let 〈b,v〉≝  head … v in if b then
252         let 〈b,v〉≝  head … v in if b then
253          ?(*〈〈ANL (U1 ACC_A (INDIRECT (from_singl … v))), pc〉, one〉*)
254         else
255          let 〈b,v〉≝  head … v in if b then
256           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ANL (U1 ACC_A (DIRECT b1)), pc〉, one〉*)
257          else
258           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ANL (U1 ACC_A (DATA b1)), pc〉, one〉*)
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 (U2 (DIRECT b1) (DATA b2)), pc〉, two〉*)
263          else
264           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ANL (U2 (DIRECT b1) A), pc〉, one〉*)
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〉, two〉
268          else
269           let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JNC … (RELATIVE b1)), pc〉, two〉
270      else
271       let 〈b,v〉≝  head … v in if b then
272        ?(*〈〈ORL (U1 ACC_A (REGISTER v)), pc〉, one〉*)
273       else
274        let 〈b,v〉≝  head … v in if b then
275         let 〈b,v〉≝  head … v in if b then
276          ?(*〈〈ORL (U1 ACC_A (INDIRECT (from_singl … v))), pc〉, one〉*)
277         else
278          let 〈b,v〉≝  head … v in if b then
279           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ORL (U1 ACC_A (DIRECT b1)), pc〉, one〉*)
280          else
281           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ORL (U1 ACC_A (DATA b1)), pc〉, one〉*)
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 (U2 (DIRECT b1) (DATA b2)), pc〉, two〉*)
286          else
287           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ORL (U2 (DIRECT b1) ACC_A), pc〉, one〉*)
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〉, two〉
291          else
292           let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JC … (RELATIVE b1)), pc〉, two〉
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〉, one〉
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〉, one〉
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〉, one〉
305          else
306           let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC … ACC_A (DATA b1), pc〉, one〉
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〉, one〉
311          else
312           〈〈RETI …, pc〉, two〉
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〉, two〉
316          else
317           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (JNB (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉
318      else
319       let 〈b,v〉≝  head … v in if b then
320        〈〈ADD … ACC_A (REGISTER v), pc〉, one〉
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〉, one〉
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〉, one〉
328          else
329           let 〈pc,b1〉≝ next pmem pc in 〈〈ADD … ACC_A (DATA b1), pc〉, one〉
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〉, one〉
334          else
335           〈〈RET …, pc〉, two〉
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〉, two〉
339          else
340           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉
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〉, one〉
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〉, one〉
349         else
350          let 〈b,v〉≝  head … v in if b then
351           let 〈pc,b1〉≝ next pmem pc in 〈〈DEC … (DIRECT b1), pc〉, one〉
352          else
353           〈〈DEC … ACC_A, pc〉, one〉
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〉, one〉
358          else
359           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LCALL … (ADDR16 (mk_word b1 b2)), pc〉, two〉
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〉, two〉
363          else
364           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉
365      else
366       let 〈b,v〉≝  head … v in if b then
367        〈〈INC … (REGISTER v), pc〉, one〉
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〉, one〉
372         else
373          let 〈b,v〉≝  head … v in if b then
374           let 〈pc,b1〉≝ next pmem pc in 〈〈INC … (DIRECT b1), pc〉, one〉
375          else
376           〈〈INC … ACC_A, pc〉, one〉
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〉, one〉
381          else
382           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LJMP … (ADDR16 (mk_word b1 b2)), pc〉, two〉
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〉, two〉
386          else
387           〈〈NOP …, pc〉, one〉.
388 @.
389nqed.
Note: See TracBrowser for help on using the repository browser.