source: extracted/aSM.mli @ 2731

Last change on this file since 2731 was 2717, checked in by sacerdot, 8 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
RevLine 
[2601]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
[2649]43open ErrorMessages
44
[2601]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
[2717]63open BitVectorTrie
64
65open Exp
66
[2601]67open Arithmetic
68
69open Integers
70
71open AST
72
73open CostLabel
74
75open LabelledObjects
76
[2649]77open String
[2601]78
79type identifier0 = PreIdentifiers.identifier
80
[2649]81val toASM_ident :
82  PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> identifier0
[2601]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
[2717]439| JMP of subaddressing_mode
[2601]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 ->
[2717]473  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
474  'a2) -> 'a1 preinstruction -> 'a2
[2601]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 ->
[2717]508  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
509  'a2) -> 'a1 preinstruction -> 'a2
[2601]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 ->
[2717]543  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
544  'a2) -> 'a1 preinstruction -> 'a2
[2601]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 ->
[2717]578  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
579  'a2) -> 'a1 preinstruction -> 'a2
[2601]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 ->
[2717]613  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
614  'a2) -> 'a1 preinstruction -> 'a2
[2601]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 ->
[2717]648  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
649  'a2) -> 'a1 preinstruction -> 'a2
[2601]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) -> (__ ->
[2717]687  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
[2601]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) -> (__ ->
[2717]725  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
[2601]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) -> (__ ->
[2717]763  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
[2601]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) -> (__ ->
[2717]801  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
[2601]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) -> (__ ->
[2717]839  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
[2601]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) ->
[2717]861  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
862  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
[2601]863
864val instruction_rect_Type5 :
865  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
866  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
[2717]867  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
868  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
[2601]869
870val instruction_rect_Type3 :
871  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
872  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
[2717]873  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
874  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
[2601]875
876val instruction_rect_Type2 :
877  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
878  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
[2717]879  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
880  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
[2601]881
882val instruction_rect_Type1 :
883  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
884  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
[2717]885  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
886  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
[2601]887
888val instruction_rect_Type0 :
889  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
890  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
[2717]891  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
892  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
[2601]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 ->
[2717]898  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
899  __ -> 'a1) -> 'a1
[2601]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 ->
[2717]905  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
906  __ -> 'a1) -> 'a1
[2601]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 ->
[2717]912  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
913  __ -> 'a1) -> 'a1
[2601]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 ->
[2717]919  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
920  __ -> 'a1) -> 'a1
[2601]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 ->
[2717]926  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
927  __ -> 'a1) -> 'a1
[2601]928
929val instruction_discr : instruction -> instruction -> __
930
931val instruction_jmdiscr : instruction -> instruction -> __
932
933val eq_instruction : instruction -> instruction -> Bool.bool
934
[2717]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
[2601]965type pseudo_instruction =
966| Instruction of identifier0 preinstruction
967| Comment of String.string
968| Cost of CostLabel.costlabel
969| Jmp of identifier0
[2717]970| Jnz of subaddressing_mode * identifier0 * identifier0
971| MovSuccessor of subaddressing_mode * word_side * identifier0
[2601]972| Call of identifier0
973| Mov of subaddressing_mode * identifier0
974
975val pseudo_instruction_rect_Type4 :
976  (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
[2717]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
[2601]981
982val pseudo_instruction_rect_Type5 :
983  (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
[2717]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
[2601]988
989val pseudo_instruction_rect_Type3 :
990  (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
[2717]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
[2601]995
996val pseudo_instruction_rect_Type2 :
997  (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
[2717]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
[2601]1002
1003val pseudo_instruction_rect_Type1 :
1004  (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
[2717]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
[2601]1009
1010val pseudo_instruction_rect_Type0 :
1011  (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
[2717]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
[2601]1016
1017val pseudo_instruction_inv_rect_Type4 :
1018  pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
1019  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
[2717]1020  (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
1021  identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
1022  identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
[2601]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) ->
[2717]1028  (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
1029  identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
1030  identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
[2601]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) ->
[2717]1036  (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
1037  identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
1038  identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
[2601]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) ->
[2717]1044  (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
1045  identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
1046  identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
[2601]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) ->
[2717]1052  (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
1053  identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
1054  identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
[2601]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
[2717]1064type preamble = (identifier0, BitVector.word) Types.prod List.list
[2601]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.