source: src/ASM/Fetch.ma @ 1571

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