source: extracted/aSM.mli @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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