source: Deliverables/D4.1/Matita/Test.ma @ 358

Last change on this file since 358 was 357, checked in by sacerdot, 10 years ago
  • stupid bug fixed in BitVectorTrie?
  • dependencies minimized, dead code removed
File size: 7.3 KB
Line 
1include "ASM.ma".
2
3ndefinition test: List instruction ≝
4 [LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;true;false;false;false]]);
5  LCALL … (ADDR16 [[false;false;false;false;false;false;false;false;false;true;true;false;false;true;false;false]]);
6  SJMP … (RELATIVE [[true;true;true;true;true;true;true;false]]);
7  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;false;true]]),(DATA [[false;false;false;false;false;true;true;true]])〉))));
8  LCALL … (ADDR16 [[false;false;false;false;false;false;false;false;false;true;true;false;true;true;true;false]]);
9  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[true;false;false;false;false;false;true;false]])〉)))));
10  Jump … (JZ … (RELATIVE [[false;false;false;false;false;false;true;true]]));
11  LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;true;true]]);
12  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
13  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;true]])〉)))));
14  ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
15  Jump … (JZ … (RELATIVE [[false;false;false;true;true;false;true;true]]));
16  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
17  MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;true;true;true;false;false;true;false]])〉)));
18  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
19  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
20  CLR … (ACC_A);
21  MOVC … (ACC_A) (ACC_DPTR);
22  MOVX … (Right … 〈(EXT_INDIRECT false),(ACC_A)〉);
23  INC … (DPTR);
24  INC … (REGISTER [[false;false;false]]);
25  Jump … (CJNE … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉) (RELATIVE [[false;false;false;false;false;false;true;false]]));
26  INC … (DIRECT [[true;false;true;false;false;false;false;false]]);
27  Jump … (DJNZ … (REGISTER [[false;false;true]]) (RELATIVE [[true;true;true;true;false;true;false;false]]));
28  Jump … (DJNZ … (REGISTER [[false;true;false]]) (RELATIVE [[true;true;true;true;false;false;true;false]]));
29  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉))));
30  CLR … (ACC_A);
31  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉)))));
32  MOV … (Left … (Left … (Left … (Left … (Right … 〈(INDIRECT false),(ACC_A)〉)))));
33  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;true]]));
34  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
35  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;false]])〉)))));
36  ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
37  Jump … (JZ … (RELATIVE [[false;false;false;false;true;false;true;false]]));
38  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
39  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
40  CLR … (ACC_A);
41  MOVX … (Right … 〈(EXT_INDIRECT true),(ACC_A)〉);
42  INC … (REGISTER [[false;false;true]]);
43  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;false]]));
44  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
45  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;false]])〉)))));
46  ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
47  Jump … (JZ … (RELATIVE [[false;false;false;false;true;true;false;false]]));
48  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
49  MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉)));
50  CLR … (ACC_A);
51  MOVX … (Right … 〈(EXT_INDIRECT_DPTR),(ACC_A)〉);
52  INC … (DPTR);
53  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;false]]));
54  Jump … (DJNZ … (REGISTER [[false;false;true]]) (RELATIVE [[true;true;true;true;true;false;true;false]]));
55  LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;true;true]]);
56  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;true;false;true]])〉)))));
57  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;true;false;true]]),(DATA [[false;false;false;false;true;true;true;true]])〉))));
58  XCHD … (ACC_A) (INDIRECT false);
59  MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉)));
60  RET … ;
61  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
62  RET … ;
63  NOP … ;
64  NOP … ;
65  NOP … ;
66  NOP … ;
67  NOP … ;
68  NOP … ;
69  NOP … ;
70  NOP … ;
71  NOP … ;
72  NOP … ;
73  NOP … ;
74  NOP … ;
75  NOP … ;
76  NOP … ;
77  NOP … ;
78  NOP … ;
79  NOP … ;
80  NOP … ;
81  NOP … ;
82  NOP … ;
83  NOP … ;
84  NOP … ;
85  NOP … ;
86  NOP … ;
87  NOP … ;
88  NOP … ;
89  NOP … ;
90  NOP … ;
91  NOP … ;
92  NOP … ;
93  NOP … ;
94  NOP … ;
95  NOP … ;
96  NOP … ;
97  NOP … ;
98  NOP … ;
99  NOP … ;
100  NOP … ;
101  NOP … ;
102  NOP … ;
103  NOP … ;
104  NOP … ;
105  NOP … ;
106  NOP … ;
107  NOP … ;
108  NOP … ;
109  NOP … ;
110  NOP … ;
111  NOP … ;
112  NOP … ;
113  NOP … ;
114  NOP … ;
115  NOP … ;
116  NOP … ;
117  NOP … ;
118  NOP … ;
119  NOP … ;
120  NOP … ;
121  NOP … ;
122  NOP … ;
123  NOP … ;
124  NOP … ;
125  NOP … ;
126  NOP … ;
127  NOP … ;
128  NOP … ;
129  NOP … ;
130  NOP … ;
131  NOP … ;
132  NOP … ;
133  NOP … ;
134  NOP … ;
135  NOP … ;
136  NOP … ;
137  NOP … ;
138  NOP … ;
139  NOP … ;
140  NOP … ;
141  NOP … ;
142  NOP … ;
143  NOP … ;
144  NOP … ;
145  NOP … ;
146  NOP … ;
147  NOP … ;
148  NOP … ;
149  NOP … ].
150 @.
151nqed.
Note: See TracBrowser for help on using the repository browser.