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

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