source: extracted/aSM.mli @ 2649

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

...

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