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

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

...

File size: 25.9 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;r3]]) ]
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;r3]]) ]
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;r3]]) ]
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
168[ ] (*
169             match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → ? with
170              [ REGISTER r1 r2 r3 ⇒ λ_. [](*
171                 [ ([[true; false; true; true; true; r1; r2; r3]]); b2; b3 ]*)
172              | INDIRECT i1 ⇒ λ_. [] (*
173                 [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ] *)
174              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)*) ]]
175  | INC addr ⇒
176     match addr return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect;dptr]] x) → ? with
177      [ ACC_A ⇒ λ_.
178         [ ([[false;false;false;false;false;true;false;false]]) ]         
179      | REGISTER r1 r2 r3 ⇒ λ_.
180         [ ([[false;false;false;false;true;r1;r2;r3]]) ]
181      | DIRECT b1 ⇒ λ_.
182         [ ([[false; false; false; false; false; true; false; true]]); b1 ]
183      | INDIRECT i1 ⇒ λ_.
184        [ ([[false; false; false; false; false; true; true; i1]]) ]
185      | DPTR ⇒ λ_.
186        [ ([[true;false;true;false;false;false;true;true]]) ]
187      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
188  | JMP addr ⇒
189     [ ([[false;true;true;true;false;false;true;true]]) ]
190  | LCALL addr ⇒
191     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
192      [ ADDR16 w ⇒ λ_.
193         let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in
194          [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
195      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
196  | LJMP addr ⇒
197     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
198      [ ADDR16 w ⇒ λ_.
199         let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in
200          [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
201      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
202  | MOV addrs ⇒
203     match addrs with
204      [ Left addrs ⇒
205         match addrs with
206          [ Left addrs ⇒
207             match addrs with
208              [ Left addrs ⇒
209                 match addrs with
210                  [ Left addrs ⇒
211                     match addrs with
212                      [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
213                         match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
214                          [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[true;true;true;false;true;r1;r2;r3]]) ]
215                          | DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ]
216                          | INDIRECT i1 ⇒ λ_. [ ([[true;true;true;false;false;true;true;i1]]) ]
217                          | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;false]]) ; b1 ]
218                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
219                      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
220[] (*
221  | `MOV (`U2 (`REG(r1,r2,r3), `A)) ->
222    [mk_byte_from_bits ((true,true,true,true),(true,r1,r2,r3))]
223  | `MOV (`U2 (`REG(r1,r2,r3), (`DIRECT b1))) ->
224    [mk_byte_from_bits ((true,false,true,false),(true,r1,r2,r3)); b1]
225  | `MOV (`U2 (`REG(r1,r2,r3), (`DATA b1))) ->
226    [mk_byte_from_bits ((false,true,true,true),(true,r1,r2,r3)); b1]
227
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
235*)
236                      ]
237                  | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in [] (*
238                     let b1 ≝
239                      match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
240                       [ DIRECT b1 ⇒ λ_. b1
241                       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
242                      match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect;data]] x) → ? with
243                       [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1]
244                       | REGISTER r1 r2 r3 ⇒ λ_.[ ([[true;false;false;false;true;r1;r2;r3]]); b1 ]
245                       | DIRECT b2 ⇒ λ_.[ ([[true;false;false;false;false;true;false;true]]); b1; b2 ]
246                       | INDIRECT i1 ⇒ λ_. [ ([[true;false;false;false;false;true;true;i1]]); b1 ]
247                       | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ]
248                       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)*)]
249              | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
250                 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
251                  [ DATA16 w ⇒ λ_.
252                     let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in
253                      [ ([[true;false;false;true;false;false;false;false]]); b1; b2]
254                  | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
255          | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
256[] (*
257  | `MOV (`U5 (`C, `BIT b1)) ->
258    [mk_byte_from_bits ((true,false,true,false),(false,false,true,false)); b1]
259*)
260          ]
261      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
262[] (*
263  | `MOV (`U6 (`BIT b1, `C)) ->
264    [mk_byte_from_bits ((true,false,false,true),(false,false,true,false)); b1]   
265*)
266      ]
267  | MOVC addr1 addr2 ⇒
268     match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with
269      [ ACC_DPTR ⇒ λ_.
270         [ ([[true;false;false;true;false;false;true;true]]) ]
271      | ACC_PC ⇒ λ_.
272         [ ([[true;false;false;false;false;false;true;true]]) ]
273      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
274  | MOVX addrs ⇒
275     match addrs with
276      [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
277         match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
278          [ EXT_INDIRECT i1 ⇒ λ_.
279             [ ([[true;true;true;false;false;false;true;i1]]) ]
280          | EXT_INDIRECT_DPTR ⇒ λ_.
281             [ ([[true;true;true;false;false;false;false;false]]) ]
282          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
283      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
284         match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
285          [ EXT_INDIRECT i1 ⇒ λ_.
286             [ ([[true;true;true;true;false;false;true;i1]]) ]
287          | EXT_INDIRECT_DPTR ⇒ λ_.
288             [ ([[true;true;true;true;false;false;false;false]]) ]
289          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
290  | MUL addr1 addr2 ⇒
291     [ ([[true;false;true;false;false;true;false;false]]) ]
292  | NOP ⇒
293     [ ([[false;false;false;false;false;false;false;false]]) ]
294  | ORL addrs ⇒
295     match addrs with
296      [ Left addrs ⇒
297         match addrs with
298          [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
299             match addr2 return λx. bool_to_Prop (is_in ? [[register;data;direct;indirect]] x) → ? with
300             [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[false;true;false;false;true;r1;r2;r3]]) ]
301             | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ]
302             | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;false;false;true;true;i1]]) ]
303             | DATA b1 ⇒ λ_. [ ([[false;true;false;false;false;true;false;false]]) ; b1 ]
304             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
305          | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
306            let b1 ≝
307              match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
308               [ DIRECT b1 ⇒ λ_. b1
309               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
310             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
311              [ ACC_A ⇒ λ_.
312                 [ ([[false;true;false;false;false;false;true;false]]); b1 ]
313              | DATA b2 ⇒ λ_.
314                 [ ([[false;true;false;false;false;false;true;true]]); b1; b2 ]
315              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
316      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in     
317         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
318          [ BIT_ADDR b1 ⇒ λ_.
319             [ ([[false;true;true;true;false;false;true;false]]); b1 ]
320          | N_BIT_ADDR b1 ⇒ λ_.
321             [ ([[true;false;true;false;false;false;false;false]]); b1 ]
322          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
323  | POP addr ⇒
324     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
325      [ DIRECT b1 ⇒ λ_.
326         [ ([[true;true;false;true;false;false;false;false]]) ; b1 ]
327      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
328  | PUSH addr ⇒
329     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
330      [ DIRECT b1 ⇒ λ_.
331         [ ([[true;true;false;false;false;false;false;false]]) ; b1 ]
332      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
333  | RET ⇒
334     [ ([[false;false;true;false;false;false;true;false]]) ]
335  | RETI ⇒
336     [ ([[false;false;true;true;false;false;true;false]]) ]
337  | RL addr ⇒
338     [ ([[false;false;true;false;false;false;true;true]]) ]
339  | RLC addr ⇒
340     [ ([[false;false;true;true;false;false;true;true]]) ]
341  | RR addr ⇒
342     [ ([[false;false;false;false;false;false;true;true]]) ]
343  | RRC addr ⇒
344     [ ([[false;false;false;true;false;false;true;true]]) ]
345  | SETB addr ⇒     
346     match addr return λx. bool_to_Prop (is_in ? [[carry;bit_addr]] x) → ? with
347      [ CARRY ⇒ λ_.
348         [ ([[true;true;false;true;false;false;true;true]]) ]
349      | BIT_ADDR b1 ⇒ λ_.
350         [ ([[true;true;false;true;false;false;true;false]]); b1 ]
351      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
352  | SJMP addr ⇒
353     match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
354      [ RELATIVE b1 ⇒ λ_.
355         [ ([[true;false;false;false;false;false;false;false]]); b1 ]
356      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
357  | SUBB addr1 addr2 ⇒
358     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
359      [ REGISTER r1 r2 r3 ⇒ λ_.
360         [ ([[true;false;false;true;true;r1;r2;r3]]) ]
361      | DIRECT b1 ⇒ λ_.
362         [ ([[true;false;false;true;false;true;false;true]]); b1]
363      | INDIRECT i1 ⇒ λ_.
364         [ ([[true;false;false;true;false;true;true;i1]]) ]
365      | DATA b1 ⇒ λ_.
366         [ ([[true;false;false;true;false;true;false;false]]); b1]
367      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
368  | SWAP addr ⇒
369     [ ([[true;true;false;false;false;true;false;false]]) ]
370  | XCH addr1 addr2 ⇒
371     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect]] x) → ? with
372      [ REGISTER r1 r2 r3 ⇒ λ_.
373         [ ([[true;true;false;false;true;r1;r2;r3]]) ]
374      | DIRECT b1 ⇒ λ_.
375         [ ([[true;true;false;false;false;true;false;true]]); b1]
376      | INDIRECT i1 ⇒ λ_.
377         [ ([[true;true;false;false;false;true;true;i1]]) ]
378      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
379  | XCHD addr1 addr2 ⇒
380     match addr2 return λx. bool_to_Prop (is_in ? [[indirect]] x) → ? with
381      [ INDIRECT i1 ⇒ λ_.
382         [ ([[true;true;false;true;false;true;true;i1]]) ]
383      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
384  | XRL addrs ⇒
385     match addrs with
386      [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
387         match addr2 return λx. bool_to_Prop (is_in ? [[data;register;direct;indirect]] x) → ? with
388          [ REGISTER r1 r2 r3 ⇒ λ_.
389             [ ([[false;true;true;false;true;r1;r2;r3]]) ]
390          | DIRECT b1 ⇒ λ_.
391             [ ([[false;true;true;false;false;true;false;true]]); b1]
392          | INDIRECT i1 ⇒ λ_.
393             [ ([[false;true;true;false;false;true;true;i1]]) ]
394          | DATA b1 ⇒ λ_.
395             [ ([[false;true;true;false;false;true;false;false]]); b1]
396          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
397      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
398         let b1 ≝
399          match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
400           [ DIRECT b1 ⇒ λ_. b1
401           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
402         match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
403          [ ACC_A ⇒ λ_.
404             [ ([[false;true;true;false;false;false;true;false]]); b1 ]         
405          | DATA b2 ⇒ λ_.
406             [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ]
407          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] 
408
409  | _ ⇒ [ ]].
410
411
412(*
413nrecord Sigma (A: Type[0]) (T: A → Type[0]) : Type[0] ≝ {
414   elem:> A;
415   witness: T elem
416}.
417
418interpretation "Sigma" 'sigma T = (Sigma ? T).
419
420naxiom daemon: False.
421
422naxiom decode_register: Vector Bool (S (S (S Z))) → [reg].
423naxiom decode_direct:   Vector Bool (S (S (S Z))) → [direct].
424
425ndefinition decode_tbl0: List ((Σn.Vector Bool n) × (Vector Bool (S (S (S Z))) → Instruction))
426 ≝
427 [mk_Cartesian ??
428   (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
429     (λl.
430       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
431             (mk_subaddressing_mode ? ?    (decode_register l) ?));
432  mk_Cartesian ??
433   (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
434     (λl.
435       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
436             (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
437ncases daemon.
438nqed.
439
440
441naxiom decode_register: List Bool → [reg].
442naxiom decode_direct: List Bool → [direct].
443
444ndefinition decode_tbl0: List (List Bool × (List Bool → Instruction))
445 ≝
446 [mk_Cartesian ??
447   [ false; false; true; false; true]
448     (λl.
449       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
450             (mk_subaddressing_mode ? ?    (decode_register l) ?));
451  mk_Cartesian ??
452   [ false; false; true; false; true]
453     (λl.
454       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
455             (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
456ncases daemon.
457nqed.
458
459
460ndefinition decode_tbl1:
461 List (List Bool × Σaddr:all_types. [addr] → Instruction)
462 ≝
463 [mk_Cartesian ??
464   [ false; false; true; false; true]
465   (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)
466     reg
467     (λa.
468       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
469             (mk_subaddressing_mode ? ? a ?))) ].
470ncases daemon.
471nqed.
472             
473ndefinition decode_tbl2:
474 List (List Bool × Σaddr:all_types. [addr] → Instruction)
475 ≝
476 [mk_Cartesian ??
477   [ false; false; true; false; false; true; false; true]
478   (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)
479     direct
480     (λa.
481       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
482             (mk_subaddressing_mode ? ?     a ?))) ].
483ncases daemon.
484nqed.
485
486ndefinition decode_tbl ≝ decode_tbl1 @ decode_tbl2.
487
488decode_addr_mode; ∀addr:all_types. List Bool → [addr].
489
490decode ≝
491 λl:List Bit.
492  List.iter
493   (fun l0 addr mk_f →
494     match split_prefix l l0 with
495      [ None ⇒ ...
496      | Some r ⇒ mk_f (decode_addr_mode r) ]
497     
498   ) decode_tbl
499
500encode ≝
501
502ndefinition decode_tbl:
503 List (List Bool × Σaddr:all_types. [addr] → Instruction)
504 ≝
505 [mk_Cartesian ??
506   [ False; False; True; False; True]
507   (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)
508     reg
509     (λa:subaddressing_mode ? [reg].
510       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
511             (mk_subaddressing_mode ? ?     a ?)));
512  mk_Cartesian ??
513   [ False; False; True; False; False; True; False; True]
514   (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)
515     direct
516     (λa:subaddressing_mode ? [direct].
517       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
518             (mk_subaddressing_mode ? ?     a ?)))
519 ].
520nnormalize;
521 
522 ].
523*)
Note: See TracBrowser for help on using the repository browser.