source: driver/extracted/aSM.mli @ 3106

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

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File size: 64.5 KB
Line 
1open Preamble
2
3open Proper
4
5open PositiveMap
6
7open Deqsets
8
9open ErrorMessages
10
11open PreIdentifiers
12
13open Errors
14
15open Extralib
16
17open Setoids
18
19open Monad
20
21open Option
22
23open Div_and_mod
24
25open Jmeq
26
27open Russell
28
29open Util
30
31open List
32
33open Lists
34
35open Bool
36
37open Relations
38
39open Nat
40
41open Positive
42
43open Hints_declaration
44
45open Core_notation
46
47open Pts
48
49open Logic
50
51open Types
52
53open Identifiers
54
55open CostLabel
56
57open LabelledObjects
58
59open Exp
60
61open Arithmetic
62
63open Vector
64
65open FoldStuff
66
67open BitVector
68
69open Extranat
70
71open Integers
72
73open AST
74
75open String
76
77open BitVectorTrie
78
79type identifier = PreIdentifiers.identifier
80
81val toASM_ident :
82  PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> identifier
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
298val is_a : addressing_mode_tag -> addressing_mode -> Bool.bool
299
300val is_in :
301  Nat.nat -> addressing_mode_tag Vector.vector -> addressing_mode ->
302  Bool.bool
303
304type subaddressing_mode =
305  addressing_mode
306  (* singleton inductive, whose constructor was mk_subaddressing_mode *)
307
308val subaddressing_mode_rect_Type4 :
309  Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
310  'a1) -> subaddressing_mode -> 'a1
311
312val subaddressing_mode_rect_Type5 :
313  Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
314  'a1) -> subaddressing_mode -> 'a1
315
316val subaddressing_mode_rect_Type3 :
317  Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
318  'a1) -> subaddressing_mode -> 'a1
319
320val subaddressing_mode_rect_Type2 :
321  Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
322  'a1) -> subaddressing_mode -> 'a1
323
324val subaddressing_mode_rect_Type1 :
325  Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
326  'a1) -> subaddressing_mode -> 'a1
327
328val subaddressing_mode_rect_Type0 :
329  Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
330  'a1) -> subaddressing_mode -> 'a1
331
332val subaddressing_modeel :
333  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
334  addressing_mode
335
336val subaddressing_mode_inv_rect_Type4 :
337  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
338  (addressing_mode -> __ -> __ -> 'a1) -> 'a1
339
340val subaddressing_mode_inv_rect_Type3 :
341  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
342  (addressing_mode -> __ -> __ -> 'a1) -> 'a1
343
344val subaddressing_mode_inv_rect_Type2 :
345  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
346  (addressing_mode -> __ -> __ -> 'a1) -> 'a1
347
348val subaddressing_mode_inv_rect_Type1 :
349  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
350  (addressing_mode -> __ -> __ -> 'a1) -> 'a1
351
352val subaddressing_mode_inv_rect_Type0 :
353  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
354  (addressing_mode -> __ -> __ -> 'a1) -> 'a1
355
356val subaddressing_mode_discr :
357  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
358  subaddressing_mode -> __
359
360val subaddressing_mode_jmdiscr :
361  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
362  subaddressing_mode -> __
363
364val dpi1__o__subaddressing_modeel__o__inject :
365  Nat.nat -> addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1)
366  Types.dPair -> addressing_mode Types.sig0
367
368val eject__o__subaddressing_modeel__o__inject :
369  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode
370  Types.sig0 -> addressing_mode Types.sig0
371
372val subaddressing_modeel__o__inject :
373  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
374  addressing_mode Types.sig0
375
376val dpi1__o__subaddressing_modeel :
377  Nat.nat -> addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1)
378  Types.dPair -> addressing_mode
379
380val eject__o__subaddressing_modeel :
381  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode
382  Types.sig0 -> addressing_mode
383
384type 'x1 dpi1__o__subaddressing_mode = subaddressing_mode
385
386type eject__o__subaddressing_mode = subaddressing_mode
387
388val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__inject :
389  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
390  addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) Types.dPair
391  -> subaddressing_mode Types.sig0
392
393val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
394  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
395  addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) Types.dPair
396  -> addressing_mode Types.sig0
397
398val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel :
399  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
400  addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) Types.dPair
401  -> addressing_mode
402
403val eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__inject :
404  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
405  addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 ->
406  subaddressing_mode Types.sig0
407
408val eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
409  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
410  addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 ->
411  addressing_mode Types.sig0
412
413val eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel :
414  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
415  addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 ->
416  addressing_mode
417
418val subaddressing_modeel__o__mk_subaddressing_mode__o__inject :
419  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
420  addressing_mode_tag Vector.vector -> subaddressing_mode ->
421  subaddressing_mode Types.sig0
422
423val subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
424  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
425  addressing_mode_tag Vector.vector -> subaddressing_mode -> addressing_mode
426  Types.sig0
427
428val subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel :
429  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
430  addressing_mode_tag Vector.vector -> subaddressing_mode -> addressing_mode
431
432val dpi1__o__mk_subaddressing_mode__o__inject :
433  Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
434  Vector.vector -> subaddressing_mode Types.sig0
435
436val dpi1__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
437  Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
438  Vector.vector -> addressing_mode Types.sig0
439
440val dpi1__o__mk_subaddressing_mode__o__subaddressing_modeel :
441  Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
442  Vector.vector -> addressing_mode
443
444val eject__o__mk_subaddressing_mode__o__inject :
445  Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag Vector.vector
446  -> subaddressing_mode Types.sig0
447
448val eject__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
449  Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag Vector.vector
450  -> addressing_mode Types.sig0
451
452val eject__o__mk_subaddressing_mode__o__subaddressing_modeel :
453  Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag Vector.vector
454  -> addressing_mode
455
456val mk_subaddressing_mode__o__subaddressing_modeel :
457  Nat.nat -> addressing_mode -> addressing_mode_tag Vector.vector ->
458  addressing_mode
459
460val mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
461  Nat.nat -> addressing_mode -> addressing_mode_tag Vector.vector ->
462  addressing_mode Types.sig0
463
464val mk_subaddressing_mode__o__inject :
465  Nat.nat -> addressing_mode -> addressing_mode_tag Vector.vector ->
466  subaddressing_mode Types.sig0
467
468val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode :
469  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
470  addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) Types.dPair
471  -> subaddressing_mode
472
473val eject__o__subaddressing_modeel__o__mk_subaddressing_mode :
474  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
475  addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 ->
476  subaddressing_mode
477
478val subaddressing_modeel__o__mk_subaddressing_mode :
479  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
480  addressing_mode_tag Vector.vector -> subaddressing_mode ->
481  subaddressing_mode
482
483val dpi1__o__mk_subaddressing_mode :
484  Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
485  Vector.vector -> subaddressing_mode
486
487val eject__o__mk_subaddressing_mode :
488  Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag Vector.vector
489  -> subaddressing_mode
490
491type 'a preinstruction =
492| ADD of subaddressing_mode * subaddressing_mode
493| ADDC of subaddressing_mode * subaddressing_mode
494| SUBB of subaddressing_mode * subaddressing_mode
495| INC of subaddressing_mode
496| DEC of subaddressing_mode
497| MUL of subaddressing_mode * subaddressing_mode
498| DIV of subaddressing_mode * subaddressing_mode
499| DA of subaddressing_mode
500| JC of 'a
501| JNC of 'a
502| JB of subaddressing_mode * 'a
503| JNB of subaddressing_mode * 'a
504| JBC of subaddressing_mode * 'a
505| JZ of 'a
506| JNZ of 'a
507| CJNE of ((subaddressing_mode, subaddressing_mode) Types.prod,
508          (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum * 
509   'a
510| DJNZ of subaddressing_mode * 'a
511| ANL of (((subaddressing_mode, subaddressing_mode) Types.prod,
512         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
513         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
514| ORL of (((subaddressing_mode, subaddressing_mode) Types.prod,
515         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
516         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
517| XRL of ((subaddressing_mode, subaddressing_mode) Types.prod,
518         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
519| CLR of subaddressing_mode
520| CPL of subaddressing_mode
521| RL of subaddressing_mode
522| RLC of subaddressing_mode
523| RR of subaddressing_mode
524| RRC of subaddressing_mode
525| SWAP of subaddressing_mode
526| MOV of ((((((subaddressing_mode, subaddressing_mode) Types.prod,
527         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
528         (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
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| MOVX of ((subaddressing_mode, subaddressing_mode) Types.prod,
533          (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
534| SETB of subaddressing_mode
535| PUSH of subaddressing_mode
536| POP of subaddressing_mode
537| XCH of subaddressing_mode * subaddressing_mode
538| XCHD of subaddressing_mode * subaddressing_mode
539| RET
540| RETI
541| NOP
542| JMP of subaddressing_mode
543
544val preinstruction_rect_Type4 :
545  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
546  subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
547  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
548  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
549  subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
550  -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
551  (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
552  ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
553  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
554  -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> '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,
559  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
560  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
561  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
562  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
563  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
564  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
565  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
566  (((((((subaddressing_mode, subaddressing_mode) Types.prod,
567  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
568  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
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 -> 'a2) ->
572  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
573  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
574  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
575  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
576  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
577  'a2) -> 'a1 preinstruction -> 'a2
578
579val preinstruction_rect_Type5 :
580  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
581  subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
582  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
583  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
584  subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
585  -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
586  (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
587  ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
588  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
589  -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> '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,
594  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
595  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
596  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
597  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
598  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
599  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
600  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
601  (((((((subaddressing_mode, subaddressing_mode) Types.prod,
602  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
603  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
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 -> 'a2) ->
607  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
608  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
609  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
610  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
611  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
612  'a2) -> 'a1 preinstruction -> 'a2
613
614val preinstruction_rect_Type3 :
615  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
616  subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
617  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
618  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
619  subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
620  -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
621  (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
622  ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
623  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
624  -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> '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,
629  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
630  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
631  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
632  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
633  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
634  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
635  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
636  (((((((subaddressing_mode, subaddressing_mode) Types.prod,
637  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
638  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
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 -> 'a2) ->
642  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
643  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
644  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
645  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
646  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
647  'a2) -> 'a1 preinstruction -> 'a2
648
649val preinstruction_rect_Type2 :
650  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
651  subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
652  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
653  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
654  subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
655  -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
656  (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
657  ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
658  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
659  -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
660  ((((subaddressing_mode, subaddressing_mode) Types.prod,
661  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
662  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
663  ((((subaddressing_mode, subaddressing_mode) Types.prod,
664  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
665  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
666  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
667  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
668  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
669  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
670  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
671  (((((((subaddressing_mode, subaddressing_mode) Types.prod,
672  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
673  (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  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
677  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
678  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
679  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
680  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
681  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
682  'a2) -> 'a1 preinstruction -> 'a2
683
684val preinstruction_rect_Type1 :
685  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
686  subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
687  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
688  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
689  subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
690  -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
691  (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
692  ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
693  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
694  -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
695  ((((subaddressing_mode, subaddressing_mode) Types.prod,
696  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
697  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
698  ((((subaddressing_mode, subaddressing_mode) Types.prod,
699  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
700  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
701  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
702  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
703  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
704  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
705  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
706  (((((((subaddressing_mode, subaddressing_mode) Types.prod,
707  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
708  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
709  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
710  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
711  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
712  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
713  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
714  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
715  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
716  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
717  'a2) -> 'a1 preinstruction -> 'a2
718
719val preinstruction_rect_Type0 :
720  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
721  subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
722  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
723  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
724  subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
725  -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
726  (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
727  ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
728  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
729  -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
730  ((((subaddressing_mode, subaddressing_mode) Types.prod,
731  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
732  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
733  ((((subaddressing_mode, subaddressing_mode) Types.prod,
734  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
735  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
736  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
737  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
738  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
739  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
740  (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
741  (((((((subaddressing_mode, subaddressing_mode) Types.prod,
742  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
743  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
744  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
745  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
746  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
747  (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
748  subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
749  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
750  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
751  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
752  'a2) -> 'a1 preinstruction -> 'a2
753
754val preinstruction_inv_rect_Type4 :
755  'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
756  'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
757  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
758  (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
759  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
760  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
761  (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
762  'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode ->
763  'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 -> __
764  -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
765  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
766  -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) ->
767  ((((subaddressing_mode, subaddressing_mode) Types.prod,
768  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
769  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
770  'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
771  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
772  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
773  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
774  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
775  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
776  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
777  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
778  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
779  subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
780  Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod)
781  Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
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  subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
789  subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
790  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
791
792val preinstruction_inv_rect_Type3 :
793  'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
794  'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
795  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
796  (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
797  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
798  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
799  (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
800  'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode ->
801  'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 -> __
802  -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
803  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
804  -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) ->
805  ((((subaddressing_mode, subaddressing_mode) Types.prod,
806  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
807  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
808  'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
809  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
810  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
811  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
812  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
813  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
814  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
815  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
816  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
817  subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
818  Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod)
819  Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
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  subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
827  subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
828  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
829
830val preinstruction_inv_rect_Type2 :
831  'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
832  'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
833  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
834  (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
835  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
836  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
837  (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
838  'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode ->
839  'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 -> __
840  -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
841  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
842  -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) ->
843  ((((subaddressing_mode, subaddressing_mode) Types.prod,
844  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
845  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
846  'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
847  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
848  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
849  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
850  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
851  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
852  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
853  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
854  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
855  subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
856  Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod)
857  Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
858  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
859  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
860  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
861  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
862  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
863  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
864  subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
865  subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
866  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
867
868val preinstruction_inv_rect_Type1 :
869  'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
870  'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
871  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
872  (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
873  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
874  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
875  (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
876  'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode ->
877  'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 -> __
878  -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
879  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
880  -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) ->
881  ((((subaddressing_mode, subaddressing_mode) Types.prod,
882  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
883  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
884  'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
885  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
886  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
887  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
888  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
889  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
890  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
891  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
892  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
893  subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
894  Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod)
895  Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
896  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
897  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
898  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
899  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
900  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
901  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
902  subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
903  subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
904  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
905
906val preinstruction_inv_rect_Type0 :
907  'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
908  'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
909  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
910  (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
911  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
912  (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
913  (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
914  'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode ->
915  'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 -> __
916  -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
917  Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
918  -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) ->
919  ((((subaddressing_mode, subaddressing_mode) Types.prod,
920  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
921  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
922  'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
923  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
924  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
925  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
926  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
927  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
928  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
929  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
930  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
931  subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
932  Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod)
933  Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
934  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
935  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
936  'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
937  (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
938  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
939  'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
940  subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
941  subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
942  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
943
944val preinstruction_discr : 'a1 preinstruction -> 'a1 preinstruction -> __
945
946val preinstruction_jmdiscr : 'a1 preinstruction -> 'a1 preinstruction -> __
947
948val eq_preinstruction :
949  subaddressing_mode preinstruction -> subaddressing_mode preinstruction ->
950  Bool.bool
951
952type instruction =
953| ACALL of subaddressing_mode
954| LCALL of subaddressing_mode
955| AJMP of subaddressing_mode
956| LJMP of subaddressing_mode
957| SJMP of subaddressing_mode
958| MOVC of subaddressing_mode * subaddressing_mode
959| RealInstruction of subaddressing_mode preinstruction
960
961val instruction_rect_Type4 :
962  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
963  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
964  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
965  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
966
967val instruction_rect_Type5 :
968  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
969  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
970  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
971  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
972
973val instruction_rect_Type3 :
974  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
975  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
976  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
977  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
978
979val instruction_rect_Type2 :
980  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
981  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
982  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
983  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
984
985val instruction_rect_Type1 :
986  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
987  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
988  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
989  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
990
991val instruction_rect_Type0 :
992  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
993  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
994  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
995  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
996
997val instruction_inv_rect_Type4 :
998  instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
999  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1000  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1001  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
1002  __ -> 'a1) -> 'a1
1003
1004val instruction_inv_rect_Type3 :
1005  instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1006  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1007  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1008  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
1009  __ -> 'a1) -> 'a1
1010
1011val instruction_inv_rect_Type2 :
1012  instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1013  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1014  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1015  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
1016  __ -> 'a1) -> 'a1
1017
1018val instruction_inv_rect_Type1 :
1019  instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1020  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1021  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1022  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
1023  __ -> 'a1) -> 'a1
1024
1025val instruction_inv_rect_Type0 :
1026  instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1027  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1028  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1029  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
1030  __ -> 'a1) -> 'a1
1031
1032val instruction_discr : instruction -> instruction -> __
1033
1034val instruction_jmdiscr : instruction -> instruction -> __
1035
1036val dpi1__o__RealInstruction__o__inject :
1037  (subaddressing_mode preinstruction, 'a1) Types.dPair -> instruction
1038  Types.sig0
1039
1040val eject__o__RealInstruction__o__inject :
1041  subaddressing_mode preinstruction Types.sig0 -> instruction Types.sig0
1042
1043val realInstruction__o__inject :
1044  subaddressing_mode preinstruction -> instruction Types.sig0
1045
1046val dpi1__o__RealInstruction :
1047  (subaddressing_mode preinstruction, 'a1) Types.dPair -> instruction
1048
1049val eject__o__RealInstruction :
1050  subaddressing_mode preinstruction Types.sig0 -> instruction
1051
1052val eq_instruction : instruction -> instruction -> Bool.bool
1053
1054type word_side =
1055| HIGH
1056| LOW
1057
1058val word_side_rect_Type4 : 'a1 -> 'a1 -> word_side -> 'a1
1059
1060val word_side_rect_Type5 : 'a1 -> 'a1 -> word_side -> 'a1
1061
1062val word_side_rect_Type3 : 'a1 -> 'a1 -> word_side -> 'a1
1063
1064val word_side_rect_Type2 : 'a1 -> 'a1 -> word_side -> 'a1
1065
1066val word_side_rect_Type1 : 'a1 -> 'a1 -> word_side -> 'a1
1067
1068val word_side_rect_Type0 : 'a1 -> 'a1 -> word_side -> 'a1
1069
1070val word_side_inv_rect_Type4 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
1071
1072val word_side_inv_rect_Type3 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
1073
1074val word_side_inv_rect_Type2 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
1075
1076val word_side_inv_rect_Type1 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
1077
1078val word_side_inv_rect_Type0 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
1079
1080val word_side_discr : word_side -> word_side -> __
1081
1082val word_side_jmdiscr : word_side -> word_side -> __
1083
1084type pseudo_instruction =
1085| Instruction of identifier preinstruction
1086| Comment of String.string
1087| Cost of CostLabel.costlabel
1088| Jmp of identifier
1089| Jnz of subaddressing_mode * identifier * identifier
1090| Call of identifier
1091| Mov of (subaddressing_mode, (subaddressing_mode, word_side) Types.prod)
1092         Types.sum * identifier * BitVector.word
1093
1094val pseudo_instruction_rect_Type4 :
1095  (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
1096  (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
1097  -> identifier -> identifier -> 'a1) -> (identifier -> 'a1) ->
1098  ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
1099  -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction -> 'a1
1100
1101val pseudo_instruction_rect_Type5 :
1102  (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
1103  (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
1104  -> identifier -> identifier -> 'a1) -> (identifier -> 'a1) ->
1105  ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
1106  -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction -> 'a1
1107
1108val pseudo_instruction_rect_Type3 :
1109  (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
1110  (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
1111  -> identifier -> identifier -> 'a1) -> (identifier -> 'a1) ->
1112  ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
1113  -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction -> 'a1
1114
1115val pseudo_instruction_rect_Type2 :
1116  (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
1117  (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
1118  -> identifier -> identifier -> 'a1) -> (identifier -> 'a1) ->
1119  ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
1120  -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction -> 'a1
1121
1122val pseudo_instruction_rect_Type1 :
1123  (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
1124  (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
1125  -> identifier -> identifier -> 'a1) -> (identifier -> 'a1) ->
1126  ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
1127  -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction -> 'a1
1128
1129val pseudo_instruction_rect_Type0 :
1130  (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
1131  (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
1132  -> identifier -> identifier -> 'a1) -> (identifier -> 'a1) ->
1133  ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
1134  -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction -> 'a1
1135
1136val pseudo_instruction_inv_rect_Type4 :
1137  pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
1138  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
1139  (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
1140  identifier -> __ -> 'a1) -> (identifier -> __ -> 'a1) ->
1141  ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
1142  -> identifier -> BitVector.word -> __ -> 'a1) -> 'a1
1143
1144val pseudo_instruction_inv_rect_Type3 :
1145  pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
1146  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
1147  (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
1148  identifier -> __ -> 'a1) -> (identifier -> __ -> 'a1) ->
1149  ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
1150  -> identifier -> BitVector.word -> __ -> 'a1) -> 'a1
1151
1152val pseudo_instruction_inv_rect_Type2 :
1153  pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
1154  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
1155  (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
1156  identifier -> __ -> 'a1) -> (identifier -> __ -> 'a1) ->
1157  ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
1158  -> identifier -> BitVector.word -> __ -> 'a1) -> 'a1
1159
1160val pseudo_instruction_inv_rect_Type1 :
1161  pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
1162  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
1163  (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
1164  identifier -> __ -> 'a1) -> (identifier -> __ -> 'a1) ->
1165  ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
1166  -> identifier -> BitVector.word -> __ -> 'a1) -> 'a1
1167
1168val pseudo_instruction_inv_rect_Type0 :
1169  pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
1170  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
1171  (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
1172  identifier -> __ -> 'a1) -> (identifier -> __ -> 'a1) ->
1173  ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
1174  -> identifier -> BitVector.word -> __ -> 'a1) -> 'a1
1175
1176val pseudo_instruction_discr : pseudo_instruction -> pseudo_instruction -> __
1177
1178val pseudo_instruction_jmdiscr :
1179  pseudo_instruction -> pseudo_instruction -> __
1180
1181type labelled_instruction = pseudo_instruction LabelledObjects.labelled_obj
1182
1183type assembly_program = instruction List.list
1184
1185val fetch_pseudo_instruction :
1186  labelled_instruction List.list -> BitVector.word -> (pseudo_instruction,
1187  BitVector.word) Types.prod
1188
1189val is_jump' : identifier preinstruction -> Bool.bool
1190
1191val is_relative_jump : pseudo_instruction -> Bool.bool
1192
1193val is_jump : pseudo_instruction -> Bool.bool
1194
1195val is_call : pseudo_instruction -> Bool.bool
1196
1197val asm_cost_label :
1198  labelled_instruction List.list -> BitVector.word Types.sig0 ->
1199  CostLabel.costlabel Types.option
1200
1201val aDDRESS_WIDTH : Nat.nat
1202
1203val mAX_CODE_SIZE : Nat.nat
1204
1205val code_size_opt : labelled_instruction List.list -> __ Types.option
1206
1207type pseudo_assembly_program = { preamble : (identifier, BitVector.word)
1208                                            Types.prod List.list;
1209                                 code : labelled_instruction List.list;
1210                                 renamed_symbols : (identifier, AST.ident)
1211                                                   Types.prod List.list;
1212                                 final_label : identifier }
1213
1214val pseudo_assembly_program_rect_Type4 :
1215  ((identifier, BitVector.word) Types.prod List.list -> labelled_instruction
1216  List.list -> __ -> (identifier, AST.ident) Types.prod List.list ->
1217  identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1
1218
1219val pseudo_assembly_program_rect_Type5 :
1220  ((identifier, BitVector.word) Types.prod List.list -> labelled_instruction
1221  List.list -> __ -> (identifier, AST.ident) Types.prod List.list ->
1222  identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1
1223
1224val pseudo_assembly_program_rect_Type3 :
1225  ((identifier, BitVector.word) Types.prod List.list -> labelled_instruction
1226  List.list -> __ -> (identifier, AST.ident) Types.prod List.list ->
1227  identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1
1228
1229val pseudo_assembly_program_rect_Type2 :
1230  ((identifier, BitVector.word) Types.prod List.list -> labelled_instruction
1231  List.list -> __ -> (identifier, AST.ident) Types.prod List.list ->
1232  identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1
1233
1234val pseudo_assembly_program_rect_Type1 :
1235  ((identifier, BitVector.word) Types.prod List.list -> labelled_instruction
1236  List.list -> __ -> (identifier, AST.ident) Types.prod List.list ->
1237  identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1
1238
1239val pseudo_assembly_program_rect_Type0 :
1240  ((identifier, BitVector.word) Types.prod List.list -> labelled_instruction
1241  List.list -> __ -> (identifier, AST.ident) Types.prod List.list ->
1242  identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1
1243
1244val preamble :
1245  pseudo_assembly_program -> (identifier, BitVector.word) Types.prod
1246  List.list
1247
1248val code : pseudo_assembly_program -> labelled_instruction List.list
1249
1250val renamed_symbols :
1251  pseudo_assembly_program -> (identifier, AST.ident) Types.prod List.list
1252
1253val final_label : pseudo_assembly_program -> identifier
1254
1255val pseudo_assembly_program_inv_rect_Type4 :
1256  pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
1257  List.list -> labelled_instruction List.list -> __ -> (identifier,
1258  AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1) ->
1259  'a1
1260
1261val pseudo_assembly_program_inv_rect_Type3 :
1262  pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
1263  List.list -> labelled_instruction List.list -> __ -> (identifier,
1264  AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1) ->
1265  'a1
1266
1267val pseudo_assembly_program_inv_rect_Type2 :
1268  pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
1269  List.list -> labelled_instruction List.list -> __ -> (identifier,
1270  AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1) ->
1271  'a1
1272
1273val pseudo_assembly_program_inv_rect_Type1 :
1274  pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
1275  List.list -> labelled_instruction List.list -> __ -> (identifier,
1276  AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1) ->
1277  'a1
1278
1279val pseudo_assembly_program_inv_rect_Type0 :
1280  pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
1281  List.list -> labelled_instruction List.list -> __ -> (identifier,
1282  AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1) ->
1283  'a1
1284
1285val pseudo_assembly_program_jmdiscr :
1286  pseudo_assembly_program -> pseudo_assembly_program -> __
1287
1288type object_code = BitVector.byte List.list
1289
1290val next :
1291  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
1292  (BitVector.word, BitVector.byte) Types.prod
1293
1294val load_code_memory0 :
1295  object_code -> BitVector.byte BitVectorTrie.bitVectorTrie Types.sig0
1296
1297val load_code_memory :
1298  object_code -> BitVector.byte BitVectorTrie.bitVectorTrie
1299
1300type costlabel_map = CostLabel.costlabel BitVectorTrie.bitVectorTrie
1301
1302type symboltable_type = AST.ident BitVectorTrie.bitVectorTrie
1303
1304type labelled_object_code = { oc : object_code;
1305                              cm : BitVector.byte BitVectorTrie.bitVectorTrie;
1306                              costlabels : costlabel_map;
1307                              symboltable : symboltable_type;
1308                              final_pc : BitVector.word }
1309
1310val labelled_object_code_rect_Type4 :
1311  (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
1312  costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
1313  labelled_object_code -> 'a1
1314
1315val labelled_object_code_rect_Type5 :
1316  (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
1317  costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
1318  labelled_object_code -> 'a1
1319
1320val labelled_object_code_rect_Type3 :
1321  (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
1322  costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
1323  labelled_object_code -> 'a1
1324
1325val labelled_object_code_rect_Type2 :
1326  (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
1327  costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
1328  labelled_object_code -> 'a1
1329
1330val labelled_object_code_rect_Type1 :
1331  (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
1332  costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
1333  labelled_object_code -> 'a1
1334
1335val labelled_object_code_rect_Type0 :
1336  (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
1337  costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
1338  labelled_object_code -> 'a1
1339
1340val oc : labelled_object_code -> object_code
1341
1342val cm : labelled_object_code -> BitVector.byte BitVectorTrie.bitVectorTrie
1343
1344val costlabels : labelled_object_code -> costlabel_map
1345
1346val symboltable : labelled_object_code -> symboltable_type
1347
1348val final_pc : labelled_object_code -> BitVector.word
1349
1350val labelled_object_code_inv_rect_Type4 :
1351  labelled_object_code -> (object_code -> BitVector.byte
1352  BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
1353  BitVector.word -> __ -> __ -> 'a1) -> 'a1
1354
1355val labelled_object_code_inv_rect_Type3 :
1356  labelled_object_code -> (object_code -> BitVector.byte
1357  BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
1358  BitVector.word -> __ -> __ -> 'a1) -> 'a1
1359
1360val labelled_object_code_inv_rect_Type2 :
1361  labelled_object_code -> (object_code -> BitVector.byte
1362  BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
1363  BitVector.word -> __ -> __ -> 'a1) -> 'a1
1364
1365val labelled_object_code_inv_rect_Type1 :
1366  labelled_object_code -> (object_code -> BitVector.byte
1367  BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
1368  BitVector.word -> __ -> __ -> 'a1) -> 'a1
1369
1370val labelled_object_code_inv_rect_Type0 :
1371  labelled_object_code -> (object_code -> BitVector.byte
1372  BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
1373  BitVector.word -> __ -> __ -> 'a1) -> 'a1
1374
1375val labelled_object_code_jmdiscr :
1376  labelled_object_code -> labelled_object_code -> __
1377
Note: See TracBrowser for help on using the repository browser.