source: extracted/aSM.mli @ 3015

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

code_memory added to labelled_object_code to avoid recomputing it every time.
This gives a major speed up in the semantics of the extracted code.

File size: 64.3 KB
RevLine 
[2601]1open Preamble
2
[2773]3open Proper
[2601]4
[2773]5open PositiveMap
[2601]6
[2773]7open Deqsets
8
9open ErrorMessages
10
11open PreIdentifiers
12
13open Errors
14
15open Extralib
16
17open Setoids
18
19open Monad
20
21open Option
22
[2601]23open Div_and_mod
24
25open Jmeq
26
27open Russell
28
[2773]29open Util
[2601]30
31open List
32
[2773]33open Lists
[2601]34
35open Bool
36
37open Relations
38
39open Nat
40
[2773]41open Positive
[2601]42
[2773]43open Hints_declaration
[2601]44
[2773]45open Core_notation
[2601]46
[2773]47open Pts
[2601]48
[2773]49open Logic
[2649]50
[2773]51open Types
[2601]52
[2773]53open Identifiers
[2601]54
[2773]55open CostLabel
[2601]56
[2773]57open LabelledObjects
[2601]58
[2773]59open Exp
[2601]60
[2773]61open Arithmetic
[2601]62
[2773]63open Vector
[2601]64
[2773]65open FoldStuff
[2601]66
[2773]67open BitVector
[2601]68
[2773]69open Extranat
[2717]70
[2601]71open Integers
72
73open AST
74
[2773]75open String
[2601]76
[2773]77open BitVectorTrie
[2601]78
[2773]79type identifier = PreIdentifiers.identifier
[2601]80
[2649]81val toASM_ident :
[2773]82  PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> identifier
[2601]83
84type addressing_mode =
85| DIRECT of BitVector.byte
86| INDIRECT of BitVector.bit
87| EXT_INDIRECT of BitVector.bit
88| REGISTER of BitVector.bitVector
89| ACC_A
90| ACC_B
91| DPTR
92| DATA of BitVector.byte
93| DATA16 of BitVector.word
94| ACC_DPTR
95| ACC_PC
96| EXT_INDIRECT_DPTR
97| INDIRECT_DPTR
98| CARRY
99| BIT_ADDR of BitVector.byte
100| N_BIT_ADDR of BitVector.byte
101| RELATIVE of BitVector.byte
102| ADDR11 of BitVector.word11
103| ADDR16 of BitVector.word
104
105val addressing_mode_rect_Type4 :
106  (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> 'a1)
107  -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (BitVector.byte ->
108  'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
109  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (BitVector.byte ->
110  'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) ->
111  addressing_mode -> 'a1
112
113val addressing_mode_rect_Type5 :
114  (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> 'a1)
115  -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (BitVector.byte ->
116  'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
117  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (BitVector.byte ->
118  'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) ->
119  addressing_mode -> 'a1
120
121val addressing_mode_rect_Type3 :
122  (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> 'a1)
123  -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (BitVector.byte ->
124  'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
125  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (BitVector.byte ->
126  'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) ->
127  addressing_mode -> 'a1
128
129val addressing_mode_rect_Type2 :
130  (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> 'a1)
131  -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (BitVector.byte ->
132  'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
133  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (BitVector.byte ->
134  'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) ->
135  addressing_mode -> 'a1
136
137val addressing_mode_rect_Type1 :
138  (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> 'a1)
139  -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (BitVector.byte ->
140  'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
141  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (BitVector.byte ->
142  'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) ->
143  addressing_mode -> 'a1
144
145val addressing_mode_rect_Type0 :
146  (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> 'a1)
147  -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (BitVector.byte ->
148  'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
149  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (BitVector.byte ->
150  'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) ->
151  addressing_mode -> 'a1
152
153val addressing_mode_inv_rect_Type4 :
154  addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ ->
155  'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> 'a1)
156  -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
157  'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
158  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
159  (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
160  (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1
161
162val addressing_mode_inv_rect_Type3 :
163  addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ ->
164  'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> 'a1)
165  -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
166  'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
167  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
168  (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
169  (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1
170
171val addressing_mode_inv_rect_Type2 :
172  addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ ->
173  'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> 'a1)
174  -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
175  'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
176  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
177  (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
178  (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1
179
180val addressing_mode_inv_rect_Type1 :
181  addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ ->
182  'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> 'a1)
183  -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
184  'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
185  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
186  (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
187  (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1
188
189val addressing_mode_inv_rect_Type0 :
190  addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ ->
191  'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> 'a1)
192  -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
193  'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
194  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
195  (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
196  (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1
197
198val addressing_mode_discr : addressing_mode -> addressing_mode -> __
199
200val addressing_mode_jmdiscr : addressing_mode -> addressing_mode -> __
201
202val eq_addressing_mode : addressing_mode -> addressing_mode -> Bool.bool
203
204type addressing_mode_tag =
205| Direct
206| Indirect
207| Ext_indirect
208| Registr
209| Acc_a
210| Acc_b
211| Dptr
212| Data
213| Data16
214| Acc_dptr
215| Acc_pc
216| Ext_indirect_dptr
217| Indirect_dptr
218| Carry
219| Bit_addr
220| N_bit_addr
221| Relative
222| Addr11
223| Addr16
224
225val addressing_mode_tag_rect_Type4 :
226  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
227  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
228  addressing_mode_tag -> 'a1
229
230val addressing_mode_tag_rect_Type5 :
231  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
232  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
233  addressing_mode_tag -> 'a1
234
235val addressing_mode_tag_rect_Type3 :
236  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
237  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
238  addressing_mode_tag -> 'a1
239
240val addressing_mode_tag_rect_Type2 :
241  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
242  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
243  addressing_mode_tag -> 'a1
244
245val addressing_mode_tag_rect_Type1 :
246  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
247  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
248  addressing_mode_tag -> 'a1
249
250val addressing_mode_tag_rect_Type0 :
251  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
252  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
253  addressing_mode_tag -> 'a1
254
255val addressing_mode_tag_inv_rect_Type4 :
256  addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
257  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
258  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
259  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
260  'a1) -> 'a1
261
262val addressing_mode_tag_inv_rect_Type3 :
263  addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
264  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
265  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
266  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
267  'a1) -> 'a1
268
269val addressing_mode_tag_inv_rect_Type2 :
270  addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
271  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
272  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
273  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
274  'a1) -> 'a1
275
276val addressing_mode_tag_inv_rect_Type1 :
277  addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
278  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
279  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
280  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
281  'a1) -> 'a1
282
283val addressing_mode_tag_inv_rect_Type0 :
284  addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
285  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
286  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
287  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
288  'a1) -> 'a1
289
290val addressing_mode_tag_discr :
291  addressing_mode_tag -> addressing_mode_tag -> __
292
293val addressing_mode_tag_jmdiscr :
294  addressing_mode_tag -> addressing_mode_tag -> __
295
296val eq_a : addressing_mode_tag -> addressing_mode_tag -> Bool.bool
297
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
[2743]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
[2601]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
[2717]542| JMP of subaddressing_mode
[2601]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 ->
[2717]576  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
577  'a2) -> 'a1 preinstruction -> 'a2
[2601]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 ->
[2717]611  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
612  'a2) -> 'a1 preinstruction -> 'a2
[2601]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 ->
[2717]646  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
647  'a2) -> 'a1 preinstruction -> 'a2
[2601]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 ->
[2717]681  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
682  'a2) -> 'a1 preinstruction -> 'a2
[2601]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 ->
[2717]716  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
717  'a2) -> 'a1 preinstruction -> 'a2
[2601]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 ->
[2717]751  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
752  'a2) -> 'a1 preinstruction -> 'a2
[2601]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) -> (__ ->
[2717]790  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
[2601]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) -> (__ ->
[2717]828  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
[2601]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) -> (__ ->
[2717]866  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
[2601]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) -> (__ ->
[2717]904  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
[2601]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) -> (__ ->
[2717]942  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
[2601]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) ->
[2717]964  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
965  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
[2601]966
967val instruction_rect_Type5 :
968  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
969  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
[2717]970  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
971  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
[2601]972
973val instruction_rect_Type3 :
974  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
975  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
[2717]976  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
977  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
[2601]978
979val instruction_rect_Type2 :
980  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
981  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
[2717]982  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
983  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
[2601]984
985val instruction_rect_Type1 :
986  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
987  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
[2717]988  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
989  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
[2601]990
991val instruction_rect_Type0 :
992  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
993  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
[2717]994  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
995  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
[2601]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 ->
[2717]1001  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
1002  __ -> 'a1) -> 'a1
[2601]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 ->
[2717]1008  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
1009  __ -> 'a1) -> 'a1
[2601]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 ->
[2717]1015  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
1016  __ -> 'a1) -> 'a1
[2601]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 ->
[2717]1022  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
1023  __ -> 'a1) -> 'a1
[2601]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 ->
[2717]1029  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
1030  __ -> 'a1) -> 'a1
[2601]1031
1032val instruction_discr : instruction -> instruction -> __
1033
1034val instruction_jmdiscr : instruction -> instruction -> __
1035
[2743]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
[2601]1052val eq_instruction : instruction -> instruction -> Bool.bool
1053
[2717]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
[2601]1084type pseudo_instruction =
[2773]1085| Instruction of identifier preinstruction
[2601]1086| Comment of String.string
1087| Cost of CostLabel.costlabel
[2773]1088| Jmp of identifier
1089| Jnz of subaddressing_mode * identifier * identifier
1090| MovSuccessor of subaddressing_mode * word_side * identifier
1091| Call of identifier
1092| Mov of subaddressing_mode * identifier
[2601]1093
1094val pseudo_instruction_rect_Type4 :
[2773]1095  (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
1096  (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
1097  -> identifier -> identifier -> 'a1) -> (subaddressing_mode -> word_side ->
1098  identifier -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode ->
1099  identifier -> 'a1) -> pseudo_instruction -> 'a1
[2601]1100
1101val pseudo_instruction_rect_Type5 :
[2773]1102  (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
1103  (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
1104  -> identifier -> identifier -> 'a1) -> (subaddressing_mode -> word_side ->
1105  identifier -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode ->
1106  identifier -> 'a1) -> pseudo_instruction -> 'a1
[2601]1107
1108val pseudo_instruction_rect_Type3 :
[2773]1109  (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
1110  (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
1111  -> identifier -> identifier -> 'a1) -> (subaddressing_mode -> word_side ->
1112  identifier -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode ->
1113  identifier -> 'a1) -> pseudo_instruction -> 'a1
[2601]1114
1115val pseudo_instruction_rect_Type2 :
[2773]1116  (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
1117  (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
1118  -> identifier -> identifier -> 'a1) -> (subaddressing_mode -> word_side ->
1119  identifier -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode ->
1120  identifier -> 'a1) -> pseudo_instruction -> 'a1
[2601]1121
1122val pseudo_instruction_rect_Type1 :
[2773]1123  (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
1124  (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
1125  -> identifier -> identifier -> 'a1) -> (subaddressing_mode -> word_side ->
1126  identifier -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode ->
1127  identifier -> 'a1) -> pseudo_instruction -> 'a1
[2601]1128
1129val pseudo_instruction_rect_Type0 :
[2773]1130  (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
1131  (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
1132  -> identifier -> identifier -> 'a1) -> (subaddressing_mode -> word_side ->
1133  identifier -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode ->
1134  identifier -> 'a1) -> pseudo_instruction -> 'a1
[2601]1135
1136val pseudo_instruction_inv_rect_Type4 :
[2773]1137  pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
[2601]1138  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
[2773]1139  (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
1140  identifier -> __ -> 'a1) -> (subaddressing_mode -> word_side -> identifier
1141  -> __ -> 'a1) -> (identifier -> __ -> 'a1) -> (subaddressing_mode ->
1142  identifier -> __ -> 'a1) -> 'a1
[2601]1143
1144val pseudo_instruction_inv_rect_Type3 :
[2773]1145  pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
[2601]1146  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
[2773]1147  (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
1148  identifier -> __ -> 'a1) -> (subaddressing_mode -> word_side -> identifier
1149  -> __ -> 'a1) -> (identifier -> __ -> 'a1) -> (subaddressing_mode ->
1150  identifier -> __ -> 'a1) -> 'a1
[2601]1151
1152val pseudo_instruction_inv_rect_Type2 :
[2773]1153  pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
[2601]1154  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
[2773]1155  (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
1156  identifier -> __ -> 'a1) -> (subaddressing_mode -> word_side -> identifier
1157  -> __ -> 'a1) -> (identifier -> __ -> 'a1) -> (subaddressing_mode ->
1158  identifier -> __ -> 'a1) -> 'a1
[2601]1159
1160val pseudo_instruction_inv_rect_Type1 :
[2773]1161  pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
[2601]1162  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
[2773]1163  (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
1164  identifier -> __ -> 'a1) -> (subaddressing_mode -> word_side -> identifier
1165  -> __ -> 'a1) -> (identifier -> __ -> 'a1) -> (subaddressing_mode ->
1166  identifier -> __ -> 'a1) -> 'a1
[2601]1167
1168val pseudo_instruction_inv_rect_Type0 :
[2773]1169  pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
[2601]1170  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
[2773]1171  (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
1172  identifier -> __ -> 'a1) -> (subaddressing_mode -> word_side -> identifier
1173  -> __ -> 'a1) -> (identifier -> __ -> 'a1) -> (subaddressing_mode ->
1174  identifier -> __ -> 'a1) -> 'a1
[2601]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
[2773]1185val fetch_pseudo_instruction :
1186  labelled_instruction List.list -> BitVector.word -> (pseudo_instruction,
1187  BitVector.word) Types.prod
[2601]1188
[2773]1189val is_jump' : identifier preinstruction -> Bool.bool
[2601]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
[2773]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
[2999]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
[2773]1300type costlabel_map = CostLabel.costlabel BitVectorTrie.bitVectorTrie
1301
1302type symboltable_type = AST.ident BitVectorTrie.bitVectorTrie
1303
[2999]1304type labelled_object_code = { oc : object_code;
1305                              cm : BitVector.byte BitVectorTrie.bitVectorTrie;
1306                              costlabels : costlabel_map;
[2773]1307                              symboltable : symboltable_type;
1308                              final_pc : BitVector.word }
1309
1310val labelled_object_code_rect_Type4 :
[2999]1311  (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
1312  costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
1313  labelled_object_code -> 'a1
[2773]1314
1315val labelled_object_code_rect_Type5 :
[2999]1316  (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
1317  costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
1318  labelled_object_code -> 'a1
[2773]1319
1320val labelled_object_code_rect_Type3 :
[2999]1321  (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
1322  costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
1323  labelled_object_code -> 'a1
[2773]1324
1325val labelled_object_code_rect_Type2 :
[2999]1326  (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
1327  costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
1328  labelled_object_code -> 'a1
[2773]1329
1330val labelled_object_code_rect_Type1 :
[2999]1331  (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
1332  costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
1333  labelled_object_code -> 'a1
[2773]1334
1335val labelled_object_code_rect_Type0 :
[2999]1336  (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
1337  costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
1338  labelled_object_code -> 'a1
[2773]1339
1340val oc : labelled_object_code -> object_code
1341
[2999]1342val cm : labelled_object_code -> BitVector.byte BitVectorTrie.bitVectorTrie
1343
[2773]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 :
[2999]1351  labelled_object_code -> (object_code -> BitVector.byte
1352  BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
1353  BitVector.word -> __ -> __ -> 'a1) -> 'a1
[2773]1354
1355val labelled_object_code_inv_rect_Type3 :
[2999]1356  labelled_object_code -> (object_code -> BitVector.byte
1357  BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
1358  BitVector.word -> __ -> __ -> 'a1) -> 'a1
[2773]1359
1360val labelled_object_code_inv_rect_Type2 :
[2999]1361  labelled_object_code -> (object_code -> BitVector.byte
1362  BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
1363  BitVector.word -> __ -> __ -> 'a1) -> 'a1
[2773]1364
1365val labelled_object_code_inv_rect_Type1 :
[2999]1366  labelled_object_code -> (object_code -> BitVector.byte
1367  BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
1368  BitVector.word -> __ -> __ -> 'a1) -> 'a1
[2773]1369
1370val labelled_object_code_inv_rect_Type0 :
[2999]1371  labelled_object_code -> (object_code -> BitVector.byte
1372  BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
1373  BitVector.word -> __ -> __ -> 'a1) -> 'a1
[2773]1374
1375val labelled_object_code_jmdiscr :
1376  labelled_object_code -> labelled_object_code -> __
1377
Note: See TracBrowser for help on using the repository browser.