extracted/aSM.mli

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