source: Deliverables/D4.1/Matita/Assembly.ma @ 294

Last change on this file since 294 was 293, checked in by sacerdot, 10 years ago

...
File size: 20.7 KB
Line 
1include "ASM.ma".
2
3ndefinition assembly1 ≝
4 λi: instruction.match i with
5  [ ACALL addr ⇒
6     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
7      [ ADDR11 w ⇒ λ_.
8         let 〈v1,v2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S Z))) w in
9          [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
10      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
11  | ADD addr1 addr2 ⇒
12     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
13      [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[false;false;true;false;true;r1;r2;r2]]) ]
14      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ]
15      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;false;false;true;true;i1]]) ]
16      | DATA b1 ⇒ λ_. [ ([[false;false;true;false;false;true;false;false]]) ; b1 ]
17      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
18  | ADDC addr1 addr2 ⇒
19     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
20      [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[false;false;true;true;true;r1;r2;r2]]) ]
21      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;true;false;true;false;true]]); b1 ]
22      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;true;false;true;true;i1]]) ]
23      | DATA b1 ⇒ λ_. [ ([[false;false;true;true;false;true;false;false]]) ; b1 ]
24      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
25  | AJMP addr ⇒
26     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
27      [ ADDR11 w ⇒ λ_.
28         let 〈v1,v2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S Z))) w in
29          [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
30      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
31  | ANL addrs ⇒
32     match addrs with
33      [ Left addrs ⇒ match addrs with
34         [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
35           match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
36            [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[false;true;false;true;true;r1;r2;r2]]) ]
37            | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ]
38            | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;true;false;true;true;i1]]) ]
39            | DATA b1 ⇒ λ_. [ ([[false;true;false;true;false;true;false;false]]) ; b1 ]
40            | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
41         | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
42            let b1 ≝
43             match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
44              [ DIRECT b1 ⇒ λ_.b1
45              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
46            match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
47             [ ACC_A ⇒ λ_.[ ([[false;true;false;true;false;false;true;false]]) ; b1 ]
48             | DATA b2 ⇒ λ_. [ ([[false;true;false;true;false;false;true;true]]) ; b1 ; b2 ]
49             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
50         ]
51      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
52         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
53          [ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ]
54          | N_BIT_ADDR b1 ⇒ λ_. [ ([[true;false;true;true;false;false;false;false]]) ; b1 ]
55          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
56  | CLR addr ⇒
57     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
58      [ ACC_A ⇒ λ_.
59         [ ([[true; true; true; false; false; true; false; false]]) ]
60      | CARRY ⇒ λ_.
61         [ ([[true; true; false; false; false; false; true; true]]) ]
62      | BIT_ADDR b1 ⇒ λ_.
63         [ ([[true; true; false; false; false; false; true; false]]) ; b1 ]
64      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
65  | CPL addr ⇒
66     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
67      [ ACC_A ⇒ λ_.
68         [ ([[true; true; true; true; false; true; false; false]]) ]
69      | CARRY ⇒ λ_.
70         [ ([[true; false; true; true; false; false; true; true]]) ]
71      | BIT_ADDR b1 ⇒ λ_.
72         [ ([[true; false; true; true; false; false; true; false]]) ; b1 ]
73      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
74  | DA addr ⇒
75     [ ([[true; true; false; true; false; true; false; false]]) ]
76  | DEC addr ⇒
77     match addr return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect]] x) → ? with
78      [ ACC_A ⇒ λ_.
79         [ ([[false; false; false; true; false; true; false; false]]) ]
80      | REGISTER r1 r2 r3 ⇒ λ_.
81         [ ([[false; false; false; true; true; r1; r2; r3]]) ]
82      | DIRECT b1 ⇒ λ_.
83         [ ([[false; false; false; true; false; true; false; true]]); b1 ]
84      | INDIRECT i1 ⇒ λ_.
85         [ ([[false; false; false; true; false; true; true; i1]]) ]
86      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
87  | DIV addr1 addr2 ⇒
88     [ ([[true;false;false;false;false;true;false;false]]) ]
89  | Jump j ⇒
90     match j with
91      [ DJNZ addr1 addr2 ⇒
92         let b2 ≝
93          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
94           [ RELATIVE b2 ⇒ λ_. b2
95           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
96         match addr1 return λx. bool_to_Prop (is_in ? [[register;direct]] x) → ? with
97          [ REGISTER r1 r2 r3 ⇒ λ_.
98             [ ([[true; true; false; true; true; r1; r2; r3]]) ; b2 ]
99          | DIRECT b1 ⇒ λ_.
100             [ ([[true; true; false; true; false; true; false; true]]); b1; b2 ]
101          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
102      | JC addr ⇒
103         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
104          [ RELATIVE b1 ⇒ λ_.
105             [ ([[false; true; false; false; false; false; false; false]]); b1 ]
106          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
107      | JNC addr ⇒
108         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
109          [ RELATIVE b1 ⇒ λ_.
110             [ ([[false; true; false; true; false; false; false; false]]); b1 ]
111          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
112      | JZ addr ⇒
113         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
114          [ RELATIVE b1 ⇒ λ_.
115             [ ([[false; true; true; false; false; false; false; false]]); b1 ]
116          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
117      | JNZ addr ⇒
118         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
119          [ RELATIVE b1 ⇒ λ_.
120             [ ([[false; true; true; true; false; false; false; false]]); b1 ]
121          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
122      | JB addr1 addr2 ⇒
123         let b2 ≝
124          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
125           [ RELATIVE b2 ⇒ λ_. b2
126           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
127         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
128          [ BIT_ADDR b1 ⇒ λ_.
129             [ ([[false; false; true; false; false; false; false; false]]); b1; b2 ]
130          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
131      | JNB addr1 addr2 ⇒
132         let b2 ≝
133          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
134           [ RELATIVE b2 ⇒ λ_. b2
135           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
136         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
137          [ BIT_ADDR b1 ⇒ λ_.
138             [ ([[false; false; true; true; false; false; false; false]]); b1; b2 ]
139          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
140      | JBC addr1 addr2 ⇒
141         let b2 ≝
142          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
143           [ RELATIVE b2 ⇒ λ_. b2
144           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
145         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
146          [ BIT_ADDR b1 ⇒ λ_.
147             [ ([[false; false; false; true; false; false; false; false]]); b1; b2 ]
148          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
149      | CJNE addrs addr3 ⇒
150         let b3 ≝
151          match addr3 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
152           [ RELATIVE b3 ⇒ λ_. b3
153           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr3) in
154         match addrs with
155          [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
156             match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with
157              [ DIRECT b1 ⇒ λ_.
158                 [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ]
159              [ DATA b1 ⇒ λ_.
160                 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
161              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
162          | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
163             let b2 ≝
164              match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with
165               [ DATA b2 ⇒ λ_. b2
166               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
167             match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with
168              [ DIRECT b1 ⇒ λ_.
169                 [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ]
170              [ DATA b1 ⇒ λ_.
171                 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
172              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
173
174          ]
175      | _ ⇒ [ ]
176      ]
177  | _ ⇒ [ ]].
178
179(*
180  | `CJNE (`U2 (`REG(r1,r2,r3), `DATA b1), `REL b2) ->
181    [mk_byte_from_bits ((true,false,true,true),(true,r1,r2,r3)); b1; b2]
182  | `CJNE (`U2 (`INDIRECT i1, `DATA b1), `REL b2) ->
183    [mk_byte_from_bits ((true,false,true,true),(false,true,true,i1)); b1; b2]
184
185
186  | `INC `A ->
187    [mk_byte_from_bits ((false,false,false,false),(false,true,false,false))]
188  | `INC (`REG(r1,r2,r3)) ->
189    [mk_byte_from_bits ((false,false,false,false),(true,r1,r2,r3))]
190  | `INC (`DIRECT b1) ->
191    [mk_byte_from_bits ((false,false,false,false),(false,true,false,true)); b1]
192  | `INC (`INDIRECT i1) ->
193    [mk_byte_from_bits ((false,false,false,false),(false,true,true,i1))]
194  | `INC `DPTR ->
195    [mk_byte_from_bits ((true,false,true,false),(false,false,true,true))]
196  | `JMP `IND_DPTR ->
197    [mk_byte_from_bits ((false,true,true,true),(false,false,true,true))]
198  | `LCALL (`ADDR16 w) ->
199      let (b1,b2) = from_word w in
200        [mk_byte_from_bits ((false,false,false,true),(false,false,true,false)); b1; b2]
201  | `LJMP (`ADDR16 w) ->
202      let (b1,b2) = from_word w in
203        [mk_byte_from_bits ((false,false,false,false),(false,false,true,false)); b1; b2]
204  | `MOV (`U1 (`A, `REG(r1,r2,r3))) ->
205    [mk_byte_from_bits ((true,true,true,false),(true,r1,r2,r3))]
206  | `MOV (`U1 (`A, `DIRECT b1)) ->
207    [mk_byte_from_bits ((true,true,true,false),(false,true,false,true)); b1]
208  | `MOV (`U1 (`A, `INDIRECT i1)) ->
209    [mk_byte_from_bits ((true,true,true,false),(false,true,true,i1))]
210  | `MOV (`U1 (`A, `DATA b1)) ->
211    [mk_byte_from_bits ((false,true,true,true),(false,true,false,false)); b1]
212  | `MOV (`U2 (`REG(r1,r2,r3), `A)) ->
213    [mk_byte_from_bits ((true,true,true,true),(true,r1,r2,r3))]
214  | `MOV (`U2 (`REG(r1,r2,r3), (`DIRECT b1))) ->
215    [mk_byte_from_bits ((true,false,true,false),(true,r1,r2,r3)); b1]
216  | `MOV (`U2 (`REG(r1,r2,r3), (`DATA b1))) ->
217    [mk_byte_from_bits ((false,true,true,true),(true,r1,r2,r3)); b1]
218  | `MOV (`U3 (`DIRECT b1, `A)) ->
219    [mk_byte_from_bits ((true,true,true,true),(false,true,false,true)); b1]
220  | `MOV (`U3 (`DIRECT b1, `REG(r1,r2,r3))) ->
221    [mk_byte_from_bits ((true,false,false,false),(true,r1,r2,r3)); b1]
222  | `MOV (`U3 (`DIRECT b1, `DIRECT b2)) ->
223    [mk_byte_from_bits ((true,false,false,false),(false,true,false,true)); b1; b2]
224  | `MOV (`U3 (`DIRECT b1, `INDIRECT i1)) ->
225    [mk_byte_from_bits ((true,false,false,false),(false,true,true,i1)); b1]
226  | `MOV (`U3 (`DIRECT b1, `DATA b2)) ->
227    [mk_byte_from_bits ((false,true,true,true),(false,true,false,true)); b1; b2]
228  | `MOV (`U2 (`INDIRECT i1, `A)) ->
229    [mk_byte_from_bits ((true,true,true,true),(false,true,true,i1))]
230  | `MOV (`U2 (`INDIRECT i1, `DIRECT b1)) ->
231    [mk_byte_from_bits ((true,false,true,false),(false,true,true,i1)); b1]
232  | `MOV (`U2 (`INDIRECT i1, `DATA b1)) ->
233    [mk_byte_from_bits ((false,true,true,true),(false,true,true,i1)); b1]
234  | `MOV (`U5 (`C, `BIT b1)) ->
235    [mk_byte_from_bits ((true,false,true,false),(false,false,true,false)); b1]
236  | `MOV (`U6 (`BIT b1, `C)) ->
237    [mk_byte_from_bits ((true,false,false,true),(false,false,true,false)); b1]
238  | `MOV (`U4 (`DPTR, `DATA16 w)) ->
239    let (b1,b2) = from_word w in
240      [mk_byte_from_bits ((true,false,false,true),(false,false,false,false)); b1; b2]
241  | `MOVC (`A, `A_DPTR) ->
242    [mk_byte_from_bits ((true,false,false,true),(false,false,true,true))]
243  | `MOVC (`A, `A_PC) ->
244    [mk_byte_from_bits ((true,false,false,false),(false,false,true,true))]
245  | `MOVX (`U1 (`A, `EXT_INDIRECT i1)) ->
246    [mk_byte_from_bits ((true,true,true,false),(false,false,true,i1))]
247  | `MOVX (`U1 (`A, `EXT_IND_DPTR)) ->
248    [mk_byte_from_bits ((true,true,true,false),(false,false,false,false))]
249  | `MOVX (`U2 (`EXT_INDIRECT i1, `A)) ->
250    [mk_byte_from_bits ((true,true,true,true),(false,false,true,i1))]
251  | `MOVX (`U2 (`EXT_IND_DPTR, `A)) ->
252    [mk_byte_from_bits ((true,true,true,true),(false,false,false,false))]
253  | `MUL(`A, `B) ->
254    [mk_byte_from_bits ((true,false,true,false),(false,true,false,false))]
255  | `NOP ->
256    [mk_byte_from_bits ((false,false,false,false),(false,false,false,false))]
257  | `ORL (`U1(`A, `REG(r1,r2,r3))) ->
258    [mk_byte_from_bits ((false,true,false,false),(true,r1,r2,r3))]
259  | `ORL (`U1(`A, `DIRECT b1)) ->
260    [mk_byte_from_bits ((false,true,false,false),(false,true,false,true)); b1]
261  | `ORL (`U1(`A, `INDIRECT i1)) ->
262    [mk_byte_from_bits ((false,true,false,false),(false,true,true,i1))]
263  | `ORL (`U1(`A, `DATA b1)) ->
264    [mk_byte_from_bits ((false,true,false,false),(false,true,false,false)); b1]
265  | `ORL (`U2(`DIRECT b1, `A)) ->
266    [mk_byte_from_bits ((false,true,false,false),(false,false,true,false)); b1]
267  | `ORL (`U2 (`DIRECT b1, `DATA b2)) ->
268    [mk_byte_from_bits ((false,true,false,false),(false,false,true,true)); b1; b2]
269  | `ORL (`U3 (`C, `BIT b1)) ->
270    [mk_byte_from_bits ((false,true,true,true),(false,false,true,false)); b1]
271  | `ORL (`U3 (`C, `NBIT b1)) ->
272    [mk_byte_from_bits ((true,false,true,false),(false,false,false,false)); b1]
273  | `POP (`DIRECT b1) ->
274    [mk_byte_from_bits ((true,true,false,true),(false,false,false,false)); b1]
275  | `PUSH (`DIRECT b1) ->
276    [mk_byte_from_bits ((true,true,false,false),(false,false,false,false)); b1]
277  | `RET ->
278    [mk_byte_from_bits ((false,false,true,false),(false,false,true,false))]
279  | `RETI ->
280    [mk_byte_from_bits ((false,false,true,true),(false,false,true,false))]
281  | `RL `A ->
282    [mk_byte_from_bits ((false,false,true,false),(false,false,true,true))]
283  | `RLC `A ->
284    [mk_byte_from_bits ((false,false,true,true),(false,false,true,true))]
285  | `RR `A ->
286    [mk_byte_from_bits ((false,false,false,false),(false,false,true,true))]
287  | `RRC `A ->
288    [mk_byte_from_bits ((false,false,false,true),(false,false,true,true))]
289  | `SETB `C ->
290    [mk_byte_from_bits ((true,true,false,true),(false,false,true,true))]
291  | `SETB (`BIT b1) ->
292    [mk_byte_from_bits ((true,true,false,true),(false,false,true,false)); b1]
293  | `SJMP (`REL b1) ->
294    [mk_byte_from_bits ((true,false,false,false),(false,false,false,false)); b1]
295  | `SUBB (`A, `REG(r1,r2,r3)) ->
296    [mk_byte_from_bits ((true,false,false,true),(true,r1,r2,r3))]
297  | `SUBB (`A, `DIRECT b1) ->
298    [mk_byte_from_bits ((true,false,false,true),(false,true,false,true)); b1]
299  | `SUBB (`A, `INDIRECT i1) ->
300    [mk_byte_from_bits ((true,false,false,true),(false,true,true,i1))]
301  | `SUBB (`A, `DATA b1) ->
302    [mk_byte_from_bits ((true,false,false,true),(false,true,false,false)); b1]
303  | `SWAP `A ->
304    [mk_byte_from_bits ((true,true,false,false),(false,true,false,false))]
305  | `XCH (`A, `REG(r1,r2,r3)) ->
306    [mk_byte_from_bits ((true,true,false,false),(true,r1,r2,r3))]
307  | `XCH (`A, `DIRECT b1) ->
308    [mk_byte_from_bits ((true,true,false,false),(false,true,false,true)); b1]
309  | `XCH (`A, `INDIRECT i1) ->
310    [mk_byte_from_bits ((true,true,false,false),(false,true,true,i1))]
311  | `XCHD(`A, `INDIRECT i1) ->
312    [mk_byte_from_bits ((true,true,false,true),(false,true,true,i1))]
313  | `XRL(`U1(`A, `REG(r1,r2,r3))) ->
314    [mk_byte_from_bits ((false,true,true,false),(true,r1,r2,r3))]
315  | `XRL(`U1(`A, `DIRECT b1)) ->
316    [mk_byte_from_bits ((false,true,true,false),(false,true,false,true)); b1]
317  | `XRL(`U1(`A, `INDIRECT i1)) ->
318    [mk_byte_from_bits ((false,true,true,false),(false,true,true,i1))]
319  | `XRL(`U1(`A, `DATA b1)) ->
320    [mk_byte_from_bits ((false,true,true,false),(false,true,false,false)); b1]
321  | `XRL(`U2(`DIRECT b1, `A)) ->
322    [mk_byte_from_bits ((false,true,true,false),(false,false,true,false)); b1]
323  | `XRL(`U2(`DIRECT b1, `DATA b2)) ->
324    [mk_byte_from_bits ((false,true,true,false),(false,false,true,true)); b1; b2]
325;;
326
327
328
329nrecord Sigma (A: Type[0]) (T: A → Type[0]) : Type[0] ≝ {
330   elem:> A;
331   witness: T elem
332}.
333
334interpretation "Sigma" 'sigma T = (Sigma ? T).
335
336naxiom daemon: False.
337
338naxiom decode_register: Vector Bool (S (S (S Z))) → [reg].
339naxiom decode_direct:   Vector Bool (S (S (S Z))) → [direct].
340
341ndefinition decode_tbl0: List ((Σn.Vector Bool n) × (Vector Bool (S (S (S Z))) → Instruction))
342 ≝
343 [mk_Cartesian ??
344   (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
345     (λl.
346       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
347             (mk_subaddressing_mode ? ?    (decode_register l) ?));
348  mk_Cartesian ??
349   (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
350     (λl.
351       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
352             (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
353ncases daemon.
354nqed.
355
356
357naxiom decode_register: List Bool → [reg].
358naxiom decode_direct: List Bool → [direct].
359
360ndefinition decode_tbl0: List (List Bool × (List Bool → Instruction))
361 ≝
362 [mk_Cartesian ??
363   [ false; false; true; false; true]
364     (λl.
365       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
366             (mk_subaddressing_mode ? ?    (decode_register l) ?));
367  mk_Cartesian ??
368   [ false; false; true; false; true]
369     (λl.
370       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
371             (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
372ncases daemon.
373nqed.
374
375
376ndefinition decode_tbl1:
377 List (List Bool × Σaddr:all_types. [addr] → Instruction)
378 ≝
379 [mk_Cartesian ??
380   [ false; false; true; false; true]
381   (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)
382     reg
383     (λa.
384       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
385             (mk_subaddressing_mode ? ? a ?))) ].
386ncases daemon.
387nqed.
388             
389ndefinition decode_tbl2:
390 List (List Bool × Σaddr:all_types. [addr] → Instruction)
391 ≝
392 [mk_Cartesian ??
393   [ false; false; true; false; false; true; false; true]
394   (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)
395     direct
396     (λa.
397       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
398             (mk_subaddressing_mode ? ?     a ?))) ].
399ncases daemon.
400nqed.
401
402ndefinition decode_tbl ≝ decode_tbl1 @ decode_tbl2.
403
404decode_addr_mode; ∀addr:all_types. List Bool → [addr].
405
406decode ≝
407 λl:List Bit.
408  List.iter
409   (fun l0 addr mk_f →
410     match split_prefix l l0 with
411      [ None ⇒ ...
412      | Some r ⇒ mk_f (decode_addr_mode r) ]
413     
414   ) decode_tbl
415
416encode ≝
417
418ndefinition decode_tbl:
419 List (List Bool × Σaddr:all_types. [addr] → Instruction)
420 ≝
421 [mk_Cartesian ??
422   [ False; False; True; False; True]
423   (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)
424     reg
425     (λa:subaddressing_mode ? [reg].
426       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
427             (mk_subaddressing_mode ? ?     a ?)));
428  mk_Cartesian ??
429   [ False; False; True; False; False; True; False; True]
430   (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)
431     direct
432     (λa:subaddressing_mode ? [direct].
433       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
434             (mk_subaddressing_mode ? ?     a ?)))
435 ].
436nnormalize;
437 
438 ].
439*)
Note: See TracBrowser for help on using the repository browser.