1 | open Preamble |
---|
2 | |
---|
3 | open Extranat |
---|
4 | |
---|
5 | open Vector |
---|
6 | |
---|
7 | open Div_and_mod |
---|
8 | |
---|
9 | open Jmeq |
---|
10 | |
---|
11 | open Russell |
---|
12 | |
---|
13 | open Types |
---|
14 | |
---|
15 | open List |
---|
16 | |
---|
17 | open Util |
---|
18 | |
---|
19 | open FoldStuff |
---|
20 | |
---|
21 | open Bool |
---|
22 | |
---|
23 | open Hints_declaration |
---|
24 | |
---|
25 | open Core_notation |
---|
26 | |
---|
27 | open Pts |
---|
28 | |
---|
29 | open Logic |
---|
30 | |
---|
31 | open Relations |
---|
32 | |
---|
33 | open Nat |
---|
34 | |
---|
35 | open BitVector |
---|
36 | |
---|
37 | open Proper |
---|
38 | |
---|
39 | open PositiveMap |
---|
40 | |
---|
41 | open Deqsets |
---|
42 | |
---|
43 | open ErrorMessages |
---|
44 | |
---|
45 | open PreIdentifiers |
---|
46 | |
---|
47 | open Errors |
---|
48 | |
---|
49 | open Extralib |
---|
50 | |
---|
51 | open Setoids |
---|
52 | |
---|
53 | open Monad |
---|
54 | |
---|
55 | open Option |
---|
56 | |
---|
57 | open Lists |
---|
58 | |
---|
59 | open Positive |
---|
60 | |
---|
61 | open Identifiers |
---|
62 | |
---|
63 | open BitVectorTrie |
---|
64 | |
---|
65 | open Exp |
---|
66 | |
---|
67 | open Arithmetic |
---|
68 | |
---|
69 | open Integers |
---|
70 | |
---|
71 | open AST |
---|
72 | |
---|
73 | open CostLabel |
---|
74 | |
---|
75 | open LabelledObjects |
---|
76 | |
---|
77 | open String |
---|
78 | |
---|
79 | type identifier0 = PreIdentifiers.identifier |
---|
80 | |
---|
81 | (** val toASM_ident : |
---|
82 | PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> identifier0 **) |
---|
83 | let toASM_ident t i = |
---|
84 | let id = i in id |
---|
85 | |
---|
86 | type addressing_mode = |
---|
87 | | DIRECT of BitVector.byte |
---|
88 | | INDIRECT of BitVector.bit |
---|
89 | | EXT_INDIRECT of BitVector.bit |
---|
90 | | REGISTER of BitVector.bitVector |
---|
91 | | ACC_A |
---|
92 | | ACC_B |
---|
93 | | DPTR |
---|
94 | | DATA of BitVector.byte |
---|
95 | | DATA16 of BitVector.word |
---|
96 | | ACC_DPTR |
---|
97 | | ACC_PC |
---|
98 | | EXT_INDIRECT_DPTR |
---|
99 | | INDIRECT_DPTR |
---|
100 | | CARRY |
---|
101 | | BIT_ADDR of BitVector.byte |
---|
102 | | N_BIT_ADDR of BitVector.byte |
---|
103 | | RELATIVE of BitVector.byte |
---|
104 | | ADDR11 of BitVector.word11 |
---|
105 | | ADDR16 of BitVector.word |
---|
106 | |
---|
107 | (** val addressing_mode_rect_Type4 : |
---|
108 | (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> |
---|
109 | 'a1) -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> |
---|
110 | (BitVector.byte -> 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 |
---|
111 | -> 'a1 -> 'a1 -> (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> |
---|
112 | (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word |
---|
113 | -> 'a1) -> addressing_mode -> 'a1 **) |
---|
114 | let rec addressing_mode_rect_Type4 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function |
---|
115 | | DIRECT x_18716 -> h_DIRECT x_18716 |
---|
116 | | INDIRECT x_18717 -> h_INDIRECT x_18717 |
---|
117 | | EXT_INDIRECT x_18718 -> h_EXT_INDIRECT x_18718 |
---|
118 | | REGISTER x_18719 -> h_REGISTER x_18719 |
---|
119 | | ACC_A -> h_ACC_A |
---|
120 | | ACC_B -> h_ACC_B |
---|
121 | | DPTR -> h_DPTR |
---|
122 | | DATA x_18720 -> h_DATA x_18720 |
---|
123 | | DATA16 x_18721 -> h_DATA16 x_18721 |
---|
124 | | ACC_DPTR -> h_ACC_DPTR |
---|
125 | | ACC_PC -> h_ACC_PC |
---|
126 | | EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR |
---|
127 | | INDIRECT_DPTR -> h_INDIRECT_DPTR |
---|
128 | | CARRY -> h_CARRY |
---|
129 | | BIT_ADDR x_18722 -> h_BIT_ADDR x_18722 |
---|
130 | | N_BIT_ADDR x_18723 -> h_N_BIT_ADDR x_18723 |
---|
131 | | RELATIVE x_18724 -> h_RELATIVE x_18724 |
---|
132 | | ADDR11 x_18725 -> h_ADDR11 x_18725 |
---|
133 | | ADDR16 x_18726 -> h_ADDR16 x_18726 |
---|
134 | |
---|
135 | (** val addressing_mode_rect_Type5 : |
---|
136 | (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> |
---|
137 | 'a1) -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> |
---|
138 | (BitVector.byte -> 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 |
---|
139 | -> 'a1 -> 'a1 -> (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> |
---|
140 | (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word |
---|
141 | -> 'a1) -> addressing_mode -> 'a1 **) |
---|
142 | let rec addressing_mode_rect_Type5 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function |
---|
143 | | DIRECT x_18747 -> h_DIRECT x_18747 |
---|
144 | | INDIRECT x_18748 -> h_INDIRECT x_18748 |
---|
145 | | EXT_INDIRECT x_18749 -> h_EXT_INDIRECT x_18749 |
---|
146 | | REGISTER x_18750 -> h_REGISTER x_18750 |
---|
147 | | ACC_A -> h_ACC_A |
---|
148 | | ACC_B -> h_ACC_B |
---|
149 | | DPTR -> h_DPTR |
---|
150 | | DATA x_18751 -> h_DATA x_18751 |
---|
151 | | DATA16 x_18752 -> h_DATA16 x_18752 |
---|
152 | | ACC_DPTR -> h_ACC_DPTR |
---|
153 | | ACC_PC -> h_ACC_PC |
---|
154 | | EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR |
---|
155 | | INDIRECT_DPTR -> h_INDIRECT_DPTR |
---|
156 | | CARRY -> h_CARRY |
---|
157 | | BIT_ADDR x_18753 -> h_BIT_ADDR x_18753 |
---|
158 | | N_BIT_ADDR x_18754 -> h_N_BIT_ADDR x_18754 |
---|
159 | | RELATIVE x_18755 -> h_RELATIVE x_18755 |
---|
160 | | ADDR11 x_18756 -> h_ADDR11 x_18756 |
---|
161 | | ADDR16 x_18757 -> h_ADDR16 x_18757 |
---|
162 | |
---|
163 | (** val addressing_mode_rect_Type3 : |
---|
164 | (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> |
---|
165 | 'a1) -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> |
---|
166 | (BitVector.byte -> 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 |
---|
167 | -> 'a1 -> 'a1 -> (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> |
---|
168 | (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word |
---|
169 | -> 'a1) -> addressing_mode -> 'a1 **) |
---|
170 | let rec addressing_mode_rect_Type3 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function |
---|
171 | | DIRECT x_18778 -> h_DIRECT x_18778 |
---|
172 | | INDIRECT x_18779 -> h_INDIRECT x_18779 |
---|
173 | | EXT_INDIRECT x_18780 -> h_EXT_INDIRECT x_18780 |
---|
174 | | REGISTER x_18781 -> h_REGISTER x_18781 |
---|
175 | | ACC_A -> h_ACC_A |
---|
176 | | ACC_B -> h_ACC_B |
---|
177 | | DPTR -> h_DPTR |
---|
178 | | DATA x_18782 -> h_DATA x_18782 |
---|
179 | | DATA16 x_18783 -> h_DATA16 x_18783 |
---|
180 | | ACC_DPTR -> h_ACC_DPTR |
---|
181 | | ACC_PC -> h_ACC_PC |
---|
182 | | EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR |
---|
183 | | INDIRECT_DPTR -> h_INDIRECT_DPTR |
---|
184 | | CARRY -> h_CARRY |
---|
185 | | BIT_ADDR x_18784 -> h_BIT_ADDR x_18784 |
---|
186 | | N_BIT_ADDR x_18785 -> h_N_BIT_ADDR x_18785 |
---|
187 | | RELATIVE x_18786 -> h_RELATIVE x_18786 |
---|
188 | | ADDR11 x_18787 -> h_ADDR11 x_18787 |
---|
189 | | ADDR16 x_18788 -> h_ADDR16 x_18788 |
---|
190 | |
---|
191 | (** val addressing_mode_rect_Type2 : |
---|
192 | (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> |
---|
193 | 'a1) -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> |
---|
194 | (BitVector.byte -> 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 |
---|
195 | -> 'a1 -> 'a1 -> (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> |
---|
196 | (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word |
---|
197 | -> 'a1) -> addressing_mode -> 'a1 **) |
---|
198 | let rec addressing_mode_rect_Type2 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function |
---|
199 | | DIRECT x_18809 -> h_DIRECT x_18809 |
---|
200 | | INDIRECT x_18810 -> h_INDIRECT x_18810 |
---|
201 | | EXT_INDIRECT x_18811 -> h_EXT_INDIRECT x_18811 |
---|
202 | | REGISTER x_18812 -> h_REGISTER x_18812 |
---|
203 | | ACC_A -> h_ACC_A |
---|
204 | | ACC_B -> h_ACC_B |
---|
205 | | DPTR -> h_DPTR |
---|
206 | | DATA x_18813 -> h_DATA x_18813 |
---|
207 | | DATA16 x_18814 -> h_DATA16 x_18814 |
---|
208 | | ACC_DPTR -> h_ACC_DPTR |
---|
209 | | ACC_PC -> h_ACC_PC |
---|
210 | | EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR |
---|
211 | | INDIRECT_DPTR -> h_INDIRECT_DPTR |
---|
212 | | CARRY -> h_CARRY |
---|
213 | | BIT_ADDR x_18815 -> h_BIT_ADDR x_18815 |
---|
214 | | N_BIT_ADDR x_18816 -> h_N_BIT_ADDR x_18816 |
---|
215 | | RELATIVE x_18817 -> h_RELATIVE x_18817 |
---|
216 | | ADDR11 x_18818 -> h_ADDR11 x_18818 |
---|
217 | | ADDR16 x_18819 -> h_ADDR16 x_18819 |
---|
218 | |
---|
219 | (** val addressing_mode_rect_Type1 : |
---|
220 | (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> |
---|
221 | 'a1) -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> |
---|
222 | (BitVector.byte -> 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 |
---|
223 | -> 'a1 -> 'a1 -> (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> |
---|
224 | (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word |
---|
225 | -> 'a1) -> addressing_mode -> 'a1 **) |
---|
226 | let rec addressing_mode_rect_Type1 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function |
---|
227 | | DIRECT x_18840 -> h_DIRECT x_18840 |
---|
228 | | INDIRECT x_18841 -> h_INDIRECT x_18841 |
---|
229 | | EXT_INDIRECT x_18842 -> h_EXT_INDIRECT x_18842 |
---|
230 | | REGISTER x_18843 -> h_REGISTER x_18843 |
---|
231 | | ACC_A -> h_ACC_A |
---|
232 | | ACC_B -> h_ACC_B |
---|
233 | | DPTR -> h_DPTR |
---|
234 | | DATA x_18844 -> h_DATA x_18844 |
---|
235 | | DATA16 x_18845 -> h_DATA16 x_18845 |
---|
236 | | ACC_DPTR -> h_ACC_DPTR |
---|
237 | | ACC_PC -> h_ACC_PC |
---|
238 | | EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR |
---|
239 | | INDIRECT_DPTR -> h_INDIRECT_DPTR |
---|
240 | | CARRY -> h_CARRY |
---|
241 | | BIT_ADDR x_18846 -> h_BIT_ADDR x_18846 |
---|
242 | | N_BIT_ADDR x_18847 -> h_N_BIT_ADDR x_18847 |
---|
243 | | RELATIVE x_18848 -> h_RELATIVE x_18848 |
---|
244 | | ADDR11 x_18849 -> h_ADDR11 x_18849 |
---|
245 | | ADDR16 x_18850 -> h_ADDR16 x_18850 |
---|
246 | |
---|
247 | (** val addressing_mode_rect_Type0 : |
---|
248 | (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> |
---|
249 | 'a1) -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> |
---|
250 | (BitVector.byte -> 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 |
---|
251 | -> 'a1 -> 'a1 -> (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> |
---|
252 | (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word |
---|
253 | -> 'a1) -> addressing_mode -> 'a1 **) |
---|
254 | let rec addressing_mode_rect_Type0 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function |
---|
255 | | DIRECT x_18871 -> h_DIRECT x_18871 |
---|
256 | | INDIRECT x_18872 -> h_INDIRECT x_18872 |
---|
257 | | EXT_INDIRECT x_18873 -> h_EXT_INDIRECT x_18873 |
---|
258 | | REGISTER x_18874 -> h_REGISTER x_18874 |
---|
259 | | ACC_A -> h_ACC_A |
---|
260 | | ACC_B -> h_ACC_B |
---|
261 | | DPTR -> h_DPTR |
---|
262 | | DATA x_18875 -> h_DATA x_18875 |
---|
263 | | DATA16 x_18876 -> h_DATA16 x_18876 |
---|
264 | | ACC_DPTR -> h_ACC_DPTR |
---|
265 | | ACC_PC -> h_ACC_PC |
---|
266 | | EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR |
---|
267 | | INDIRECT_DPTR -> h_INDIRECT_DPTR |
---|
268 | | CARRY -> h_CARRY |
---|
269 | | BIT_ADDR x_18877 -> h_BIT_ADDR x_18877 |
---|
270 | | N_BIT_ADDR x_18878 -> h_N_BIT_ADDR x_18878 |
---|
271 | | RELATIVE x_18879 -> h_RELATIVE x_18879 |
---|
272 | | ADDR11 x_18880 -> h_ADDR11 x_18880 |
---|
273 | | ADDR16 x_18881 -> h_ADDR16 x_18881 |
---|
274 | |
---|
275 | (** val addressing_mode_inv_rect_Type4 : |
---|
276 | addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ |
---|
277 | -> 'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> |
---|
278 | 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> |
---|
279 | __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) |
---|
280 | -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> |
---|
281 | 'a1) -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) -> |
---|
282 | (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1 **) |
---|
283 | let addressing_mode_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 = |
---|
284 | let hcut = |
---|
285 | addressing_mode_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 |
---|
286 | h15 h16 h17 h18 h19 hterm |
---|
287 | in |
---|
288 | hcut __ |
---|
289 | |
---|
290 | (** val addressing_mode_inv_rect_Type3 : |
---|
291 | addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ |
---|
292 | -> 'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> |
---|
293 | 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> |
---|
294 | __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) |
---|
295 | -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> |
---|
296 | 'a1) -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) -> |
---|
297 | (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1 **) |
---|
298 | let addressing_mode_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 = |
---|
299 | let hcut = |
---|
300 | addressing_mode_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 |
---|
301 | h15 h16 h17 h18 h19 hterm |
---|
302 | in |
---|
303 | hcut __ |
---|
304 | |
---|
305 | (** val addressing_mode_inv_rect_Type2 : |
---|
306 | addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ |
---|
307 | -> 'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> |
---|
308 | 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> |
---|
309 | __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) |
---|
310 | -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> |
---|
311 | 'a1) -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) -> |
---|
312 | (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1 **) |
---|
313 | let addressing_mode_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 = |
---|
314 | let hcut = |
---|
315 | addressing_mode_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 |
---|
316 | h15 h16 h17 h18 h19 hterm |
---|
317 | in |
---|
318 | hcut __ |
---|
319 | |
---|
320 | (** val addressing_mode_inv_rect_Type1 : |
---|
321 | addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ |
---|
322 | -> 'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> |
---|
323 | 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> |
---|
324 | __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) |
---|
325 | -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> |
---|
326 | 'a1) -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) -> |
---|
327 | (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1 **) |
---|
328 | let addressing_mode_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 = |
---|
329 | let hcut = |
---|
330 | addressing_mode_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 |
---|
331 | h15 h16 h17 h18 h19 hterm |
---|
332 | in |
---|
333 | hcut __ |
---|
334 | |
---|
335 | (** val addressing_mode_inv_rect_Type0 : |
---|
336 | addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ |
---|
337 | -> 'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> |
---|
338 | 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> |
---|
339 | __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) |
---|
340 | -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> |
---|
341 | 'a1) -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) -> |
---|
342 | (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1 **) |
---|
343 | let addressing_mode_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 = |
---|
344 | let hcut = |
---|
345 | addressing_mode_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 |
---|
346 | h15 h16 h17 h18 h19 hterm |
---|
347 | in |
---|
348 | hcut __ |
---|
349 | |
---|
350 | (** val addressing_mode_discr : addressing_mode -> addressing_mode -> __ **) |
---|
351 | let addressing_mode_discr x y = |
---|
352 | Logic.eq_rect_Type2 x |
---|
353 | (match x with |
---|
354 | | DIRECT a0 -> Obj.magic (fun _ dH -> dH __) |
---|
355 | | INDIRECT a0 -> Obj.magic (fun _ dH -> dH __) |
---|
356 | | EXT_INDIRECT a0 -> Obj.magic (fun _ dH -> dH __) |
---|
357 | | REGISTER a0 -> Obj.magic (fun _ dH -> dH __) |
---|
358 | | ACC_A -> Obj.magic (fun _ dH -> dH) |
---|
359 | | ACC_B -> Obj.magic (fun _ dH -> dH) |
---|
360 | | DPTR -> Obj.magic (fun _ dH -> dH) |
---|
361 | | DATA a0 -> Obj.magic (fun _ dH -> dH __) |
---|
362 | | DATA16 a0 -> Obj.magic (fun _ dH -> dH __) |
---|
363 | | ACC_DPTR -> Obj.magic (fun _ dH -> dH) |
---|
364 | | ACC_PC -> Obj.magic (fun _ dH -> dH) |
---|
365 | | EXT_INDIRECT_DPTR -> Obj.magic (fun _ dH -> dH) |
---|
366 | | INDIRECT_DPTR -> Obj.magic (fun _ dH -> dH) |
---|
367 | | CARRY -> Obj.magic (fun _ dH -> dH) |
---|
368 | | BIT_ADDR a0 -> Obj.magic (fun _ dH -> dH __) |
---|
369 | | N_BIT_ADDR a0 -> Obj.magic (fun _ dH -> dH __) |
---|
370 | | RELATIVE a0 -> Obj.magic (fun _ dH -> dH __) |
---|
371 | | ADDR11 a0 -> Obj.magic (fun _ dH -> dH __) |
---|
372 | | ADDR16 a0 -> Obj.magic (fun _ dH -> dH __)) y |
---|
373 | |
---|
374 | (** val addressing_mode_jmdiscr : |
---|
375 | addressing_mode -> addressing_mode -> __ **) |
---|
376 | let addressing_mode_jmdiscr x y = |
---|
377 | Logic.eq_rect_Type2 x |
---|
378 | (match x with |
---|
379 | | DIRECT a0 -> Obj.magic (fun _ dH -> dH __) |
---|
380 | | INDIRECT a0 -> Obj.magic (fun _ dH -> dH __) |
---|
381 | | EXT_INDIRECT a0 -> Obj.magic (fun _ dH -> dH __) |
---|
382 | | REGISTER a0 -> Obj.magic (fun _ dH -> dH __) |
---|
383 | | ACC_A -> Obj.magic (fun _ dH -> dH) |
---|
384 | | ACC_B -> Obj.magic (fun _ dH -> dH) |
---|
385 | | DPTR -> Obj.magic (fun _ dH -> dH) |
---|
386 | | DATA a0 -> Obj.magic (fun _ dH -> dH __) |
---|
387 | | DATA16 a0 -> Obj.magic (fun _ dH -> dH __) |
---|
388 | | ACC_DPTR -> Obj.magic (fun _ dH -> dH) |
---|
389 | | ACC_PC -> Obj.magic (fun _ dH -> dH) |
---|
390 | | EXT_INDIRECT_DPTR -> Obj.magic (fun _ dH -> dH) |
---|
391 | | INDIRECT_DPTR -> Obj.magic (fun _ dH -> dH) |
---|
392 | | CARRY -> Obj.magic (fun _ dH -> dH) |
---|
393 | | BIT_ADDR a0 -> Obj.magic (fun _ dH -> dH __) |
---|
394 | | N_BIT_ADDR a0 -> Obj.magic (fun _ dH -> dH __) |
---|
395 | | RELATIVE a0 -> Obj.magic (fun _ dH -> dH __) |
---|
396 | | ADDR11 a0 -> Obj.magic (fun _ dH -> dH __) |
---|
397 | | ADDR16 a0 -> Obj.magic (fun _ dH -> dH __)) y |
---|
398 | |
---|
399 | (** val eq_addressing_mode : |
---|
400 | addressing_mode -> addressing_mode -> Bool.bool **) |
---|
401 | let eq_addressing_mode a b = |
---|
402 | match a with |
---|
403 | | DIRECT d -> |
---|
404 | (match b with |
---|
405 | | DIRECT e0 -> |
---|
406 | BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
407 | (Nat.S Nat.O)))))))) d e0 |
---|
408 | | INDIRECT x -> Bool.False |
---|
409 | | EXT_INDIRECT x -> Bool.False |
---|
410 | | REGISTER x -> Bool.False |
---|
411 | | ACC_A -> Bool.False |
---|
412 | | ACC_B -> Bool.False |
---|
413 | | DPTR -> Bool.False |
---|
414 | | DATA x -> Bool.False |
---|
415 | | DATA16 x -> Bool.False |
---|
416 | | ACC_DPTR -> Bool.False |
---|
417 | | ACC_PC -> Bool.False |
---|
418 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
419 | | INDIRECT_DPTR -> Bool.False |
---|
420 | | CARRY -> Bool.False |
---|
421 | | BIT_ADDR x -> Bool.False |
---|
422 | | N_BIT_ADDR x -> Bool.False |
---|
423 | | RELATIVE x -> Bool.False |
---|
424 | | ADDR11 x -> Bool.False |
---|
425 | | ADDR16 x -> Bool.False) |
---|
426 | | INDIRECT b' -> |
---|
427 | (match b with |
---|
428 | | DIRECT x -> Bool.False |
---|
429 | | INDIRECT e0 -> BitVector.eq_b b' e0 |
---|
430 | | EXT_INDIRECT x -> Bool.False |
---|
431 | | REGISTER x -> Bool.False |
---|
432 | | ACC_A -> Bool.False |
---|
433 | | ACC_B -> Bool.False |
---|
434 | | DPTR -> Bool.False |
---|
435 | | DATA x -> Bool.False |
---|
436 | | DATA16 x -> Bool.False |
---|
437 | | ACC_DPTR -> Bool.False |
---|
438 | | ACC_PC -> Bool.False |
---|
439 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
440 | | INDIRECT_DPTR -> Bool.False |
---|
441 | | CARRY -> Bool.False |
---|
442 | | BIT_ADDR x -> Bool.False |
---|
443 | | N_BIT_ADDR x -> Bool.False |
---|
444 | | RELATIVE x -> Bool.False |
---|
445 | | ADDR11 x -> Bool.False |
---|
446 | | ADDR16 x -> Bool.False) |
---|
447 | | EXT_INDIRECT b' -> |
---|
448 | (match b with |
---|
449 | | DIRECT x -> Bool.False |
---|
450 | | INDIRECT x -> Bool.False |
---|
451 | | EXT_INDIRECT e0 -> BitVector.eq_b b' e0 |
---|
452 | | REGISTER x -> Bool.False |
---|
453 | | ACC_A -> Bool.False |
---|
454 | | ACC_B -> Bool.False |
---|
455 | | DPTR -> Bool.False |
---|
456 | | DATA x -> Bool.False |
---|
457 | | DATA16 x -> Bool.False |
---|
458 | | ACC_DPTR -> Bool.False |
---|
459 | | ACC_PC -> Bool.False |
---|
460 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
461 | | INDIRECT_DPTR -> Bool.False |
---|
462 | | CARRY -> Bool.False |
---|
463 | | BIT_ADDR x -> Bool.False |
---|
464 | | N_BIT_ADDR x -> Bool.False |
---|
465 | | RELATIVE x -> Bool.False |
---|
466 | | ADDR11 x -> Bool.False |
---|
467 | | ADDR16 x -> Bool.False) |
---|
468 | | REGISTER bv -> |
---|
469 | (match b with |
---|
470 | | DIRECT x -> Bool.False |
---|
471 | | INDIRECT x -> Bool.False |
---|
472 | | EXT_INDIRECT x -> Bool.False |
---|
473 | | REGISTER bv' -> BitVector.eq_bv (Nat.S (Nat.S (Nat.S Nat.O))) bv bv' |
---|
474 | | ACC_A -> Bool.False |
---|
475 | | ACC_B -> Bool.False |
---|
476 | | DPTR -> Bool.False |
---|
477 | | DATA x -> Bool.False |
---|
478 | | DATA16 x -> Bool.False |
---|
479 | | ACC_DPTR -> Bool.False |
---|
480 | | ACC_PC -> Bool.False |
---|
481 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
482 | | INDIRECT_DPTR -> Bool.False |
---|
483 | | CARRY -> Bool.False |
---|
484 | | BIT_ADDR x -> Bool.False |
---|
485 | | N_BIT_ADDR x -> Bool.False |
---|
486 | | RELATIVE x -> Bool.False |
---|
487 | | ADDR11 x -> Bool.False |
---|
488 | | ADDR16 x -> Bool.False) |
---|
489 | | ACC_A -> |
---|
490 | (match b with |
---|
491 | | DIRECT x -> Bool.False |
---|
492 | | INDIRECT x -> Bool.False |
---|
493 | | EXT_INDIRECT x -> Bool.False |
---|
494 | | REGISTER x -> Bool.False |
---|
495 | | ACC_A -> Bool.True |
---|
496 | | ACC_B -> Bool.False |
---|
497 | | DPTR -> Bool.False |
---|
498 | | DATA x -> Bool.False |
---|
499 | | DATA16 x -> Bool.False |
---|
500 | | ACC_DPTR -> Bool.False |
---|
501 | | ACC_PC -> Bool.False |
---|
502 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
503 | | INDIRECT_DPTR -> Bool.False |
---|
504 | | CARRY -> Bool.False |
---|
505 | | BIT_ADDR x -> Bool.False |
---|
506 | | N_BIT_ADDR x -> Bool.False |
---|
507 | | RELATIVE x -> Bool.False |
---|
508 | | ADDR11 x -> Bool.False |
---|
509 | | ADDR16 x -> Bool.False) |
---|
510 | | ACC_B -> |
---|
511 | (match b with |
---|
512 | | DIRECT x -> Bool.False |
---|
513 | | INDIRECT x -> Bool.False |
---|
514 | | EXT_INDIRECT x -> Bool.False |
---|
515 | | REGISTER x -> Bool.False |
---|
516 | | ACC_A -> Bool.False |
---|
517 | | ACC_B -> Bool.True |
---|
518 | | DPTR -> Bool.False |
---|
519 | | DATA x -> Bool.False |
---|
520 | | DATA16 x -> Bool.False |
---|
521 | | ACC_DPTR -> Bool.False |
---|
522 | | ACC_PC -> Bool.False |
---|
523 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
524 | | INDIRECT_DPTR -> Bool.False |
---|
525 | | CARRY -> Bool.False |
---|
526 | | BIT_ADDR x -> Bool.False |
---|
527 | | N_BIT_ADDR x -> Bool.False |
---|
528 | | RELATIVE x -> Bool.False |
---|
529 | | ADDR11 x -> Bool.False |
---|
530 | | ADDR16 x -> Bool.False) |
---|
531 | | DPTR -> |
---|
532 | (match b with |
---|
533 | | DIRECT x -> Bool.False |
---|
534 | | INDIRECT x -> Bool.False |
---|
535 | | EXT_INDIRECT x -> Bool.False |
---|
536 | | REGISTER x -> Bool.False |
---|
537 | | ACC_A -> Bool.False |
---|
538 | | ACC_B -> Bool.False |
---|
539 | | DPTR -> Bool.True |
---|
540 | | DATA x -> Bool.False |
---|
541 | | DATA16 x -> Bool.False |
---|
542 | | ACC_DPTR -> Bool.False |
---|
543 | | ACC_PC -> Bool.False |
---|
544 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
545 | | INDIRECT_DPTR -> Bool.False |
---|
546 | | CARRY -> Bool.False |
---|
547 | | BIT_ADDR x -> Bool.False |
---|
548 | | N_BIT_ADDR x -> Bool.False |
---|
549 | | RELATIVE x -> Bool.False |
---|
550 | | ADDR11 x -> Bool.False |
---|
551 | | ADDR16 x -> Bool.False) |
---|
552 | | DATA b' -> |
---|
553 | (match b with |
---|
554 | | DIRECT x -> Bool.False |
---|
555 | | INDIRECT x -> Bool.False |
---|
556 | | EXT_INDIRECT x -> Bool.False |
---|
557 | | REGISTER x -> Bool.False |
---|
558 | | ACC_A -> Bool.False |
---|
559 | | ACC_B -> Bool.False |
---|
560 | | DPTR -> Bool.False |
---|
561 | | DATA e0 -> |
---|
562 | BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
563 | (Nat.S Nat.O)))))))) b' e0 |
---|
564 | | DATA16 x -> Bool.False |
---|
565 | | ACC_DPTR -> Bool.False |
---|
566 | | ACC_PC -> Bool.False |
---|
567 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
568 | | INDIRECT_DPTR -> Bool.False |
---|
569 | | CARRY -> Bool.False |
---|
570 | | BIT_ADDR x -> Bool.False |
---|
571 | | N_BIT_ADDR x -> Bool.False |
---|
572 | | RELATIVE x -> Bool.False |
---|
573 | | ADDR11 x -> Bool.False |
---|
574 | | ADDR16 x -> Bool.False) |
---|
575 | | DATA16 w -> |
---|
576 | (match b with |
---|
577 | | DIRECT x -> Bool.False |
---|
578 | | INDIRECT x -> Bool.False |
---|
579 | | EXT_INDIRECT x -> Bool.False |
---|
580 | | REGISTER x -> Bool.False |
---|
581 | | ACC_A -> Bool.False |
---|
582 | | ACC_B -> Bool.False |
---|
583 | | DPTR -> Bool.False |
---|
584 | | DATA x -> Bool.False |
---|
585 | | DATA16 e0 -> |
---|
586 | BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
587 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
588 | Nat.O)))))))))))))))) w e0 |
---|
589 | | ACC_DPTR -> Bool.False |
---|
590 | | ACC_PC -> Bool.False |
---|
591 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
592 | | INDIRECT_DPTR -> Bool.False |
---|
593 | | CARRY -> Bool.False |
---|
594 | | BIT_ADDR x -> Bool.False |
---|
595 | | N_BIT_ADDR x -> Bool.False |
---|
596 | | RELATIVE x -> Bool.False |
---|
597 | | ADDR11 x -> Bool.False |
---|
598 | | ADDR16 x -> Bool.False) |
---|
599 | | ACC_DPTR -> |
---|
600 | (match b with |
---|
601 | | DIRECT x -> Bool.False |
---|
602 | | INDIRECT x -> Bool.False |
---|
603 | | EXT_INDIRECT x -> Bool.False |
---|
604 | | REGISTER x -> Bool.False |
---|
605 | | ACC_A -> Bool.False |
---|
606 | | ACC_B -> Bool.False |
---|
607 | | DPTR -> Bool.False |
---|
608 | | DATA x -> Bool.False |
---|
609 | | DATA16 x -> Bool.False |
---|
610 | | ACC_DPTR -> Bool.True |
---|
611 | | ACC_PC -> Bool.False |
---|
612 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
613 | | INDIRECT_DPTR -> Bool.False |
---|
614 | | CARRY -> Bool.False |
---|
615 | | BIT_ADDR x -> Bool.False |
---|
616 | | N_BIT_ADDR x -> Bool.False |
---|
617 | | RELATIVE x -> Bool.False |
---|
618 | | ADDR11 x -> Bool.False |
---|
619 | | ADDR16 x -> Bool.False) |
---|
620 | | ACC_PC -> |
---|
621 | (match b with |
---|
622 | | DIRECT x -> Bool.False |
---|
623 | | INDIRECT x -> Bool.False |
---|
624 | | EXT_INDIRECT x -> Bool.False |
---|
625 | | REGISTER x -> Bool.False |
---|
626 | | ACC_A -> Bool.False |
---|
627 | | ACC_B -> Bool.False |
---|
628 | | DPTR -> Bool.False |
---|
629 | | DATA x -> Bool.False |
---|
630 | | DATA16 x -> Bool.False |
---|
631 | | ACC_DPTR -> Bool.False |
---|
632 | | ACC_PC -> Bool.True |
---|
633 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
634 | | INDIRECT_DPTR -> Bool.False |
---|
635 | | CARRY -> Bool.False |
---|
636 | | BIT_ADDR x -> Bool.False |
---|
637 | | N_BIT_ADDR x -> Bool.False |
---|
638 | | RELATIVE x -> Bool.False |
---|
639 | | ADDR11 x -> Bool.False |
---|
640 | | ADDR16 x -> Bool.False) |
---|
641 | | EXT_INDIRECT_DPTR -> |
---|
642 | (match b with |
---|
643 | | DIRECT x -> Bool.False |
---|
644 | | INDIRECT x -> Bool.False |
---|
645 | | EXT_INDIRECT x -> Bool.False |
---|
646 | | REGISTER x -> Bool.False |
---|
647 | | ACC_A -> Bool.False |
---|
648 | | ACC_B -> Bool.False |
---|
649 | | DPTR -> Bool.False |
---|
650 | | DATA x -> Bool.False |
---|
651 | | DATA16 x -> Bool.False |
---|
652 | | ACC_DPTR -> Bool.False |
---|
653 | | ACC_PC -> Bool.False |
---|
654 | | EXT_INDIRECT_DPTR -> Bool.True |
---|
655 | | INDIRECT_DPTR -> Bool.False |
---|
656 | | CARRY -> Bool.False |
---|
657 | | BIT_ADDR x -> Bool.False |
---|
658 | | N_BIT_ADDR x -> Bool.False |
---|
659 | | RELATIVE x -> Bool.False |
---|
660 | | ADDR11 x -> Bool.False |
---|
661 | | ADDR16 x -> Bool.False) |
---|
662 | | INDIRECT_DPTR -> |
---|
663 | (match b with |
---|
664 | | DIRECT x -> Bool.False |
---|
665 | | INDIRECT x -> Bool.False |
---|
666 | | EXT_INDIRECT x -> Bool.False |
---|
667 | | REGISTER x -> Bool.False |
---|
668 | | ACC_A -> Bool.False |
---|
669 | | ACC_B -> Bool.False |
---|
670 | | DPTR -> Bool.False |
---|
671 | | DATA x -> Bool.False |
---|
672 | | DATA16 x -> Bool.False |
---|
673 | | ACC_DPTR -> Bool.False |
---|
674 | | ACC_PC -> Bool.False |
---|
675 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
676 | | INDIRECT_DPTR -> Bool.True |
---|
677 | | CARRY -> Bool.False |
---|
678 | | BIT_ADDR x -> Bool.False |
---|
679 | | N_BIT_ADDR x -> Bool.False |
---|
680 | | RELATIVE x -> Bool.False |
---|
681 | | ADDR11 x -> Bool.False |
---|
682 | | ADDR16 x -> Bool.False) |
---|
683 | | CARRY -> |
---|
684 | (match b with |
---|
685 | | DIRECT x -> Bool.False |
---|
686 | | INDIRECT x -> Bool.False |
---|
687 | | EXT_INDIRECT x -> Bool.False |
---|
688 | | REGISTER x -> Bool.False |
---|
689 | | ACC_A -> Bool.False |
---|
690 | | ACC_B -> Bool.False |
---|
691 | | DPTR -> Bool.False |
---|
692 | | DATA x -> Bool.False |
---|
693 | | DATA16 x -> Bool.False |
---|
694 | | ACC_DPTR -> Bool.False |
---|
695 | | ACC_PC -> Bool.False |
---|
696 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
697 | | INDIRECT_DPTR -> Bool.False |
---|
698 | | CARRY -> Bool.True |
---|
699 | | BIT_ADDR x -> Bool.False |
---|
700 | | N_BIT_ADDR x -> Bool.False |
---|
701 | | RELATIVE x -> Bool.False |
---|
702 | | ADDR11 x -> Bool.False |
---|
703 | | ADDR16 x -> Bool.False) |
---|
704 | | BIT_ADDR b' -> |
---|
705 | (match b with |
---|
706 | | DIRECT x -> Bool.False |
---|
707 | | INDIRECT x -> Bool.False |
---|
708 | | EXT_INDIRECT x -> Bool.False |
---|
709 | | REGISTER x -> Bool.False |
---|
710 | | ACC_A -> Bool.False |
---|
711 | | ACC_B -> Bool.False |
---|
712 | | DPTR -> Bool.False |
---|
713 | | DATA x -> Bool.False |
---|
714 | | DATA16 x -> Bool.False |
---|
715 | | ACC_DPTR -> Bool.False |
---|
716 | | ACC_PC -> Bool.False |
---|
717 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
718 | | INDIRECT_DPTR -> Bool.False |
---|
719 | | CARRY -> Bool.False |
---|
720 | | BIT_ADDR e0 -> |
---|
721 | BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
722 | (Nat.S Nat.O)))))))) b' e0 |
---|
723 | | N_BIT_ADDR x -> Bool.False |
---|
724 | | RELATIVE x -> Bool.False |
---|
725 | | ADDR11 x -> Bool.False |
---|
726 | | ADDR16 x -> Bool.False) |
---|
727 | | N_BIT_ADDR b' -> |
---|
728 | (match b with |
---|
729 | | DIRECT x -> Bool.False |
---|
730 | | INDIRECT x -> Bool.False |
---|
731 | | EXT_INDIRECT x -> Bool.False |
---|
732 | | REGISTER x -> Bool.False |
---|
733 | | ACC_A -> Bool.False |
---|
734 | | ACC_B -> Bool.False |
---|
735 | | DPTR -> Bool.False |
---|
736 | | DATA x -> Bool.False |
---|
737 | | DATA16 x -> Bool.False |
---|
738 | | ACC_DPTR -> Bool.False |
---|
739 | | ACC_PC -> Bool.False |
---|
740 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
741 | | INDIRECT_DPTR -> Bool.False |
---|
742 | | CARRY -> Bool.False |
---|
743 | | BIT_ADDR x -> Bool.False |
---|
744 | | N_BIT_ADDR e0 -> |
---|
745 | BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
746 | (Nat.S Nat.O)))))))) b' e0 |
---|
747 | | RELATIVE x -> Bool.False |
---|
748 | | ADDR11 x -> Bool.False |
---|
749 | | ADDR16 x -> Bool.False) |
---|
750 | | RELATIVE n -> |
---|
751 | (match b with |
---|
752 | | DIRECT x -> Bool.False |
---|
753 | | INDIRECT x -> Bool.False |
---|
754 | | EXT_INDIRECT x -> Bool.False |
---|
755 | | REGISTER x -> Bool.False |
---|
756 | | ACC_A -> Bool.False |
---|
757 | | ACC_B -> Bool.False |
---|
758 | | DPTR -> Bool.False |
---|
759 | | DATA x -> Bool.False |
---|
760 | | DATA16 x -> Bool.False |
---|
761 | | ACC_DPTR -> Bool.False |
---|
762 | | ACC_PC -> Bool.False |
---|
763 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
764 | | INDIRECT_DPTR -> Bool.False |
---|
765 | | CARRY -> Bool.False |
---|
766 | | BIT_ADDR x -> Bool.False |
---|
767 | | N_BIT_ADDR x -> Bool.False |
---|
768 | | RELATIVE e0 -> |
---|
769 | BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
770 | (Nat.S Nat.O)))))))) n e0 |
---|
771 | | ADDR11 x -> Bool.False |
---|
772 | | ADDR16 x -> Bool.False) |
---|
773 | | ADDR11 w -> |
---|
774 | (match b with |
---|
775 | | DIRECT x -> Bool.False |
---|
776 | | INDIRECT x -> Bool.False |
---|
777 | | EXT_INDIRECT x -> Bool.False |
---|
778 | | REGISTER x -> Bool.False |
---|
779 | | ACC_A -> Bool.False |
---|
780 | | ACC_B -> Bool.False |
---|
781 | | DPTR -> Bool.False |
---|
782 | | DATA x -> Bool.False |
---|
783 | | DATA16 x -> Bool.False |
---|
784 | | ACC_DPTR -> Bool.False |
---|
785 | | ACC_PC -> Bool.False |
---|
786 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
787 | | INDIRECT_DPTR -> Bool.False |
---|
788 | | CARRY -> Bool.False |
---|
789 | | BIT_ADDR x -> Bool.False |
---|
790 | | N_BIT_ADDR x -> Bool.False |
---|
791 | | RELATIVE x -> Bool.False |
---|
792 | | ADDR11 e0 -> |
---|
793 | BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
794 | (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))) w e0 |
---|
795 | | ADDR16 x -> Bool.False) |
---|
796 | | ADDR16 w -> |
---|
797 | (match b with |
---|
798 | | DIRECT x -> Bool.False |
---|
799 | | INDIRECT x -> Bool.False |
---|
800 | | EXT_INDIRECT x -> Bool.False |
---|
801 | | REGISTER x -> Bool.False |
---|
802 | | ACC_A -> Bool.False |
---|
803 | | ACC_B -> Bool.False |
---|
804 | | DPTR -> Bool.False |
---|
805 | | DATA x -> Bool.False |
---|
806 | | DATA16 x -> Bool.False |
---|
807 | | ACC_DPTR -> Bool.False |
---|
808 | | ACC_PC -> Bool.False |
---|
809 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
810 | | INDIRECT_DPTR -> Bool.False |
---|
811 | | CARRY -> Bool.False |
---|
812 | | BIT_ADDR x -> Bool.False |
---|
813 | | N_BIT_ADDR x -> Bool.False |
---|
814 | | RELATIVE x -> Bool.False |
---|
815 | | ADDR11 x -> Bool.False |
---|
816 | | ADDR16 e0 -> |
---|
817 | BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
818 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
819 | Nat.O)))))))))))))))) w e0) |
---|
820 | |
---|
821 | type addressing_mode_tag = |
---|
822 | | Direct |
---|
823 | | Indirect |
---|
824 | | Ext_indirect |
---|
825 | | Registr |
---|
826 | | Acc_a |
---|
827 | | Acc_b |
---|
828 | | Dptr |
---|
829 | | Data |
---|
830 | | Data16 |
---|
831 | | Acc_dptr |
---|
832 | | Acc_pc |
---|
833 | | Ext_indirect_dptr |
---|
834 | | Indirect_dptr |
---|
835 | | Carry |
---|
836 | | Bit_addr |
---|
837 | | N_bit_addr |
---|
838 | | Relative |
---|
839 | | Addr11 |
---|
840 | | Addr16 |
---|
841 | |
---|
842 | (** val addressing_mode_tag_rect_Type4 : |
---|
843 | 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 |
---|
844 | -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> |
---|
845 | addressing_mode_tag -> 'a1 **) |
---|
846 | let rec addressing_mode_tag_rect_Type4 h_direct h_indirect h_ext_indirect h_registr h_acc_a h_acc_b h_dptr h_data h_data16 h_acc_dptr h_acc_pc h_ext_indirect_dptr h_indirect_dptr h_carry h_bit_addr h_n_bit_addr h_relative h_addr11 h_addr16 = function |
---|
847 | | Direct -> h_direct |
---|
848 | | Indirect -> h_indirect |
---|
849 | | Ext_indirect -> h_ext_indirect |
---|
850 | | Registr -> h_registr |
---|
851 | | Acc_a -> h_acc_a |
---|
852 | | Acc_b -> h_acc_b |
---|
853 | | Dptr -> h_dptr |
---|
854 | | Data -> h_data |
---|
855 | | Data16 -> h_data16 |
---|
856 | | Acc_dptr -> h_acc_dptr |
---|
857 | | Acc_pc -> h_acc_pc |
---|
858 | | Ext_indirect_dptr -> h_ext_indirect_dptr |
---|
859 | | Indirect_dptr -> h_indirect_dptr |
---|
860 | | Carry -> h_carry |
---|
861 | | Bit_addr -> h_bit_addr |
---|
862 | | N_bit_addr -> h_n_bit_addr |
---|
863 | | Relative -> h_relative |
---|
864 | | Addr11 -> h_addr11 |
---|
865 | | Addr16 -> h_addr16 |
---|
866 | |
---|
867 | (** val addressing_mode_tag_rect_Type5 : |
---|
868 | 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 |
---|
869 | -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> |
---|
870 | addressing_mode_tag -> 'a1 **) |
---|
871 | let rec addressing_mode_tag_rect_Type5 h_direct h_indirect h_ext_indirect h_registr h_acc_a h_acc_b h_dptr h_data h_data16 h_acc_dptr h_acc_pc h_ext_indirect_dptr h_indirect_dptr h_carry h_bit_addr h_n_bit_addr h_relative h_addr11 h_addr16 = function |
---|
872 | | Direct -> h_direct |
---|
873 | | Indirect -> h_indirect |
---|
874 | | Ext_indirect -> h_ext_indirect |
---|
875 | | Registr -> h_registr |
---|
876 | | Acc_a -> h_acc_a |
---|
877 | | Acc_b -> h_acc_b |
---|
878 | | Dptr -> h_dptr |
---|
879 | | Data -> h_data |
---|
880 | | Data16 -> h_data16 |
---|
881 | | Acc_dptr -> h_acc_dptr |
---|
882 | | Acc_pc -> h_acc_pc |
---|
883 | | Ext_indirect_dptr -> h_ext_indirect_dptr |
---|
884 | | Indirect_dptr -> h_indirect_dptr |
---|
885 | | Carry -> h_carry |
---|
886 | | Bit_addr -> h_bit_addr |
---|
887 | | N_bit_addr -> h_n_bit_addr |
---|
888 | | Relative -> h_relative |
---|
889 | | Addr11 -> h_addr11 |
---|
890 | | Addr16 -> h_addr16 |
---|
891 | |
---|
892 | (** val addressing_mode_tag_rect_Type3 : |
---|
893 | 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 |
---|
894 | -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> |
---|
895 | addressing_mode_tag -> 'a1 **) |
---|
896 | let rec addressing_mode_tag_rect_Type3 h_direct h_indirect h_ext_indirect h_registr h_acc_a h_acc_b h_dptr h_data h_data16 h_acc_dptr h_acc_pc h_ext_indirect_dptr h_indirect_dptr h_carry h_bit_addr h_n_bit_addr h_relative h_addr11 h_addr16 = function |
---|
897 | | Direct -> h_direct |
---|
898 | | Indirect -> h_indirect |
---|
899 | | Ext_indirect -> h_ext_indirect |
---|
900 | | Registr -> h_registr |
---|
901 | | Acc_a -> h_acc_a |
---|
902 | | Acc_b -> h_acc_b |
---|
903 | | Dptr -> h_dptr |
---|
904 | | Data -> h_data |
---|
905 | | Data16 -> h_data16 |
---|
906 | | Acc_dptr -> h_acc_dptr |
---|
907 | | Acc_pc -> h_acc_pc |
---|
908 | | Ext_indirect_dptr -> h_ext_indirect_dptr |
---|
909 | | Indirect_dptr -> h_indirect_dptr |
---|
910 | | Carry -> h_carry |
---|
911 | | Bit_addr -> h_bit_addr |
---|
912 | | N_bit_addr -> h_n_bit_addr |
---|
913 | | Relative -> h_relative |
---|
914 | | Addr11 -> h_addr11 |
---|
915 | | Addr16 -> h_addr16 |
---|
916 | |
---|
917 | (** val addressing_mode_tag_rect_Type2 : |
---|
918 | 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 |
---|
919 | -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> |
---|
920 | addressing_mode_tag -> 'a1 **) |
---|
921 | let rec addressing_mode_tag_rect_Type2 h_direct h_indirect h_ext_indirect h_registr h_acc_a h_acc_b h_dptr h_data h_data16 h_acc_dptr h_acc_pc h_ext_indirect_dptr h_indirect_dptr h_carry h_bit_addr h_n_bit_addr h_relative h_addr11 h_addr16 = function |
---|
922 | | Direct -> h_direct |
---|
923 | | Indirect -> h_indirect |
---|
924 | | Ext_indirect -> h_ext_indirect |
---|
925 | | Registr -> h_registr |
---|
926 | | Acc_a -> h_acc_a |
---|
927 | | Acc_b -> h_acc_b |
---|
928 | | Dptr -> h_dptr |
---|
929 | | Data -> h_data |
---|
930 | | Data16 -> h_data16 |
---|
931 | | Acc_dptr -> h_acc_dptr |
---|
932 | | Acc_pc -> h_acc_pc |
---|
933 | | Ext_indirect_dptr -> h_ext_indirect_dptr |
---|
934 | | Indirect_dptr -> h_indirect_dptr |
---|
935 | | Carry -> h_carry |
---|
936 | | Bit_addr -> h_bit_addr |
---|
937 | | N_bit_addr -> h_n_bit_addr |
---|
938 | | Relative -> h_relative |
---|
939 | | Addr11 -> h_addr11 |
---|
940 | | Addr16 -> h_addr16 |
---|
941 | |
---|
942 | (** val addressing_mode_tag_rect_Type1 : |
---|
943 | 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 |
---|
944 | -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> |
---|
945 | addressing_mode_tag -> 'a1 **) |
---|
946 | let rec addressing_mode_tag_rect_Type1 h_direct h_indirect h_ext_indirect h_registr h_acc_a h_acc_b h_dptr h_data h_data16 h_acc_dptr h_acc_pc h_ext_indirect_dptr h_indirect_dptr h_carry h_bit_addr h_n_bit_addr h_relative h_addr11 h_addr16 = function |
---|
947 | | Direct -> h_direct |
---|
948 | | Indirect -> h_indirect |
---|
949 | | Ext_indirect -> h_ext_indirect |
---|
950 | | Registr -> h_registr |
---|
951 | | Acc_a -> h_acc_a |
---|
952 | | Acc_b -> h_acc_b |
---|
953 | | Dptr -> h_dptr |
---|
954 | | Data -> h_data |
---|
955 | | Data16 -> h_data16 |
---|
956 | | Acc_dptr -> h_acc_dptr |
---|
957 | | Acc_pc -> h_acc_pc |
---|
958 | | Ext_indirect_dptr -> h_ext_indirect_dptr |
---|
959 | | Indirect_dptr -> h_indirect_dptr |
---|
960 | | Carry -> h_carry |
---|
961 | | Bit_addr -> h_bit_addr |
---|
962 | | N_bit_addr -> h_n_bit_addr |
---|
963 | | Relative -> h_relative |
---|
964 | | Addr11 -> h_addr11 |
---|
965 | | Addr16 -> h_addr16 |
---|
966 | |
---|
967 | (** val addressing_mode_tag_rect_Type0 : |
---|
968 | 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 |
---|
969 | -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> |
---|
970 | addressing_mode_tag -> 'a1 **) |
---|
971 | let rec addressing_mode_tag_rect_Type0 h_direct h_indirect h_ext_indirect h_registr h_acc_a h_acc_b h_dptr h_data h_data16 h_acc_dptr h_acc_pc h_ext_indirect_dptr h_indirect_dptr h_carry h_bit_addr h_n_bit_addr h_relative h_addr11 h_addr16 = function |
---|
972 | | Direct -> h_direct |
---|
973 | | Indirect -> h_indirect |
---|
974 | | Ext_indirect -> h_ext_indirect |
---|
975 | | Registr -> h_registr |
---|
976 | | Acc_a -> h_acc_a |
---|
977 | | Acc_b -> h_acc_b |
---|
978 | | Dptr -> h_dptr |
---|
979 | | Data -> h_data |
---|
980 | | Data16 -> h_data16 |
---|
981 | | Acc_dptr -> h_acc_dptr |
---|
982 | | Acc_pc -> h_acc_pc |
---|
983 | | Ext_indirect_dptr -> h_ext_indirect_dptr |
---|
984 | | Indirect_dptr -> h_indirect_dptr |
---|
985 | | Carry -> h_carry |
---|
986 | | Bit_addr -> h_bit_addr |
---|
987 | | N_bit_addr -> h_n_bit_addr |
---|
988 | | Relative -> h_relative |
---|
989 | | Addr11 -> h_addr11 |
---|
990 | | Addr16 -> h_addr16 |
---|
991 | |
---|
992 | (** val addressing_mode_tag_inv_rect_Type4 : |
---|
993 | addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ |
---|
994 | -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> |
---|
995 | (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) |
---|
996 | -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> |
---|
997 | 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
998 | let addressing_mode_tag_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 = |
---|
999 | let hcut = |
---|
1000 | addressing_mode_tag_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 |
---|
1001 | h14 h15 h16 h17 h18 h19 hterm |
---|
1002 | in |
---|
1003 | hcut __ |
---|
1004 | |
---|
1005 | (** val addressing_mode_tag_inv_rect_Type3 : |
---|
1006 | addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ |
---|
1007 | -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> |
---|
1008 | (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) |
---|
1009 | -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> |
---|
1010 | 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
1011 | let addressing_mode_tag_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 = |
---|
1012 | let hcut = |
---|
1013 | addressing_mode_tag_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 |
---|
1014 | h14 h15 h16 h17 h18 h19 hterm |
---|
1015 | in |
---|
1016 | hcut __ |
---|
1017 | |
---|
1018 | (** val addressing_mode_tag_inv_rect_Type2 : |
---|
1019 | addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ |
---|
1020 | -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> |
---|
1021 | (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) |
---|
1022 | -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> |
---|
1023 | 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
1024 | let addressing_mode_tag_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 = |
---|
1025 | let hcut = |
---|
1026 | addressing_mode_tag_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 |
---|
1027 | h14 h15 h16 h17 h18 h19 hterm |
---|
1028 | in |
---|
1029 | hcut __ |
---|
1030 | |
---|
1031 | (** val addressing_mode_tag_inv_rect_Type1 : |
---|
1032 | addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ |
---|
1033 | -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> |
---|
1034 | (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) |
---|
1035 | -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> |
---|
1036 | 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
1037 | let addressing_mode_tag_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 = |
---|
1038 | let hcut = |
---|
1039 | addressing_mode_tag_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 |
---|
1040 | h14 h15 h16 h17 h18 h19 hterm |
---|
1041 | in |
---|
1042 | hcut __ |
---|
1043 | |
---|
1044 | (** val addressing_mode_tag_inv_rect_Type0 : |
---|
1045 | addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ |
---|
1046 | -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> |
---|
1047 | (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) |
---|
1048 | -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> |
---|
1049 | 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
1050 | let addressing_mode_tag_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 = |
---|
1051 | let hcut = |
---|
1052 | addressing_mode_tag_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 |
---|
1053 | h14 h15 h16 h17 h18 h19 hterm |
---|
1054 | in |
---|
1055 | hcut __ |
---|
1056 | |
---|
1057 | (** val addressing_mode_tag_discr : |
---|
1058 | addressing_mode_tag -> addressing_mode_tag -> __ **) |
---|
1059 | let addressing_mode_tag_discr x y = |
---|
1060 | Logic.eq_rect_Type2 x |
---|
1061 | (match x with |
---|
1062 | | Direct -> Obj.magic (fun _ dH -> dH) |
---|
1063 | | Indirect -> Obj.magic (fun _ dH -> dH) |
---|
1064 | | Ext_indirect -> Obj.magic (fun _ dH -> dH) |
---|
1065 | | Registr -> Obj.magic (fun _ dH -> dH) |
---|
1066 | | Acc_a -> Obj.magic (fun _ dH -> dH) |
---|
1067 | | Acc_b -> Obj.magic (fun _ dH -> dH) |
---|
1068 | | Dptr -> Obj.magic (fun _ dH -> dH) |
---|
1069 | | Data -> Obj.magic (fun _ dH -> dH) |
---|
1070 | | Data16 -> Obj.magic (fun _ dH -> dH) |
---|
1071 | | Acc_dptr -> Obj.magic (fun _ dH -> dH) |
---|
1072 | | Acc_pc -> Obj.magic (fun _ dH -> dH) |
---|
1073 | | Ext_indirect_dptr -> Obj.magic (fun _ dH -> dH) |
---|
1074 | | Indirect_dptr -> Obj.magic (fun _ dH -> dH) |
---|
1075 | | Carry -> Obj.magic (fun _ dH -> dH) |
---|
1076 | | Bit_addr -> Obj.magic (fun _ dH -> dH) |
---|
1077 | | N_bit_addr -> Obj.magic (fun _ dH -> dH) |
---|
1078 | | Relative -> Obj.magic (fun _ dH -> dH) |
---|
1079 | | Addr11 -> Obj.magic (fun _ dH -> dH) |
---|
1080 | | Addr16 -> Obj.magic (fun _ dH -> dH)) y |
---|
1081 | |
---|
1082 | (** val addressing_mode_tag_jmdiscr : |
---|
1083 | addressing_mode_tag -> addressing_mode_tag -> __ **) |
---|
1084 | let addressing_mode_tag_jmdiscr x y = |
---|
1085 | Logic.eq_rect_Type2 x |
---|
1086 | (match x with |
---|
1087 | | Direct -> Obj.magic (fun _ dH -> dH) |
---|
1088 | | Indirect -> Obj.magic (fun _ dH -> dH) |
---|
1089 | | Ext_indirect -> Obj.magic (fun _ dH -> dH) |
---|
1090 | | Registr -> Obj.magic (fun _ dH -> dH) |
---|
1091 | | Acc_a -> Obj.magic (fun _ dH -> dH) |
---|
1092 | | Acc_b -> Obj.magic (fun _ dH -> dH) |
---|
1093 | | Dptr -> Obj.magic (fun _ dH -> dH) |
---|
1094 | | Data -> Obj.magic (fun _ dH -> dH) |
---|
1095 | | Data16 -> Obj.magic (fun _ dH -> dH) |
---|
1096 | | Acc_dptr -> Obj.magic (fun _ dH -> dH) |
---|
1097 | | Acc_pc -> Obj.magic (fun _ dH -> dH) |
---|
1098 | | Ext_indirect_dptr -> Obj.magic (fun _ dH -> dH) |
---|
1099 | | Indirect_dptr -> Obj.magic (fun _ dH -> dH) |
---|
1100 | | Carry -> Obj.magic (fun _ dH -> dH) |
---|
1101 | | Bit_addr -> Obj.magic (fun _ dH -> dH) |
---|
1102 | | N_bit_addr -> Obj.magic (fun _ dH -> dH) |
---|
1103 | | Relative -> Obj.magic (fun _ dH -> dH) |
---|
1104 | | Addr11 -> Obj.magic (fun _ dH -> dH) |
---|
1105 | | Addr16 -> Obj.magic (fun _ dH -> dH)) y |
---|
1106 | |
---|
1107 | (** val eq_a : addressing_mode_tag -> addressing_mode_tag -> Bool.bool **) |
---|
1108 | let eq_a a b = |
---|
1109 | match a with |
---|
1110 | | Direct -> |
---|
1111 | (match b with |
---|
1112 | | Direct -> Bool.True |
---|
1113 | | Indirect -> Bool.False |
---|
1114 | | Ext_indirect -> Bool.False |
---|
1115 | | Registr -> Bool.False |
---|
1116 | | Acc_a -> Bool.False |
---|
1117 | | Acc_b -> Bool.False |
---|
1118 | | Dptr -> Bool.False |
---|
1119 | | Data -> Bool.False |
---|
1120 | | Data16 -> Bool.False |
---|
1121 | | Acc_dptr -> Bool.False |
---|
1122 | | Acc_pc -> Bool.False |
---|
1123 | | Ext_indirect_dptr -> Bool.False |
---|
1124 | | Indirect_dptr -> Bool.False |
---|
1125 | | Carry -> Bool.False |
---|
1126 | | Bit_addr -> Bool.False |
---|
1127 | | N_bit_addr -> Bool.False |
---|
1128 | | Relative -> Bool.False |
---|
1129 | | Addr11 -> Bool.False |
---|
1130 | | Addr16 -> Bool.False) |
---|
1131 | | Indirect -> |
---|
1132 | (match b with |
---|
1133 | | Direct -> Bool.False |
---|
1134 | | Indirect -> Bool.True |
---|
1135 | | Ext_indirect -> Bool.False |
---|
1136 | | Registr -> Bool.False |
---|
1137 | | Acc_a -> Bool.False |
---|
1138 | | Acc_b -> Bool.False |
---|
1139 | | Dptr -> Bool.False |
---|
1140 | | Data -> Bool.False |
---|
1141 | | Data16 -> Bool.False |
---|
1142 | | Acc_dptr -> Bool.False |
---|
1143 | | Acc_pc -> Bool.False |
---|
1144 | | Ext_indirect_dptr -> Bool.False |
---|
1145 | | Indirect_dptr -> Bool.False |
---|
1146 | | Carry -> Bool.False |
---|
1147 | | Bit_addr -> Bool.False |
---|
1148 | | N_bit_addr -> Bool.False |
---|
1149 | | Relative -> Bool.False |
---|
1150 | | Addr11 -> Bool.False |
---|
1151 | | Addr16 -> Bool.False) |
---|
1152 | | Ext_indirect -> |
---|
1153 | (match b with |
---|
1154 | | Direct -> Bool.False |
---|
1155 | | Indirect -> Bool.False |
---|
1156 | | Ext_indirect -> Bool.True |
---|
1157 | | Registr -> Bool.False |
---|
1158 | | Acc_a -> Bool.False |
---|
1159 | | Acc_b -> Bool.False |
---|
1160 | | Dptr -> Bool.False |
---|
1161 | | Data -> Bool.False |
---|
1162 | | Data16 -> Bool.False |
---|
1163 | | Acc_dptr -> Bool.False |
---|
1164 | | Acc_pc -> Bool.False |
---|
1165 | | Ext_indirect_dptr -> Bool.False |
---|
1166 | | Indirect_dptr -> Bool.False |
---|
1167 | | Carry -> Bool.False |
---|
1168 | | Bit_addr -> Bool.False |
---|
1169 | | N_bit_addr -> Bool.False |
---|
1170 | | Relative -> Bool.False |
---|
1171 | | Addr11 -> Bool.False |
---|
1172 | | Addr16 -> Bool.False) |
---|
1173 | | Registr -> |
---|
1174 | (match b with |
---|
1175 | | Direct -> Bool.False |
---|
1176 | | Indirect -> Bool.False |
---|
1177 | | Ext_indirect -> Bool.False |
---|
1178 | | Registr -> Bool.True |
---|
1179 | | Acc_a -> Bool.False |
---|
1180 | | Acc_b -> Bool.False |
---|
1181 | | Dptr -> Bool.False |
---|
1182 | | Data -> Bool.False |
---|
1183 | | Data16 -> Bool.False |
---|
1184 | | Acc_dptr -> Bool.False |
---|
1185 | | Acc_pc -> Bool.False |
---|
1186 | | Ext_indirect_dptr -> Bool.False |
---|
1187 | | Indirect_dptr -> Bool.False |
---|
1188 | | Carry -> Bool.False |
---|
1189 | | Bit_addr -> Bool.False |
---|
1190 | | N_bit_addr -> Bool.False |
---|
1191 | | Relative -> Bool.False |
---|
1192 | | Addr11 -> Bool.False |
---|
1193 | | Addr16 -> Bool.False) |
---|
1194 | | Acc_a -> |
---|
1195 | (match b with |
---|
1196 | | Direct -> Bool.False |
---|
1197 | | Indirect -> Bool.False |
---|
1198 | | Ext_indirect -> Bool.False |
---|
1199 | | Registr -> Bool.False |
---|
1200 | | Acc_a -> Bool.True |
---|
1201 | | Acc_b -> Bool.False |
---|
1202 | | Dptr -> Bool.False |
---|
1203 | | Data -> Bool.False |
---|
1204 | | Data16 -> Bool.False |
---|
1205 | | Acc_dptr -> Bool.False |
---|
1206 | | Acc_pc -> Bool.False |
---|
1207 | | Ext_indirect_dptr -> Bool.False |
---|
1208 | | Indirect_dptr -> Bool.False |
---|
1209 | | Carry -> Bool.False |
---|
1210 | | Bit_addr -> Bool.False |
---|
1211 | | N_bit_addr -> Bool.False |
---|
1212 | | Relative -> Bool.False |
---|
1213 | | Addr11 -> Bool.False |
---|
1214 | | Addr16 -> Bool.False) |
---|
1215 | | Acc_b -> |
---|
1216 | (match b with |
---|
1217 | | Direct -> Bool.False |
---|
1218 | | Indirect -> Bool.False |
---|
1219 | | Ext_indirect -> Bool.False |
---|
1220 | | Registr -> Bool.False |
---|
1221 | | Acc_a -> Bool.False |
---|
1222 | | Acc_b -> Bool.True |
---|
1223 | | Dptr -> Bool.False |
---|
1224 | | Data -> Bool.False |
---|
1225 | | Data16 -> Bool.False |
---|
1226 | | Acc_dptr -> Bool.False |
---|
1227 | | Acc_pc -> Bool.False |
---|
1228 | | Ext_indirect_dptr -> Bool.False |
---|
1229 | | Indirect_dptr -> Bool.False |
---|
1230 | | Carry -> Bool.False |
---|
1231 | | Bit_addr -> Bool.False |
---|
1232 | | N_bit_addr -> Bool.False |
---|
1233 | | Relative -> Bool.False |
---|
1234 | | Addr11 -> Bool.False |
---|
1235 | | Addr16 -> Bool.False) |
---|
1236 | | Dptr -> |
---|
1237 | (match b with |
---|
1238 | | Direct -> Bool.False |
---|
1239 | | Indirect -> Bool.False |
---|
1240 | | Ext_indirect -> Bool.False |
---|
1241 | | Registr -> Bool.False |
---|
1242 | | Acc_a -> Bool.False |
---|
1243 | | Acc_b -> Bool.False |
---|
1244 | | Dptr -> Bool.True |
---|
1245 | | Data -> Bool.False |
---|
1246 | | Data16 -> Bool.False |
---|
1247 | | Acc_dptr -> Bool.False |
---|
1248 | | Acc_pc -> Bool.False |
---|
1249 | | Ext_indirect_dptr -> Bool.False |
---|
1250 | | Indirect_dptr -> Bool.False |
---|
1251 | | Carry -> Bool.False |
---|
1252 | | Bit_addr -> Bool.False |
---|
1253 | | N_bit_addr -> Bool.False |
---|
1254 | | Relative -> Bool.False |
---|
1255 | | Addr11 -> Bool.False |
---|
1256 | | Addr16 -> Bool.False) |
---|
1257 | | Data -> |
---|
1258 | (match b with |
---|
1259 | | Direct -> Bool.False |
---|
1260 | | Indirect -> Bool.False |
---|
1261 | | Ext_indirect -> Bool.False |
---|
1262 | | Registr -> Bool.False |
---|
1263 | | Acc_a -> Bool.False |
---|
1264 | | Acc_b -> Bool.False |
---|
1265 | | Dptr -> Bool.False |
---|
1266 | | Data -> Bool.True |
---|
1267 | | Data16 -> Bool.False |
---|
1268 | | Acc_dptr -> Bool.False |
---|
1269 | | Acc_pc -> Bool.False |
---|
1270 | | Ext_indirect_dptr -> Bool.False |
---|
1271 | | Indirect_dptr -> Bool.False |
---|
1272 | | Carry -> Bool.False |
---|
1273 | | Bit_addr -> Bool.False |
---|
1274 | | N_bit_addr -> Bool.False |
---|
1275 | | Relative -> Bool.False |
---|
1276 | | Addr11 -> Bool.False |
---|
1277 | | Addr16 -> Bool.False) |
---|
1278 | | Data16 -> |
---|
1279 | (match b with |
---|
1280 | | Direct -> Bool.False |
---|
1281 | | Indirect -> Bool.False |
---|
1282 | | Ext_indirect -> Bool.False |
---|
1283 | | Registr -> Bool.False |
---|
1284 | | Acc_a -> Bool.False |
---|
1285 | | Acc_b -> Bool.False |
---|
1286 | | Dptr -> Bool.False |
---|
1287 | | Data -> Bool.False |
---|
1288 | | Data16 -> Bool.True |
---|
1289 | | Acc_dptr -> Bool.False |
---|
1290 | | Acc_pc -> Bool.False |
---|
1291 | | Ext_indirect_dptr -> Bool.False |
---|
1292 | | Indirect_dptr -> Bool.False |
---|
1293 | | Carry -> Bool.False |
---|
1294 | | Bit_addr -> Bool.False |
---|
1295 | | N_bit_addr -> Bool.False |
---|
1296 | | Relative -> Bool.False |
---|
1297 | | Addr11 -> Bool.False |
---|
1298 | | Addr16 -> Bool.False) |
---|
1299 | | Acc_dptr -> |
---|
1300 | (match b with |
---|
1301 | | Direct -> Bool.False |
---|
1302 | | Indirect -> Bool.False |
---|
1303 | | Ext_indirect -> Bool.False |
---|
1304 | | Registr -> Bool.False |
---|
1305 | | Acc_a -> Bool.False |
---|
1306 | | Acc_b -> Bool.False |
---|
1307 | | Dptr -> Bool.False |
---|
1308 | | Data -> Bool.False |
---|
1309 | | Data16 -> Bool.False |
---|
1310 | | Acc_dptr -> Bool.True |
---|
1311 | | Acc_pc -> Bool.False |
---|
1312 | | Ext_indirect_dptr -> Bool.False |
---|
1313 | | Indirect_dptr -> Bool.False |
---|
1314 | | Carry -> Bool.False |
---|
1315 | | Bit_addr -> Bool.False |
---|
1316 | | N_bit_addr -> Bool.False |
---|
1317 | | Relative -> Bool.False |
---|
1318 | | Addr11 -> Bool.False |
---|
1319 | | Addr16 -> Bool.False) |
---|
1320 | | Acc_pc -> |
---|
1321 | (match b with |
---|
1322 | | Direct -> Bool.False |
---|
1323 | | Indirect -> Bool.False |
---|
1324 | | Ext_indirect -> Bool.False |
---|
1325 | | Registr -> Bool.False |
---|
1326 | | Acc_a -> Bool.False |
---|
1327 | | Acc_b -> Bool.False |
---|
1328 | | Dptr -> Bool.False |
---|
1329 | | Data -> Bool.False |
---|
1330 | | Data16 -> Bool.False |
---|
1331 | | Acc_dptr -> Bool.False |
---|
1332 | | Acc_pc -> Bool.True |
---|
1333 | | Ext_indirect_dptr -> Bool.False |
---|
1334 | | Indirect_dptr -> Bool.False |
---|
1335 | | Carry -> Bool.False |
---|
1336 | | Bit_addr -> Bool.False |
---|
1337 | | N_bit_addr -> Bool.False |
---|
1338 | | Relative -> Bool.False |
---|
1339 | | Addr11 -> Bool.False |
---|
1340 | | Addr16 -> Bool.False) |
---|
1341 | | Ext_indirect_dptr -> |
---|
1342 | (match b with |
---|
1343 | | Direct -> Bool.False |
---|
1344 | | Indirect -> Bool.False |
---|
1345 | | Ext_indirect -> Bool.False |
---|
1346 | | Registr -> Bool.False |
---|
1347 | | Acc_a -> Bool.False |
---|
1348 | | Acc_b -> Bool.False |
---|
1349 | | Dptr -> Bool.False |
---|
1350 | | Data -> Bool.False |
---|
1351 | | Data16 -> Bool.False |
---|
1352 | | Acc_dptr -> Bool.False |
---|
1353 | | Acc_pc -> Bool.False |
---|
1354 | | Ext_indirect_dptr -> Bool.True |
---|
1355 | | Indirect_dptr -> Bool.False |
---|
1356 | | Carry -> Bool.False |
---|
1357 | | Bit_addr -> Bool.False |
---|
1358 | | N_bit_addr -> Bool.False |
---|
1359 | | Relative -> Bool.False |
---|
1360 | | Addr11 -> Bool.False |
---|
1361 | | Addr16 -> Bool.False) |
---|
1362 | | Indirect_dptr -> |
---|
1363 | (match b with |
---|
1364 | | Direct -> Bool.False |
---|
1365 | | Indirect -> Bool.False |
---|
1366 | | Ext_indirect -> Bool.False |
---|
1367 | | Registr -> Bool.False |
---|
1368 | | Acc_a -> Bool.False |
---|
1369 | | Acc_b -> Bool.False |
---|
1370 | | Dptr -> Bool.False |
---|
1371 | | Data -> Bool.False |
---|
1372 | | Data16 -> Bool.False |
---|
1373 | | Acc_dptr -> Bool.False |
---|
1374 | | Acc_pc -> Bool.False |
---|
1375 | | Ext_indirect_dptr -> Bool.False |
---|
1376 | | Indirect_dptr -> Bool.True |
---|
1377 | | Carry -> Bool.False |
---|
1378 | | Bit_addr -> Bool.False |
---|
1379 | | N_bit_addr -> Bool.False |
---|
1380 | | Relative -> Bool.False |
---|
1381 | | Addr11 -> Bool.False |
---|
1382 | | Addr16 -> Bool.False) |
---|
1383 | | Carry -> |
---|
1384 | (match b with |
---|
1385 | | Direct -> Bool.False |
---|
1386 | | Indirect -> Bool.False |
---|
1387 | | Ext_indirect -> Bool.False |
---|
1388 | | Registr -> Bool.False |
---|
1389 | | Acc_a -> Bool.False |
---|
1390 | | Acc_b -> Bool.False |
---|
1391 | | Dptr -> Bool.False |
---|
1392 | | Data -> Bool.False |
---|
1393 | | Data16 -> Bool.False |
---|
1394 | | Acc_dptr -> Bool.False |
---|
1395 | | Acc_pc -> Bool.False |
---|
1396 | | Ext_indirect_dptr -> Bool.False |
---|
1397 | | Indirect_dptr -> Bool.False |
---|
1398 | | Carry -> Bool.True |
---|
1399 | | Bit_addr -> Bool.False |
---|
1400 | | N_bit_addr -> Bool.False |
---|
1401 | | Relative -> Bool.False |
---|
1402 | | Addr11 -> Bool.False |
---|
1403 | | Addr16 -> Bool.False) |
---|
1404 | | Bit_addr -> |
---|
1405 | (match b with |
---|
1406 | | Direct -> Bool.False |
---|
1407 | | Indirect -> Bool.False |
---|
1408 | | Ext_indirect -> Bool.False |
---|
1409 | | Registr -> Bool.False |
---|
1410 | | Acc_a -> Bool.False |
---|
1411 | | Acc_b -> Bool.False |
---|
1412 | | Dptr -> Bool.False |
---|
1413 | | Data -> Bool.False |
---|
1414 | | Data16 -> Bool.False |
---|
1415 | | Acc_dptr -> Bool.False |
---|
1416 | | Acc_pc -> Bool.False |
---|
1417 | | Ext_indirect_dptr -> Bool.False |
---|
1418 | | Indirect_dptr -> Bool.False |
---|
1419 | | Carry -> Bool.False |
---|
1420 | | Bit_addr -> Bool.True |
---|
1421 | | N_bit_addr -> Bool.False |
---|
1422 | | Relative -> Bool.False |
---|
1423 | | Addr11 -> Bool.False |
---|
1424 | | Addr16 -> Bool.False) |
---|
1425 | | N_bit_addr -> |
---|
1426 | (match b with |
---|
1427 | | Direct -> Bool.False |
---|
1428 | | Indirect -> Bool.False |
---|
1429 | | Ext_indirect -> Bool.False |
---|
1430 | | Registr -> Bool.False |
---|
1431 | | Acc_a -> Bool.False |
---|
1432 | | Acc_b -> Bool.False |
---|
1433 | | Dptr -> Bool.False |
---|
1434 | | Data -> Bool.False |
---|
1435 | | Data16 -> Bool.False |
---|
1436 | | Acc_dptr -> Bool.False |
---|
1437 | | Acc_pc -> Bool.False |
---|
1438 | | Ext_indirect_dptr -> Bool.False |
---|
1439 | | Indirect_dptr -> Bool.False |
---|
1440 | | Carry -> Bool.False |
---|
1441 | | Bit_addr -> Bool.False |
---|
1442 | | N_bit_addr -> Bool.True |
---|
1443 | | Relative -> Bool.False |
---|
1444 | | Addr11 -> Bool.False |
---|
1445 | | Addr16 -> Bool.False) |
---|
1446 | | Relative -> |
---|
1447 | (match b with |
---|
1448 | | Direct -> Bool.False |
---|
1449 | | Indirect -> Bool.False |
---|
1450 | | Ext_indirect -> Bool.False |
---|
1451 | | Registr -> Bool.False |
---|
1452 | | Acc_a -> Bool.False |
---|
1453 | | Acc_b -> Bool.False |
---|
1454 | | Dptr -> Bool.False |
---|
1455 | | Data -> Bool.False |
---|
1456 | | Data16 -> Bool.False |
---|
1457 | | Acc_dptr -> Bool.False |
---|
1458 | | Acc_pc -> Bool.False |
---|
1459 | | Ext_indirect_dptr -> Bool.False |
---|
1460 | | Indirect_dptr -> Bool.False |
---|
1461 | | Carry -> Bool.False |
---|
1462 | | Bit_addr -> Bool.False |
---|
1463 | | N_bit_addr -> Bool.False |
---|
1464 | | Relative -> Bool.True |
---|
1465 | | Addr11 -> Bool.False |
---|
1466 | | Addr16 -> Bool.False) |
---|
1467 | | Addr11 -> |
---|
1468 | (match b with |
---|
1469 | | Direct -> Bool.False |
---|
1470 | | Indirect -> Bool.False |
---|
1471 | | Ext_indirect -> Bool.False |
---|
1472 | | Registr -> Bool.False |
---|
1473 | | Acc_a -> Bool.False |
---|
1474 | | Acc_b -> Bool.False |
---|
1475 | | Dptr -> Bool.False |
---|
1476 | | Data -> Bool.False |
---|
1477 | | Data16 -> Bool.False |
---|
1478 | | Acc_dptr -> Bool.False |
---|
1479 | | Acc_pc -> Bool.False |
---|
1480 | | Ext_indirect_dptr -> Bool.False |
---|
1481 | | Indirect_dptr -> Bool.False |
---|
1482 | | Carry -> Bool.False |
---|
1483 | | Bit_addr -> Bool.False |
---|
1484 | | N_bit_addr -> Bool.False |
---|
1485 | | Relative -> Bool.False |
---|
1486 | | Addr11 -> Bool.True |
---|
1487 | | Addr16 -> Bool.False) |
---|
1488 | | Addr16 -> |
---|
1489 | (match b with |
---|
1490 | | Direct -> Bool.False |
---|
1491 | | Indirect -> Bool.False |
---|
1492 | | Ext_indirect -> Bool.False |
---|
1493 | | Registr -> Bool.False |
---|
1494 | | Acc_a -> Bool.False |
---|
1495 | | Acc_b -> Bool.False |
---|
1496 | | Dptr -> Bool.False |
---|
1497 | | Data -> Bool.False |
---|
1498 | | Data16 -> Bool.False |
---|
1499 | | Acc_dptr -> Bool.False |
---|
1500 | | Acc_pc -> Bool.False |
---|
1501 | | Ext_indirect_dptr -> Bool.False |
---|
1502 | | Indirect_dptr -> Bool.False |
---|
1503 | | Carry -> Bool.False |
---|
1504 | | Bit_addr -> Bool.False |
---|
1505 | | N_bit_addr -> Bool.False |
---|
1506 | | Relative -> Bool.False |
---|
1507 | | Addr11 -> Bool.False |
---|
1508 | | Addr16 -> Bool.True) |
---|
1509 | |
---|
1510 | type member_addressing_mode_tag = __ |
---|
1511 | |
---|
1512 | (** val is_a : addressing_mode_tag -> addressing_mode -> Bool.bool **) |
---|
1513 | let rec is_a d a = |
---|
1514 | match d with |
---|
1515 | | Direct -> |
---|
1516 | (match a with |
---|
1517 | | DIRECT x -> Bool.True |
---|
1518 | | INDIRECT x -> Bool.False |
---|
1519 | | EXT_INDIRECT x -> Bool.False |
---|
1520 | | REGISTER x -> Bool.False |
---|
1521 | | ACC_A -> Bool.False |
---|
1522 | | ACC_B -> Bool.False |
---|
1523 | | DPTR -> Bool.False |
---|
1524 | | DATA x -> Bool.False |
---|
1525 | | DATA16 x -> Bool.False |
---|
1526 | | ACC_DPTR -> Bool.False |
---|
1527 | | ACC_PC -> Bool.False |
---|
1528 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
1529 | | INDIRECT_DPTR -> Bool.False |
---|
1530 | | CARRY -> Bool.False |
---|
1531 | | BIT_ADDR x -> Bool.False |
---|
1532 | | N_BIT_ADDR x -> Bool.False |
---|
1533 | | RELATIVE x -> Bool.False |
---|
1534 | | ADDR11 x -> Bool.False |
---|
1535 | | ADDR16 x -> Bool.False) |
---|
1536 | | Indirect -> |
---|
1537 | (match a with |
---|
1538 | | DIRECT x -> Bool.False |
---|
1539 | | INDIRECT x -> Bool.True |
---|
1540 | | EXT_INDIRECT x -> Bool.False |
---|
1541 | | REGISTER x -> Bool.False |
---|
1542 | | ACC_A -> Bool.False |
---|
1543 | | ACC_B -> Bool.False |
---|
1544 | | DPTR -> Bool.False |
---|
1545 | | DATA x -> Bool.False |
---|
1546 | | DATA16 x -> Bool.False |
---|
1547 | | ACC_DPTR -> Bool.False |
---|
1548 | | ACC_PC -> Bool.False |
---|
1549 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
1550 | | INDIRECT_DPTR -> Bool.False |
---|
1551 | | CARRY -> Bool.False |
---|
1552 | | BIT_ADDR x -> Bool.False |
---|
1553 | | N_BIT_ADDR x -> Bool.False |
---|
1554 | | RELATIVE x -> Bool.False |
---|
1555 | | ADDR11 x -> Bool.False |
---|
1556 | | ADDR16 x -> Bool.False) |
---|
1557 | | Ext_indirect -> |
---|
1558 | (match a with |
---|
1559 | | DIRECT x -> Bool.False |
---|
1560 | | INDIRECT x -> Bool.False |
---|
1561 | | EXT_INDIRECT x -> Bool.True |
---|
1562 | | REGISTER x -> Bool.False |
---|
1563 | | ACC_A -> Bool.False |
---|
1564 | | ACC_B -> Bool.False |
---|
1565 | | DPTR -> Bool.False |
---|
1566 | | DATA x -> Bool.False |
---|
1567 | | DATA16 x -> Bool.False |
---|
1568 | | ACC_DPTR -> Bool.False |
---|
1569 | | ACC_PC -> Bool.False |
---|
1570 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
1571 | | INDIRECT_DPTR -> Bool.False |
---|
1572 | | CARRY -> Bool.False |
---|
1573 | | BIT_ADDR x -> Bool.False |
---|
1574 | | N_BIT_ADDR x -> Bool.False |
---|
1575 | | RELATIVE x -> Bool.False |
---|
1576 | | ADDR11 x -> Bool.False |
---|
1577 | | ADDR16 x -> Bool.False) |
---|
1578 | | Registr -> |
---|
1579 | (match a with |
---|
1580 | | DIRECT x -> Bool.False |
---|
1581 | | INDIRECT x -> Bool.False |
---|
1582 | | EXT_INDIRECT x -> Bool.False |
---|
1583 | | REGISTER x -> Bool.True |
---|
1584 | | ACC_A -> Bool.False |
---|
1585 | | ACC_B -> Bool.False |
---|
1586 | | DPTR -> Bool.False |
---|
1587 | | DATA x -> Bool.False |
---|
1588 | | DATA16 x -> Bool.False |
---|
1589 | | ACC_DPTR -> Bool.False |
---|
1590 | | ACC_PC -> Bool.False |
---|
1591 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
1592 | | INDIRECT_DPTR -> Bool.False |
---|
1593 | | CARRY -> Bool.False |
---|
1594 | | BIT_ADDR x -> Bool.False |
---|
1595 | | N_BIT_ADDR x -> Bool.False |
---|
1596 | | RELATIVE x -> Bool.False |
---|
1597 | | ADDR11 x -> Bool.False |
---|
1598 | | ADDR16 x -> Bool.False) |
---|
1599 | | Acc_a -> |
---|
1600 | (match a with |
---|
1601 | | DIRECT x -> Bool.False |
---|
1602 | | INDIRECT x -> Bool.False |
---|
1603 | | EXT_INDIRECT x -> Bool.False |
---|
1604 | | REGISTER x -> Bool.False |
---|
1605 | | ACC_A -> Bool.True |
---|
1606 | | ACC_B -> Bool.False |
---|
1607 | | DPTR -> Bool.False |
---|
1608 | | DATA x -> Bool.False |
---|
1609 | | DATA16 x -> Bool.False |
---|
1610 | | ACC_DPTR -> Bool.False |
---|
1611 | | ACC_PC -> Bool.False |
---|
1612 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
1613 | | INDIRECT_DPTR -> Bool.False |
---|
1614 | | CARRY -> Bool.False |
---|
1615 | | BIT_ADDR x -> Bool.False |
---|
1616 | | N_BIT_ADDR x -> Bool.False |
---|
1617 | | RELATIVE x -> Bool.False |
---|
1618 | | ADDR11 x -> Bool.False |
---|
1619 | | ADDR16 x -> Bool.False) |
---|
1620 | | Acc_b -> |
---|
1621 | (match a with |
---|
1622 | | DIRECT x -> Bool.False |
---|
1623 | | INDIRECT x -> Bool.False |
---|
1624 | | EXT_INDIRECT x -> Bool.False |
---|
1625 | | REGISTER x -> Bool.False |
---|
1626 | | ACC_A -> Bool.False |
---|
1627 | | ACC_B -> Bool.True |
---|
1628 | | DPTR -> Bool.False |
---|
1629 | | DATA x -> Bool.False |
---|
1630 | | DATA16 x -> Bool.False |
---|
1631 | | ACC_DPTR -> Bool.False |
---|
1632 | | ACC_PC -> Bool.False |
---|
1633 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
1634 | | INDIRECT_DPTR -> Bool.False |
---|
1635 | | CARRY -> Bool.False |
---|
1636 | | BIT_ADDR x -> Bool.False |
---|
1637 | | N_BIT_ADDR x -> Bool.False |
---|
1638 | | RELATIVE x -> Bool.False |
---|
1639 | | ADDR11 x -> Bool.False |
---|
1640 | | ADDR16 x -> Bool.False) |
---|
1641 | | Dptr -> |
---|
1642 | (match a with |
---|
1643 | | DIRECT x -> Bool.False |
---|
1644 | | INDIRECT x -> Bool.False |
---|
1645 | | EXT_INDIRECT x -> Bool.False |
---|
1646 | | REGISTER x -> Bool.False |
---|
1647 | | ACC_A -> Bool.False |
---|
1648 | | ACC_B -> Bool.False |
---|
1649 | | DPTR -> Bool.True |
---|
1650 | | DATA x -> Bool.False |
---|
1651 | | DATA16 x -> Bool.False |
---|
1652 | | ACC_DPTR -> Bool.False |
---|
1653 | | ACC_PC -> Bool.False |
---|
1654 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
1655 | | INDIRECT_DPTR -> Bool.False |
---|
1656 | | CARRY -> Bool.False |
---|
1657 | | BIT_ADDR x -> Bool.False |
---|
1658 | | N_BIT_ADDR x -> Bool.False |
---|
1659 | | RELATIVE x -> Bool.False |
---|
1660 | | ADDR11 x -> Bool.False |
---|
1661 | | ADDR16 x -> Bool.False) |
---|
1662 | | Data -> |
---|
1663 | (match a with |
---|
1664 | | DIRECT x -> Bool.False |
---|
1665 | | INDIRECT x -> Bool.False |
---|
1666 | | EXT_INDIRECT x -> Bool.False |
---|
1667 | | REGISTER x -> Bool.False |
---|
1668 | | ACC_A -> Bool.False |
---|
1669 | | ACC_B -> Bool.False |
---|
1670 | | DPTR -> Bool.False |
---|
1671 | | DATA x -> Bool.True |
---|
1672 | | DATA16 x -> Bool.False |
---|
1673 | | ACC_DPTR -> Bool.False |
---|
1674 | | ACC_PC -> Bool.False |
---|
1675 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
1676 | | INDIRECT_DPTR -> Bool.False |
---|
1677 | | CARRY -> Bool.False |
---|
1678 | | BIT_ADDR x -> Bool.False |
---|
1679 | | N_BIT_ADDR x -> Bool.False |
---|
1680 | | RELATIVE x -> Bool.False |
---|
1681 | | ADDR11 x -> Bool.False |
---|
1682 | | ADDR16 x -> Bool.False) |
---|
1683 | | Data16 -> |
---|
1684 | (match a with |
---|
1685 | | DIRECT x -> Bool.False |
---|
1686 | | INDIRECT x -> Bool.False |
---|
1687 | | EXT_INDIRECT x -> Bool.False |
---|
1688 | | REGISTER x -> Bool.False |
---|
1689 | | ACC_A -> Bool.False |
---|
1690 | | ACC_B -> Bool.False |
---|
1691 | | DPTR -> Bool.False |
---|
1692 | | DATA x -> Bool.False |
---|
1693 | | DATA16 x -> Bool.True |
---|
1694 | | ACC_DPTR -> Bool.False |
---|
1695 | | ACC_PC -> Bool.False |
---|
1696 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
1697 | | INDIRECT_DPTR -> Bool.False |
---|
1698 | | CARRY -> Bool.False |
---|
1699 | | BIT_ADDR x -> Bool.False |
---|
1700 | | N_BIT_ADDR x -> Bool.False |
---|
1701 | | RELATIVE x -> Bool.False |
---|
1702 | | ADDR11 x -> Bool.False |
---|
1703 | | ADDR16 x -> Bool.False) |
---|
1704 | | Acc_dptr -> |
---|
1705 | (match a with |
---|
1706 | | DIRECT x -> Bool.False |
---|
1707 | | INDIRECT x -> Bool.False |
---|
1708 | | EXT_INDIRECT x -> Bool.False |
---|
1709 | | REGISTER x -> Bool.False |
---|
1710 | | ACC_A -> Bool.False |
---|
1711 | | ACC_B -> Bool.False |
---|
1712 | | DPTR -> Bool.False |
---|
1713 | | DATA x -> Bool.False |
---|
1714 | | DATA16 x -> Bool.False |
---|
1715 | | ACC_DPTR -> Bool.True |
---|
1716 | | ACC_PC -> Bool.False |
---|
1717 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
1718 | | INDIRECT_DPTR -> Bool.False |
---|
1719 | | CARRY -> Bool.False |
---|
1720 | | BIT_ADDR x -> Bool.False |
---|
1721 | | N_BIT_ADDR x -> Bool.False |
---|
1722 | | RELATIVE x -> Bool.False |
---|
1723 | | ADDR11 x -> Bool.False |
---|
1724 | | ADDR16 x -> Bool.False) |
---|
1725 | | Acc_pc -> |
---|
1726 | (match a with |
---|
1727 | | DIRECT x -> Bool.False |
---|
1728 | | INDIRECT x -> Bool.False |
---|
1729 | | EXT_INDIRECT x -> Bool.False |
---|
1730 | | REGISTER x -> Bool.False |
---|
1731 | | ACC_A -> Bool.False |
---|
1732 | | ACC_B -> Bool.False |
---|
1733 | | DPTR -> Bool.False |
---|
1734 | | DATA x -> Bool.False |
---|
1735 | | DATA16 x -> Bool.False |
---|
1736 | | ACC_DPTR -> Bool.False |
---|
1737 | | ACC_PC -> Bool.True |
---|
1738 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
1739 | | INDIRECT_DPTR -> Bool.False |
---|
1740 | | CARRY -> Bool.False |
---|
1741 | | BIT_ADDR x -> Bool.False |
---|
1742 | | N_BIT_ADDR x -> Bool.False |
---|
1743 | | RELATIVE x -> Bool.False |
---|
1744 | | ADDR11 x -> Bool.False |
---|
1745 | | ADDR16 x -> Bool.False) |
---|
1746 | | Ext_indirect_dptr -> |
---|
1747 | (match a with |
---|
1748 | | DIRECT x -> Bool.False |
---|
1749 | | INDIRECT x -> Bool.False |
---|
1750 | | EXT_INDIRECT x -> Bool.False |
---|
1751 | | REGISTER x -> Bool.False |
---|
1752 | | ACC_A -> Bool.False |
---|
1753 | | ACC_B -> Bool.False |
---|
1754 | | DPTR -> Bool.False |
---|
1755 | | DATA x -> Bool.False |
---|
1756 | | DATA16 x -> Bool.False |
---|
1757 | | ACC_DPTR -> Bool.False |
---|
1758 | | ACC_PC -> Bool.False |
---|
1759 | | EXT_INDIRECT_DPTR -> Bool.True |
---|
1760 | | INDIRECT_DPTR -> Bool.False |
---|
1761 | | CARRY -> Bool.False |
---|
1762 | | BIT_ADDR x -> Bool.False |
---|
1763 | | N_BIT_ADDR x -> Bool.False |
---|
1764 | | RELATIVE x -> Bool.False |
---|
1765 | | ADDR11 x -> Bool.False |
---|
1766 | | ADDR16 x -> Bool.False) |
---|
1767 | | Indirect_dptr -> |
---|
1768 | (match a with |
---|
1769 | | DIRECT x -> Bool.False |
---|
1770 | | INDIRECT x -> Bool.False |
---|
1771 | | EXT_INDIRECT x -> Bool.False |
---|
1772 | | REGISTER x -> Bool.False |
---|
1773 | | ACC_A -> Bool.False |
---|
1774 | | ACC_B -> Bool.False |
---|
1775 | | DPTR -> Bool.False |
---|
1776 | | DATA x -> Bool.False |
---|
1777 | | DATA16 x -> Bool.False |
---|
1778 | | ACC_DPTR -> Bool.False |
---|
1779 | | ACC_PC -> Bool.False |
---|
1780 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
1781 | | INDIRECT_DPTR -> Bool.True |
---|
1782 | | CARRY -> Bool.False |
---|
1783 | | BIT_ADDR x -> Bool.False |
---|
1784 | | N_BIT_ADDR x -> Bool.False |
---|
1785 | | RELATIVE x -> Bool.False |
---|
1786 | | ADDR11 x -> Bool.False |
---|
1787 | | ADDR16 x -> Bool.False) |
---|
1788 | | Carry -> |
---|
1789 | (match a with |
---|
1790 | | DIRECT x -> Bool.False |
---|
1791 | | INDIRECT x -> Bool.False |
---|
1792 | | EXT_INDIRECT x -> Bool.False |
---|
1793 | | REGISTER x -> Bool.False |
---|
1794 | | ACC_A -> Bool.False |
---|
1795 | | ACC_B -> Bool.False |
---|
1796 | | DPTR -> Bool.False |
---|
1797 | | DATA x -> Bool.False |
---|
1798 | | DATA16 x -> Bool.False |
---|
1799 | | ACC_DPTR -> Bool.False |
---|
1800 | | ACC_PC -> Bool.False |
---|
1801 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
1802 | | INDIRECT_DPTR -> Bool.False |
---|
1803 | | CARRY -> Bool.True |
---|
1804 | | BIT_ADDR x -> Bool.False |
---|
1805 | | N_BIT_ADDR x -> Bool.False |
---|
1806 | | RELATIVE x -> Bool.False |
---|
1807 | | ADDR11 x -> Bool.False |
---|
1808 | | ADDR16 x -> Bool.False) |
---|
1809 | | Bit_addr -> |
---|
1810 | (match a with |
---|
1811 | | DIRECT x -> Bool.False |
---|
1812 | | INDIRECT x -> Bool.False |
---|
1813 | | EXT_INDIRECT x -> Bool.False |
---|
1814 | | REGISTER x -> Bool.False |
---|
1815 | | ACC_A -> Bool.False |
---|
1816 | | ACC_B -> Bool.False |
---|
1817 | | DPTR -> Bool.False |
---|
1818 | | DATA x -> Bool.False |
---|
1819 | | DATA16 x -> Bool.False |
---|
1820 | | ACC_DPTR -> Bool.False |
---|
1821 | | ACC_PC -> Bool.False |
---|
1822 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
1823 | | INDIRECT_DPTR -> Bool.False |
---|
1824 | | CARRY -> Bool.False |
---|
1825 | | BIT_ADDR x -> Bool.True |
---|
1826 | | N_BIT_ADDR x -> Bool.False |
---|
1827 | | RELATIVE x -> Bool.False |
---|
1828 | | ADDR11 x -> Bool.False |
---|
1829 | | ADDR16 x -> Bool.False) |
---|
1830 | | N_bit_addr -> |
---|
1831 | (match a with |
---|
1832 | | DIRECT x -> Bool.False |
---|
1833 | | INDIRECT x -> Bool.False |
---|
1834 | | EXT_INDIRECT x -> Bool.False |
---|
1835 | | REGISTER x -> Bool.False |
---|
1836 | | ACC_A -> Bool.False |
---|
1837 | | ACC_B -> Bool.False |
---|
1838 | | DPTR -> Bool.False |
---|
1839 | | DATA x -> Bool.False |
---|
1840 | | DATA16 x -> Bool.False |
---|
1841 | | ACC_DPTR -> Bool.False |
---|
1842 | | ACC_PC -> Bool.False |
---|
1843 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
1844 | | INDIRECT_DPTR -> Bool.False |
---|
1845 | | CARRY -> Bool.False |
---|
1846 | | BIT_ADDR x -> Bool.False |
---|
1847 | | N_BIT_ADDR x -> Bool.True |
---|
1848 | | RELATIVE x -> Bool.False |
---|
1849 | | ADDR11 x -> Bool.False |
---|
1850 | | ADDR16 x -> Bool.False) |
---|
1851 | | Relative -> |
---|
1852 | (match a with |
---|
1853 | | DIRECT x -> Bool.False |
---|
1854 | | INDIRECT x -> Bool.False |
---|
1855 | | EXT_INDIRECT x -> Bool.False |
---|
1856 | | REGISTER x -> Bool.False |
---|
1857 | | ACC_A -> Bool.False |
---|
1858 | | ACC_B -> Bool.False |
---|
1859 | | DPTR -> Bool.False |
---|
1860 | | DATA x -> Bool.False |
---|
1861 | | DATA16 x -> Bool.False |
---|
1862 | | ACC_DPTR -> Bool.False |
---|
1863 | | ACC_PC -> Bool.False |
---|
1864 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
1865 | | INDIRECT_DPTR -> Bool.False |
---|
1866 | | CARRY -> Bool.False |
---|
1867 | | BIT_ADDR x -> Bool.False |
---|
1868 | | N_BIT_ADDR x -> Bool.False |
---|
1869 | | RELATIVE x -> Bool.True |
---|
1870 | | ADDR11 x -> Bool.False |
---|
1871 | | ADDR16 x -> Bool.False) |
---|
1872 | | Addr11 -> |
---|
1873 | (match a with |
---|
1874 | | DIRECT x -> Bool.False |
---|
1875 | | INDIRECT x -> Bool.False |
---|
1876 | | EXT_INDIRECT x -> Bool.False |
---|
1877 | | REGISTER x -> Bool.False |
---|
1878 | | ACC_A -> Bool.False |
---|
1879 | | ACC_B -> Bool.False |
---|
1880 | | DPTR -> Bool.False |
---|
1881 | | DATA x -> Bool.False |
---|
1882 | | DATA16 x -> Bool.False |
---|
1883 | | ACC_DPTR -> Bool.False |
---|
1884 | | ACC_PC -> Bool.False |
---|
1885 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
1886 | | INDIRECT_DPTR -> Bool.False |
---|
1887 | | CARRY -> Bool.False |
---|
1888 | | BIT_ADDR x -> Bool.False |
---|
1889 | | N_BIT_ADDR x -> Bool.False |
---|
1890 | | RELATIVE x -> Bool.False |
---|
1891 | | ADDR11 x -> Bool.True |
---|
1892 | | ADDR16 x -> Bool.False) |
---|
1893 | | Addr16 -> |
---|
1894 | (match a with |
---|
1895 | | DIRECT x -> Bool.False |
---|
1896 | | INDIRECT x -> Bool.False |
---|
1897 | | EXT_INDIRECT x -> Bool.False |
---|
1898 | | REGISTER x -> Bool.False |
---|
1899 | | ACC_A -> Bool.False |
---|
1900 | | ACC_B -> Bool.False |
---|
1901 | | DPTR -> Bool.False |
---|
1902 | | DATA x -> Bool.False |
---|
1903 | | DATA16 x -> Bool.False |
---|
1904 | | ACC_DPTR -> Bool.False |
---|
1905 | | ACC_PC -> Bool.False |
---|
1906 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
1907 | | INDIRECT_DPTR -> Bool.False |
---|
1908 | | CARRY -> Bool.False |
---|
1909 | | BIT_ADDR x -> Bool.False |
---|
1910 | | N_BIT_ADDR x -> Bool.False |
---|
1911 | | RELATIVE x -> Bool.False |
---|
1912 | | ADDR11 x -> Bool.False |
---|
1913 | | ADDR16 x -> Bool.True) |
---|
1914 | |
---|
1915 | (** val is_in : |
---|
1916 | Nat.nat -> addressing_mode_tag Vector.vector -> addressing_mode -> |
---|
1917 | Bool.bool **) |
---|
1918 | let rec is_in n l a = |
---|
1919 | match l with |
---|
1920 | | Vector.VEmpty -> Bool.False |
---|
1921 | | Vector.VCons (m, he, tl) -> Bool.orb (is_a he a) (is_in m tl a) |
---|
1922 | |
---|
1923 | type subaddressing_mode = |
---|
1924 | addressing_mode |
---|
1925 | (* singleton inductive, whose constructor was mk_subaddressing_mode *) |
---|
1926 | |
---|
1927 | (** val subaddressing_mode_rect_Type4 : |
---|
1928 | Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ -> |
---|
1929 | 'a1) -> subaddressing_mode -> 'a1 **) |
---|
1930 | let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_19349 = |
---|
1931 | let subaddressing_modeel = x_19349 in |
---|
1932 | h_mk_subaddressing_mode subaddressing_modeel __ |
---|
1933 | |
---|
1934 | (** val subaddressing_mode_rect_Type5 : |
---|
1935 | Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ -> |
---|
1936 | 'a1) -> subaddressing_mode -> 'a1 **) |
---|
1937 | let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_19351 = |
---|
1938 | let subaddressing_modeel = x_19351 in |
---|
1939 | h_mk_subaddressing_mode subaddressing_modeel __ |
---|
1940 | |
---|
1941 | (** val subaddressing_mode_rect_Type3 : |
---|
1942 | Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ -> |
---|
1943 | 'a1) -> subaddressing_mode -> 'a1 **) |
---|
1944 | let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_19353 = |
---|
1945 | let subaddressing_modeel = x_19353 in |
---|
1946 | h_mk_subaddressing_mode subaddressing_modeel __ |
---|
1947 | |
---|
1948 | (** val subaddressing_mode_rect_Type2 : |
---|
1949 | Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ -> |
---|
1950 | 'a1) -> subaddressing_mode -> 'a1 **) |
---|
1951 | let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_19355 = |
---|
1952 | let subaddressing_modeel = x_19355 in |
---|
1953 | h_mk_subaddressing_mode subaddressing_modeel __ |
---|
1954 | |
---|
1955 | (** val subaddressing_mode_rect_Type1 : |
---|
1956 | Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ -> |
---|
1957 | 'a1) -> subaddressing_mode -> 'a1 **) |
---|
1958 | let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_19357 = |
---|
1959 | let subaddressing_modeel = x_19357 in |
---|
1960 | h_mk_subaddressing_mode subaddressing_modeel __ |
---|
1961 | |
---|
1962 | (** val subaddressing_mode_rect_Type0 : |
---|
1963 | Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ -> |
---|
1964 | 'a1) -> subaddressing_mode -> 'a1 **) |
---|
1965 | let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_19359 = |
---|
1966 | let subaddressing_modeel = x_19359 in |
---|
1967 | h_mk_subaddressing_mode subaddressing_modeel __ |
---|
1968 | |
---|
1969 | (** val subaddressing_modeel : |
---|
1970 | Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode -> |
---|
1971 | addressing_mode **) |
---|
1972 | let rec subaddressing_modeel n l xxx = |
---|
1973 | let yyy = xxx in yyy |
---|
1974 | |
---|
1975 | (** val subaddressing_mode_inv_rect_Type4 : |
---|
1976 | Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode -> |
---|
1977 | (addressing_mode -> __ -> __ -> 'a1) -> 'a1 **) |
---|
1978 | let subaddressing_mode_inv_rect_Type4 x1 x2 hterm h1 = |
---|
1979 | let hcut = subaddressing_mode_rect_Type4 x1 x2 h1 hterm in hcut __ |
---|
1980 | |
---|
1981 | (** val subaddressing_mode_inv_rect_Type3 : |
---|
1982 | Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode -> |
---|
1983 | (addressing_mode -> __ -> __ -> 'a1) -> 'a1 **) |
---|
1984 | let subaddressing_mode_inv_rect_Type3 x1 x2 hterm h1 = |
---|
1985 | let hcut = subaddressing_mode_rect_Type3 x1 x2 h1 hterm in hcut __ |
---|
1986 | |
---|
1987 | (** val subaddressing_mode_inv_rect_Type2 : |
---|
1988 | Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode -> |
---|
1989 | (addressing_mode -> __ -> __ -> 'a1) -> 'a1 **) |
---|
1990 | let subaddressing_mode_inv_rect_Type2 x1 x2 hterm h1 = |
---|
1991 | let hcut = subaddressing_mode_rect_Type2 x1 x2 h1 hterm in hcut __ |
---|
1992 | |
---|
1993 | (** val subaddressing_mode_inv_rect_Type1 : |
---|
1994 | Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode -> |
---|
1995 | (addressing_mode -> __ -> __ -> 'a1) -> 'a1 **) |
---|
1996 | let subaddressing_mode_inv_rect_Type1 x1 x2 hterm h1 = |
---|
1997 | let hcut = subaddressing_mode_rect_Type1 x1 x2 h1 hterm in hcut __ |
---|
1998 | |
---|
1999 | (** val subaddressing_mode_inv_rect_Type0 : |
---|
2000 | Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode -> |
---|
2001 | (addressing_mode -> __ -> __ -> 'a1) -> 'a1 **) |
---|
2002 | let subaddressing_mode_inv_rect_Type0 x1 x2 hterm h1 = |
---|
2003 | let hcut = subaddressing_mode_rect_Type0 x1 x2 h1 hterm in hcut __ |
---|
2004 | |
---|
2005 | (** val subaddressing_mode_discr : |
---|
2006 | Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode -> |
---|
2007 | subaddressing_mode -> __ **) |
---|
2008 | let subaddressing_mode_discr a1 a2 x y = |
---|
2009 | Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y |
---|
2010 | |
---|
2011 | (** val subaddressing_mode_jmdiscr : |
---|
2012 | Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode -> |
---|
2013 | subaddressing_mode -> __ **) |
---|
2014 | let subaddressing_mode_jmdiscr a1 a2 x y = |
---|
2015 | Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y |
---|
2016 | |
---|
2017 | (** val dpi1__o__subaddressing_modeel__o__inject : |
---|
2018 | Nat.nat -> addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) |
---|
2019 | Types.dPair -> addressing_mode Types.sig0 **) |
---|
2020 | let dpi1__o__subaddressing_modeel__o__inject x1 x2 x4 = |
---|
2021 | subaddressing_modeel x1 x2 x4.Types.dpi1 |
---|
2022 | |
---|
2023 | (** val eject__o__subaddressing_modeel__o__inject : |
---|
2024 | Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode |
---|
2025 | Types.sig0 -> addressing_mode Types.sig0 **) |
---|
2026 | let eject__o__subaddressing_modeel__o__inject x1 x2 x4 = |
---|
2027 | subaddressing_modeel x1 x2 (Types.pi1 x4) |
---|
2028 | |
---|
2029 | (** val subaddressing_modeel__o__inject : |
---|
2030 | Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode -> |
---|
2031 | addressing_mode Types.sig0 **) |
---|
2032 | let subaddressing_modeel__o__inject x1 x2 x3 = |
---|
2033 | subaddressing_modeel x1 x2 x3 |
---|
2034 | |
---|
2035 | (** val dpi1__o__subaddressing_modeel : |
---|
2036 | Nat.nat -> addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) |
---|
2037 | Types.dPair -> addressing_mode **) |
---|
2038 | let dpi1__o__subaddressing_modeel x0 x1 x3 = |
---|
2039 | subaddressing_modeel x0 x1 x3.Types.dpi1 |
---|
2040 | |
---|
2041 | (** val eject__o__subaddressing_modeel : |
---|
2042 | Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode |
---|
2043 | Types.sig0 -> addressing_mode **) |
---|
2044 | let eject__o__subaddressing_modeel x0 x1 x3 = |
---|
2045 | subaddressing_modeel x0 x1 (Types.pi1 x3) |
---|
2046 | |
---|
2047 | type subaddressing_mode_elim_type = __ |
---|
2048 | |
---|
2049 | type 'a preinstruction = |
---|
2050 | | ADD of subaddressing_mode * subaddressing_mode |
---|
2051 | | ADDC of subaddressing_mode * subaddressing_mode |
---|
2052 | | SUBB of subaddressing_mode * subaddressing_mode |
---|
2053 | | INC of subaddressing_mode |
---|
2054 | | DEC of subaddressing_mode |
---|
2055 | | MUL of subaddressing_mode * subaddressing_mode |
---|
2056 | | DIV of subaddressing_mode * subaddressing_mode |
---|
2057 | | DA of subaddressing_mode |
---|
2058 | | JC of 'a |
---|
2059 | | JNC of 'a |
---|
2060 | | JB of subaddressing_mode * 'a |
---|
2061 | | JNB of subaddressing_mode * 'a |
---|
2062 | | JBC of subaddressing_mode * 'a |
---|
2063 | | JZ of 'a |
---|
2064 | | JNZ of 'a |
---|
2065 | | CJNE of ((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2066 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum * |
---|
2067 | 'a |
---|
2068 | | DJNZ of subaddressing_mode * 'a |
---|
2069 | | ANL of (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2070 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2071 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum |
---|
2072 | | ORL of (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2073 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2074 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum |
---|
2075 | | XRL of ((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2076 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum |
---|
2077 | | CLR of subaddressing_mode |
---|
2078 | | CPL of subaddressing_mode |
---|
2079 | | RL of subaddressing_mode |
---|
2080 | | RLC of subaddressing_mode |
---|
2081 | | RR of subaddressing_mode |
---|
2082 | | RRC of subaddressing_mode |
---|
2083 | | SWAP of subaddressing_mode |
---|
2084 | | MOV of ((((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2085 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2086 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2087 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2088 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2089 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum |
---|
2090 | | MOVX of ((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2091 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum |
---|
2092 | | SETB of subaddressing_mode |
---|
2093 | | PUSH of subaddressing_mode |
---|
2094 | | POP of subaddressing_mode |
---|
2095 | | XCH of subaddressing_mode * subaddressing_mode |
---|
2096 | | XCHD of subaddressing_mode * subaddressing_mode |
---|
2097 | | RET |
---|
2098 | | RETI |
---|
2099 | | NOP |
---|
2100 | | JMP of subaddressing_mode |
---|
2101 | |
---|
2102 | (** val preinstruction_rect_Type4 : |
---|
2103 | (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode |
---|
2104 | -> subaddressing_mode -> 'a2) -> (subaddressing_mode -> |
---|
2105 | subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2106 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode |
---|
2107 | -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> |
---|
2108 | (subaddressing_mode -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) -> |
---|
2109 | (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) |
---|
2110 | -> (subaddressing_mode -> 'a1 -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) -> |
---|
2111 | (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2112 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a1 -> |
---|
2113 | 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) -> ((((subaddressing_mode, |
---|
2114 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2115 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2116 | Types.prod) Types.sum -> 'a2) -> ((((subaddressing_mode, |
---|
2117 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2118 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2119 | Types.prod) Types.sum -> 'a2) -> (((subaddressing_mode, |
---|
2120 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2121 | Types.prod) Types.sum -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2122 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2123 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2124 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2125 | (((((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2126 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2127 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2128 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2129 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2130 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) -> |
---|
2131 | (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2132 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) -> |
---|
2133 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2134 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode |
---|
2135 | -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 -> |
---|
2136 | 'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **) |
---|
2137 | let rec preinstruction_rect_Type4 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function |
---|
2138 | | ADD (x_19461, x_19460) -> h_ADD x_19461 x_19460 |
---|
2139 | | ADDC (x_19463, x_19462) -> h_ADDC x_19463 x_19462 |
---|
2140 | | SUBB (x_19465, x_19464) -> h_SUBB x_19465 x_19464 |
---|
2141 | | INC x_19466 -> h_INC x_19466 |
---|
2142 | | DEC x_19467 -> h_DEC x_19467 |
---|
2143 | | MUL (x_19469, x_19468) -> h_MUL x_19469 x_19468 |
---|
2144 | | DIV (x_19471, x_19470) -> h_DIV x_19471 x_19470 |
---|
2145 | | DA x_19472 -> h_DA x_19472 |
---|
2146 | | JC x_19473 -> h_JC x_19473 |
---|
2147 | | JNC x_19474 -> h_JNC x_19474 |
---|
2148 | | JB (x_19476, x_19475) -> h_JB x_19476 x_19475 |
---|
2149 | | JNB (x_19478, x_19477) -> h_JNB x_19478 x_19477 |
---|
2150 | | JBC (x_19480, x_19479) -> h_JBC x_19480 x_19479 |
---|
2151 | | JZ x_19481 -> h_JZ x_19481 |
---|
2152 | | JNZ x_19482 -> h_JNZ x_19482 |
---|
2153 | | CJNE (x_19484, x_19483) -> h_CJNE x_19484 x_19483 |
---|
2154 | | DJNZ (x_19486, x_19485) -> h_DJNZ x_19486 x_19485 |
---|
2155 | | ANL x_19487 -> h_ANL x_19487 |
---|
2156 | | ORL x_19488 -> h_ORL x_19488 |
---|
2157 | | XRL x_19489 -> h_XRL x_19489 |
---|
2158 | | CLR x_19490 -> h_CLR x_19490 |
---|
2159 | | CPL x_19491 -> h_CPL x_19491 |
---|
2160 | | RL x_19492 -> h_RL x_19492 |
---|
2161 | | RLC x_19493 -> h_RLC x_19493 |
---|
2162 | | RR x_19494 -> h_RR x_19494 |
---|
2163 | | RRC x_19495 -> h_RRC x_19495 |
---|
2164 | | SWAP x_19496 -> h_SWAP x_19496 |
---|
2165 | | MOV x_19497 -> h_MOV x_19497 |
---|
2166 | | MOVX x_19498 -> h_MOVX x_19498 |
---|
2167 | | SETB x_19499 -> h_SETB x_19499 |
---|
2168 | | PUSH x_19500 -> h_PUSH x_19500 |
---|
2169 | | POP x_19501 -> h_POP x_19501 |
---|
2170 | | XCH (x_19503, x_19502) -> h_XCH x_19503 x_19502 |
---|
2171 | | XCHD (x_19505, x_19504) -> h_XCHD x_19505 x_19504 |
---|
2172 | | RET -> h_RET |
---|
2173 | | RETI -> h_RETI |
---|
2174 | | NOP -> h_NOP |
---|
2175 | | JMP x_19506 -> h_JMP x_19506 |
---|
2176 | |
---|
2177 | (** val preinstruction_rect_Type5 : |
---|
2178 | (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode |
---|
2179 | -> subaddressing_mode -> 'a2) -> (subaddressing_mode -> |
---|
2180 | subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2181 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode |
---|
2182 | -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> |
---|
2183 | (subaddressing_mode -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) -> |
---|
2184 | (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) |
---|
2185 | -> (subaddressing_mode -> 'a1 -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) -> |
---|
2186 | (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2187 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a1 -> |
---|
2188 | 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) -> ((((subaddressing_mode, |
---|
2189 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2190 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2191 | Types.prod) Types.sum -> 'a2) -> ((((subaddressing_mode, |
---|
2192 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2193 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2194 | Types.prod) Types.sum -> 'a2) -> (((subaddressing_mode, |
---|
2195 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2196 | Types.prod) Types.sum -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2197 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2198 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2199 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2200 | (((((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2201 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2202 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2203 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2204 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2205 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) -> |
---|
2206 | (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2207 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) -> |
---|
2208 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2209 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode |
---|
2210 | -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 -> |
---|
2211 | 'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **) |
---|
2212 | let rec preinstruction_rect_Type5 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function |
---|
2213 | | ADD (x_19547, x_19546) -> h_ADD x_19547 x_19546 |
---|
2214 | | ADDC (x_19549, x_19548) -> h_ADDC x_19549 x_19548 |
---|
2215 | | SUBB (x_19551, x_19550) -> h_SUBB x_19551 x_19550 |
---|
2216 | | INC x_19552 -> h_INC x_19552 |
---|
2217 | | DEC x_19553 -> h_DEC x_19553 |
---|
2218 | | MUL (x_19555, x_19554) -> h_MUL x_19555 x_19554 |
---|
2219 | | DIV (x_19557, x_19556) -> h_DIV x_19557 x_19556 |
---|
2220 | | DA x_19558 -> h_DA x_19558 |
---|
2221 | | JC x_19559 -> h_JC x_19559 |
---|
2222 | | JNC x_19560 -> h_JNC x_19560 |
---|
2223 | | JB (x_19562, x_19561) -> h_JB x_19562 x_19561 |
---|
2224 | | JNB (x_19564, x_19563) -> h_JNB x_19564 x_19563 |
---|
2225 | | JBC (x_19566, x_19565) -> h_JBC x_19566 x_19565 |
---|
2226 | | JZ x_19567 -> h_JZ x_19567 |
---|
2227 | | JNZ x_19568 -> h_JNZ x_19568 |
---|
2228 | | CJNE (x_19570, x_19569) -> h_CJNE x_19570 x_19569 |
---|
2229 | | DJNZ (x_19572, x_19571) -> h_DJNZ x_19572 x_19571 |
---|
2230 | | ANL x_19573 -> h_ANL x_19573 |
---|
2231 | | ORL x_19574 -> h_ORL x_19574 |
---|
2232 | | XRL x_19575 -> h_XRL x_19575 |
---|
2233 | | CLR x_19576 -> h_CLR x_19576 |
---|
2234 | | CPL x_19577 -> h_CPL x_19577 |
---|
2235 | | RL x_19578 -> h_RL x_19578 |
---|
2236 | | RLC x_19579 -> h_RLC x_19579 |
---|
2237 | | RR x_19580 -> h_RR x_19580 |
---|
2238 | | RRC x_19581 -> h_RRC x_19581 |
---|
2239 | | SWAP x_19582 -> h_SWAP x_19582 |
---|
2240 | | MOV x_19583 -> h_MOV x_19583 |
---|
2241 | | MOVX x_19584 -> h_MOVX x_19584 |
---|
2242 | | SETB x_19585 -> h_SETB x_19585 |
---|
2243 | | PUSH x_19586 -> h_PUSH x_19586 |
---|
2244 | | POP x_19587 -> h_POP x_19587 |
---|
2245 | | XCH (x_19589, x_19588) -> h_XCH x_19589 x_19588 |
---|
2246 | | XCHD (x_19591, x_19590) -> h_XCHD x_19591 x_19590 |
---|
2247 | | RET -> h_RET |
---|
2248 | | RETI -> h_RETI |
---|
2249 | | NOP -> h_NOP |
---|
2250 | | JMP x_19592 -> h_JMP x_19592 |
---|
2251 | |
---|
2252 | (** val preinstruction_rect_Type3 : |
---|
2253 | (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode |
---|
2254 | -> subaddressing_mode -> 'a2) -> (subaddressing_mode -> |
---|
2255 | subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2256 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode |
---|
2257 | -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> |
---|
2258 | (subaddressing_mode -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) -> |
---|
2259 | (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) |
---|
2260 | -> (subaddressing_mode -> 'a1 -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) -> |
---|
2261 | (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2262 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a1 -> |
---|
2263 | 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) -> ((((subaddressing_mode, |
---|
2264 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2265 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2266 | Types.prod) Types.sum -> 'a2) -> ((((subaddressing_mode, |
---|
2267 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2268 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2269 | Types.prod) Types.sum -> 'a2) -> (((subaddressing_mode, |
---|
2270 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2271 | Types.prod) Types.sum -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2272 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2273 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2274 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2275 | (((((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2276 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2277 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2278 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2279 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2280 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) -> |
---|
2281 | (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2282 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) -> |
---|
2283 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2284 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode |
---|
2285 | -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 -> |
---|
2286 | 'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **) |
---|
2287 | let rec preinstruction_rect_Type3 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function |
---|
2288 | | ADD (x_19633, x_19632) -> h_ADD x_19633 x_19632 |
---|
2289 | | ADDC (x_19635, x_19634) -> h_ADDC x_19635 x_19634 |
---|
2290 | | SUBB (x_19637, x_19636) -> h_SUBB x_19637 x_19636 |
---|
2291 | | INC x_19638 -> h_INC x_19638 |
---|
2292 | | DEC x_19639 -> h_DEC x_19639 |
---|
2293 | | MUL (x_19641, x_19640) -> h_MUL x_19641 x_19640 |
---|
2294 | | DIV (x_19643, x_19642) -> h_DIV x_19643 x_19642 |
---|
2295 | | DA x_19644 -> h_DA x_19644 |
---|
2296 | | JC x_19645 -> h_JC x_19645 |
---|
2297 | | JNC x_19646 -> h_JNC x_19646 |
---|
2298 | | JB (x_19648, x_19647) -> h_JB x_19648 x_19647 |
---|
2299 | | JNB (x_19650, x_19649) -> h_JNB x_19650 x_19649 |
---|
2300 | | JBC (x_19652, x_19651) -> h_JBC x_19652 x_19651 |
---|
2301 | | JZ x_19653 -> h_JZ x_19653 |
---|
2302 | | JNZ x_19654 -> h_JNZ x_19654 |
---|
2303 | | CJNE (x_19656, x_19655) -> h_CJNE x_19656 x_19655 |
---|
2304 | | DJNZ (x_19658, x_19657) -> h_DJNZ x_19658 x_19657 |
---|
2305 | | ANL x_19659 -> h_ANL x_19659 |
---|
2306 | | ORL x_19660 -> h_ORL x_19660 |
---|
2307 | | XRL x_19661 -> h_XRL x_19661 |
---|
2308 | | CLR x_19662 -> h_CLR x_19662 |
---|
2309 | | CPL x_19663 -> h_CPL x_19663 |
---|
2310 | | RL x_19664 -> h_RL x_19664 |
---|
2311 | | RLC x_19665 -> h_RLC x_19665 |
---|
2312 | | RR x_19666 -> h_RR x_19666 |
---|
2313 | | RRC x_19667 -> h_RRC x_19667 |
---|
2314 | | SWAP x_19668 -> h_SWAP x_19668 |
---|
2315 | | MOV x_19669 -> h_MOV x_19669 |
---|
2316 | | MOVX x_19670 -> h_MOVX x_19670 |
---|
2317 | | SETB x_19671 -> h_SETB x_19671 |
---|
2318 | | PUSH x_19672 -> h_PUSH x_19672 |
---|
2319 | | POP x_19673 -> h_POP x_19673 |
---|
2320 | | XCH (x_19675, x_19674) -> h_XCH x_19675 x_19674 |
---|
2321 | | XCHD (x_19677, x_19676) -> h_XCHD x_19677 x_19676 |
---|
2322 | | RET -> h_RET |
---|
2323 | | RETI -> h_RETI |
---|
2324 | | NOP -> h_NOP |
---|
2325 | | JMP x_19678 -> h_JMP x_19678 |
---|
2326 | |
---|
2327 | (** val preinstruction_rect_Type2 : |
---|
2328 | (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode |
---|
2329 | -> subaddressing_mode -> 'a2) -> (subaddressing_mode -> |
---|
2330 | subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2331 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode |
---|
2332 | -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> |
---|
2333 | (subaddressing_mode -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) -> |
---|
2334 | (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) |
---|
2335 | -> (subaddressing_mode -> 'a1 -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) -> |
---|
2336 | (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2337 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a1 -> |
---|
2338 | 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) -> ((((subaddressing_mode, |
---|
2339 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2340 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2341 | Types.prod) Types.sum -> 'a2) -> ((((subaddressing_mode, |
---|
2342 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2343 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2344 | Types.prod) Types.sum -> 'a2) -> (((subaddressing_mode, |
---|
2345 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2346 | Types.prod) Types.sum -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2347 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2348 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2349 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2350 | (((((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2351 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2352 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2353 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2354 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2355 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) -> |
---|
2356 | (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2357 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) -> |
---|
2358 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2359 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode |
---|
2360 | -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 -> |
---|
2361 | 'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **) |
---|
2362 | let rec preinstruction_rect_Type2 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function |
---|
2363 | | ADD (x_19719, x_19718) -> h_ADD x_19719 x_19718 |
---|
2364 | | ADDC (x_19721, x_19720) -> h_ADDC x_19721 x_19720 |
---|
2365 | | SUBB (x_19723, x_19722) -> h_SUBB x_19723 x_19722 |
---|
2366 | | INC x_19724 -> h_INC x_19724 |
---|
2367 | | DEC x_19725 -> h_DEC x_19725 |
---|
2368 | | MUL (x_19727, x_19726) -> h_MUL x_19727 x_19726 |
---|
2369 | | DIV (x_19729, x_19728) -> h_DIV x_19729 x_19728 |
---|
2370 | | DA x_19730 -> h_DA x_19730 |
---|
2371 | | JC x_19731 -> h_JC x_19731 |
---|
2372 | | JNC x_19732 -> h_JNC x_19732 |
---|
2373 | | JB (x_19734, x_19733) -> h_JB x_19734 x_19733 |
---|
2374 | | JNB (x_19736, x_19735) -> h_JNB x_19736 x_19735 |
---|
2375 | | JBC (x_19738, x_19737) -> h_JBC x_19738 x_19737 |
---|
2376 | | JZ x_19739 -> h_JZ x_19739 |
---|
2377 | | JNZ x_19740 -> h_JNZ x_19740 |
---|
2378 | | CJNE (x_19742, x_19741) -> h_CJNE x_19742 x_19741 |
---|
2379 | | DJNZ (x_19744, x_19743) -> h_DJNZ x_19744 x_19743 |
---|
2380 | | ANL x_19745 -> h_ANL x_19745 |
---|
2381 | | ORL x_19746 -> h_ORL x_19746 |
---|
2382 | | XRL x_19747 -> h_XRL x_19747 |
---|
2383 | | CLR x_19748 -> h_CLR x_19748 |
---|
2384 | | CPL x_19749 -> h_CPL x_19749 |
---|
2385 | | RL x_19750 -> h_RL x_19750 |
---|
2386 | | RLC x_19751 -> h_RLC x_19751 |
---|
2387 | | RR x_19752 -> h_RR x_19752 |
---|
2388 | | RRC x_19753 -> h_RRC x_19753 |
---|
2389 | | SWAP x_19754 -> h_SWAP x_19754 |
---|
2390 | | MOV x_19755 -> h_MOV x_19755 |
---|
2391 | | MOVX x_19756 -> h_MOVX x_19756 |
---|
2392 | | SETB x_19757 -> h_SETB x_19757 |
---|
2393 | | PUSH x_19758 -> h_PUSH x_19758 |
---|
2394 | | POP x_19759 -> h_POP x_19759 |
---|
2395 | | XCH (x_19761, x_19760) -> h_XCH x_19761 x_19760 |
---|
2396 | | XCHD (x_19763, x_19762) -> h_XCHD x_19763 x_19762 |
---|
2397 | | RET -> h_RET |
---|
2398 | | RETI -> h_RETI |
---|
2399 | | NOP -> h_NOP |
---|
2400 | | JMP x_19764 -> h_JMP x_19764 |
---|
2401 | |
---|
2402 | (** val preinstruction_rect_Type1 : |
---|
2403 | (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode |
---|
2404 | -> subaddressing_mode -> 'a2) -> (subaddressing_mode -> |
---|
2405 | subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2406 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode |
---|
2407 | -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> |
---|
2408 | (subaddressing_mode -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) -> |
---|
2409 | (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) |
---|
2410 | -> (subaddressing_mode -> 'a1 -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) -> |
---|
2411 | (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2412 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a1 -> |
---|
2413 | 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) -> ((((subaddressing_mode, |
---|
2414 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2415 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2416 | Types.prod) Types.sum -> 'a2) -> ((((subaddressing_mode, |
---|
2417 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2418 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2419 | Types.prod) Types.sum -> 'a2) -> (((subaddressing_mode, |
---|
2420 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2421 | Types.prod) Types.sum -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2422 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2423 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2424 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2425 | (((((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2426 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2427 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2428 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2429 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2430 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) -> |
---|
2431 | (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2432 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) -> |
---|
2433 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2434 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode |
---|
2435 | -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 -> |
---|
2436 | 'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **) |
---|
2437 | let rec preinstruction_rect_Type1 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function |
---|
2438 | | ADD (x_19805, x_19804) -> h_ADD x_19805 x_19804 |
---|
2439 | | ADDC (x_19807, x_19806) -> h_ADDC x_19807 x_19806 |
---|
2440 | | SUBB (x_19809, x_19808) -> h_SUBB x_19809 x_19808 |
---|
2441 | | INC x_19810 -> h_INC x_19810 |
---|
2442 | | DEC x_19811 -> h_DEC x_19811 |
---|
2443 | | MUL (x_19813, x_19812) -> h_MUL x_19813 x_19812 |
---|
2444 | | DIV (x_19815, x_19814) -> h_DIV x_19815 x_19814 |
---|
2445 | | DA x_19816 -> h_DA x_19816 |
---|
2446 | | JC x_19817 -> h_JC x_19817 |
---|
2447 | | JNC x_19818 -> h_JNC x_19818 |
---|
2448 | | JB (x_19820, x_19819) -> h_JB x_19820 x_19819 |
---|
2449 | | JNB (x_19822, x_19821) -> h_JNB x_19822 x_19821 |
---|
2450 | | JBC (x_19824, x_19823) -> h_JBC x_19824 x_19823 |
---|
2451 | | JZ x_19825 -> h_JZ x_19825 |
---|
2452 | | JNZ x_19826 -> h_JNZ x_19826 |
---|
2453 | | CJNE (x_19828, x_19827) -> h_CJNE x_19828 x_19827 |
---|
2454 | | DJNZ (x_19830, x_19829) -> h_DJNZ x_19830 x_19829 |
---|
2455 | | ANL x_19831 -> h_ANL x_19831 |
---|
2456 | | ORL x_19832 -> h_ORL x_19832 |
---|
2457 | | XRL x_19833 -> h_XRL x_19833 |
---|
2458 | | CLR x_19834 -> h_CLR x_19834 |
---|
2459 | | CPL x_19835 -> h_CPL x_19835 |
---|
2460 | | RL x_19836 -> h_RL x_19836 |
---|
2461 | | RLC x_19837 -> h_RLC x_19837 |
---|
2462 | | RR x_19838 -> h_RR x_19838 |
---|
2463 | | RRC x_19839 -> h_RRC x_19839 |
---|
2464 | | SWAP x_19840 -> h_SWAP x_19840 |
---|
2465 | | MOV x_19841 -> h_MOV x_19841 |
---|
2466 | | MOVX x_19842 -> h_MOVX x_19842 |
---|
2467 | | SETB x_19843 -> h_SETB x_19843 |
---|
2468 | | PUSH x_19844 -> h_PUSH x_19844 |
---|
2469 | | POP x_19845 -> h_POP x_19845 |
---|
2470 | | XCH (x_19847, x_19846) -> h_XCH x_19847 x_19846 |
---|
2471 | | XCHD (x_19849, x_19848) -> h_XCHD x_19849 x_19848 |
---|
2472 | | RET -> h_RET |
---|
2473 | | RETI -> h_RETI |
---|
2474 | | NOP -> h_NOP |
---|
2475 | | JMP x_19850 -> h_JMP x_19850 |
---|
2476 | |
---|
2477 | (** val preinstruction_rect_Type0 : |
---|
2478 | (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode |
---|
2479 | -> subaddressing_mode -> 'a2) -> (subaddressing_mode -> |
---|
2480 | subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2481 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode |
---|
2482 | -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> |
---|
2483 | (subaddressing_mode -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) -> |
---|
2484 | (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) |
---|
2485 | -> (subaddressing_mode -> 'a1 -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) -> |
---|
2486 | (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2487 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a1 -> |
---|
2488 | 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) -> ((((subaddressing_mode, |
---|
2489 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2490 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2491 | Types.prod) Types.sum -> 'a2) -> ((((subaddressing_mode, |
---|
2492 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2493 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2494 | Types.prod) Types.sum -> 'a2) -> (((subaddressing_mode, |
---|
2495 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2496 | Types.prod) Types.sum -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2497 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2498 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2499 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2500 | (((((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2501 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2502 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2503 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2504 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2505 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) -> |
---|
2506 | (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2507 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) -> |
---|
2508 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
2509 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode |
---|
2510 | -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 -> |
---|
2511 | 'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **) |
---|
2512 | let rec preinstruction_rect_Type0 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function |
---|
2513 | | ADD (x_19891, x_19890) -> h_ADD x_19891 x_19890 |
---|
2514 | | ADDC (x_19893, x_19892) -> h_ADDC x_19893 x_19892 |
---|
2515 | | SUBB (x_19895, x_19894) -> h_SUBB x_19895 x_19894 |
---|
2516 | | INC x_19896 -> h_INC x_19896 |
---|
2517 | | DEC x_19897 -> h_DEC x_19897 |
---|
2518 | | MUL (x_19899, x_19898) -> h_MUL x_19899 x_19898 |
---|
2519 | | DIV (x_19901, x_19900) -> h_DIV x_19901 x_19900 |
---|
2520 | | DA x_19902 -> h_DA x_19902 |
---|
2521 | | JC x_19903 -> h_JC x_19903 |
---|
2522 | | JNC x_19904 -> h_JNC x_19904 |
---|
2523 | | JB (x_19906, x_19905) -> h_JB x_19906 x_19905 |
---|
2524 | | JNB (x_19908, x_19907) -> h_JNB x_19908 x_19907 |
---|
2525 | | JBC (x_19910, x_19909) -> h_JBC x_19910 x_19909 |
---|
2526 | | JZ x_19911 -> h_JZ x_19911 |
---|
2527 | | JNZ x_19912 -> h_JNZ x_19912 |
---|
2528 | | CJNE (x_19914, x_19913) -> h_CJNE x_19914 x_19913 |
---|
2529 | | DJNZ (x_19916, x_19915) -> h_DJNZ x_19916 x_19915 |
---|
2530 | | ANL x_19917 -> h_ANL x_19917 |
---|
2531 | | ORL x_19918 -> h_ORL x_19918 |
---|
2532 | | XRL x_19919 -> h_XRL x_19919 |
---|
2533 | | CLR x_19920 -> h_CLR x_19920 |
---|
2534 | | CPL x_19921 -> h_CPL x_19921 |
---|
2535 | | RL x_19922 -> h_RL x_19922 |
---|
2536 | | RLC x_19923 -> h_RLC x_19923 |
---|
2537 | | RR x_19924 -> h_RR x_19924 |
---|
2538 | | RRC x_19925 -> h_RRC x_19925 |
---|
2539 | | SWAP x_19926 -> h_SWAP x_19926 |
---|
2540 | | MOV x_19927 -> h_MOV x_19927 |
---|
2541 | | MOVX x_19928 -> h_MOVX x_19928 |
---|
2542 | | SETB x_19929 -> h_SETB x_19929 |
---|
2543 | | PUSH x_19930 -> h_PUSH x_19930 |
---|
2544 | | POP x_19931 -> h_POP x_19931 |
---|
2545 | | XCH (x_19933, x_19932) -> h_XCH x_19933 x_19932 |
---|
2546 | | XCHD (x_19935, x_19934) -> h_XCHD x_19935 x_19934 |
---|
2547 | | RET -> h_RET |
---|
2548 | | RETI -> h_RETI |
---|
2549 | | NOP -> h_NOP |
---|
2550 | | JMP x_19936 -> h_JMP x_19936 |
---|
2551 | |
---|
2552 | (** val preinstruction_inv_rect_Type4 : |
---|
2553 | 'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ -> |
---|
2554 | 'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
2555 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
2556 | (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) -> |
---|
2557 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
2558 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
2559 | (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ -> |
---|
2560 | 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode |
---|
2561 | -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 |
---|
2562 | -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, |
---|
2563 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2564 | Types.prod) Types.sum -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 |
---|
2565 | -> __ -> 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2566 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2567 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
2568 | 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2569 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2570 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
2571 | 'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2572 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
2573 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
2574 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
2575 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
2576 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode, |
---|
2577 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2578 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2579 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2580 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2581 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2582 | Types.prod) Types.sum -> __ -> 'a2) -> (((subaddressing_mode, |
---|
2583 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2584 | Types.prod) Types.sum -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) |
---|
2585 | -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) |
---|
2586 | -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
2587 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> |
---|
2588 | (__ -> 'a2) -> (__ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2 **) |
---|
2589 | let preinstruction_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 h38 = |
---|
2590 | let hcut = |
---|
2591 | preinstruction_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 |
---|
2592 | h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 |
---|
2593 | h33 h34 h35 h36 h37 h38 hterm |
---|
2594 | in |
---|
2595 | hcut __ |
---|
2596 | |
---|
2597 | (** val preinstruction_inv_rect_Type3 : |
---|
2598 | 'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ -> |
---|
2599 | 'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
2600 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
2601 | (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) -> |
---|
2602 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
2603 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
2604 | (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ -> |
---|
2605 | 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode |
---|
2606 | -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 |
---|
2607 | -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, |
---|
2608 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2609 | Types.prod) Types.sum -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 |
---|
2610 | -> __ -> 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2611 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2612 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
2613 | 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2614 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2615 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
2616 | 'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2617 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
2618 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
2619 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
2620 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
2621 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode, |
---|
2622 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2623 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2624 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2625 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2626 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2627 | Types.prod) Types.sum -> __ -> 'a2) -> (((subaddressing_mode, |
---|
2628 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2629 | Types.prod) Types.sum -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) |
---|
2630 | -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) |
---|
2631 | -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
2632 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> |
---|
2633 | (__ -> 'a2) -> (__ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2 **) |
---|
2634 | let preinstruction_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 h38 = |
---|
2635 | let hcut = |
---|
2636 | preinstruction_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 |
---|
2637 | h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 |
---|
2638 | h33 h34 h35 h36 h37 h38 hterm |
---|
2639 | in |
---|
2640 | hcut __ |
---|
2641 | |
---|
2642 | (** val preinstruction_inv_rect_Type2 : |
---|
2643 | 'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ -> |
---|
2644 | 'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
2645 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
2646 | (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) -> |
---|
2647 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
2648 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
2649 | (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ -> |
---|
2650 | 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode |
---|
2651 | -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 |
---|
2652 | -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, |
---|
2653 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2654 | Types.prod) Types.sum -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 |
---|
2655 | -> __ -> 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2656 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2657 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
2658 | 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2659 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2660 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
2661 | 'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2662 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
2663 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
2664 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
2665 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
2666 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode, |
---|
2667 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2668 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2669 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2670 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2671 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2672 | Types.prod) Types.sum -> __ -> 'a2) -> (((subaddressing_mode, |
---|
2673 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2674 | Types.prod) Types.sum -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) |
---|
2675 | -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) |
---|
2676 | -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
2677 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> |
---|
2678 | (__ -> 'a2) -> (__ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2 **) |
---|
2679 | let preinstruction_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 h38 = |
---|
2680 | let hcut = |
---|
2681 | preinstruction_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 |
---|
2682 | h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 |
---|
2683 | h33 h34 h35 h36 h37 h38 hterm |
---|
2684 | in |
---|
2685 | hcut __ |
---|
2686 | |
---|
2687 | (** val preinstruction_inv_rect_Type1 : |
---|
2688 | 'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ -> |
---|
2689 | 'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
2690 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
2691 | (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) -> |
---|
2692 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
2693 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
2694 | (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ -> |
---|
2695 | 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode |
---|
2696 | -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 |
---|
2697 | -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, |
---|
2698 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2699 | Types.prod) Types.sum -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 |
---|
2700 | -> __ -> 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2701 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2702 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
2703 | 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2704 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2705 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
2706 | 'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2707 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
2708 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
2709 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
2710 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
2711 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode, |
---|
2712 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2713 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2714 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2715 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2716 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2717 | Types.prod) Types.sum -> __ -> 'a2) -> (((subaddressing_mode, |
---|
2718 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2719 | Types.prod) Types.sum -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) |
---|
2720 | -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) |
---|
2721 | -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
2722 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> |
---|
2723 | (__ -> 'a2) -> (__ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2 **) |
---|
2724 | let preinstruction_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 h38 = |
---|
2725 | let hcut = |
---|
2726 | preinstruction_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 |
---|
2727 | h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 |
---|
2728 | h33 h34 h35 h36 h37 h38 hterm |
---|
2729 | in |
---|
2730 | hcut __ |
---|
2731 | |
---|
2732 | (** val preinstruction_inv_rect_Type0 : |
---|
2733 | 'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ -> |
---|
2734 | 'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
2735 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
2736 | (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) -> |
---|
2737 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
2738 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
2739 | (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ -> |
---|
2740 | 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode |
---|
2741 | -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 |
---|
2742 | -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, |
---|
2743 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2744 | Types.prod) Types.sum -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 |
---|
2745 | -> __ -> 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2746 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2747 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
2748 | 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2749 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
2750 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
2751 | 'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
2752 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
2753 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
2754 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
2755 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
2756 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode, |
---|
2757 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2758 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2759 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2760 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2761 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
2762 | Types.prod) Types.sum -> __ -> 'a2) -> (((subaddressing_mode, |
---|
2763 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
2764 | Types.prod) Types.sum -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) |
---|
2765 | -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) |
---|
2766 | -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
2767 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> |
---|
2768 | (__ -> 'a2) -> (__ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2 **) |
---|
2769 | let preinstruction_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 h38 = |
---|
2770 | let hcut = |
---|
2771 | preinstruction_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 |
---|
2772 | h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 |
---|
2773 | h33 h34 h35 h36 h37 h38 hterm |
---|
2774 | in |
---|
2775 | hcut __ |
---|
2776 | |
---|
2777 | (** val preinstruction_discr : |
---|
2778 | 'a1 preinstruction -> 'a1 preinstruction -> __ **) |
---|
2779 | let preinstruction_discr x y = |
---|
2780 | Logic.eq_rect_Type2 x |
---|
2781 | (match x with |
---|
2782 | | ADD (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
2783 | | ADDC (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
2784 | | SUBB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
2785 | | INC a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2786 | | DEC a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2787 | | MUL (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
2788 | | DIV (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
2789 | | DA a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2790 | | JC a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2791 | | JNC a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2792 | | JB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
2793 | | JNB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
2794 | | JBC (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
2795 | | JZ a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2796 | | JNZ a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2797 | | CJNE (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
2798 | | DJNZ (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
2799 | | ANL a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2800 | | ORL a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2801 | | XRL a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2802 | | CLR a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2803 | | CPL a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2804 | | RL a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2805 | | RLC a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2806 | | RR a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2807 | | RRC a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2808 | | SWAP a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2809 | | MOV a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2810 | | MOVX a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2811 | | SETB a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2812 | | PUSH a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2813 | | POP a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2814 | | XCH (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
2815 | | XCHD (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
2816 | | RET -> Obj.magic (fun _ dH -> dH) |
---|
2817 | | RETI -> Obj.magic (fun _ dH -> dH) |
---|
2818 | | NOP -> Obj.magic (fun _ dH -> dH) |
---|
2819 | | JMP a0 -> Obj.magic (fun _ dH -> dH __)) y |
---|
2820 | |
---|
2821 | (** val preinstruction_jmdiscr : |
---|
2822 | 'a1 preinstruction -> 'a1 preinstruction -> __ **) |
---|
2823 | let preinstruction_jmdiscr x y = |
---|
2824 | Logic.eq_rect_Type2 x |
---|
2825 | (match x with |
---|
2826 | | ADD (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
2827 | | ADDC (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
2828 | | SUBB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
2829 | | INC a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2830 | | DEC a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2831 | | MUL (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
2832 | | DIV (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
2833 | | DA a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2834 | | JC a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2835 | | JNC a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2836 | | JB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
2837 | | JNB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
2838 | | JBC (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
2839 | | JZ a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2840 | | JNZ a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2841 | | CJNE (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
2842 | | DJNZ (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
2843 | | ANL a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2844 | | ORL a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2845 | | XRL a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2846 | | CLR a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2847 | | CPL a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2848 | | RL a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2849 | | RLC a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2850 | | RR a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2851 | | RRC a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2852 | | SWAP a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2853 | | MOV a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2854 | | MOVX a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2855 | | SETB a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2856 | | PUSH a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2857 | | POP a0 -> Obj.magic (fun _ dH -> dH __) |
---|
2858 | | XCH (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
2859 | | XCHD (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
2860 | | RET -> Obj.magic (fun _ dH -> dH) |
---|
2861 | | RETI -> Obj.magic (fun _ dH -> dH) |
---|
2862 | | NOP -> Obj.magic (fun _ dH -> dH) |
---|
2863 | | JMP a0 -> Obj.magic (fun _ dH -> dH __)) y |
---|
2864 | |
---|
2865 | (** val eq_preinstruction : |
---|
2866 | subaddressing_mode preinstruction -> subaddressing_mode preinstruction -> |
---|
2867 | Bool.bool **) |
---|
2868 | let eq_preinstruction i j = |
---|
2869 | match i with |
---|
2870 | | ADD (arg1, arg2) -> |
---|
2871 | (match j with |
---|
2872 | | ADD (arg1', arg2') -> |
---|
2873 | Bool.andb |
---|
2874 | (eq_addressing_mode |
---|
2875 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
2876 | Vector.VEmpty)) arg1) |
---|
2877 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
2878 | Vector.VEmpty)) arg1')) |
---|
2879 | (eq_addressing_mode |
---|
2880 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons |
---|
2881 | ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S |
---|
2882 | (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect, |
---|
2883 | (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2) |
---|
2884 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons |
---|
2885 | ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S |
---|
2886 | (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect, |
---|
2887 | (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2')) |
---|
2888 | | ADDC (x, x0) -> Bool.False |
---|
2889 | | SUBB (x, x0) -> Bool.False |
---|
2890 | | INC x -> Bool.False |
---|
2891 | | DEC x -> Bool.False |
---|
2892 | | MUL (x, x0) -> Bool.False |
---|
2893 | | DIV (x, x0) -> Bool.False |
---|
2894 | | DA x -> Bool.False |
---|
2895 | | JC x -> Bool.False |
---|
2896 | | JNC x -> Bool.False |
---|
2897 | | JB (x, x0) -> Bool.False |
---|
2898 | | JNB (x, x0) -> Bool.False |
---|
2899 | | JBC (x, x0) -> Bool.False |
---|
2900 | | JZ x -> Bool.False |
---|
2901 | | JNZ x -> Bool.False |
---|
2902 | | CJNE (x, x0) -> Bool.False |
---|
2903 | | DJNZ (x, x0) -> Bool.False |
---|
2904 | | ANL x -> Bool.False |
---|
2905 | | ORL x -> Bool.False |
---|
2906 | | XRL x -> Bool.False |
---|
2907 | | CLR x -> Bool.False |
---|
2908 | | CPL x -> Bool.False |
---|
2909 | | RL x -> Bool.False |
---|
2910 | | RLC x -> Bool.False |
---|
2911 | | RR x -> Bool.False |
---|
2912 | | RRC x -> Bool.False |
---|
2913 | | SWAP x -> Bool.False |
---|
2914 | | MOV x -> Bool.False |
---|
2915 | | MOVX x -> Bool.False |
---|
2916 | | SETB x -> Bool.False |
---|
2917 | | PUSH x -> Bool.False |
---|
2918 | | POP x -> Bool.False |
---|
2919 | | XCH (x, x0) -> Bool.False |
---|
2920 | | XCHD (x, x0) -> Bool.False |
---|
2921 | | RET -> Bool.False |
---|
2922 | | RETI -> Bool.False |
---|
2923 | | NOP -> Bool.False |
---|
2924 | | JMP x -> Bool.False) |
---|
2925 | | ADDC (arg1, arg2) -> |
---|
2926 | (match j with |
---|
2927 | | ADD (x, x0) -> Bool.False |
---|
2928 | | ADDC (arg1', arg2') -> |
---|
2929 | Bool.andb |
---|
2930 | (eq_addressing_mode |
---|
2931 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
2932 | Vector.VEmpty)) arg1) |
---|
2933 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
2934 | Vector.VEmpty)) arg1')) |
---|
2935 | (eq_addressing_mode |
---|
2936 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons |
---|
2937 | ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S |
---|
2938 | (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect, |
---|
2939 | (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2) |
---|
2940 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons |
---|
2941 | ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S |
---|
2942 | (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect, |
---|
2943 | (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2')) |
---|
2944 | | SUBB (x, x0) -> Bool.False |
---|
2945 | | INC x -> Bool.False |
---|
2946 | | DEC x -> Bool.False |
---|
2947 | | MUL (x, x0) -> Bool.False |
---|
2948 | | DIV (x, x0) -> Bool.False |
---|
2949 | | DA x -> Bool.False |
---|
2950 | | JC x -> Bool.False |
---|
2951 | | JNC x -> Bool.False |
---|
2952 | | JB (x, x0) -> Bool.False |
---|
2953 | | JNB (x, x0) -> Bool.False |
---|
2954 | | JBC (x, x0) -> Bool.False |
---|
2955 | | JZ x -> Bool.False |
---|
2956 | | JNZ x -> Bool.False |
---|
2957 | | CJNE (x, x0) -> Bool.False |
---|
2958 | | DJNZ (x, x0) -> Bool.False |
---|
2959 | | ANL x -> Bool.False |
---|
2960 | | ORL x -> Bool.False |
---|
2961 | | XRL x -> Bool.False |
---|
2962 | | CLR x -> Bool.False |
---|
2963 | | CPL x -> Bool.False |
---|
2964 | | RL x -> Bool.False |
---|
2965 | | RLC x -> Bool.False |
---|
2966 | | RR x -> Bool.False |
---|
2967 | | RRC x -> Bool.False |
---|
2968 | | SWAP x -> Bool.False |
---|
2969 | | MOV x -> Bool.False |
---|
2970 | | MOVX x -> Bool.False |
---|
2971 | | SETB x -> Bool.False |
---|
2972 | | PUSH x -> Bool.False |
---|
2973 | | POP x -> Bool.False |
---|
2974 | | XCH (x, x0) -> Bool.False |
---|
2975 | | XCHD (x, x0) -> Bool.False |
---|
2976 | | RET -> Bool.False |
---|
2977 | | RETI -> Bool.False |
---|
2978 | | NOP -> Bool.False |
---|
2979 | | JMP x -> Bool.False) |
---|
2980 | | SUBB (arg1, arg2) -> |
---|
2981 | (match j with |
---|
2982 | | ADD (x, x0) -> Bool.False |
---|
2983 | | ADDC (x, x0) -> Bool.False |
---|
2984 | | SUBB (arg1', arg2') -> |
---|
2985 | Bool.andb |
---|
2986 | (eq_addressing_mode |
---|
2987 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
2988 | Vector.VEmpty)) arg1) |
---|
2989 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
2990 | Vector.VEmpty)) arg1')) |
---|
2991 | (eq_addressing_mode |
---|
2992 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons |
---|
2993 | ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S |
---|
2994 | (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect, |
---|
2995 | (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2) |
---|
2996 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons |
---|
2997 | ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S |
---|
2998 | (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect, |
---|
2999 | (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2')) |
---|
3000 | | INC x -> Bool.False |
---|
3001 | | DEC x -> Bool.False |
---|
3002 | | MUL (x, x0) -> Bool.False |
---|
3003 | | DIV (x, x0) -> Bool.False |
---|
3004 | | DA x -> Bool.False |
---|
3005 | | JC x -> Bool.False |
---|
3006 | | JNC x -> Bool.False |
---|
3007 | | JB (x, x0) -> Bool.False |
---|
3008 | | JNB (x, x0) -> Bool.False |
---|
3009 | | JBC (x, x0) -> Bool.False |
---|
3010 | | JZ x -> Bool.False |
---|
3011 | | JNZ x -> Bool.False |
---|
3012 | | CJNE (x, x0) -> Bool.False |
---|
3013 | | DJNZ (x, x0) -> Bool.False |
---|
3014 | | ANL x -> Bool.False |
---|
3015 | | ORL x -> Bool.False |
---|
3016 | | XRL x -> Bool.False |
---|
3017 | | CLR x -> Bool.False |
---|
3018 | | CPL x -> Bool.False |
---|
3019 | | RL x -> Bool.False |
---|
3020 | | RLC x -> Bool.False |
---|
3021 | | RR x -> Bool.False |
---|
3022 | | RRC x -> Bool.False |
---|
3023 | | SWAP x -> Bool.False |
---|
3024 | | MOV x -> Bool.False |
---|
3025 | | MOVX x -> Bool.False |
---|
3026 | | SETB x -> Bool.False |
---|
3027 | | PUSH x -> Bool.False |
---|
3028 | | POP x -> Bool.False |
---|
3029 | | XCH (x, x0) -> Bool.False |
---|
3030 | | XCHD (x, x0) -> Bool.False |
---|
3031 | | RET -> Bool.False |
---|
3032 | | RETI -> Bool.False |
---|
3033 | | NOP -> Bool.False |
---|
3034 | | JMP x -> Bool.False) |
---|
3035 | | INC arg -> |
---|
3036 | (match j with |
---|
3037 | | ADD (x, x0) -> Bool.False |
---|
3038 | | ADDC (x, x0) -> Bool.False |
---|
3039 | | SUBB (x, x0) -> Bool.False |
---|
3040 | | INC arg' -> |
---|
3041 | eq_addressing_mode |
---|
3042 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) |
---|
3043 | (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Acc_a, |
---|
3044 | (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, |
---|
3045 | (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons |
---|
3046 | ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Dptr, |
---|
3047 | Vector.VEmpty)))))))))) arg) |
---|
3048 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) |
---|
3049 | (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Acc_a, |
---|
3050 | (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, |
---|
3051 | (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons |
---|
3052 | ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Dptr, |
---|
3053 | Vector.VEmpty)))))))))) arg') |
---|
3054 | | DEC x -> Bool.False |
---|
3055 | | MUL (x, x0) -> Bool.False |
---|
3056 | | DIV (x, x0) -> Bool.False |
---|
3057 | | DA x -> Bool.False |
---|
3058 | | JC x -> Bool.False |
---|
3059 | | JNC x -> Bool.False |
---|
3060 | | JB (x, x0) -> Bool.False |
---|
3061 | | JNB (x, x0) -> Bool.False |
---|
3062 | | JBC (x, x0) -> Bool.False |
---|
3063 | | JZ x -> Bool.False |
---|
3064 | | JNZ x -> Bool.False |
---|
3065 | | CJNE (x, x0) -> Bool.False |
---|
3066 | | DJNZ (x, x0) -> Bool.False |
---|
3067 | | ANL x -> Bool.False |
---|
3068 | | ORL x -> Bool.False |
---|
3069 | | XRL x -> Bool.False |
---|
3070 | | CLR x -> Bool.False |
---|
3071 | | CPL x -> Bool.False |
---|
3072 | | RL x -> Bool.False |
---|
3073 | | RLC x -> Bool.False |
---|
3074 | | RR x -> Bool.False |
---|
3075 | | RRC x -> Bool.False |
---|
3076 | | SWAP x -> Bool.False |
---|
3077 | | MOV x -> Bool.False |
---|
3078 | | MOVX x -> Bool.False |
---|
3079 | | SETB x -> Bool.False |
---|
3080 | | PUSH x -> Bool.False |
---|
3081 | | POP x -> Bool.False |
---|
3082 | | XCH (x, x0) -> Bool.False |
---|
3083 | | XCHD (x, x0) -> Bool.False |
---|
3084 | | RET -> Bool.False |
---|
3085 | | RETI -> Bool.False |
---|
3086 | | NOP -> Bool.False |
---|
3087 | | JMP x -> Bool.False) |
---|
3088 | | DEC arg -> |
---|
3089 | (match j with |
---|
3090 | | ADD (x, x0) -> Bool.False |
---|
3091 | | ADDC (x, x0) -> Bool.False |
---|
3092 | | SUBB (x, x0) -> Bool.False |
---|
3093 | | INC x -> Bool.False |
---|
3094 | | DEC arg' -> |
---|
3095 | eq_addressing_mode |
---|
3096 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons |
---|
3097 | ((Nat.S (Nat.S (Nat.S Nat.O))), Acc_a, (Vector.VCons ((Nat.S |
---|
3098 | (Nat.S Nat.O)), Registr, (Vector.VCons ((Nat.S Nat.O), Direct, |
---|
3099 | (Vector.VCons (Nat.O, Indirect, Vector.VEmpty)))))))) arg) |
---|
3100 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons |
---|
3101 | ((Nat.S (Nat.S (Nat.S Nat.O))), Acc_a, (Vector.VCons ((Nat.S |
---|
3102 | (Nat.S Nat.O)), Registr, (Vector.VCons ((Nat.S Nat.O), Direct, |
---|
3103 | (Vector.VCons (Nat.O, Indirect, Vector.VEmpty)))))))) arg') |
---|
3104 | | MUL (x, x0) -> Bool.False |
---|
3105 | | DIV (x, x0) -> Bool.False |
---|
3106 | | DA x -> Bool.False |
---|
3107 | | JC x -> Bool.False |
---|
3108 | | JNC x -> Bool.False |
---|
3109 | | JB (x, x0) -> Bool.False |
---|
3110 | | JNB (x, x0) -> Bool.False |
---|
3111 | | JBC (x, x0) -> Bool.False |
---|
3112 | | JZ x -> Bool.False |
---|
3113 | | JNZ x -> Bool.False |
---|
3114 | | CJNE (x, x0) -> Bool.False |
---|
3115 | | DJNZ (x, x0) -> Bool.False |
---|
3116 | | ANL x -> Bool.False |
---|
3117 | | ORL x -> Bool.False |
---|
3118 | | XRL x -> Bool.False |
---|
3119 | | CLR x -> Bool.False |
---|
3120 | | CPL x -> Bool.False |
---|
3121 | | RL x -> Bool.False |
---|
3122 | | RLC x -> Bool.False |
---|
3123 | | RR x -> Bool.False |
---|
3124 | | RRC x -> Bool.False |
---|
3125 | | SWAP x -> Bool.False |
---|
3126 | | MOV x -> Bool.False |
---|
3127 | | MOVX x -> Bool.False |
---|
3128 | | SETB x -> Bool.False |
---|
3129 | | PUSH x -> Bool.False |
---|
3130 | | POP x -> Bool.False |
---|
3131 | | XCH (x, x0) -> Bool.False |
---|
3132 | | XCHD (x, x0) -> Bool.False |
---|
3133 | | RET -> Bool.False |
---|
3134 | | RETI -> Bool.False |
---|
3135 | | NOP -> Bool.False |
---|
3136 | | JMP x -> Bool.False) |
---|
3137 | | MUL (arg1, arg2) -> |
---|
3138 | (match j with |
---|
3139 | | ADD (x, x0) -> Bool.False |
---|
3140 | | ADDC (x, x0) -> Bool.False |
---|
3141 | | SUBB (x, x0) -> Bool.False |
---|
3142 | | INC x -> Bool.False |
---|
3143 | | DEC x -> Bool.False |
---|
3144 | | MUL (arg1', arg2') -> |
---|
3145 | Bool.andb |
---|
3146 | (eq_addressing_mode |
---|
3147 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
3148 | Vector.VEmpty)) arg1) |
---|
3149 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
3150 | Vector.VEmpty)) arg1')) |
---|
3151 | (eq_addressing_mode |
---|
3152 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_b, |
---|
3153 | Vector.VEmpty)) arg2) |
---|
3154 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_b, |
---|
3155 | Vector.VEmpty)) arg2')) |
---|
3156 | | DIV (x, x0) -> Bool.False |
---|
3157 | | DA x -> Bool.False |
---|
3158 | | JC x -> Bool.False |
---|
3159 | | JNC x -> Bool.False |
---|
3160 | | JB (x, x0) -> Bool.False |
---|
3161 | | JNB (x, x0) -> Bool.False |
---|
3162 | | JBC (x, x0) -> Bool.False |
---|
3163 | | JZ x -> Bool.False |
---|
3164 | | JNZ x -> Bool.False |
---|
3165 | | CJNE (x, x0) -> Bool.False |
---|
3166 | | DJNZ (x, x0) -> Bool.False |
---|
3167 | | ANL x -> Bool.False |
---|
3168 | | ORL x -> Bool.False |
---|
3169 | | XRL x -> Bool.False |
---|
3170 | | CLR x -> Bool.False |
---|
3171 | | CPL x -> Bool.False |
---|
3172 | | RL x -> Bool.False |
---|
3173 | | RLC x -> Bool.False |
---|
3174 | | RR x -> Bool.False |
---|
3175 | | RRC x -> Bool.False |
---|
3176 | | SWAP x -> Bool.False |
---|
3177 | | MOV x -> Bool.False |
---|
3178 | | MOVX x -> Bool.False |
---|
3179 | | SETB x -> Bool.False |
---|
3180 | | PUSH x -> Bool.False |
---|
3181 | | POP x -> Bool.False |
---|
3182 | | XCH (x, x0) -> Bool.False |
---|
3183 | | XCHD (x, x0) -> Bool.False |
---|
3184 | | RET -> Bool.False |
---|
3185 | | RETI -> Bool.False |
---|
3186 | | NOP -> Bool.False |
---|
3187 | | JMP x -> Bool.False) |
---|
3188 | | DIV (arg1, arg2) -> |
---|
3189 | (match j with |
---|
3190 | | ADD (x, x0) -> Bool.False |
---|
3191 | | ADDC (x, x0) -> Bool.False |
---|
3192 | | SUBB (x, x0) -> Bool.False |
---|
3193 | | INC x -> Bool.False |
---|
3194 | | DEC x -> Bool.False |
---|
3195 | | MUL (x, x0) -> Bool.False |
---|
3196 | | DIV (arg1', arg2') -> |
---|
3197 | Bool.andb |
---|
3198 | (eq_addressing_mode |
---|
3199 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
3200 | Vector.VEmpty)) arg1) |
---|
3201 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
3202 | Vector.VEmpty)) arg1')) |
---|
3203 | (eq_addressing_mode |
---|
3204 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_b, |
---|
3205 | Vector.VEmpty)) arg2) |
---|
3206 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_b, |
---|
3207 | Vector.VEmpty)) arg2')) |
---|
3208 | | DA x -> Bool.False |
---|
3209 | | JC x -> Bool.False |
---|
3210 | | JNC x -> Bool.False |
---|
3211 | | JB (x, x0) -> Bool.False |
---|
3212 | | JNB (x, x0) -> Bool.False |
---|
3213 | | JBC (x, x0) -> Bool.False |
---|
3214 | | JZ x -> Bool.False |
---|
3215 | | JNZ x -> Bool.False |
---|
3216 | | CJNE (x, x0) -> Bool.False |
---|
3217 | | DJNZ (x, x0) -> Bool.False |
---|
3218 | | ANL x -> Bool.False |
---|
3219 | | ORL x -> Bool.False |
---|
3220 | | XRL x -> Bool.False |
---|
3221 | | CLR x -> Bool.False |
---|
3222 | | CPL x -> Bool.False |
---|
3223 | | RL x -> Bool.False |
---|
3224 | | RLC x -> Bool.False |
---|
3225 | | RR x -> Bool.False |
---|
3226 | | RRC x -> Bool.False |
---|
3227 | | SWAP x -> Bool.False |
---|
3228 | | MOV x -> Bool.False |
---|
3229 | | MOVX x -> Bool.False |
---|
3230 | | SETB x -> Bool.False |
---|
3231 | | PUSH x -> Bool.False |
---|
3232 | | POP x -> Bool.False |
---|
3233 | | XCH (x, x0) -> Bool.False |
---|
3234 | | XCHD (x, x0) -> Bool.False |
---|
3235 | | RET -> Bool.False |
---|
3236 | | RETI -> Bool.False |
---|
3237 | | NOP -> Bool.False |
---|
3238 | | JMP x -> Bool.False) |
---|
3239 | | DA arg -> |
---|
3240 | (match j with |
---|
3241 | | ADD (x, x0) -> Bool.False |
---|
3242 | | ADDC (x, x0) -> Bool.False |
---|
3243 | | SUBB (x, x0) -> Bool.False |
---|
3244 | | INC x -> Bool.False |
---|
3245 | | DEC x -> Bool.False |
---|
3246 | | MUL (x, x0) -> Bool.False |
---|
3247 | | DIV (x, x0) -> Bool.False |
---|
3248 | | DA arg' -> |
---|
3249 | eq_addressing_mode |
---|
3250 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
3251 | Vector.VEmpty)) arg) |
---|
3252 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
3253 | Vector.VEmpty)) arg') |
---|
3254 | | JC x -> Bool.False |
---|
3255 | | JNC x -> Bool.False |
---|
3256 | | JB (x, x0) -> Bool.False |
---|
3257 | | JNB (x, x0) -> Bool.False |
---|
3258 | | JBC (x, x0) -> Bool.False |
---|
3259 | | JZ x -> Bool.False |
---|
3260 | | JNZ x -> Bool.False |
---|
3261 | | CJNE (x, x0) -> Bool.False |
---|
3262 | | DJNZ (x, x0) -> Bool.False |
---|
3263 | | ANL x -> Bool.False |
---|
3264 | | ORL x -> Bool.False |
---|
3265 | | XRL x -> Bool.False |
---|
3266 | | CLR x -> Bool.False |
---|
3267 | | CPL x -> Bool.False |
---|
3268 | | RL x -> Bool.False |
---|
3269 | | RLC x -> Bool.False |
---|
3270 | | RR x -> Bool.False |
---|
3271 | | RRC x -> Bool.False |
---|
3272 | | SWAP x -> Bool.False |
---|
3273 | | MOV x -> Bool.False |
---|
3274 | | MOVX x -> Bool.False |
---|
3275 | | SETB x -> Bool.False |
---|
3276 | | PUSH x -> Bool.False |
---|
3277 | | POP x -> Bool.False |
---|
3278 | | XCH (x, x0) -> Bool.False |
---|
3279 | | XCHD (x, x0) -> Bool.False |
---|
3280 | | RET -> Bool.False |
---|
3281 | | RETI -> Bool.False |
---|
3282 | | NOP -> Bool.False |
---|
3283 | | JMP x -> Bool.False) |
---|
3284 | | JC arg -> |
---|
3285 | (match j with |
---|
3286 | | ADD (x, x0) -> Bool.False |
---|
3287 | | ADDC (x, x0) -> Bool.False |
---|
3288 | | SUBB (x, x0) -> Bool.False |
---|
3289 | | INC x -> Bool.False |
---|
3290 | | DEC x -> Bool.False |
---|
3291 | | MUL (x, x0) -> Bool.False |
---|
3292 | | DIV (x, x0) -> Bool.False |
---|
3293 | | DA x -> Bool.False |
---|
3294 | | JC arg' -> |
---|
3295 | eq_addressing_mode |
---|
3296 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative, |
---|
3297 | Vector.VEmpty)) arg) |
---|
3298 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative, |
---|
3299 | Vector.VEmpty)) arg') |
---|
3300 | | JNC x -> Bool.False |
---|
3301 | | JB (x, x0) -> Bool.False |
---|
3302 | | JNB (x, x0) -> Bool.False |
---|
3303 | | JBC (x, x0) -> Bool.False |
---|
3304 | | JZ x -> Bool.False |
---|
3305 | | JNZ x -> Bool.False |
---|
3306 | | CJNE (x, x0) -> Bool.False |
---|
3307 | | DJNZ (x, x0) -> Bool.False |
---|
3308 | | ANL x -> Bool.False |
---|
3309 | | ORL x -> Bool.False |
---|
3310 | | XRL x -> Bool.False |
---|
3311 | | CLR x -> Bool.False |
---|
3312 | | CPL x -> Bool.False |
---|
3313 | | RL x -> Bool.False |
---|
3314 | | RLC x -> Bool.False |
---|
3315 | | RR x -> Bool.False |
---|
3316 | | RRC x -> Bool.False |
---|
3317 | | SWAP x -> Bool.False |
---|
3318 | | MOV x -> Bool.False |
---|
3319 | | MOVX x -> Bool.False |
---|
3320 | | SETB x -> Bool.False |
---|
3321 | | PUSH x -> Bool.False |
---|
3322 | | POP x -> Bool.False |
---|
3323 | | XCH (x, x0) -> Bool.False |
---|
3324 | | XCHD (x, x0) -> Bool.False |
---|
3325 | | RET -> Bool.False |
---|
3326 | | RETI -> Bool.False |
---|
3327 | | NOP -> Bool.False |
---|
3328 | | JMP x -> Bool.False) |
---|
3329 | | JNC arg -> |
---|
3330 | (match j with |
---|
3331 | | ADD (x, x0) -> Bool.False |
---|
3332 | | ADDC (x, x0) -> Bool.False |
---|
3333 | | SUBB (x, x0) -> Bool.False |
---|
3334 | | INC x -> Bool.False |
---|
3335 | | DEC x -> Bool.False |
---|
3336 | | MUL (x, x0) -> Bool.False |
---|
3337 | | DIV (x, x0) -> Bool.False |
---|
3338 | | DA x -> Bool.False |
---|
3339 | | JC x -> Bool.False |
---|
3340 | | JNC arg' -> |
---|
3341 | eq_addressing_mode |
---|
3342 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative, |
---|
3343 | Vector.VEmpty)) arg) |
---|
3344 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative, |
---|
3345 | Vector.VEmpty)) arg') |
---|
3346 | | JB (x, x0) -> Bool.False |
---|
3347 | | JNB (x, x0) -> Bool.False |
---|
3348 | | JBC (x, x0) -> Bool.False |
---|
3349 | | JZ x -> Bool.False |
---|
3350 | | JNZ x -> Bool.False |
---|
3351 | | CJNE (x, x0) -> Bool.False |
---|
3352 | | DJNZ (x, x0) -> Bool.False |
---|
3353 | | ANL x -> Bool.False |
---|
3354 | | ORL x -> Bool.False |
---|
3355 | | XRL x -> Bool.False |
---|
3356 | | CLR x -> Bool.False |
---|
3357 | | CPL x -> Bool.False |
---|
3358 | | RL x -> Bool.False |
---|
3359 | | RLC x -> Bool.False |
---|
3360 | | RR x -> Bool.False |
---|
3361 | | RRC x -> Bool.False |
---|
3362 | | SWAP x -> Bool.False |
---|
3363 | | MOV x -> Bool.False |
---|
3364 | | MOVX x -> Bool.False |
---|
3365 | | SETB x -> Bool.False |
---|
3366 | | PUSH x -> Bool.False |
---|
3367 | | POP x -> Bool.False |
---|
3368 | | XCH (x, x0) -> Bool.False |
---|
3369 | | XCHD (x, x0) -> Bool.False |
---|
3370 | | RET -> Bool.False |
---|
3371 | | RETI -> Bool.False |
---|
3372 | | NOP -> Bool.False |
---|
3373 | | JMP x -> Bool.False) |
---|
3374 | | JB (arg1, arg2) -> |
---|
3375 | (match j with |
---|
3376 | | ADD (x, x0) -> Bool.False |
---|
3377 | | ADDC (x, x0) -> Bool.False |
---|
3378 | | SUBB (x, x0) -> Bool.False |
---|
3379 | | INC x -> Bool.False |
---|
3380 | | DEC x -> Bool.False |
---|
3381 | | MUL (x, x0) -> Bool.False |
---|
3382 | | DIV (x, x0) -> Bool.False |
---|
3383 | | DA x -> Bool.False |
---|
3384 | | JC x -> Bool.False |
---|
3385 | | JNC x -> Bool.False |
---|
3386 | | JB (arg1', arg2') -> |
---|
3387 | Bool.andb |
---|
3388 | (eq_addressing_mode |
---|
3389 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Bit_addr, |
---|
3390 | Vector.VEmpty)) arg1) |
---|
3391 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Bit_addr, |
---|
3392 | Vector.VEmpty)) arg1')) |
---|
3393 | (eq_addressing_mode |
---|
3394 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative, |
---|
3395 | Vector.VEmpty)) arg2) |
---|
3396 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative, |
---|
3397 | Vector.VEmpty)) arg2')) |
---|
3398 | | JNB (x, x0) -> Bool.False |
---|
3399 | | JBC (x, x0) -> Bool.False |
---|
3400 | | JZ x -> Bool.False |
---|
3401 | | JNZ x -> Bool.False |
---|
3402 | | CJNE (x, x0) -> Bool.False |
---|
3403 | | DJNZ (x, x0) -> Bool.False |
---|
3404 | | ANL x -> Bool.False |
---|
3405 | | ORL x -> Bool.False |
---|
3406 | | XRL x -> Bool.False |
---|
3407 | | CLR x -> Bool.False |
---|
3408 | | CPL x -> Bool.False |
---|
3409 | | RL x -> Bool.False |
---|
3410 | | RLC x -> Bool.False |
---|
3411 | | RR x -> Bool.False |
---|
3412 | | RRC x -> Bool.False |
---|
3413 | | SWAP x -> Bool.False |
---|
3414 | | MOV x -> Bool.False |
---|
3415 | | MOVX x -> Bool.False |
---|
3416 | | SETB x -> Bool.False |
---|
3417 | | PUSH x -> Bool.False |
---|
3418 | | POP x -> Bool.False |
---|
3419 | | XCH (x, x0) -> Bool.False |
---|
3420 | | XCHD (x, x0) -> Bool.False |
---|
3421 | | RET -> Bool.False |
---|
3422 | | RETI -> Bool.False |
---|
3423 | | NOP -> Bool.False |
---|
3424 | | JMP x -> Bool.False) |
---|
3425 | | JNB (arg1, arg2) -> |
---|
3426 | (match j with |
---|
3427 | | ADD (x, x0) -> Bool.False |
---|
3428 | | ADDC (x, x0) -> Bool.False |
---|
3429 | | SUBB (x, x0) -> Bool.False |
---|
3430 | | INC x -> Bool.False |
---|
3431 | | DEC x -> Bool.False |
---|
3432 | | MUL (x, x0) -> Bool.False |
---|
3433 | | DIV (x, x0) -> Bool.False |
---|
3434 | | DA x -> Bool.False |
---|
3435 | | JC x -> Bool.False |
---|
3436 | | JNC x -> Bool.False |
---|
3437 | | JB (x, x0) -> Bool.False |
---|
3438 | | JNB (arg1', arg2') -> |
---|
3439 | Bool.andb |
---|
3440 | (eq_addressing_mode |
---|
3441 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Bit_addr, |
---|
3442 | Vector.VEmpty)) arg1) |
---|
3443 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Bit_addr, |
---|
3444 | Vector.VEmpty)) arg1')) |
---|
3445 | (eq_addressing_mode |
---|
3446 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative, |
---|
3447 | Vector.VEmpty)) arg2) |
---|
3448 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative, |
---|
3449 | Vector.VEmpty)) arg2')) |
---|
3450 | | JBC (x, x0) -> Bool.False |
---|
3451 | | JZ x -> Bool.False |
---|
3452 | | JNZ x -> Bool.False |
---|
3453 | | CJNE (x, x0) -> Bool.False |
---|
3454 | | DJNZ (x, x0) -> Bool.False |
---|
3455 | | ANL x -> Bool.False |
---|
3456 | | ORL x -> Bool.False |
---|
3457 | | XRL x -> Bool.False |
---|
3458 | | CLR x -> Bool.False |
---|
3459 | | CPL x -> Bool.False |
---|
3460 | | RL x -> Bool.False |
---|
3461 | | RLC x -> Bool.False |
---|
3462 | | RR x -> Bool.False |
---|
3463 | | RRC x -> Bool.False |
---|
3464 | | SWAP x -> Bool.False |
---|
3465 | | MOV x -> Bool.False |
---|
3466 | | MOVX x -> Bool.False |
---|
3467 | | SETB x -> Bool.False |
---|
3468 | | PUSH x -> Bool.False |
---|
3469 | | POP x -> Bool.False |
---|
3470 | | XCH (x, x0) -> Bool.False |
---|
3471 | | XCHD (x, x0) -> Bool.False |
---|
3472 | | RET -> Bool.False |
---|
3473 | | RETI -> Bool.False |
---|
3474 | | NOP -> Bool.False |
---|
3475 | | JMP x -> Bool.False) |
---|
3476 | | JBC (arg1, arg2) -> |
---|
3477 | (match j with |
---|
3478 | | ADD (x, x0) -> Bool.False |
---|
3479 | | ADDC (x, x0) -> Bool.False |
---|
3480 | | SUBB (x, x0) -> Bool.False |
---|
3481 | | INC x -> Bool.False |
---|
3482 | | DEC x -> Bool.False |
---|
3483 | | MUL (x, x0) -> Bool.False |
---|
3484 | | DIV (x, x0) -> Bool.False |
---|
3485 | | DA x -> Bool.False |
---|
3486 | | JC x -> Bool.False |
---|
3487 | | JNC x -> Bool.False |
---|
3488 | | JB (x, x0) -> Bool.False |
---|
3489 | | JNB (x, x0) -> Bool.False |
---|
3490 | | JBC (arg1', arg2') -> |
---|
3491 | Bool.andb |
---|
3492 | (eq_addressing_mode |
---|
3493 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Bit_addr, |
---|
3494 | Vector.VEmpty)) arg1) |
---|
3495 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Bit_addr, |
---|
3496 | Vector.VEmpty)) arg1')) |
---|
3497 | (eq_addressing_mode |
---|
3498 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative, |
---|
3499 | Vector.VEmpty)) arg2) |
---|
3500 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative, |
---|
3501 | Vector.VEmpty)) arg2')) |
---|
3502 | | JZ x -> Bool.False |
---|
3503 | | JNZ x -> Bool.False |
---|
3504 | | CJNE (x, x0) -> Bool.False |
---|
3505 | | DJNZ (x, x0) -> Bool.False |
---|
3506 | | ANL x -> Bool.False |
---|
3507 | | ORL x -> Bool.False |
---|
3508 | | XRL x -> Bool.False |
---|
3509 | | CLR x -> Bool.False |
---|
3510 | | CPL x -> Bool.False |
---|
3511 | | RL x -> Bool.False |
---|
3512 | | RLC x -> Bool.False |
---|
3513 | | RR x -> Bool.False |
---|
3514 | | RRC x -> Bool.False |
---|
3515 | | SWAP x -> Bool.False |
---|
3516 | | MOV x -> Bool.False |
---|
3517 | | MOVX x -> Bool.False |
---|
3518 | | SETB x -> Bool.False |
---|
3519 | | PUSH x -> Bool.False |
---|
3520 | | POP x -> Bool.False |
---|
3521 | | XCH (x, x0) -> Bool.False |
---|
3522 | | XCHD (x, x0) -> Bool.False |
---|
3523 | | RET -> Bool.False |
---|
3524 | | RETI -> Bool.False |
---|
3525 | | NOP -> Bool.False |
---|
3526 | | JMP x -> Bool.False) |
---|
3527 | | JZ arg -> |
---|
3528 | (match j with |
---|
3529 | | ADD (x, x0) -> Bool.False |
---|
3530 | | ADDC (x, x0) -> Bool.False |
---|
3531 | | SUBB (x, x0) -> Bool.False |
---|
3532 | | INC x -> Bool.False |
---|
3533 | | DEC x -> Bool.False |
---|
3534 | | MUL (x, x0) -> Bool.False |
---|
3535 | | DIV (x, x0) -> Bool.False |
---|
3536 | | DA x -> Bool.False |
---|
3537 | | JC x -> Bool.False |
---|
3538 | | JNC x -> Bool.False |
---|
3539 | | JB (x, x0) -> Bool.False |
---|
3540 | | JNB (x, x0) -> Bool.False |
---|
3541 | | JBC (x, x0) -> Bool.False |
---|
3542 | | JZ arg' -> |
---|
3543 | eq_addressing_mode |
---|
3544 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative, |
---|
3545 | Vector.VEmpty)) arg) |
---|
3546 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative, |
---|
3547 | Vector.VEmpty)) arg') |
---|
3548 | | JNZ x -> Bool.False |
---|
3549 | | CJNE (x, x0) -> Bool.False |
---|
3550 | | DJNZ (x, x0) -> Bool.False |
---|
3551 | | ANL x -> Bool.False |
---|
3552 | | ORL x -> Bool.False |
---|
3553 | | XRL x -> Bool.False |
---|
3554 | | CLR x -> Bool.False |
---|
3555 | | CPL x -> Bool.False |
---|
3556 | | RL x -> Bool.False |
---|
3557 | | RLC x -> Bool.False |
---|
3558 | | RR x -> Bool.False |
---|
3559 | | RRC x -> Bool.False |
---|
3560 | | SWAP x -> Bool.False |
---|
3561 | | MOV x -> Bool.False |
---|
3562 | | MOVX x -> Bool.False |
---|
3563 | | SETB x -> Bool.False |
---|
3564 | | PUSH x -> Bool.False |
---|
3565 | | POP x -> Bool.False |
---|
3566 | | XCH (x, x0) -> Bool.False |
---|
3567 | | XCHD (x, x0) -> Bool.False |
---|
3568 | | RET -> Bool.False |
---|
3569 | | RETI -> Bool.False |
---|
3570 | | NOP -> Bool.False |
---|
3571 | | JMP x -> Bool.False) |
---|
3572 | | JNZ arg -> |
---|
3573 | (match j with |
---|
3574 | | ADD (x, x0) -> Bool.False |
---|
3575 | | ADDC (x, x0) -> Bool.False |
---|
3576 | | SUBB (x, x0) -> Bool.False |
---|
3577 | | INC x -> Bool.False |
---|
3578 | | DEC x -> Bool.False |
---|
3579 | | MUL (x, x0) -> Bool.False |
---|
3580 | | DIV (x, x0) -> Bool.False |
---|
3581 | | DA x -> Bool.False |
---|
3582 | | JC x -> Bool.False |
---|
3583 | | JNC x -> Bool.False |
---|
3584 | | JB (x, x0) -> Bool.False |
---|
3585 | | JNB (x, x0) -> Bool.False |
---|
3586 | | JBC (x, x0) -> Bool.False |
---|
3587 | | JZ x -> Bool.False |
---|
3588 | | JNZ arg' -> |
---|
3589 | eq_addressing_mode |
---|
3590 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative, |
---|
3591 | Vector.VEmpty)) arg) |
---|
3592 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative, |
---|
3593 | Vector.VEmpty)) arg') |
---|
3594 | | CJNE (x, x0) -> Bool.False |
---|
3595 | | DJNZ (x, x0) -> Bool.False |
---|
3596 | | ANL x -> Bool.False |
---|
3597 | | ORL x -> Bool.False |
---|
3598 | | XRL x -> Bool.False |
---|
3599 | | CLR x -> Bool.False |
---|
3600 | | CPL x -> Bool.False |
---|
3601 | | RL x -> Bool.False |
---|
3602 | | RLC x -> Bool.False |
---|
3603 | | RR x -> Bool.False |
---|
3604 | | RRC x -> Bool.False |
---|
3605 | | SWAP x -> Bool.False |
---|
3606 | | MOV x -> Bool.False |
---|
3607 | | MOVX x -> Bool.False |
---|
3608 | | SETB x -> Bool.False |
---|
3609 | | PUSH x -> Bool.False |
---|
3610 | | POP x -> Bool.False |
---|
3611 | | XCH (x, x0) -> Bool.False |
---|
3612 | | XCHD (x, x0) -> Bool.False |
---|
3613 | | RET -> Bool.False |
---|
3614 | | RETI -> Bool.False |
---|
3615 | | NOP -> Bool.False |
---|
3616 | | JMP x -> Bool.False) |
---|
3617 | | CJNE (arg1, arg2) -> |
---|
3618 | (match j with |
---|
3619 | | ADD (x, x0) -> Bool.False |
---|
3620 | | ADDC (x, x0) -> Bool.False |
---|
3621 | | SUBB (x, x0) -> Bool.False |
---|
3622 | | INC x -> Bool.False |
---|
3623 | | DEC x -> Bool.False |
---|
3624 | | MUL (x, x0) -> Bool.False |
---|
3625 | | DIV (x, x0) -> Bool.False |
---|
3626 | | DA x -> Bool.False |
---|
3627 | | JC x -> Bool.False |
---|
3628 | | JNC x -> Bool.False |
---|
3629 | | JB (x, x0) -> Bool.False |
---|
3630 | | JNB (x, x0) -> Bool.False |
---|
3631 | | JBC (x, x0) -> Bool.False |
---|
3632 | | JZ x -> Bool.False |
---|
3633 | | JNZ x -> Bool.False |
---|
3634 | | CJNE (arg1', arg2') -> |
---|
3635 | let prod_eq_left = |
---|
3636 | Util.eq_prod (fun h h1 -> |
---|
3637 | eq_addressing_mode |
---|
3638 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
3639 | Vector.VEmpty)) h) |
---|
3640 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
3641 | Vector.VEmpty)) h1)) (fun h h1 -> |
---|
3642 | eq_addressing_mode |
---|
3643 | (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S |
---|
3644 | Nat.O), Direct, (Vector.VCons (Nat.O, Data, Vector.VEmpty)))) |
---|
3645 | h) |
---|
3646 | (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S |
---|
3647 | Nat.O), Direct, (Vector.VCons (Nat.O, Data, Vector.VEmpty)))) |
---|
3648 | h1)) |
---|
3649 | in |
---|
3650 | let prod_eq_right = |
---|
3651 | Util.eq_prod (fun h h1 -> |
---|
3652 | eq_addressing_mode |
---|
3653 | (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S |
---|
3654 | Nat.O), Registr, (Vector.VCons (Nat.O, Indirect, |
---|
3655 | Vector.VEmpty)))) h) |
---|
3656 | (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S |
---|
3657 | Nat.O), Registr, (Vector.VCons (Nat.O, Indirect, |
---|
3658 | Vector.VEmpty)))) h1)) (fun h h1 -> |
---|
3659 | eq_addressing_mode |
---|
3660 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Data, |
---|
3661 | Vector.VEmpty)) h) |
---|
3662 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Data, |
---|
3663 | Vector.VEmpty)) h1)) |
---|
3664 | in |
---|
3665 | let arg1_eq = Util.eq_sum prod_eq_left prod_eq_right in |
---|
3666 | Bool.andb (arg1_eq arg1 arg1') |
---|
3667 | (eq_addressing_mode |
---|
3668 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative, |
---|
3669 | Vector.VEmpty)) arg2) |
---|
3670 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative, |
---|
3671 | Vector.VEmpty)) arg2')) |
---|
3672 | | DJNZ (x, x0) -> Bool.False |
---|
3673 | | ANL x -> Bool.False |
---|
3674 | | ORL x -> Bool.False |
---|
3675 | | XRL x -> Bool.False |
---|
3676 | | CLR x -> Bool.False |
---|
3677 | | CPL x -> Bool.False |
---|
3678 | | RL x -> Bool.False |
---|
3679 | | RLC x -> Bool.False |
---|
3680 | | RR x -> Bool.False |
---|
3681 | | RRC x -> Bool.False |
---|
3682 | | SWAP x -> Bool.False |
---|
3683 | | MOV x -> Bool.False |
---|
3684 | | MOVX x -> Bool.False |
---|
3685 | | SETB x -> Bool.False |
---|
3686 | | PUSH x -> Bool.False |
---|
3687 | | POP x -> Bool.False |
---|
3688 | | XCH (x, x0) -> Bool.False |
---|
3689 | | XCHD (x, x0) -> Bool.False |
---|
3690 | | RET -> Bool.False |
---|
3691 | | RETI -> Bool.False |
---|
3692 | | NOP -> Bool.False |
---|
3693 | | JMP x -> Bool.False) |
---|
3694 | | DJNZ (arg1, arg2) -> |
---|
3695 | (match j with |
---|
3696 | | ADD (x, x0) -> Bool.False |
---|
3697 | | ADDC (x, x0) -> Bool.False |
---|
3698 | | SUBB (x, x0) -> Bool.False |
---|
3699 | | INC x -> Bool.False |
---|
3700 | | DEC x -> Bool.False |
---|
3701 | | MUL (x, x0) -> Bool.False |
---|
3702 | | DIV (x, x0) -> Bool.False |
---|
3703 | | DA x -> Bool.False |
---|
3704 | | JC x -> Bool.False |
---|
3705 | | JNC x -> Bool.False |
---|
3706 | | JB (x, x0) -> Bool.False |
---|
3707 | | JNB (x, x0) -> Bool.False |
---|
3708 | | JBC (x, x0) -> Bool.False |
---|
3709 | | JZ x -> Bool.False |
---|
3710 | | JNZ x -> Bool.False |
---|
3711 | | CJNE (x, x0) -> Bool.False |
---|
3712 | | DJNZ (arg1', arg2') -> |
---|
3713 | Bool.andb |
---|
3714 | (eq_addressing_mode |
---|
3715 | (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O), |
---|
3716 | Registr, (Vector.VCons (Nat.O, Direct, Vector.VEmpty)))) arg1) |
---|
3717 | (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O), |
---|
3718 | Registr, (Vector.VCons (Nat.O, Direct, Vector.VEmpty)))) arg1')) |
---|
3719 | (eq_addressing_mode |
---|
3720 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative, |
---|
3721 | Vector.VEmpty)) arg2) |
---|
3722 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative, |
---|
3723 | Vector.VEmpty)) arg2')) |
---|
3724 | | ANL x -> Bool.False |
---|
3725 | | ORL x -> Bool.False |
---|
3726 | | XRL x -> Bool.False |
---|
3727 | | CLR x -> Bool.False |
---|
3728 | | CPL x -> Bool.False |
---|
3729 | | RL x -> Bool.False |
---|
3730 | | RLC x -> Bool.False |
---|
3731 | | RR x -> Bool.False |
---|
3732 | | RRC x -> Bool.False |
---|
3733 | | SWAP x -> Bool.False |
---|
3734 | | MOV x -> Bool.False |
---|
3735 | | MOVX x -> Bool.False |
---|
3736 | | SETB x -> Bool.False |
---|
3737 | | PUSH x -> Bool.False |
---|
3738 | | POP x -> Bool.False |
---|
3739 | | XCH (x, x0) -> Bool.False |
---|
3740 | | XCHD (x, x0) -> Bool.False |
---|
3741 | | RET -> Bool.False |
---|
3742 | | RETI -> Bool.False |
---|
3743 | | NOP -> Bool.False |
---|
3744 | | JMP x -> Bool.False) |
---|
3745 | | ANL arg -> |
---|
3746 | (match j with |
---|
3747 | | ADD (x, x0) -> Bool.False |
---|
3748 | | ADDC (x, x0) -> Bool.False |
---|
3749 | | SUBB (x, x0) -> Bool.False |
---|
3750 | | INC x -> Bool.False |
---|
3751 | | DEC x -> Bool.False |
---|
3752 | | MUL (x, x0) -> Bool.False |
---|
3753 | | DIV (x, x0) -> Bool.False |
---|
3754 | | DA x -> Bool.False |
---|
3755 | | JC x -> Bool.False |
---|
3756 | | JNC x -> Bool.False |
---|
3757 | | JB (x, x0) -> Bool.False |
---|
3758 | | JNB (x, x0) -> Bool.False |
---|
3759 | | JBC (x, x0) -> Bool.False |
---|
3760 | | JZ x -> Bool.False |
---|
3761 | | JNZ x -> Bool.False |
---|
3762 | | CJNE (x, x0) -> Bool.False |
---|
3763 | | DJNZ (x, x0) -> Bool.False |
---|
3764 | | ANL arg' -> |
---|
3765 | let prod_eq_left1 = |
---|
3766 | Util.eq_prod (fun h h1 -> |
---|
3767 | eq_addressing_mode |
---|
3768 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
3769 | Vector.VEmpty)) h) |
---|
3770 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
3771 | Vector.VEmpty)) h1)) (fun h h1 -> |
---|
3772 | eq_addressing_mode |
---|
3773 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) |
---|
3774 | (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, |
---|
3775 | (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons |
---|
3776 | ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Data, |
---|
3777 | Vector.VEmpty)))))))) h) |
---|
3778 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) |
---|
3779 | (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, |
---|
3780 | (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons |
---|
3781 | ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Data, |
---|
3782 | Vector.VEmpty)))))))) h1)) |
---|
3783 | in |
---|
3784 | let prod_eq_left2 = |
---|
3785 | Util.eq_prod (fun h h1 -> |
---|
3786 | eq_addressing_mode |
---|
3787 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct, |
---|
3788 | Vector.VEmpty)) h) |
---|
3789 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct, |
---|
3790 | Vector.VEmpty)) h1)) (fun h h1 -> |
---|
3791 | eq_addressing_mode |
---|
3792 | (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S |
---|
3793 | Nat.O), Acc_a, (Vector.VCons (Nat.O, Data, Vector.VEmpty)))) |
---|
3794 | h) |
---|
3795 | (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S |
---|
3796 | Nat.O), Acc_a, (Vector.VCons (Nat.O, Data, Vector.VEmpty)))) |
---|
3797 | h1)) |
---|
3798 | in |
---|
3799 | let prod_eq_left = Util.eq_sum prod_eq_left1 prod_eq_left2 in |
---|
3800 | let prod_eq_right = |
---|
3801 | Util.eq_prod (fun h h1 -> |
---|
3802 | eq_addressing_mode |
---|
3803 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Carry, |
---|
3804 | Vector.VEmpty)) h) |
---|
3805 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Carry, |
---|
3806 | Vector.VEmpty)) h1)) (fun h h1 -> |
---|
3807 | eq_addressing_mode |
---|
3808 | (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S |
---|
3809 | Nat.O), Bit_addr, (Vector.VCons (Nat.O, N_bit_addr, |
---|
3810 | Vector.VEmpty)))) h) |
---|
3811 | (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S |
---|
3812 | Nat.O), Bit_addr, (Vector.VCons (Nat.O, N_bit_addr, |
---|
3813 | Vector.VEmpty)))) h1)) |
---|
3814 | in |
---|
3815 | let sum_eq = Util.eq_sum prod_eq_left prod_eq_right in sum_eq arg arg' |
---|
3816 | | ORL x -> Bool.False |
---|
3817 | | XRL x -> Bool.False |
---|
3818 | | CLR x -> Bool.False |
---|
3819 | | CPL x -> Bool.False |
---|
3820 | | RL x -> Bool.False |
---|
3821 | | RLC x -> Bool.False |
---|
3822 | | RR x -> Bool.False |
---|
3823 | | RRC x -> Bool.False |
---|
3824 | | SWAP x -> Bool.False |
---|
3825 | | MOV x -> Bool.False |
---|
3826 | | MOVX x -> Bool.False |
---|
3827 | | SETB x -> Bool.False |
---|
3828 | | PUSH x -> Bool.False |
---|
3829 | | POP x -> Bool.False |
---|
3830 | | XCH (x, x0) -> Bool.False |
---|
3831 | | XCHD (x, x0) -> Bool.False |
---|
3832 | | RET -> Bool.False |
---|
3833 | | RETI -> Bool.False |
---|
3834 | | NOP -> Bool.False |
---|
3835 | | JMP x -> Bool.False) |
---|
3836 | | ORL arg -> |
---|
3837 | (match j with |
---|
3838 | | ADD (x, x0) -> Bool.False |
---|
3839 | | ADDC (x, x0) -> Bool.False |
---|
3840 | | SUBB (x, x0) -> Bool.False |
---|
3841 | | INC x -> Bool.False |
---|
3842 | | DEC x -> Bool.False |
---|
3843 | | MUL (x, x0) -> Bool.False |
---|
3844 | | DIV (x, x0) -> Bool.False |
---|
3845 | | DA x -> Bool.False |
---|
3846 | | JC x -> Bool.False |
---|
3847 | | JNC x -> Bool.False |
---|
3848 | | JB (x, x0) -> Bool.False |
---|
3849 | | JNB (x, x0) -> Bool.False |
---|
3850 | | JBC (x, x0) -> Bool.False |
---|
3851 | | JZ x -> Bool.False |
---|
3852 | | JNZ x -> Bool.False |
---|
3853 | | CJNE (x, x0) -> Bool.False |
---|
3854 | | DJNZ (x, x0) -> Bool.False |
---|
3855 | | ANL x -> Bool.False |
---|
3856 | | ORL arg' -> |
---|
3857 | let prod_eq_left1 = |
---|
3858 | Util.eq_prod (fun h h1 -> |
---|
3859 | eq_addressing_mode |
---|
3860 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
3861 | Vector.VEmpty)) h) |
---|
3862 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
3863 | Vector.VEmpty)) h1)) (fun h h1 -> |
---|
3864 | eq_addressing_mode |
---|
3865 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) |
---|
3866 | (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, |
---|
3867 | (Vector.VCons ((Nat.S (Nat.S Nat.O)), Data, (Vector.VCons |
---|
3868 | ((Nat.S Nat.O), Direct, (Vector.VCons (Nat.O, Indirect, |
---|
3869 | Vector.VEmpty)))))))) h) |
---|
3870 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) |
---|
3871 | (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, |
---|
3872 | (Vector.VCons ((Nat.S (Nat.S Nat.O)), Data, (Vector.VCons |
---|
3873 | ((Nat.S Nat.O), Direct, (Vector.VCons (Nat.O, Indirect, |
---|
3874 | Vector.VEmpty)))))))) h1)) |
---|
3875 | in |
---|
3876 | let prod_eq_left2 = |
---|
3877 | Util.eq_prod (fun h h1 -> |
---|
3878 | eq_addressing_mode |
---|
3879 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct, |
---|
3880 | Vector.VEmpty)) h) |
---|
3881 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct, |
---|
3882 | Vector.VEmpty)) h1)) (fun h h1 -> |
---|
3883 | eq_addressing_mode |
---|
3884 | (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S |
---|
3885 | Nat.O), Acc_a, (Vector.VCons (Nat.O, Data, Vector.VEmpty)))) |
---|
3886 | h) |
---|
3887 | (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S |
---|
3888 | Nat.O), Acc_a, (Vector.VCons (Nat.O, Data, Vector.VEmpty)))) |
---|
3889 | h1)) |
---|
3890 | in |
---|
3891 | let prod_eq_left = Util.eq_sum prod_eq_left1 prod_eq_left2 in |
---|
3892 | let prod_eq_right = |
---|
3893 | Util.eq_prod (fun h h1 -> |
---|
3894 | eq_addressing_mode |
---|
3895 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Carry, |
---|
3896 | Vector.VEmpty)) h) |
---|
3897 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Carry, |
---|
3898 | Vector.VEmpty)) h1)) (fun h h1 -> |
---|
3899 | eq_addressing_mode |
---|
3900 | (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S |
---|
3901 | Nat.O), Bit_addr, (Vector.VCons (Nat.O, N_bit_addr, |
---|
3902 | Vector.VEmpty)))) h) |
---|
3903 | (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S |
---|
3904 | Nat.O), Bit_addr, (Vector.VCons (Nat.O, N_bit_addr, |
---|
3905 | Vector.VEmpty)))) h1)) |
---|
3906 | in |
---|
3907 | let sum_eq = Util.eq_sum prod_eq_left prod_eq_right in sum_eq arg arg' |
---|
3908 | | XRL x -> Bool.False |
---|
3909 | | CLR x -> Bool.False |
---|
3910 | | CPL x -> Bool.False |
---|
3911 | | RL x -> Bool.False |
---|
3912 | | RLC x -> Bool.False |
---|
3913 | | RR x -> Bool.False |
---|
3914 | | RRC x -> Bool.False |
---|
3915 | | SWAP x -> Bool.False |
---|
3916 | | MOV x -> Bool.False |
---|
3917 | | MOVX x -> Bool.False |
---|
3918 | | SETB x -> Bool.False |
---|
3919 | | PUSH x -> Bool.False |
---|
3920 | | POP x -> Bool.False |
---|
3921 | | XCH (x, x0) -> Bool.False |
---|
3922 | | XCHD (x, x0) -> Bool.False |
---|
3923 | | RET -> Bool.False |
---|
3924 | | RETI -> Bool.False |
---|
3925 | | NOP -> Bool.False |
---|
3926 | | JMP x -> Bool.False) |
---|
3927 | | XRL arg -> |
---|
3928 | (match j with |
---|
3929 | | ADD (x, x0) -> Bool.False |
---|
3930 | | ADDC (x, x0) -> Bool.False |
---|
3931 | | SUBB (x, x0) -> Bool.False |
---|
3932 | | INC x -> Bool.False |
---|
3933 | | DEC x -> Bool.False |
---|
3934 | | MUL (x, x0) -> Bool.False |
---|
3935 | | DIV (x, x0) -> Bool.False |
---|
3936 | | DA x -> Bool.False |
---|
3937 | | JC x -> Bool.False |
---|
3938 | | JNC x -> Bool.False |
---|
3939 | | JB (x, x0) -> Bool.False |
---|
3940 | | JNB (x, x0) -> Bool.False |
---|
3941 | | JBC (x, x0) -> Bool.False |
---|
3942 | | JZ x -> Bool.False |
---|
3943 | | JNZ x -> Bool.False |
---|
3944 | | CJNE (x, x0) -> Bool.False |
---|
3945 | | DJNZ (x, x0) -> Bool.False |
---|
3946 | | ANL x -> Bool.False |
---|
3947 | | ORL x -> Bool.False |
---|
3948 | | XRL arg' -> |
---|
3949 | let prod_eq_left = |
---|
3950 | Util.eq_prod (fun h h1 -> |
---|
3951 | eq_addressing_mode |
---|
3952 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
3953 | Vector.VEmpty)) h) |
---|
3954 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
3955 | Vector.VEmpty)) h1)) (fun h h1 -> |
---|
3956 | eq_addressing_mode |
---|
3957 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) |
---|
3958 | (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Data, |
---|
3959 | (Vector.VCons ((Nat.S (Nat.S Nat.O)), Registr, (Vector.VCons |
---|
3960 | ((Nat.S Nat.O), Direct, (Vector.VCons (Nat.O, Indirect, |
---|
3961 | Vector.VEmpty)))))))) h) |
---|
3962 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) |
---|
3963 | (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Data, |
---|
3964 | (Vector.VCons ((Nat.S (Nat.S Nat.O)), Registr, (Vector.VCons |
---|
3965 | ((Nat.S Nat.O), Direct, (Vector.VCons (Nat.O, Indirect, |
---|
3966 | Vector.VEmpty)))))))) h1)) |
---|
3967 | in |
---|
3968 | let prod_eq_right = |
---|
3969 | Util.eq_prod (fun h h1 -> |
---|
3970 | eq_addressing_mode |
---|
3971 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct, |
---|
3972 | Vector.VEmpty)) h) |
---|
3973 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct, |
---|
3974 | Vector.VEmpty)) h1)) (fun h h1 -> |
---|
3975 | eq_addressing_mode |
---|
3976 | (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S |
---|
3977 | Nat.O), Acc_a, (Vector.VCons (Nat.O, Data, Vector.VEmpty)))) |
---|
3978 | h) |
---|
3979 | (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S |
---|
3980 | Nat.O), Acc_a, (Vector.VCons (Nat.O, Data, Vector.VEmpty)))) |
---|
3981 | h1)) |
---|
3982 | in |
---|
3983 | let sum_eq = Util.eq_sum prod_eq_left prod_eq_right in sum_eq arg arg' |
---|
3984 | | CLR x -> Bool.False |
---|
3985 | | CPL x -> Bool.False |
---|
3986 | | RL x -> Bool.False |
---|
3987 | | RLC x -> Bool.False |
---|
3988 | | RR x -> Bool.False |
---|
3989 | | RRC x -> Bool.False |
---|
3990 | | SWAP x -> Bool.False |
---|
3991 | | MOV x -> Bool.False |
---|
3992 | | MOVX x -> Bool.False |
---|
3993 | | SETB x -> Bool.False |
---|
3994 | | PUSH x -> Bool.False |
---|
3995 | | POP x -> Bool.False |
---|
3996 | | XCH (x, x0) -> Bool.False |
---|
3997 | | XCHD (x, x0) -> Bool.False |
---|
3998 | | RET -> Bool.False |
---|
3999 | | RETI -> Bool.False |
---|
4000 | | NOP -> Bool.False |
---|
4001 | | JMP x -> Bool.False) |
---|
4002 | | CLR arg -> |
---|
4003 | (match j with |
---|
4004 | | ADD (x, x0) -> Bool.False |
---|
4005 | | ADDC (x, x0) -> Bool.False |
---|
4006 | | SUBB (x, x0) -> Bool.False |
---|
4007 | | INC x -> Bool.False |
---|
4008 | | DEC x -> Bool.False |
---|
4009 | | MUL (x, x0) -> Bool.False |
---|
4010 | | DIV (x, x0) -> Bool.False |
---|
4011 | | DA x -> Bool.False |
---|
4012 | | JC x -> Bool.False |
---|
4013 | | JNC x -> Bool.False |
---|
4014 | | JB (x, x0) -> Bool.False |
---|
4015 | | JNB (x, x0) -> Bool.False |
---|
4016 | | JBC (x, x0) -> Bool.False |
---|
4017 | | JZ x -> Bool.False |
---|
4018 | | JNZ x -> Bool.False |
---|
4019 | | CJNE (x, x0) -> Bool.False |
---|
4020 | | DJNZ (x, x0) -> Bool.False |
---|
4021 | | ANL x -> Bool.False |
---|
4022 | | ORL x -> Bool.False |
---|
4023 | | XRL x -> Bool.False |
---|
4024 | | CLR arg' -> |
---|
4025 | eq_addressing_mode |
---|
4026 | (subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S |
---|
4027 | (Nat.S Nat.O)), Acc_a, (Vector.VCons ((Nat.S Nat.O), Carry, |
---|
4028 | (Vector.VCons (Nat.O, Bit_addr, Vector.VEmpty)))))) arg) |
---|
4029 | (subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S |
---|
4030 | (Nat.S Nat.O)), Acc_a, (Vector.VCons ((Nat.S Nat.O), Carry, |
---|
4031 | (Vector.VCons (Nat.O, Bit_addr, Vector.VEmpty)))))) arg') |
---|
4032 | | CPL x -> Bool.False |
---|
4033 | | RL x -> Bool.False |
---|
4034 | | RLC x -> Bool.False |
---|
4035 | | RR x -> Bool.False |
---|
4036 | | RRC x -> Bool.False |
---|
4037 | | SWAP x -> Bool.False |
---|
4038 | | MOV x -> Bool.False |
---|
4039 | | MOVX x -> Bool.False |
---|
4040 | | SETB x -> Bool.False |
---|
4041 | | PUSH x -> Bool.False |
---|
4042 | | POP x -> Bool.False |
---|
4043 | | XCH (x, x0) -> Bool.False |
---|
4044 | | XCHD (x, x0) -> Bool.False |
---|
4045 | | RET -> Bool.False |
---|
4046 | | RETI -> Bool.False |
---|
4047 | | NOP -> Bool.False |
---|
4048 | | JMP x -> Bool.False) |
---|
4049 | | CPL arg -> |
---|
4050 | (match j with |
---|
4051 | | ADD (x, x0) -> Bool.False |
---|
4052 | | ADDC (x, x0) -> Bool.False |
---|
4053 | | SUBB (x, x0) -> Bool.False |
---|
4054 | | INC x -> Bool.False |
---|
4055 | | DEC x -> Bool.False |
---|
4056 | | MUL (x, x0) -> Bool.False |
---|
4057 | | DIV (x, x0) -> Bool.False |
---|
4058 | | DA x -> Bool.False |
---|
4059 | | JC x -> Bool.False |
---|
4060 | | JNC x -> Bool.False |
---|
4061 | | JB (x, x0) -> Bool.False |
---|
4062 | | JNB (x, x0) -> Bool.False |
---|
4063 | | JBC (x, x0) -> Bool.False |
---|
4064 | | JZ x -> Bool.False |
---|
4065 | | JNZ x -> Bool.False |
---|
4066 | | CJNE (x, x0) -> Bool.False |
---|
4067 | | DJNZ (x, x0) -> Bool.False |
---|
4068 | | ANL x -> Bool.False |
---|
4069 | | ORL x -> Bool.False |
---|
4070 | | XRL x -> Bool.False |
---|
4071 | | CLR x -> Bool.False |
---|
4072 | | CPL arg' -> |
---|
4073 | eq_addressing_mode |
---|
4074 | (subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S |
---|
4075 | (Nat.S Nat.O)), Acc_a, (Vector.VCons ((Nat.S Nat.O), Carry, |
---|
4076 | (Vector.VCons (Nat.O, Bit_addr, Vector.VEmpty)))))) arg) |
---|
4077 | (subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S |
---|
4078 | (Nat.S Nat.O)), Acc_a, (Vector.VCons ((Nat.S Nat.O), Carry, |
---|
4079 | (Vector.VCons (Nat.O, Bit_addr, Vector.VEmpty)))))) arg') |
---|
4080 | | RL x -> Bool.False |
---|
4081 | | RLC x -> Bool.False |
---|
4082 | | RR x -> Bool.False |
---|
4083 | | RRC x -> Bool.False |
---|
4084 | | SWAP x -> Bool.False |
---|
4085 | | MOV x -> Bool.False |
---|
4086 | | MOVX x -> Bool.False |
---|
4087 | | SETB x -> Bool.False |
---|
4088 | | PUSH x -> Bool.False |
---|
4089 | | POP x -> Bool.False |
---|
4090 | | XCH (x, x0) -> Bool.False |
---|
4091 | | XCHD (x, x0) -> Bool.False |
---|
4092 | | RET -> Bool.False |
---|
4093 | | RETI -> Bool.False |
---|
4094 | | NOP -> Bool.False |
---|
4095 | | JMP x -> Bool.False) |
---|
4096 | | RL arg -> |
---|
4097 | (match j with |
---|
4098 | | ADD (x, x0) -> Bool.False |
---|
4099 | | ADDC (x, x0) -> Bool.False |
---|
4100 | | SUBB (x, x0) -> Bool.False |
---|
4101 | | INC x -> Bool.False |
---|
4102 | | DEC x -> Bool.False |
---|
4103 | | MUL (x, x0) -> Bool.False |
---|
4104 | | DIV (x, x0) -> Bool.False |
---|
4105 | | DA x -> Bool.False |
---|
4106 | | JC x -> Bool.False |
---|
4107 | | JNC x -> Bool.False |
---|
4108 | | JB (x, x0) -> Bool.False |
---|
4109 | | JNB (x, x0) -> Bool.False |
---|
4110 | | JBC (x, x0) -> Bool.False |
---|
4111 | | JZ x -> Bool.False |
---|
4112 | | JNZ x -> Bool.False |
---|
4113 | | CJNE (x, x0) -> Bool.False |
---|
4114 | | DJNZ (x, x0) -> Bool.False |
---|
4115 | | ANL x -> Bool.False |
---|
4116 | | ORL x -> Bool.False |
---|
4117 | | XRL x -> Bool.False |
---|
4118 | | CLR x -> Bool.False |
---|
4119 | | CPL x -> Bool.False |
---|
4120 | | RL arg' -> |
---|
4121 | eq_addressing_mode |
---|
4122 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
4123 | Vector.VEmpty)) arg) |
---|
4124 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
4125 | Vector.VEmpty)) arg') |
---|
4126 | | RLC x -> Bool.False |
---|
4127 | | RR x -> Bool.False |
---|
4128 | | RRC x -> Bool.False |
---|
4129 | | SWAP x -> Bool.False |
---|
4130 | | MOV x -> Bool.False |
---|
4131 | | MOVX x -> Bool.False |
---|
4132 | | SETB x -> Bool.False |
---|
4133 | | PUSH x -> Bool.False |
---|
4134 | | POP x -> Bool.False |
---|
4135 | | XCH (x, x0) -> Bool.False |
---|
4136 | | XCHD (x, x0) -> Bool.False |
---|
4137 | | RET -> Bool.False |
---|
4138 | | RETI -> Bool.False |
---|
4139 | | NOP -> Bool.False |
---|
4140 | | JMP x -> Bool.False) |
---|
4141 | | RLC arg -> |
---|
4142 | (match j with |
---|
4143 | | ADD (x, x0) -> Bool.False |
---|
4144 | | ADDC (x, x0) -> Bool.False |
---|
4145 | | SUBB (x, x0) -> Bool.False |
---|
4146 | | INC x -> Bool.False |
---|
4147 | | DEC x -> Bool.False |
---|
4148 | | MUL (x, x0) -> Bool.False |
---|
4149 | | DIV (x, x0) -> Bool.False |
---|
4150 | | DA x -> Bool.False |
---|
4151 | | JC x -> Bool.False |
---|
4152 | | JNC x -> Bool.False |
---|
4153 | | JB (x, x0) -> Bool.False |
---|
4154 | | JNB (x, x0) -> Bool.False |
---|
4155 | | JBC (x, x0) -> Bool.False |
---|
4156 | | JZ x -> Bool.False |
---|
4157 | | JNZ x -> Bool.False |
---|
4158 | | CJNE (x, x0) -> Bool.False |
---|
4159 | | DJNZ (x, x0) -> Bool.False |
---|
4160 | | ANL x -> Bool.False |
---|
4161 | | ORL x -> Bool.False |
---|
4162 | | XRL x -> Bool.False |
---|
4163 | | CLR x -> Bool.False |
---|
4164 | | CPL x -> Bool.False |
---|
4165 | | RL x -> Bool.False |
---|
4166 | | RLC arg' -> |
---|
4167 | eq_addressing_mode |
---|
4168 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
4169 | Vector.VEmpty)) arg) |
---|
4170 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
4171 | Vector.VEmpty)) arg') |
---|
4172 | | RR x -> Bool.False |
---|
4173 | | RRC x -> Bool.False |
---|
4174 | | SWAP x -> Bool.False |
---|
4175 | | MOV x -> Bool.False |
---|
4176 | | MOVX x -> Bool.False |
---|
4177 | | SETB x -> Bool.False |
---|
4178 | | PUSH x -> Bool.False |
---|
4179 | | POP x -> Bool.False |
---|
4180 | | XCH (x, x0) -> Bool.False |
---|
4181 | | XCHD (x, x0) -> Bool.False |
---|
4182 | | RET -> Bool.False |
---|
4183 | | RETI -> Bool.False |
---|
4184 | | NOP -> Bool.False |
---|
4185 | | JMP x -> Bool.False) |
---|
4186 | | RR arg -> |
---|
4187 | (match j with |
---|
4188 | | ADD (x, x0) -> Bool.False |
---|
4189 | | ADDC (x, x0) -> Bool.False |
---|
4190 | | SUBB (x, x0) -> Bool.False |
---|
4191 | | INC x -> Bool.False |
---|
4192 | | DEC x -> Bool.False |
---|
4193 | | MUL (x, x0) -> Bool.False |
---|
4194 | | DIV (x, x0) -> Bool.False |
---|
4195 | | DA x -> Bool.False |
---|
4196 | | JC x -> Bool.False |
---|
4197 | | JNC x -> Bool.False |
---|
4198 | | JB (x, x0) -> Bool.False |
---|
4199 | | JNB (x, x0) -> Bool.False |
---|
4200 | | JBC (x, x0) -> Bool.False |
---|
4201 | | JZ x -> Bool.False |
---|
4202 | | JNZ x -> Bool.False |
---|
4203 | | CJNE (x, x0) -> Bool.False |
---|
4204 | | DJNZ (x, x0) -> Bool.False |
---|
4205 | | ANL x -> Bool.False |
---|
4206 | | ORL x -> Bool.False |
---|
4207 | | XRL x -> Bool.False |
---|
4208 | | CLR x -> Bool.False |
---|
4209 | | CPL x -> Bool.False |
---|
4210 | | RL x -> Bool.False |
---|
4211 | | RLC x -> Bool.False |
---|
4212 | | RR arg' -> |
---|
4213 | eq_addressing_mode |
---|
4214 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
4215 | Vector.VEmpty)) arg) |
---|
4216 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
4217 | Vector.VEmpty)) arg') |
---|
4218 | | RRC x -> Bool.False |
---|
4219 | | SWAP x -> Bool.False |
---|
4220 | | MOV x -> Bool.False |
---|
4221 | | MOVX x -> Bool.False |
---|
4222 | | SETB x -> Bool.False |
---|
4223 | | PUSH x -> Bool.False |
---|
4224 | | POP x -> Bool.False |
---|
4225 | | XCH (x, x0) -> Bool.False |
---|
4226 | | XCHD (x, x0) -> Bool.False |
---|
4227 | | RET -> Bool.False |
---|
4228 | | RETI -> Bool.False |
---|
4229 | | NOP -> Bool.False |
---|
4230 | | JMP x -> Bool.False) |
---|
4231 | | RRC arg -> |
---|
4232 | (match j with |
---|
4233 | | ADD (x, x0) -> Bool.False |
---|
4234 | | ADDC (x, x0) -> Bool.False |
---|
4235 | | SUBB (x, x0) -> Bool.False |
---|
4236 | | INC x -> Bool.False |
---|
4237 | | DEC x -> Bool.False |
---|
4238 | | MUL (x, x0) -> Bool.False |
---|
4239 | | DIV (x, x0) -> Bool.False |
---|
4240 | | DA x -> Bool.False |
---|
4241 | | JC x -> Bool.False |
---|
4242 | | JNC x -> Bool.False |
---|
4243 | | JB (x, x0) -> Bool.False |
---|
4244 | | JNB (x, x0) -> Bool.False |
---|
4245 | | JBC (x, x0) -> Bool.False |
---|
4246 | | JZ x -> Bool.False |
---|
4247 | | JNZ x -> Bool.False |
---|
4248 | | CJNE (x, x0) -> Bool.False |
---|
4249 | | DJNZ (x, x0) -> Bool.False |
---|
4250 | | ANL x -> Bool.False |
---|
4251 | | ORL x -> Bool.False |
---|
4252 | | XRL x -> Bool.False |
---|
4253 | | CLR x -> Bool.False |
---|
4254 | | CPL x -> Bool.False |
---|
4255 | | RL x -> Bool.False |
---|
4256 | | RLC x -> Bool.False |
---|
4257 | | RR x -> Bool.False |
---|
4258 | | RRC arg' -> |
---|
4259 | eq_addressing_mode |
---|
4260 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
4261 | Vector.VEmpty)) arg) |
---|
4262 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
4263 | Vector.VEmpty)) arg') |
---|
4264 | | SWAP x -> Bool.False |
---|
4265 | | MOV x -> Bool.False |
---|
4266 | | MOVX x -> Bool.False |
---|
4267 | | SETB x -> Bool.False |
---|
4268 | | PUSH x -> Bool.False |
---|
4269 | | POP x -> Bool.False |
---|
4270 | | XCH (x, x0) -> Bool.False |
---|
4271 | | XCHD (x, x0) -> Bool.False |
---|
4272 | | RET -> Bool.False |
---|
4273 | | RETI -> Bool.False |
---|
4274 | | NOP -> Bool.False |
---|
4275 | | JMP x -> Bool.False) |
---|
4276 | | SWAP arg -> |
---|
4277 | (match j with |
---|
4278 | | ADD (x, x0) -> Bool.False |
---|
4279 | | ADDC (x, x0) -> Bool.False |
---|
4280 | | SUBB (x, x0) -> Bool.False |
---|
4281 | | INC x -> Bool.False |
---|
4282 | | DEC x -> Bool.False |
---|
4283 | | MUL (x, x0) -> Bool.False |
---|
4284 | | DIV (x, x0) -> Bool.False |
---|
4285 | | DA x -> Bool.False |
---|
4286 | | JC x -> Bool.False |
---|
4287 | | JNC x -> Bool.False |
---|
4288 | | JB (x, x0) -> Bool.False |
---|
4289 | | JNB (x, x0) -> Bool.False |
---|
4290 | | JBC (x, x0) -> Bool.False |
---|
4291 | | JZ x -> Bool.False |
---|
4292 | | JNZ x -> Bool.False |
---|
4293 | | CJNE (x, x0) -> Bool.False |
---|
4294 | | DJNZ (x, x0) -> Bool.False |
---|
4295 | | ANL x -> Bool.False |
---|
4296 | | ORL x -> Bool.False |
---|
4297 | | XRL x -> Bool.False |
---|
4298 | | CLR x -> Bool.False |
---|
4299 | | CPL x -> Bool.False |
---|
4300 | | RL x -> Bool.False |
---|
4301 | | RLC x -> Bool.False |
---|
4302 | | RR x -> Bool.False |
---|
4303 | | RRC x -> Bool.False |
---|
4304 | | SWAP arg' -> |
---|
4305 | eq_addressing_mode |
---|
4306 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
4307 | Vector.VEmpty)) arg) |
---|
4308 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
4309 | Vector.VEmpty)) arg') |
---|
4310 | | MOV x -> Bool.False |
---|
4311 | | MOVX x -> Bool.False |
---|
4312 | | SETB x -> Bool.False |
---|
4313 | | PUSH x -> Bool.False |
---|
4314 | | POP x -> Bool.False |
---|
4315 | | XCH (x, x0) -> Bool.False |
---|
4316 | | XCHD (x, x0) -> Bool.False |
---|
4317 | | RET -> Bool.False |
---|
4318 | | RETI -> Bool.False |
---|
4319 | | NOP -> Bool.False |
---|
4320 | | JMP x -> Bool.False) |
---|
4321 | | MOV arg -> |
---|
4322 | (match j with |
---|
4323 | | ADD (x, x0) -> Bool.False |
---|
4324 | | ADDC (x, x0) -> Bool.False |
---|
4325 | | SUBB (x, x0) -> Bool.False |
---|
4326 | | INC x -> Bool.False |
---|
4327 | | DEC x -> Bool.False |
---|
4328 | | MUL (x, x0) -> Bool.False |
---|
4329 | | DIV (x, x0) -> Bool.False |
---|
4330 | | DA x -> Bool.False |
---|
4331 | | JC x -> Bool.False |
---|
4332 | | JNC x -> Bool.False |
---|
4333 | | JB (x, x0) -> Bool.False |
---|
4334 | | JNB (x, x0) -> Bool.False |
---|
4335 | | JBC (x, x0) -> Bool.False |
---|
4336 | | JZ x -> Bool.False |
---|
4337 | | JNZ x -> Bool.False |
---|
4338 | | CJNE (x, x0) -> Bool.False |
---|
4339 | | DJNZ (x, x0) -> Bool.False |
---|
4340 | | ANL x -> Bool.False |
---|
4341 | | ORL x -> Bool.False |
---|
4342 | | XRL x -> Bool.False |
---|
4343 | | CLR x -> Bool.False |
---|
4344 | | CPL x -> Bool.False |
---|
4345 | | RL x -> Bool.False |
---|
4346 | | RLC x -> Bool.False |
---|
4347 | | RR x -> Bool.False |
---|
4348 | | RRC x -> Bool.False |
---|
4349 | | SWAP x -> Bool.False |
---|
4350 | | MOV arg' -> |
---|
4351 | let prod_eq_6 = |
---|
4352 | Util.eq_prod (fun h h1 -> |
---|
4353 | eq_addressing_mode |
---|
4354 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
4355 | Vector.VEmpty)) h) |
---|
4356 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
4357 | Vector.VEmpty)) h1)) (fun h h1 -> |
---|
4358 | eq_addressing_mode |
---|
4359 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) |
---|
4360 | (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, |
---|
4361 | (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons |
---|
4362 | ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Data, |
---|
4363 | Vector.VEmpty)))))))) h) |
---|
4364 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) |
---|
4365 | (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, |
---|
4366 | (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons |
---|
4367 | ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Data, |
---|
4368 | Vector.VEmpty)))))))) h1)) |
---|
4369 | in |
---|
4370 | let prod_eq_5 = |
---|
4371 | Util.eq_prod (fun h h1 -> |
---|
4372 | eq_addressing_mode |
---|
4373 | (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S |
---|
4374 | Nat.O), Registr, (Vector.VCons (Nat.O, Indirect, |
---|
4375 | Vector.VEmpty)))) h) |
---|
4376 | (subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S |
---|
4377 | Nat.O), Registr, (Vector.VCons (Nat.O, Indirect, |
---|
4378 | Vector.VEmpty)))) h1)) (fun h h1 -> |
---|
4379 | eq_addressing_mode |
---|
4380 | (subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons |
---|
4381 | ((Nat.S (Nat.S Nat.O)), Acc_a, (Vector.VCons ((Nat.S Nat.O), |
---|
4382 | Direct, (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))) h) |
---|
4383 | (subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons |
---|
4384 | ((Nat.S (Nat.S Nat.O)), Acc_a, (Vector.VCons ((Nat.S Nat.O), |
---|
4385 | Direct, (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))) h1)) |
---|
4386 | in |
---|
4387 | let prod_eq_4 = |
---|
4388 | Util.eq_prod (fun h h1 -> |
---|
4389 | eq_addressing_mode |
---|
4390 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct, |
---|
4391 | Vector.VEmpty)) h) |
---|
4392 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Direct, |
---|
4393 | Vector.VEmpty)) h1)) (fun h h1 -> |
---|
4394 | eq_addressing_mode |
---|
4395 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) |
---|
4396 | (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Acc_a, |
---|
4397 | (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, |
---|
4398 | (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons |
---|
4399 | ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Data, |
---|
4400 | Vector.VEmpty)))))))))) h) |
---|
4401 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) |
---|
4402 | (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Acc_a, |
---|
4403 | (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, |
---|
4404 | (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons |
---|
4405 | ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Data, |
---|
4406 | Vector.VEmpty)))))))))) h1)) |
---|
4407 | in |
---|
4408 | let prod_eq_3 = |
---|
4409 | Util.eq_prod (fun h h1 -> |
---|
4410 | eq_addressing_mode |
---|
4411 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Dptr, |
---|
4412 | Vector.VEmpty)) h) |
---|
4413 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Dptr, |
---|
4414 | Vector.VEmpty)) h1)) (fun h h1 -> |
---|
4415 | eq_addressing_mode |
---|
|
---|