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

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

...

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