source: extracted/aSM.mli @ 2746

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 57.2 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 'x1 dpi1__o__subaddressing_mode = subaddressing_mode
387
388type eject__o__subaddressing_mode = subaddressing_mode
389
390val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__inject :
391  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
392  addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) Types.dPair
393  -> subaddressing_mode Types.sig0
394
395val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
396  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
397  addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) Types.dPair
398  -> addressing_mode Types.sig0
399
400val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel :
401  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
402  addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) Types.dPair
403  -> addressing_mode
404
405val eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__inject :
406  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
407  addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 ->
408  subaddressing_mode Types.sig0
409
410val eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
411  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
412  addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 ->
413  addressing_mode Types.sig0
414
415val eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel :
416  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
417  addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 ->
418  addressing_mode
419
420val subaddressing_modeel__o__mk_subaddressing_mode__o__inject :
421  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
422  addressing_mode_tag Vector.vector -> subaddressing_mode ->
423  subaddressing_mode Types.sig0
424
425val subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
426  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
427  addressing_mode_tag Vector.vector -> subaddressing_mode -> addressing_mode
428  Types.sig0
429
430val subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel :
431  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
432  addressing_mode_tag Vector.vector -> subaddressing_mode -> addressing_mode
433
434val dpi1__o__mk_subaddressing_mode__o__inject :
435  Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
436  Vector.vector -> subaddressing_mode Types.sig0
437
438val dpi1__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
439  Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
440  Vector.vector -> addressing_mode Types.sig0
441
442val dpi1__o__mk_subaddressing_mode__o__subaddressing_modeel :
443  Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
444  Vector.vector -> addressing_mode
445
446val eject__o__mk_subaddressing_mode__o__inject :
447  Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag Vector.vector
448  -> subaddressing_mode Types.sig0
449
450val eject__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
451  Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag Vector.vector
452  -> addressing_mode Types.sig0
453
454val eject__o__mk_subaddressing_mode__o__subaddressing_modeel :
455  Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag Vector.vector
456  -> addressing_mode
457
458val mk_subaddressing_mode__o__subaddressing_modeel :
459  Nat.nat -> addressing_mode -> addressing_mode_tag Vector.vector ->
460  addressing_mode
461
462val mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
463  Nat.nat -> addressing_mode -> addressing_mode_tag Vector.vector ->
464  addressing_mode Types.sig0
465
466val mk_subaddressing_mode__o__inject :
467  Nat.nat -> addressing_mode -> addressing_mode_tag Vector.vector ->
468  subaddressing_mode Types.sig0
469
470val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode :
471  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
472  addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) Types.dPair
473  -> subaddressing_mode
474
475val eject__o__subaddressing_modeel__o__mk_subaddressing_mode :
476  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
477  addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 ->
478  subaddressing_mode
479
480val subaddressing_modeel__o__mk_subaddressing_mode :
481  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
482  addressing_mode_tag Vector.vector -> subaddressing_mode ->
483  subaddressing_mode
484
485val dpi1__o__mk_subaddressing_mode :
486  Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
487  Vector.vector -> subaddressing_mode
488
489val eject__o__mk_subaddressing_mode :
490  Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag Vector.vector
491  -> subaddressing_mode
492
493type subaddressing_mode_elim_type = __
494
495type 'a preinstruction =
496| ADD of subaddressing_mode * subaddressing_mode
497| ADDC of subaddressing_mode * subaddressing_mode
498| SUBB of subaddressing_mode * subaddressing_mode
499| INC of subaddressing_mode
500| DEC of subaddressing_mode
501| MUL of subaddressing_mode * subaddressing_mode
502| DIV of subaddressing_mode * subaddressing_mode
503| DA of subaddressing_mode
504| JC of 'a
505| JNC of 'a
506| JB of subaddressing_mode * 'a
507| JNB of subaddressing_mode * 'a
508| JBC of subaddressing_mode * 'a
509| JZ of 'a
510| JNZ of 'a
511| CJNE of ((subaddressing_mode, subaddressing_mode) Types.prod,
512          (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum * 
513   'a
514| DJNZ of subaddressing_mode * 'a
515| ANL of (((subaddressing_mode, subaddressing_mode) Types.prod,
516         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
517         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
518| ORL of (((subaddressing_mode, subaddressing_mode) Types.prod,
519         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
520         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
521| XRL of ((subaddressing_mode, subaddressing_mode) Types.prod,
522         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
523| CLR of subaddressing_mode
524| CPL of subaddressing_mode
525| RL of subaddressing_mode
526| RLC of subaddressing_mode
527| RR of subaddressing_mode
528| RRC of subaddressing_mode
529| SWAP of subaddressing_mode
530| MOV of ((((((subaddressing_mode, subaddressing_mode) Types.prod,
531         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
532         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
533         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
534         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
535         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
536| MOVX of ((subaddressing_mode, subaddressing_mode) Types.prod,
537          (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
538| SETB of subaddressing_mode
539| PUSH of subaddressing_mode
540| POP of subaddressing_mode
541| XCH of subaddressing_mode * subaddressing_mode
542| XCHD of subaddressing_mode * subaddressing_mode
543| RET
544| RETI
545| NOP
546| JMP of subaddressing_mode
547
548val preinstruction_rect_Type4 :
549  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
550  subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
551  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
552  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
553  subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
554  -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
555  (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
556  ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
557  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
558  -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
559  ((((subaddressing_mode, subaddressing_mode) Types.prod,
560  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
561  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
562  ((((subaddressing_mode, subaddressing_mode) Types.prod,
563  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
564  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
565  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
566  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
567  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
568  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
569  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
570  (((((((subaddressing_mode, subaddressing_mode) Types.prod,
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,
574  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
575  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
576  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
577  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
578  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
579  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
580  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
581  'a2) -> 'a1 preinstruction -> 'a2
582
583val preinstruction_rect_Type5 :
584  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
585  subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
586  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
587  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
588  subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
589  -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
590  (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
591  ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
592  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
593  -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
594  ((((subaddressing_mode, subaddressing_mode) Types.prod,
595  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
596  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
597  ((((subaddressing_mode, subaddressing_mode) Types.prod,
598  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
599  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
600  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
601  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
602  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
603  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
604  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
605  (((((((subaddressing_mode, subaddressing_mode) Types.prod,
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,
609  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
610  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
611  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
612  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
613  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
614  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
615  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
616  'a2) -> 'a1 preinstruction -> 'a2
617
618val preinstruction_rect_Type3 :
619  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
620  subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
621  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
622  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
623  subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
624  -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
625  (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
626  ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
627  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
628  -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
629  ((((subaddressing_mode, subaddressing_mode) Types.prod,
630  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
631  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
632  ((((subaddressing_mode, subaddressing_mode) Types.prod,
633  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
634  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
635  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
636  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
637  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
638  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
639  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
640  (((((((subaddressing_mode, subaddressing_mode) Types.prod,
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,
644  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
645  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
646  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
647  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
648  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
649  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
650  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
651  'a2) -> 'a1 preinstruction -> 'a2
652
653val preinstruction_rect_Type2 :
654  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
655  subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
656  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
657  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
658  subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
659  -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
660  (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
661  ('a1 -> '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 -> 'a2) ->
667  ((((subaddressing_mode, subaddressing_mode) Types.prod,
668  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
669  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
670  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
671  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
672  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
673  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
674  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
675  (((((((subaddressing_mode, subaddressing_mode) Types.prod,
676  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
677  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
678  (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 -> 'a2) ->
681  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
682  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
683  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
684  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
685  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
686  'a2) -> 'a1 preinstruction -> 'a2
687
688val preinstruction_rect_Type1 :
689  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
690  subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
691  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
692  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
693  subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
694  -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
695  (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
696  ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
697  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
698  -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
699  ((((subaddressing_mode, subaddressing_mode) Types.prod,
700  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
701  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> '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 -> 'a2) ->
705  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
706  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
707  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
708  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
709  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
710  (((((((subaddressing_mode, subaddressing_mode) Types.prod,
711  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
712  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
713  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
714  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
715  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
716  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
717  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
718  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
719  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
720  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
721  'a2) -> 'a1 preinstruction -> 'a2
722
723val preinstruction_rect_Type0 :
724  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
725  subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
726  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
727  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
728  subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
729  -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
730  (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
731  ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
732  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
733  -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
734  ((((subaddressing_mode, subaddressing_mode) Types.prod,
735  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
736  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
737  ((((subaddressing_mode, subaddressing_mode) Types.prod,
738  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
739  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
740  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
741  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
742  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
743  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
744  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
745  (((((((subaddressing_mode, subaddressing_mode) Types.prod,
746  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
747  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
748  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
749  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
750  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
751  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
752  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
753  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
754  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
755  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
756  'a2) -> 'a1 preinstruction -> 'a2
757
758val preinstruction_inv_rect_Type4 :
759  'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
760  'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
761  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
762  (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
763  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
764  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
765  (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
766  'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode ->
767  'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 -> __
768  -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
769  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
770  -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) ->
771  ((((subaddressing_mode, subaddressing_mode) Types.prod,
772  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
773  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
774  'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
775  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
776  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
777  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
778  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
779  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
780  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
781  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
782  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
783  subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
784  Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod)
785  Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
786  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
787  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
788  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
789  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
790  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
791  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
792  subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
793  subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
794  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
795
796val preinstruction_inv_rect_Type3 :
797  'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
798  'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
799  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
800  (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
801  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
802  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
803  (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
804  'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode ->
805  'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 -> __
806  -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
807  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
808  -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) ->
809  ((((subaddressing_mode, subaddressing_mode) Types.prod,
810  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
811  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
812  'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
813  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
814  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
815  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
816  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
817  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
818  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
819  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
820  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
821  subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
822  Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod)
823  Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
824  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
825  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
826  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
827  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
828  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
829  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
830  subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
831  subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
832  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
833
834val preinstruction_inv_rect_Type2 :
835  'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
836  'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
837  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
838  (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
839  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
840  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
841  (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
842  'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode ->
843  'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 -> __
844  -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
845  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
846  -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) ->
847  ((((subaddressing_mode, subaddressing_mode) Types.prod,
848  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
849  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
850  'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
851  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
852  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
853  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
854  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
855  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
856  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
857  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
858  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
859  subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
860  Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod)
861  Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
862  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
863  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
864  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
865  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
866  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
867  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
868  subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
869  subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
870  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
871
872val preinstruction_inv_rect_Type1 :
873  'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
874  'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
875  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
876  (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
877  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
878  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
879  (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
880  'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode ->
881  'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 -> __
882  -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
883  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
884  -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) ->
885  ((((subaddressing_mode, subaddressing_mode) Types.prod,
886  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
887  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
888  'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
889  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
890  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
891  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
892  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
893  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
894  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
895  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
896  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
897  subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
898  Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod)
899  Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
900  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
901  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
902  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
903  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
904  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
905  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
906  subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
907  subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
908  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
909
910val preinstruction_inv_rect_Type0 :
911  'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
912  'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
913  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
914  (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
915  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
916  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
917  (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
918  'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode ->
919  'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 -> __
920  -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
921  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
922  -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) ->
923  ((((subaddressing_mode, subaddressing_mode) Types.prod,
924  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
925  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
926  'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
927  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
928  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
929  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
930  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
931  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
932  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
933  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
934  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
935  subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
936  Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod)
937  Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
938  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
939  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
940  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
941  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
942  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
943  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
944  subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
945  subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
946  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
947
948val preinstruction_discr : 'a1 preinstruction -> 'a1 preinstruction -> __
949
950val preinstruction_jmdiscr : 'a1 preinstruction -> 'a1 preinstruction -> __
951
952val eq_preinstruction :
953  subaddressing_mode preinstruction -> subaddressing_mode preinstruction ->
954  Bool.bool
955
956type instruction =
957| ACALL of subaddressing_mode
958| LCALL of subaddressing_mode
959| AJMP of subaddressing_mode
960| LJMP of subaddressing_mode
961| SJMP of subaddressing_mode
962| MOVC of subaddressing_mode * subaddressing_mode
963| RealInstruction of subaddressing_mode preinstruction
964
965val instruction_rect_Type4 :
966  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
967  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
968  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
969  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
970
971val instruction_rect_Type5 :
972  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
973  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
974  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
975  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
976
977val instruction_rect_Type3 :
978  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
979  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
980  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
981  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
982
983val instruction_rect_Type2 :
984  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
985  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
986  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
987  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
988
989val instruction_rect_Type1 :
990  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
991  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
992  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
993  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
994
995val instruction_rect_Type0 :
996  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
997  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
998  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
999  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
1000
1001val instruction_inv_rect_Type4 :
1002  instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1003  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1004  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1005  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
1006  __ -> 'a1) -> 'a1
1007
1008val instruction_inv_rect_Type3 :
1009  instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1010  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1011  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1012  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
1013  __ -> 'a1) -> 'a1
1014
1015val instruction_inv_rect_Type2 :
1016  instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1017  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1018  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1019  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
1020  __ -> 'a1) -> 'a1
1021
1022val instruction_inv_rect_Type1 :
1023  instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1024  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1025  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1026  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
1027  __ -> 'a1) -> 'a1
1028
1029val instruction_inv_rect_Type0 :
1030  instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1031  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1032  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1033  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
1034  __ -> 'a1) -> 'a1
1035
1036val instruction_discr : instruction -> instruction -> __
1037
1038val instruction_jmdiscr : instruction -> instruction -> __
1039
1040val dpi1__o__RealInstruction__o__inject :
1041  (subaddressing_mode preinstruction, 'a1) Types.dPair -> instruction
1042  Types.sig0
1043
1044val eject__o__RealInstruction__o__inject :
1045  subaddressing_mode preinstruction Types.sig0 -> instruction Types.sig0
1046
1047val realInstruction__o__inject :
1048  subaddressing_mode preinstruction -> instruction Types.sig0
1049
1050val dpi1__o__RealInstruction :
1051  (subaddressing_mode preinstruction, 'a1) Types.dPair -> instruction
1052
1053val eject__o__RealInstruction :
1054  subaddressing_mode preinstruction Types.sig0 -> instruction
1055
1056val eq_instruction : instruction -> instruction -> Bool.bool
1057
1058type word_side =
1059| HIGH
1060| LOW
1061
1062val word_side_rect_Type4 : 'a1 -> 'a1 -> word_side -> 'a1
1063
1064val word_side_rect_Type5 : 'a1 -> 'a1 -> word_side -> 'a1
1065
1066val word_side_rect_Type3 : 'a1 -> 'a1 -> word_side -> 'a1
1067
1068val word_side_rect_Type2 : 'a1 -> 'a1 -> word_side -> 'a1
1069
1070val word_side_rect_Type1 : 'a1 -> 'a1 -> word_side -> 'a1
1071
1072val word_side_rect_Type0 : 'a1 -> 'a1 -> word_side -> 'a1
1073
1074val word_side_inv_rect_Type4 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
1075
1076val word_side_inv_rect_Type3 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
1077
1078val word_side_inv_rect_Type2 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
1079
1080val word_side_inv_rect_Type1 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
1081
1082val word_side_inv_rect_Type0 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
1083
1084val word_side_discr : word_side -> word_side -> __
1085
1086val word_side_jmdiscr : word_side -> word_side -> __
1087
1088type pseudo_instruction =
1089| Instruction of identifier0 preinstruction
1090| Comment of String.string
1091| Cost of CostLabel.costlabel
1092| Jmp of identifier0
1093| Jnz of subaddressing_mode * identifier0 * identifier0
1094| MovSuccessor of subaddressing_mode * word_side * identifier0
1095| Call of identifier0
1096| Mov of subaddressing_mode * identifier0
1097
1098val pseudo_instruction_rect_Type4 :
1099  (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
1100  (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode
1101  -> identifier0 -> identifier0 -> 'a1) -> (subaddressing_mode -> word_side
1102  -> identifier0 -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode ->
1103  identifier0 -> 'a1) -> pseudo_instruction -> 'a1
1104
1105val pseudo_instruction_rect_Type5 :
1106  (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
1107  (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode
1108  -> identifier0 -> identifier0 -> 'a1) -> (subaddressing_mode -> word_side
1109  -> identifier0 -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode ->
1110  identifier0 -> 'a1) -> pseudo_instruction -> 'a1
1111
1112val pseudo_instruction_rect_Type3 :
1113  (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
1114  (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode
1115  -> identifier0 -> identifier0 -> 'a1) -> (subaddressing_mode -> word_side
1116  -> identifier0 -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode ->
1117  identifier0 -> 'a1) -> pseudo_instruction -> 'a1
1118
1119val pseudo_instruction_rect_Type2 :
1120  (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
1121  (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode
1122  -> identifier0 -> identifier0 -> 'a1) -> (subaddressing_mode -> word_side
1123  -> identifier0 -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode ->
1124  identifier0 -> 'a1) -> pseudo_instruction -> 'a1
1125
1126val pseudo_instruction_rect_Type1 :
1127  (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
1128  (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode
1129  -> identifier0 -> identifier0 -> 'a1) -> (subaddressing_mode -> word_side
1130  -> identifier0 -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode ->
1131  identifier0 -> 'a1) -> pseudo_instruction -> 'a1
1132
1133val pseudo_instruction_rect_Type0 :
1134  (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
1135  (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode
1136  -> identifier0 -> identifier0 -> 'a1) -> (subaddressing_mode -> word_side
1137  -> identifier0 -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode ->
1138  identifier0 -> 'a1) -> pseudo_instruction -> 'a1
1139
1140val pseudo_instruction_inv_rect_Type4 :
1141  pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
1142  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
1143  (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
1144  identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
1145  identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
1146  (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1
1147
1148val pseudo_instruction_inv_rect_Type3 :
1149  pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
1150  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
1151  (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
1152  identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
1153  identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
1154  (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1
1155
1156val pseudo_instruction_inv_rect_Type2 :
1157  pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
1158  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
1159  (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
1160  identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
1161  identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
1162  (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1
1163
1164val pseudo_instruction_inv_rect_Type1 :
1165  pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
1166  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
1167  (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
1168  identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
1169  identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
1170  (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1
1171
1172val pseudo_instruction_inv_rect_Type0 :
1173  pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
1174  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
1175  (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
1176  identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
1177  identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
1178  (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1
1179
1180val pseudo_instruction_discr : pseudo_instruction -> pseudo_instruction -> __
1181
1182val pseudo_instruction_jmdiscr :
1183  pseudo_instruction -> pseudo_instruction -> __
1184
1185type labelled_instruction = pseudo_instruction LabelledObjects.labelled_obj
1186
1187type preamble = (identifier0, BitVector.word) Types.prod List.list
1188
1189type assembly_program = instruction List.list
1190
1191type pseudo_assembly_program =
1192  (preamble, labelled_instruction List.list) Types.prod
1193
1194val is_jump' : identifier0 preinstruction -> Bool.bool
1195
1196val is_relative_jump : pseudo_instruction -> Bool.bool
1197
1198val is_jump : pseudo_instruction -> Bool.bool
1199
1200val is_call : pseudo_instruction -> Bool.bool
1201
Note: See TracBrowser for help on using the repository browser.