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

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

...

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