source: extracted/aSM.mli @ 2717

Last change on this file since 2717 was 2717, checked in by sacerdot, 7 years ago

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 52.3 KB
Line 
1open Preamble
2
3open Extranat
4
5open Vector
6
7open Div_and_mod
8
9open Jmeq
10
11open Russell
12
13open Types
14
15open List
16
17open Util
18
19open FoldStuff
20
21open Bool
22
23open Hints_declaration
24
25open Core_notation
26
27open Pts
28
29open Logic
30
31open Relations
32
33open Nat
34
35open BitVector
36
37open Proper
38
39open PositiveMap
40
41open Deqsets
42
43open ErrorMessages
44
45open PreIdentifiers
46
47open Errors
48
49open Extralib
50
51open Setoids
52
53open Monad
54
55open Option
56
57open Lists
58
59open Positive
60
61open Identifiers
62
63open BitVectorTrie
64
65open Exp
66
67open Arithmetic
68
69open Integers
70
71open AST
72
73open CostLabel
74
75open LabelledObjects
76
77open String
78
79type identifier0 = PreIdentifiers.identifier
80
81val toASM_ident :
82  PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> identifier0
83
84type addressing_mode =
85| DIRECT of BitVector.byte
86| INDIRECT of BitVector.bit
87| EXT_INDIRECT of BitVector.bit
88| REGISTER of BitVector.bitVector
89| ACC_A
90| ACC_B
91| DPTR
92| DATA of BitVector.byte
93| DATA16 of BitVector.word
94| ACC_DPTR
95| ACC_PC
96| EXT_INDIRECT_DPTR
97| INDIRECT_DPTR
98| CARRY
99| BIT_ADDR of BitVector.byte
100| N_BIT_ADDR of BitVector.byte
101| RELATIVE of BitVector.byte
102| ADDR11 of BitVector.word11
103| ADDR16 of BitVector.word
104
105val addressing_mode_rect_Type4 :
106  (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> 'a1)
107  -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (BitVector.byte ->
108  'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
109  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (BitVector.byte ->
110  'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) ->
111  addressing_mode -> 'a1
112
113val addressing_mode_rect_Type5 :
114  (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> 'a1)
115  -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (BitVector.byte ->
116  'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
117  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (BitVector.byte ->
118  'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) ->
119  addressing_mode -> 'a1
120
121val addressing_mode_rect_Type3 :
122  (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> 'a1)
123  -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (BitVector.byte ->
124  'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
125  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (BitVector.byte ->
126  'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) ->
127  addressing_mode -> 'a1
128
129val addressing_mode_rect_Type2 :
130  (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> 'a1)
131  -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (BitVector.byte ->
132  'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
133  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (BitVector.byte ->
134  'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) ->
135  addressing_mode -> 'a1
136
137val addressing_mode_rect_Type1 :
138  (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> 'a1)
139  -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (BitVector.byte ->
140  'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
141  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (BitVector.byte ->
142  'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) ->
143  addressing_mode -> 'a1
144
145val addressing_mode_rect_Type0 :
146  (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> 'a1)
147  -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (BitVector.byte ->
148  'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
149  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (BitVector.byte ->
150  'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) ->
151  addressing_mode -> 'a1
152
153val addressing_mode_inv_rect_Type4 :
154  addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ ->
155  'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> 'a1)
156  -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
157  'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
158  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
159  (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
160  (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1
161
162val addressing_mode_inv_rect_Type3 :
163  addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ ->
164  'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> 'a1)
165  -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
166  'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
167  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
168  (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
169  (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1
170
171val addressing_mode_inv_rect_Type2 :
172  addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ ->
173  'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> 'a1)
174  -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
175  'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
176  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
177  (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
178  (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1
179
180val addressing_mode_inv_rect_Type1 :
181  addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ ->
182  'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> 'a1)
183  -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
184  'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
185  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
186  (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
187  (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1
188
189val addressing_mode_inv_rect_Type0 :
190  addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ ->
191  'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> 'a1)
192  -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
193  'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
194  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
195  (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
196  (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1
197
198val addressing_mode_discr : addressing_mode -> addressing_mode -> __
199
200val addressing_mode_jmdiscr : addressing_mode -> addressing_mode -> __
201
202val eq_addressing_mode : addressing_mode -> addressing_mode -> Bool.bool
203
204type addressing_mode_tag =
205| Direct
206| Indirect
207| Ext_indirect
208| Registr
209| Acc_a
210| Acc_b
211| Dptr
212| Data
213| Data16
214| Acc_dptr
215| Acc_pc
216| Ext_indirect_dptr
217| Indirect_dptr
218| Carry
219| Bit_addr
220| N_bit_addr
221| Relative
222| Addr11
223| Addr16
224
225val addressing_mode_tag_rect_Type4 :
226  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
227  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
228  addressing_mode_tag -> 'a1
229
230val addressing_mode_tag_rect_Type5 :
231  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
232  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
233  addressing_mode_tag -> 'a1
234
235val addressing_mode_tag_rect_Type3 :
236  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
237  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
238  addressing_mode_tag -> 'a1
239
240val addressing_mode_tag_rect_Type2 :
241  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
242  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
243  addressing_mode_tag -> 'a1
244
245val addressing_mode_tag_rect_Type1 :
246  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
247  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
248  addressing_mode_tag -> 'a1
249
250val addressing_mode_tag_rect_Type0 :
251  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
252  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
253  addressing_mode_tag -> 'a1
254
255val addressing_mode_tag_inv_rect_Type4 :
256  addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
257  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
258  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
259  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
260  'a1) -> 'a1
261
262val addressing_mode_tag_inv_rect_Type3 :
263  addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
264  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
265  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
266  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
267  'a1) -> 'a1
268
269val addressing_mode_tag_inv_rect_Type2 :
270  addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
271  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
272  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
273  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
274  'a1) -> 'a1
275
276val addressing_mode_tag_inv_rect_Type1 :
277  addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
278  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
279  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
280  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
281  'a1) -> 'a1
282
283val addressing_mode_tag_inv_rect_Type0 :
284  addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
285  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
286  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
287  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
288  'a1) -> 'a1
289
290val addressing_mode_tag_discr :
291  addressing_mode_tag -> addressing_mode_tag -> __
292
293val addressing_mode_tag_jmdiscr :
294  addressing_mode_tag -> addressing_mode_tag -> __
295
296val eq_a : addressing_mode_tag -> addressing_mode_tag -> Bool.bool
297
298type member_addressing_mode_tag = __
299
300val is_a : addressing_mode_tag -> addressing_mode -> Bool.bool
301
302val is_in :
303  Nat.nat -> addressing_mode_tag Vector.vector -> addressing_mode ->
304  Bool.bool
305
306type subaddressing_mode =
307  addressing_mode
308  (* singleton inductive, whose constructor was mk_subaddressing_mode *)
309
310val subaddressing_mode_rect_Type4 :
311  Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
312  'a1) -> subaddressing_mode -> 'a1
313
314val subaddressing_mode_rect_Type5 :
315  Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
316  'a1) -> subaddressing_mode -> 'a1
317
318val subaddressing_mode_rect_Type3 :
319  Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
320  'a1) -> subaddressing_mode -> 'a1
321
322val subaddressing_mode_rect_Type2 :
323  Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
324  'a1) -> subaddressing_mode -> 'a1
325
326val subaddressing_mode_rect_Type1 :
327  Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
328  'a1) -> subaddressing_mode -> 'a1
329
330val subaddressing_mode_rect_Type0 :
331  Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
332  'a1) -> subaddressing_mode -> 'a1
333
334val subaddressing_modeel :
335  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
336  addressing_mode
337
338val subaddressing_mode_inv_rect_Type4 :
339  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
340  (addressing_mode -> __ -> __ -> 'a1) -> 'a1
341
342val subaddressing_mode_inv_rect_Type3 :
343  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
344  (addressing_mode -> __ -> __ -> 'a1) -> 'a1
345
346val subaddressing_mode_inv_rect_Type2 :
347  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
348  (addressing_mode -> __ -> __ -> 'a1) -> 'a1
349
350val subaddressing_mode_inv_rect_Type1 :
351  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
352  (addressing_mode -> __ -> __ -> 'a1) -> 'a1
353
354val subaddressing_mode_inv_rect_Type0 :
355  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
356  (addressing_mode -> __ -> __ -> 'a1) -> 'a1
357
358val subaddressing_mode_discr :
359  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
360  subaddressing_mode -> __
361
362val subaddressing_mode_jmdiscr :
363  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
364  subaddressing_mode -> __
365
366val dpi1__o__subaddressing_modeel__o__inject :
367  Nat.nat -> addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1)
368  Types.dPair -> addressing_mode Types.sig0
369
370val eject__o__subaddressing_modeel__o__inject :
371  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode
372  Types.sig0 -> addressing_mode Types.sig0
373
374val subaddressing_modeel__o__inject :
375  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
376  addressing_mode Types.sig0
377
378val dpi1__o__subaddressing_modeel :
379  Nat.nat -> addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1)
380  Types.dPair -> addressing_mode
381
382val eject__o__subaddressing_modeel :
383  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode
384  Types.sig0 -> addressing_mode
385
386type subaddressing_mode_elim_type = __
387
388type 'a preinstruction =
389| ADD of subaddressing_mode * subaddressing_mode
390| ADDC of subaddressing_mode * subaddressing_mode
391| SUBB of subaddressing_mode * subaddressing_mode
392| INC of subaddressing_mode
393| DEC of subaddressing_mode
394| MUL of subaddressing_mode * subaddressing_mode
395| DIV of subaddressing_mode * subaddressing_mode
396| DA of subaddressing_mode
397| JC of 'a
398| JNC of 'a
399| JB of subaddressing_mode * 'a
400| JNB of subaddressing_mode * 'a
401| JBC of subaddressing_mode * 'a
402| JZ of 'a
403| JNZ of 'a
404| CJNE of ((subaddressing_mode, subaddressing_mode) Types.prod,
405          (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum * 
406   'a
407| DJNZ of subaddressing_mode * 'a
408| ANL of (((subaddressing_mode, subaddressing_mode) Types.prod,
409         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
410         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
411| ORL of (((subaddressing_mode, subaddressing_mode) Types.prod,
412         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
413         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
414| XRL of ((subaddressing_mode, subaddressing_mode) Types.prod,
415         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
416| CLR of subaddressing_mode
417| CPL of subaddressing_mode
418| RL of subaddressing_mode
419| RLC of subaddressing_mode
420| RR of subaddressing_mode
421| RRC of subaddressing_mode
422| SWAP of subaddressing_mode
423| MOV of ((((((subaddressing_mode, subaddressing_mode) Types.prod,
424         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
425         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
426         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
427         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
428         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
429| MOVX of ((subaddressing_mode, subaddressing_mode) Types.prod,
430          (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
431| SETB of subaddressing_mode
432| PUSH of subaddressing_mode
433| POP of subaddressing_mode
434| XCH of subaddressing_mode * subaddressing_mode
435| XCHD of subaddressing_mode * subaddressing_mode
436| RET
437| RETI
438| NOP
439| JMP of subaddressing_mode
440
441val preinstruction_rect_Type4 :
442  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
443  subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
444  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
445  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
446  subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
447  -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
448  (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
449  ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
450  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
451  -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
452  ((((subaddressing_mode, subaddressing_mode) Types.prod,
453  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
454  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
455  ((((subaddressing_mode, subaddressing_mode) Types.prod,
456  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
457  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
458  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
459  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
460  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
461  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
462  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
463  (((((((subaddressing_mode, subaddressing_mode) Types.prod,
464  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
465  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
466  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
467  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
468  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
469  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
470  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
471  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
472  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
473  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
474  'a2) -> 'a1 preinstruction -> 'a2
475
476val preinstruction_rect_Type5 :
477  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
478  subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
479  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
480  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
481  subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
482  -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
483  (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
484  ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
485  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
486  -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
487  ((((subaddressing_mode, subaddressing_mode) Types.prod,
488  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
489  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
490  ((((subaddressing_mode, subaddressing_mode) Types.prod,
491  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
492  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
493  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
494  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
495  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
496  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
497  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
498  (((((((subaddressing_mode, subaddressing_mode) Types.prod,
499  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
500  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
501  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
502  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
503  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
504  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
505  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
506  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
507  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
508  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
509  'a2) -> 'a1 preinstruction -> 'a2
510
511val preinstruction_rect_Type3 :
512  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
513  subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
514  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
515  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
516  subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
517  -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
518  (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
519  ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
520  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
521  -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
522  ((((subaddressing_mode, subaddressing_mode) Types.prod,
523  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
524  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
525  ((((subaddressing_mode, subaddressing_mode) Types.prod,
526  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
527  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
528  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
529  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
530  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
531  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
532  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
533  (((((((subaddressing_mode, subaddressing_mode) Types.prod,
534  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
535  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
536  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
537  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
538  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
539  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
540  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
541  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
542  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
543  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
544  'a2) -> 'a1 preinstruction -> 'a2
545
546val preinstruction_rect_Type2 :
547  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
548  subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
549  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
550  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
551  subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
552  -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
553  (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
554  ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
555  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
556  -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
557  ((((subaddressing_mode, subaddressing_mode) Types.prod,
558  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
559  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
560  ((((subaddressing_mode, subaddressing_mode) Types.prod,
561  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
562  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
563  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
564  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
565  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
566  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
567  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
568  (((((((subaddressing_mode, subaddressing_mode) Types.prod,
569  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
570  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
571  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
572  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
573  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
574  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
575  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
576  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
577  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
578  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
579  'a2) -> 'a1 preinstruction -> 'a2
580
581val preinstruction_rect_Type1 :
582  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
583  subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
584  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
585  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
586  subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
587  -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
588  (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
589  ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
590  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
591  -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
592  ((((subaddressing_mode, subaddressing_mode) Types.prod,
593  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
594  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
595  ((((subaddressing_mode, subaddressing_mode) Types.prod,
596  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
597  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
598  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
599  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
600  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
601  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
602  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
603  (((((((subaddressing_mode, subaddressing_mode) Types.prod,
604  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
605  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
606  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
607  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
608  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
609  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
610  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
611  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
612  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
613  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
614  'a2) -> 'a1 preinstruction -> 'a2
615
616val preinstruction_rect_Type0 :
617  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
618  subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
619  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
620  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
621  subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
622  -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
623  (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
624  ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
625  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
626  -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
627  ((((subaddressing_mode, subaddressing_mode) Types.prod,
628  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
629  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
630  ((((subaddressing_mode, subaddressing_mode) Types.prod,
631  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
632  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
633  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
634  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
635  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
636  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
637  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
638  (((((((subaddressing_mode, subaddressing_mode) Types.prod,
639  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
640  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
641  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
642  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
643  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
644  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
645  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
646  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
647  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
648  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
649  'a2) -> 'a1 preinstruction -> 'a2
650
651val preinstruction_inv_rect_Type4 :
652  'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
653  'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
654  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
655  (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
656  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
657  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
658  (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
659  'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode ->
660  'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 -> __
661  -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
662  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
663  -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) ->
664  ((((subaddressing_mode, subaddressing_mode) Types.prod,
665  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
666  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
667  'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
668  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
669  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
670  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
671  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
672  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
673  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
674  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
675  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
676  subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
677  Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod)
678  Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
679  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
680  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
681  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
682  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
683  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
684  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
685  subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
686  subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
687  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
688
689val preinstruction_inv_rect_Type3 :
690  'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
691  'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
692  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
693  (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
694  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
695  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
696  (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
697  'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode ->
698  'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 -> __
699  -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
700  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
701  -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) ->
702  ((((subaddressing_mode, subaddressing_mode) Types.prod,
703  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
704  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
705  'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
706  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
707  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
708  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
709  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
710  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
711  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
712  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
713  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
714  subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
715  Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod)
716  Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
717  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
718  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
719  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
720  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
721  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
722  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
723  subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
724  subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
725  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
726
727val preinstruction_inv_rect_Type2 :
728  'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
729  'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
730  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
731  (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
732  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
733  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
734  (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
735  'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode ->
736  'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 -> __
737  -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
738  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
739  -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) ->
740  ((((subaddressing_mode, subaddressing_mode) Types.prod,
741  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
742  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
743  'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
744  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
745  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
746  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
747  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
748  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
749  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
750  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
751  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
752  subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
753  Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod)
754  Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
755  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
756  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
757  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
758  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
759  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
760  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
761  subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
762  subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
763  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
764
765val preinstruction_inv_rect_Type1 :
766  'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
767  'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
768  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
769  (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
770  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
771  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
772  (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
773  'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode ->
774  'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 -> __
775  -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
776  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
777  -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) ->
778  ((((subaddressing_mode, subaddressing_mode) Types.prod,
779  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
780  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
781  'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
782  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
783  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
784  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
785  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
786  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
787  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
788  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
789  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
790  subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
791  Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod)
792  Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
793  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
794  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
795  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
796  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
797  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
798  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
799  subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
800  subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
801  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
802
803val preinstruction_inv_rect_Type0 :
804  'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
805  'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
806  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
807  (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
808  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
809  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
810  (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
811  'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode ->
812  'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 -> __
813  -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
814  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
815  -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) ->
816  ((((subaddressing_mode, subaddressing_mode) Types.prod,
817  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
818  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
819  'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
820  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
821  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
822  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
823  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
824  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
825  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
826  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
827  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
828  subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
829  Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod)
830  Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
831  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
832  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
833  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
834  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
835  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
836  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
837  subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
838  subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
839  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
840
841val preinstruction_discr : 'a1 preinstruction -> 'a1 preinstruction -> __
842
843val preinstruction_jmdiscr : 'a1 preinstruction -> 'a1 preinstruction -> __
844
845val eq_preinstruction :
846  subaddressing_mode preinstruction -> subaddressing_mode preinstruction ->
847  Bool.bool
848
849type instruction =
850| ACALL of subaddressing_mode
851| LCALL of subaddressing_mode
852| AJMP of subaddressing_mode
853| LJMP of subaddressing_mode
854| SJMP of subaddressing_mode
855| MOVC of subaddressing_mode * subaddressing_mode
856| RealInstruction of subaddressing_mode preinstruction
857
858val instruction_rect_Type4 :
859  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
860  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
861  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
862  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
863
864val instruction_rect_Type5 :
865  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
866  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
867  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
868  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
869
870val instruction_rect_Type3 :
871  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
872  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
873  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
874  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
875
876val instruction_rect_Type2 :
877  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
878  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
879  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
880  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
881
882val instruction_rect_Type1 :
883  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
884  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
885  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
886  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
887
888val instruction_rect_Type0 :
889  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
890  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
891  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
892  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
893
894val instruction_inv_rect_Type4 :
895  instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
896  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
897  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
898  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
899  __ -> 'a1) -> 'a1
900
901val instruction_inv_rect_Type3 :
902  instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
903  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
904  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
905  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
906  __ -> 'a1) -> 'a1
907
908val instruction_inv_rect_Type2 :
909  instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
910  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
911  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
912  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
913  __ -> 'a1) -> 'a1
914
915val instruction_inv_rect_Type1 :
916  instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
917  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
918  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
919  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
920  __ -> 'a1) -> 'a1
921
922val instruction_inv_rect_Type0 :
923  instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
924  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
925  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
926  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
927  __ -> 'a1) -> 'a1
928
929val instruction_discr : instruction -> instruction -> __
930
931val instruction_jmdiscr : instruction -> instruction -> __
932
933val eq_instruction : instruction -> instruction -> Bool.bool
934
935type word_side =
936| HIGH
937| LOW
938
939val word_side_rect_Type4 : 'a1 -> 'a1 -> word_side -> 'a1
940
941val word_side_rect_Type5 : 'a1 -> 'a1 -> word_side -> 'a1
942
943val word_side_rect_Type3 : 'a1 -> 'a1 -> word_side -> 'a1
944
945val word_side_rect_Type2 : 'a1 -> 'a1 -> word_side -> 'a1
946
947val word_side_rect_Type1 : 'a1 -> 'a1 -> word_side -> 'a1
948
949val word_side_rect_Type0 : 'a1 -> 'a1 -> word_side -> 'a1
950
951val word_side_inv_rect_Type4 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
952
953val word_side_inv_rect_Type3 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
954
955val word_side_inv_rect_Type2 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
956
957val word_side_inv_rect_Type1 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
958
959val word_side_inv_rect_Type0 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
960
961val word_side_discr : word_side -> word_side -> __
962
963val word_side_jmdiscr : word_side -> word_side -> __
964
965type pseudo_instruction =
966| Instruction of identifier0 preinstruction
967| Comment of String.string
968| Cost of CostLabel.costlabel
969| Jmp of identifier0
970| Jnz of subaddressing_mode * identifier0 * identifier0
971| MovSuccessor of subaddressing_mode * word_side * identifier0
972| Call of identifier0
973| Mov of subaddressing_mode * identifier0
974
975val pseudo_instruction_rect_Type4 :
976  (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
977  (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode
978  -> identifier0 -> identifier0 -> 'a1) -> (subaddressing_mode -> word_side
979  -> identifier0 -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode ->
980  identifier0 -> 'a1) -> pseudo_instruction -> 'a1
981
982val pseudo_instruction_rect_Type5 :
983  (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
984  (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode
985  -> identifier0 -> identifier0 -> 'a1) -> (subaddressing_mode -> word_side
986  -> identifier0 -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode ->
987  identifier0 -> 'a1) -> pseudo_instruction -> 'a1
988
989val pseudo_instruction_rect_Type3 :
990  (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
991  (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode
992  -> identifier0 -> identifier0 -> 'a1) -> (subaddressing_mode -> word_side
993  -> identifier0 -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode ->
994  identifier0 -> 'a1) -> pseudo_instruction -> 'a1
995
996val pseudo_instruction_rect_Type2 :
997  (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
998  (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode
999  -> identifier0 -> identifier0 -> 'a1) -> (subaddressing_mode -> word_side
1000  -> identifier0 -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode ->
1001  identifier0 -> 'a1) -> pseudo_instruction -> 'a1
1002
1003val pseudo_instruction_rect_Type1 :
1004  (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
1005  (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode
1006  -> identifier0 -> identifier0 -> 'a1) -> (subaddressing_mode -> word_side
1007  -> identifier0 -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode ->
1008  identifier0 -> 'a1) -> pseudo_instruction -> 'a1
1009
1010val pseudo_instruction_rect_Type0 :
1011  (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
1012  (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode
1013  -> identifier0 -> identifier0 -> 'a1) -> (subaddressing_mode -> word_side
1014  -> identifier0 -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode ->
1015  identifier0 -> 'a1) -> pseudo_instruction -> 'a1
1016
1017val pseudo_instruction_inv_rect_Type4 :
1018  pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
1019  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
1020  (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
1021  identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
1022  identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
1023  (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1
1024
1025val pseudo_instruction_inv_rect_Type3 :
1026  pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
1027  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
1028  (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
1029  identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
1030  identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
1031  (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1
1032
1033val pseudo_instruction_inv_rect_Type2 :
1034  pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
1035  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
1036  (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
1037  identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
1038  identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
1039  (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1
1040
1041val pseudo_instruction_inv_rect_Type1 :
1042  pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
1043  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
1044  (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
1045  identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
1046  identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
1047  (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1
1048
1049val pseudo_instruction_inv_rect_Type0 :
1050  pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
1051  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
1052  (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
1053  identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
1054  identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
1055  (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1
1056
1057val pseudo_instruction_discr : pseudo_instruction -> pseudo_instruction -> __
1058
1059val pseudo_instruction_jmdiscr :
1060  pseudo_instruction -> pseudo_instruction -> __
1061
1062type labelled_instruction = pseudo_instruction LabelledObjects.labelled_obj
1063
1064type preamble = (identifier0, BitVector.word) Types.prod List.list
1065
1066type assembly_program = instruction List.list
1067
1068type pseudo_assembly_program =
1069  (preamble, labelled_instruction List.list) Types.prod
1070
1071val is_jump' : identifier0 preinstruction -> Bool.bool
1072
1073val is_relative_jump : pseudo_instruction -> Bool.bool
1074
1075val is_jump : pseudo_instruction -> Bool.bool
1076
1077val is_call : pseudo_instruction -> Bool.bool
1078
1079val subaddressing_modeel__o__mk_subaddressing_mode:
1080 Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector -> addressing_mode_tag Vector.vector -> addressing_mode -> addressing_mode
Note: See TracBrowser for help on using the repository browser.