Changeset 2649 for extracted/aSM.ml


Ignore:
Timestamp:
Feb 7, 2013, 10:43:49 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/aSM.ml

    r2620 r2649  
    11open Preamble
    22
    3 open Char
     3open Extranat
     4
     5open Vector
     6
     7open Div_and_mod
     8
     9open Jmeq
     10
     11open Russell
     12
     13open Types
     14
     15open List
     16
     17open Util
     18
     19open FoldStuff
     20
     21open Bool
     22
     23open Hints_declaration
     24
     25open Core_notation
     26
     27open Pts
     28
     29open Logic
     30
     31open Relations
     32
     33open Nat
     34
     35open BitVector
     36
     37open Proper
     38
     39open PositiveMap
     40
     41open Deqsets
     42
     43open ErrorMessages
     44
     45open PreIdentifiers
     46
     47open Errors
     48
     49open Extralib
     50
     51open Setoids
     52
     53open Monad
     54
     55open Option
     56
     57open Lists
     58
     59open Positive
     60
     61open Identifiers
     62
     63open Arithmetic
     64
     65open Integers
     66
     67open AST
     68
     69open CostLabel
     70
     71open LabelledObjects
    472
    573open String
    674
    7 open Extranat
    8 
    9 open Vector
    10 
    11 open Div_and_mod
    12 
    13 open Jmeq
    14 
    15 open Russell
    16 
    17 open Types
    18 
    19 open List
    20 
    21 open Util
    22 
    23 open FoldStuff
    24 
    25 open Bool
    26 
    27 open Hints_declaration
    28 
    29 open Core_notation
    30 
    31 open Pts
    32 
    33 open Logic
    34 
    35 open Relations
    36 
    37 open Nat
    38 
    39 open BitVector
    40 
    41 open Proper
    42 
    43 open PositiveMap
    44 
    45 open Deqsets
    46 
    47 open PreIdentifiers
    48 
    49 open Errors
    50 
    51 open Extralib
    52 
    53 open Setoids
    54 
    55 open Monad
    56 
    57 open Option
    58 
    59 open Lists
    60 
    61 open Positive
    62 
    63 open Identifiers
    64 
    65 open Coqlib
    66 
    67 open Floats
    68 
    69 open Arithmetic
    70 
    71 open Integers
    72 
    73 open AST
    74 
    75 open CostLabel
    76 
    77 open LabelledObjects
    78 
    79 (** val aSMTag : String.string **)
    80 let aSMTag = "ASMTag"
    81   (* failwith "AXIOM TO BE REALIZED" *)
    82 
    8375type identifier0 = PreIdentifiers.identifier
    8476
    8577(** val toASM_ident :
    86     String.string -> PreIdentifiers.identifier -> identifier0 **)
     78    PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> identifier0 **)
    8779let toASM_ident t i =
    8880  let id = i in id
     
    117109    -> 'a1) -> addressing_mode -> 'a1 **)
    118110let rec addressing_mode_rect_Type4 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
    119 | DIRECT x_14702 -> h_DIRECT x_14702
    120 | INDIRECT x_14703 -> h_INDIRECT x_14703
    121 | EXT_INDIRECT x_14704 -> h_EXT_INDIRECT x_14704
    122 | REGISTER x_14705 -> h_REGISTER x_14705
     111| DIRECT x_59 -> h_DIRECT x_59
     112| INDIRECT x_60 -> h_INDIRECT x_60
     113| EXT_INDIRECT x_61 -> h_EXT_INDIRECT x_61
     114| REGISTER x_62 -> h_REGISTER x_62
    123115| ACC_A -> h_ACC_A
    124116| ACC_B -> h_ACC_B
    125117| DPTR -> h_DPTR
    126 | DATA x_14706 -> h_DATA x_14706
    127 | DATA16 x_14707 -> h_DATA16 x_14707
     118| DATA x_63 -> h_DATA x_63
     119| DATA16 x_64 -> h_DATA16 x_64
    128120| ACC_DPTR -> h_ACC_DPTR
    129121| ACC_PC -> h_ACC_PC
     
    131123| INDIRECT_DPTR -> h_INDIRECT_DPTR
    132124| CARRY -> h_CARRY
    133 | BIT_ADDR x_14708 -> h_BIT_ADDR x_14708
    134 | N_BIT_ADDR x_14709 -> h_N_BIT_ADDR x_14709
    135 | RELATIVE x_14710 -> h_RELATIVE x_14710
    136 | ADDR11 x_14711 -> h_ADDR11 x_14711
    137 | ADDR16 x_14712 -> h_ADDR16 x_14712
     125| BIT_ADDR x_65 -> h_BIT_ADDR x_65
     126| N_BIT_ADDR x_66 -> h_N_BIT_ADDR x_66
     127| RELATIVE x_67 -> h_RELATIVE x_67
     128| ADDR11 x_68 -> h_ADDR11 x_68
     129| ADDR16 x_69 -> h_ADDR16 x_69
    138130
    139131(** val addressing_mode_rect_Type5 :
     
    145137    -> 'a1) -> addressing_mode -> 'a1 **)
    146138let rec addressing_mode_rect_Type5 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
    147 | DIRECT x_14733 -> h_DIRECT x_14733
    148 | INDIRECT x_14734 -> h_INDIRECT x_14734
    149 | EXT_INDIRECT x_14735 -> h_EXT_INDIRECT x_14735
    150 | REGISTER x_14736 -> h_REGISTER x_14736
     139| DIRECT x_90 -> h_DIRECT x_90
     140| INDIRECT x_91 -> h_INDIRECT x_91
     141| EXT_INDIRECT x_92 -> h_EXT_INDIRECT x_92
     142| REGISTER x_93 -> h_REGISTER x_93
    151143| ACC_A -> h_ACC_A
    152144| ACC_B -> h_ACC_B
    153145| DPTR -> h_DPTR
    154 | DATA x_14737 -> h_DATA x_14737
    155 | DATA16 x_14738 -> h_DATA16 x_14738
     146| DATA x_94 -> h_DATA x_94
     147| DATA16 x_95 -> h_DATA16 x_95
    156148| ACC_DPTR -> h_ACC_DPTR
    157149| ACC_PC -> h_ACC_PC
     
    159151| INDIRECT_DPTR -> h_INDIRECT_DPTR
    160152| CARRY -> h_CARRY
    161 | BIT_ADDR x_14739 -> h_BIT_ADDR x_14739
    162 | N_BIT_ADDR x_14740 -> h_N_BIT_ADDR x_14740
    163 | RELATIVE x_14741 -> h_RELATIVE x_14741
    164 | ADDR11 x_14742 -> h_ADDR11 x_14742
    165 | ADDR16 x_14743 -> h_ADDR16 x_14743
     153| BIT_ADDR x_96 -> h_BIT_ADDR x_96
     154| N_BIT_ADDR x_97 -> h_N_BIT_ADDR x_97
     155| RELATIVE x_98 -> h_RELATIVE x_98
     156| ADDR11 x_99 -> h_ADDR11 x_99
     157| ADDR16 x_100 -> h_ADDR16 x_100
    166158
    167159(** val addressing_mode_rect_Type3 :
     
    173165    -> 'a1) -> addressing_mode -> 'a1 **)
    174166let rec addressing_mode_rect_Type3 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
    175 | DIRECT x_14764 -> h_DIRECT x_14764
    176 | INDIRECT x_14765 -> h_INDIRECT x_14765
    177 | EXT_INDIRECT x_14766 -> h_EXT_INDIRECT x_14766
    178 | REGISTER x_14767 -> h_REGISTER x_14767
     167| DIRECT x_121 -> h_DIRECT x_121
     168| INDIRECT x_122 -> h_INDIRECT x_122
     169| EXT_INDIRECT x_123 -> h_EXT_INDIRECT x_123
     170| REGISTER x_124 -> h_REGISTER x_124
    179171| ACC_A -> h_ACC_A
    180172| ACC_B -> h_ACC_B
    181173| DPTR -> h_DPTR
    182 | DATA x_14768 -> h_DATA x_14768
    183 | DATA16 x_14769 -> h_DATA16 x_14769
     174| DATA x_125 -> h_DATA x_125
     175| DATA16 x_126 -> h_DATA16 x_126
    184176| ACC_DPTR -> h_ACC_DPTR
    185177| ACC_PC -> h_ACC_PC
     
    187179| INDIRECT_DPTR -> h_INDIRECT_DPTR
    188180| CARRY -> h_CARRY
    189 | BIT_ADDR x_14770 -> h_BIT_ADDR x_14770
    190 | N_BIT_ADDR x_14771 -> h_N_BIT_ADDR x_14771
    191 | RELATIVE x_14772 -> h_RELATIVE x_14772
    192 | ADDR11 x_14773 -> h_ADDR11 x_14773
    193 | ADDR16 x_14774 -> h_ADDR16 x_14774
     181| BIT_ADDR x_127 -> h_BIT_ADDR x_127
     182| N_BIT_ADDR x_128 -> h_N_BIT_ADDR x_128
     183| RELATIVE x_129 -> h_RELATIVE x_129
     184| ADDR11 x_130 -> h_ADDR11 x_130
     185| ADDR16 x_131 -> h_ADDR16 x_131
    194186
    195187(** val addressing_mode_rect_Type2 :
     
    201193    -> 'a1) -> addressing_mode -> 'a1 **)
    202194let rec addressing_mode_rect_Type2 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
    203 | DIRECT x_14795 -> h_DIRECT x_14795
    204 | INDIRECT x_14796 -> h_INDIRECT x_14796
    205 | EXT_INDIRECT x_14797 -> h_EXT_INDIRECT x_14797
    206 | REGISTER x_14798 -> h_REGISTER x_14798
     195| DIRECT x_152 -> h_DIRECT x_152
     196| INDIRECT x_153 -> h_INDIRECT x_153
     197| EXT_INDIRECT x_154 -> h_EXT_INDIRECT x_154
     198| REGISTER x_155 -> h_REGISTER x_155
    207199| ACC_A -> h_ACC_A
    208200| ACC_B -> h_ACC_B
    209201| DPTR -> h_DPTR
    210 | DATA x_14799 -> h_DATA x_14799
    211 | DATA16 x_14800 -> h_DATA16 x_14800
     202| DATA x_156 -> h_DATA x_156
     203| DATA16 x_157 -> h_DATA16 x_157
    212204| ACC_DPTR -> h_ACC_DPTR
    213205| ACC_PC -> h_ACC_PC
     
    215207| INDIRECT_DPTR -> h_INDIRECT_DPTR
    216208| CARRY -> h_CARRY
    217 | BIT_ADDR x_14801 -> h_BIT_ADDR x_14801
    218 | N_BIT_ADDR x_14802 -> h_N_BIT_ADDR x_14802
    219 | RELATIVE x_14803 -> h_RELATIVE x_14803
    220 | ADDR11 x_14804 -> h_ADDR11 x_14804
    221 | ADDR16 x_14805 -> h_ADDR16 x_14805
     209| BIT_ADDR x_158 -> h_BIT_ADDR x_158
     210| N_BIT_ADDR x_159 -> h_N_BIT_ADDR x_159
     211| RELATIVE x_160 -> h_RELATIVE x_160
     212| ADDR11 x_161 -> h_ADDR11 x_161
     213| ADDR16 x_162 -> h_ADDR16 x_162
    222214
    223215(** val addressing_mode_rect_Type1 :
     
    229221    -> 'a1) -> addressing_mode -> 'a1 **)
    230222let rec addressing_mode_rect_Type1 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
    231 | DIRECT x_14826 -> h_DIRECT x_14826
    232 | INDIRECT x_14827 -> h_INDIRECT x_14827
    233 | EXT_INDIRECT x_14828 -> h_EXT_INDIRECT x_14828
    234 | REGISTER x_14829 -> h_REGISTER x_14829
     223| DIRECT x_183 -> h_DIRECT x_183
     224| INDIRECT x_184 -> h_INDIRECT x_184
     225| EXT_INDIRECT x_185 -> h_EXT_INDIRECT x_185
     226| REGISTER x_186 -> h_REGISTER x_186
    235227| ACC_A -> h_ACC_A
    236228| ACC_B -> h_ACC_B
    237229| DPTR -> h_DPTR
    238 | DATA x_14830 -> h_DATA x_14830
    239 | DATA16 x_14831 -> h_DATA16 x_14831
     230| DATA x_187 -> h_DATA x_187
     231| DATA16 x_188 -> h_DATA16 x_188
    240232| ACC_DPTR -> h_ACC_DPTR
    241233| ACC_PC -> h_ACC_PC
     
    243235| INDIRECT_DPTR -> h_INDIRECT_DPTR
    244236| CARRY -> h_CARRY
    245 | BIT_ADDR x_14832 -> h_BIT_ADDR x_14832
    246 | N_BIT_ADDR x_14833 -> h_N_BIT_ADDR x_14833
    247 | RELATIVE x_14834 -> h_RELATIVE x_14834
    248 | ADDR11 x_14835 -> h_ADDR11 x_14835
    249 | ADDR16 x_14836 -> h_ADDR16 x_14836
     237| BIT_ADDR x_189 -> h_BIT_ADDR x_189
     238| N_BIT_ADDR x_190 -> h_N_BIT_ADDR x_190
     239| RELATIVE x_191 -> h_RELATIVE x_191
     240| ADDR11 x_192 -> h_ADDR11 x_192
     241| ADDR16 x_193 -> h_ADDR16 x_193
    250242
    251243(** val addressing_mode_rect_Type0 :
     
    257249    -> 'a1) -> addressing_mode -> 'a1 **)
    258250let rec addressing_mode_rect_Type0 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
    259 | DIRECT x_14857 -> h_DIRECT x_14857
    260 | INDIRECT x_14858 -> h_INDIRECT x_14858
    261 | EXT_INDIRECT x_14859 -> h_EXT_INDIRECT x_14859
    262 | REGISTER x_14860 -> h_REGISTER x_14860
     251| DIRECT x_214 -> h_DIRECT x_214
     252| INDIRECT x_215 -> h_INDIRECT x_215
     253| EXT_INDIRECT x_216 -> h_EXT_INDIRECT x_216
     254| REGISTER x_217 -> h_REGISTER x_217
    263255| ACC_A -> h_ACC_A
    264256| ACC_B -> h_ACC_B
    265257| DPTR -> h_DPTR
    266 | DATA x_14861 -> h_DATA x_14861
    267 | DATA16 x_14862 -> h_DATA16 x_14862
     258| DATA x_218 -> h_DATA x_218
     259| DATA16 x_219 -> h_DATA16 x_219
    268260| ACC_DPTR -> h_ACC_DPTR
    269261| ACC_PC -> h_ACC_PC
     
    271263| INDIRECT_DPTR -> h_INDIRECT_DPTR
    272264| CARRY -> h_CARRY
    273 | BIT_ADDR x_14863 -> h_BIT_ADDR x_14863
    274 | N_BIT_ADDR x_14864 -> h_N_BIT_ADDR x_14864
    275 | RELATIVE x_14865 -> h_RELATIVE x_14865
    276 | ADDR11 x_14866 -> h_ADDR11 x_14866
    277 | ADDR16 x_14867 -> h_ADDR16 x_14867
     265| BIT_ADDR x_220 -> h_BIT_ADDR x_220
     266| N_BIT_ADDR x_221 -> h_N_BIT_ADDR x_221
     267| RELATIVE x_222 -> h_RELATIVE x_222
     268| ADDR11 x_223 -> h_ADDR11 x_223
     269| ADDR16 x_224 -> h_ADDR16 x_224
    278270
    279271(** val addressing_mode_inv_rect_Type4 :
     
    19321924    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19331925    'a1) -> subaddressing_mode -> 'a1 **)
    1934 let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_15335 =
    1935   let subaddressing_modeel = x_15335 in
     1926let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_692 =
     1927  let subaddressing_modeel = x_692 in
    19361928  h_mk_subaddressing_mode subaddressing_modeel __
    19371929
     
    19391931    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19401932    'a1) -> subaddressing_mode -> 'a1 **)
    1941 let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_15337 =
    1942   let subaddressing_modeel = x_15337 in
     1933let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_694 =
     1934  let subaddressing_modeel = x_694 in
    19431935  h_mk_subaddressing_mode subaddressing_modeel __
    19441936
     
    19461938    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19471939    'a1) -> subaddressing_mode -> 'a1 **)
    1948 let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_15339 =
    1949   let subaddressing_modeel = x_15339 in
     1940let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_696 =
     1941  let subaddressing_modeel = x_696 in
    19501942  h_mk_subaddressing_mode subaddressing_modeel __
    19511943
     
    19531945    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19541946    'a1) -> subaddressing_mode -> 'a1 **)
    1955 let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_15341 =
    1956   let subaddressing_modeel = x_15341 in
     1947let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_698 =
     1948  let subaddressing_modeel = x_698 in
    19571949  h_mk_subaddressing_mode subaddressing_modeel __
    19581950
     
    19601952    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19611953    'a1) -> subaddressing_mode -> 'a1 **)
    1962 let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_15343 =
    1963   let subaddressing_modeel = x_15343 in
     1954let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_700 =
     1955  let subaddressing_modeel = x_700 in
    19641956  h_mk_subaddressing_mode subaddressing_modeel __
    19651957
     
    19671959    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19681960    'a1) -> subaddressing_mode -> 'a1 **)
    1969 let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_15345 =
    1970   let subaddressing_modeel = x_15345 in
     1961let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_702 =
     1962  let subaddressing_modeel = x_702 in
    19711963  h_mk_subaddressing_mode subaddressing_modeel __
    19721964
     
    21392131    'a2 -> 'a2 -> 'a1 preinstruction -> 'a2 **)
    21402132let rec preinstruction_rect_Type4 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP = function
    2141 | ADD (x_15445, x_15444) -> h_ADD x_15445 x_15444
    2142 | ADDC (x_15447, x_15446) -> h_ADDC x_15447 x_15446
    2143 | SUBB (x_15449, x_15448) -> h_SUBB x_15449 x_15448
    2144 | INC x_15450 -> h_INC x_15450
    2145 | DEC x_15451 -> h_DEC x_15451
    2146 | MUL (x_15453, x_15452) -> h_MUL x_15453 x_15452
    2147 | DIV (x_15455, x_15454) -> h_DIV x_15455 x_15454
    2148 | DA x_15456 -> h_DA x_15456
    2149 | JC x_15457 -> h_JC x_15457
    2150 | JNC x_15458 -> h_JNC x_15458
    2151 | JB (x_15460, x_15459) -> h_JB x_15460 x_15459
    2152 | JNB (x_15462, x_15461) -> h_JNB x_15462 x_15461
    2153 | JBC (x_15464, x_15463) -> h_JBC x_15464 x_15463
    2154 | JZ x_15465 -> h_JZ x_15465
    2155 | JNZ x_15466 -> h_JNZ x_15466
    2156 | CJNE (x_15468, x_15467) -> h_CJNE x_15468 x_15467
    2157 | DJNZ (x_15470, x_15469) -> h_DJNZ x_15470 x_15469
    2158 | ANL x_15471 -> h_ANL x_15471
    2159 | ORL x_15472 -> h_ORL x_15472
    2160 | XRL x_15473 -> h_XRL x_15473
    2161 | CLR x_15474 -> h_CLR x_15474
    2162 | CPL x_15475 -> h_CPL x_15475
    2163 | RL x_15476 -> h_RL x_15476
    2164 | RLC x_15477 -> h_RLC x_15477
    2165 | RR x_15478 -> h_RR x_15478
    2166 | RRC x_15479 -> h_RRC x_15479
    2167 | SWAP x_15480 -> h_SWAP x_15480
    2168 | MOV x_15481 -> h_MOV x_15481
    2169 | MOVX x_15482 -> h_MOVX x_15482
    2170 | SETB x_15483 -> h_SETB x_15483
    2171 | PUSH x_15484 -> h_PUSH x_15484
    2172 | POP x_15485 -> h_POP x_15485
    2173 | XCH (x_15487, x_15486) -> h_XCH x_15487 x_15486
    2174 | XCHD (x_15489, x_15488) -> h_XCHD x_15489 x_15488
     2133| ADD (x_802, x_801) -> h_ADD x_802 x_801
     2134| ADDC (x_804, x_803) -> h_ADDC x_804 x_803
     2135| SUBB (x_806, x_805) -> h_SUBB x_806 x_805
     2136| INC x_807 -> h_INC x_807
     2137| DEC x_808 -> h_DEC x_808
     2138| MUL (x_810, x_809) -> h_MUL x_810 x_809
     2139| DIV (x_812, x_811) -> h_DIV x_812 x_811
     2140| DA x_813 -> h_DA x_813
     2141| JC x_814 -> h_JC x_814
     2142| JNC x_815 -> h_JNC x_815
     2143| JB (x_817, x_816) -> h_JB x_817 x_816
     2144| JNB (x_819, x_818) -> h_JNB x_819 x_818
     2145| JBC (x_821, x_820) -> h_JBC x_821 x_820
     2146| JZ x_822 -> h_JZ x_822
     2147| JNZ x_823 -> h_JNZ x_823
     2148| CJNE (x_825, x_824) -> h_CJNE x_825 x_824
     2149| DJNZ (x_827, x_826) -> h_DJNZ x_827 x_826
     2150| ANL x_828 -> h_ANL x_828
     2151| ORL x_829 -> h_ORL x_829
     2152| XRL x_830 -> h_XRL x_830
     2153| CLR x_831 -> h_CLR x_831
     2154| CPL x_832 -> h_CPL x_832
     2155| RL x_833 -> h_RL x_833
     2156| RLC x_834 -> h_RLC x_834
     2157| RR x_835 -> h_RR x_835
     2158| RRC x_836 -> h_RRC x_836
     2159| SWAP x_837 -> h_SWAP x_837
     2160| MOV x_838 -> h_MOV x_838
     2161| MOVX x_839 -> h_MOVX x_839
     2162| SETB x_840 -> h_SETB x_840
     2163| PUSH x_841 -> h_PUSH x_841
     2164| POP x_842 -> h_POP x_842
     2165| XCH (x_844, x_843) -> h_XCH x_844 x_843
     2166| XCHD (x_846, x_845) -> h_XCHD x_846 x_845
    21752167| RET -> h_RET
    21762168| RETI -> h_RETI
     
    22132205    'a2 -> 'a2 -> 'a1 preinstruction -> 'a2 **)
    22142206let rec preinstruction_rect_Type5 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP = function
    2215 | ADD (x_15529, x_15528) -> h_ADD x_15529 x_15528
    2216 | ADDC (x_15531, x_15530) -> h_ADDC x_15531 x_15530
    2217 | SUBB (x_15533, x_15532) -> h_SUBB x_15533 x_15532
    2218 | INC x_15534 -> h_INC x_15534
    2219 | DEC x_15535 -> h_DEC x_15535
    2220 | MUL (x_15537, x_15536) -> h_MUL x_15537 x_15536
    2221 | DIV (x_15539, x_15538) -> h_DIV x_15539 x_15538
    2222 | DA x_15540 -> h_DA x_15540
    2223 | JC x_15541 -> h_JC x_15541
    2224 | JNC x_15542 -> h_JNC x_15542
    2225 | JB (x_15544, x_15543) -> h_JB x_15544 x_15543
    2226 | JNB (x_15546, x_15545) -> h_JNB x_15546 x_15545
    2227 | JBC (x_15548, x_15547) -> h_JBC x_15548 x_15547
    2228 | JZ x_15549 -> h_JZ x_15549
    2229 | JNZ x_15550 -> h_JNZ x_15550
    2230 | CJNE (x_15552, x_15551) -> h_CJNE x_15552 x_15551
    2231 | DJNZ (x_15554, x_15553) -> h_DJNZ x_15554 x_15553
    2232 | ANL x_15555 -> h_ANL x_15555
    2233 | ORL x_15556 -> h_ORL x_15556
    2234 | XRL x_15557 -> h_XRL x_15557
    2235 | CLR x_15558 -> h_CLR x_15558
    2236 | CPL x_15559 -> h_CPL x_15559
    2237 | RL x_15560 -> h_RL x_15560
    2238 | RLC x_15561 -> h_RLC x_15561
    2239 | RR x_15562 -> h_RR x_15562
    2240 | RRC x_15563 -> h_RRC x_15563
    2241 | SWAP x_15564 -> h_SWAP x_15564
    2242 | MOV x_15565 -> h_MOV x_15565
    2243 | MOVX x_15566 -> h_MOVX x_15566
    2244 | SETB x_15567 -> h_SETB x_15567
    2245 | PUSH x_15568 -> h_PUSH x_15568
    2246 | POP x_15569 -> h_POP x_15569
    2247 | XCH (x_15571, x_15570) -> h_XCH x_15571 x_15570
    2248 | XCHD (x_15573, x_15572) -> h_XCHD x_15573 x_15572
     2207| ADD (x_886, x_885) -> h_ADD x_886 x_885
     2208| ADDC (x_888, x_887) -> h_ADDC x_888 x_887
     2209| SUBB (x_890, x_889) -> h_SUBB x_890 x_889
     2210| INC x_891 -> h_INC x_891
     2211| DEC x_892 -> h_DEC x_892
     2212| MUL (x_894, x_893) -> h_MUL x_894 x_893
     2213| DIV (x_896, x_895) -> h_DIV x_896 x_895
     2214| DA x_897 -> h_DA x_897
     2215| JC x_898 -> h_JC x_898
     2216| JNC x_899 -> h_JNC x_899
     2217| JB (x_901, x_900) -> h_JB x_901 x_900
     2218| JNB (x_903, x_902) -> h_JNB x_903 x_902
     2219| JBC (x_905, x_904) -> h_JBC x_905 x_904
     2220| JZ x_906 -> h_JZ x_906
     2221| JNZ x_907 -> h_JNZ x_907
     2222| CJNE (x_909, x_908) -> h_CJNE x_909 x_908
     2223| DJNZ (x_911, x_910) -> h_DJNZ x_911 x_910
     2224| ANL x_912 -> h_ANL x_912
     2225| ORL x_913 -> h_ORL x_913
     2226| XRL x_914 -> h_XRL x_914
     2227| CLR x_915 -> h_CLR x_915
     2228| CPL x_916 -> h_CPL x_916
     2229| RL x_917 -> h_RL x_917
     2230| RLC x_918 -> h_RLC x_918
     2231| RR x_919 -> h_RR x_919
     2232| RRC x_920 -> h_RRC x_920
     2233| SWAP x_921 -> h_SWAP x_921
     2234| MOV x_922 -> h_MOV x_922
     2235| MOVX x_923 -> h_MOVX x_923
     2236| SETB x_924 -> h_SETB x_924
     2237| PUSH x_925 -> h_PUSH x_925
     2238| POP x_926 -> h_POP x_926
     2239| XCH (x_928, x_927) -> h_XCH x_928 x_927
     2240| XCHD (x_930, x_929) -> h_XCHD x_930 x_929
    22492241| RET -> h_RET
    22502242| RETI -> h_RETI
     
    22872279    'a2 -> 'a2 -> 'a1 preinstruction -> 'a2 **)
    22882280let rec preinstruction_rect_Type3 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP = function
    2289 | ADD (x_15613, x_15612) -> h_ADD x_15613 x_15612
    2290 | ADDC (x_15615, x_15614) -> h_ADDC x_15615 x_15614
    2291 | SUBB (x_15617, x_15616) -> h_SUBB x_15617 x_15616
    2292 | INC x_15618 -> h_INC x_15618
    2293 | DEC x_15619 -> h_DEC x_15619
    2294 | MUL (x_15621, x_15620) -> h_MUL x_15621 x_15620
    2295 | DIV (x_15623, x_15622) -> h_DIV x_15623 x_15622
    2296 | DA x_15624 -> h_DA x_15624
    2297 | JC x_15625 -> h_JC x_15625
    2298 | JNC x_15626 -> h_JNC x_15626
    2299 | JB (x_15628, x_15627) -> h_JB x_15628 x_15627
    2300 | JNB (x_15630, x_15629) -> h_JNB x_15630 x_15629
    2301 | JBC (x_15632, x_15631) -> h_JBC x_15632 x_15631
    2302 | JZ x_15633 -> h_JZ x_15633
    2303 | JNZ x_15634 -> h_JNZ x_15634
    2304 | CJNE (x_15636, x_15635) -> h_CJNE x_15636 x_15635
    2305 | DJNZ (x_15638, x_15637) -> h_DJNZ x_15638 x_15637
    2306 | ANL x_15639 -> h_ANL x_15639
    2307 | ORL x_15640 -> h_ORL x_15640
    2308 | XRL x_15641 -> h_XRL x_15641
    2309 | CLR x_15642 -> h_CLR x_15642
    2310 | CPL x_15643 -> h_CPL x_15643
    2311 | RL x_15644 -> h_RL x_15644
    2312 | RLC x_15645 -> h_RLC x_15645
    2313 | RR x_15646 -> h_RR x_15646
    2314 | RRC x_15647 -> h_RRC x_15647
    2315 | SWAP x_15648 -> h_SWAP x_15648
    2316 | MOV x_15649 -> h_MOV x_15649
    2317 | MOVX x_15650 -> h_MOVX x_15650
    2318 | SETB x_15651 -> h_SETB x_15651
    2319 | PUSH x_15652 -> h_PUSH x_15652
    2320 | POP x_15653 -> h_POP x_15653
    2321 | XCH (x_15655, x_15654) -> h_XCH x_15655 x_15654
    2322 | XCHD (x_15657, x_15656) -> h_XCHD x_15657 x_15656
     2281| ADD (x_970, x_969) -> h_ADD x_970 x_969
     2282| ADDC (x_972, x_971) -> h_ADDC x_972 x_971
     2283| SUBB (x_974, x_973) -> h_SUBB x_974 x_973
     2284| INC x_975 -> h_INC x_975
     2285| DEC x_976 -> h_DEC x_976
     2286| MUL (x_978, x_977) -> h_MUL x_978 x_977
     2287| DIV (x_980, x_979) -> h_DIV x_980 x_979
     2288| DA x_981 -> h_DA x_981
     2289| JC x_982 -> h_JC x_982
     2290| JNC x_983 -> h_JNC x_983
     2291| JB (x_985, x_984) -> h_JB x_985 x_984
     2292| JNB (x_987, x_986) -> h_JNB x_987 x_986
     2293| JBC (x_989, x_988) -> h_JBC x_989 x_988
     2294| JZ x_990 -> h_JZ x_990
     2295| JNZ x_991 -> h_JNZ x_991
     2296| CJNE (x_993, x_992) -> h_CJNE x_993 x_992
     2297| DJNZ (x_995, x_994) -> h_DJNZ x_995 x_994
     2298| ANL x_996 -> h_ANL x_996
     2299| ORL x_997 -> h_ORL x_997
     2300| XRL x_998 -> h_XRL x_998
     2301| CLR x_999 -> h_CLR x_999
     2302| CPL x_1000 -> h_CPL x_1000
     2303| RL x_1001 -> h_RL x_1001
     2304| RLC x_1002 -> h_RLC x_1002
     2305| RR x_1003 -> h_RR x_1003
     2306| RRC x_1004 -> h_RRC x_1004
     2307| SWAP x_1005 -> h_SWAP x_1005
     2308| MOV x_1006 -> h_MOV x_1006
     2309| MOVX x_1007 -> h_MOVX x_1007
     2310| SETB x_1008 -> h_SETB x_1008
     2311| PUSH x_1009 -> h_PUSH x_1009
     2312| POP x_1010 -> h_POP x_1010
     2313| XCH (x_1012, x_1011) -> h_XCH x_1012 x_1011
     2314| XCHD (x_1014, x_1013) -> h_XCHD x_1014 x_1013
    23232315| RET -> h_RET
    23242316| RETI -> h_RETI
     
    23612353    'a2 -> 'a2 -> 'a1 preinstruction -> 'a2 **)
    23622354let rec preinstruction_rect_Type2 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP = function
    2363 | ADD (x_15697, x_15696) -> h_ADD x_15697 x_15696
    2364 | ADDC (x_15699, x_15698) -> h_ADDC x_15699 x_15698
    2365 | SUBB (x_15701, x_15700) -> h_SUBB x_15701 x_15700
    2366 | INC x_15702 -> h_INC x_15702
    2367 | DEC x_15703 -> h_DEC x_15703
    2368 | MUL (x_15705, x_15704) -> h_MUL x_15705 x_15704
    2369 | DIV (x_15707, x_15706) -> h_DIV x_15707 x_15706
    2370 | DA x_15708 -> h_DA x_15708
    2371 | JC x_15709 -> h_JC x_15709
    2372 | JNC x_15710 -> h_JNC x_15710
    2373 | JB (x_15712, x_15711) -> h_JB x_15712 x_15711
    2374 | JNB (x_15714, x_15713) -> h_JNB x_15714 x_15713
    2375 | JBC (x_15716, x_15715) -> h_JBC x_15716 x_15715
    2376 | JZ x_15717 -> h_JZ x_15717
    2377 | JNZ x_15718 -> h_JNZ x_15718
    2378 | CJNE (x_15720, x_15719) -> h_CJNE x_15720 x_15719
    2379 | DJNZ (x_15722, x_15721) -> h_DJNZ x_15722 x_15721
    2380 | ANL x_15723 -> h_ANL x_15723
    2381 | ORL x_15724 -> h_ORL x_15724
    2382 | XRL x_15725 -> h_XRL x_15725
    2383 | CLR x_15726 -> h_CLR x_15726
    2384 | CPL x_15727 -> h_CPL x_15727
    2385 | RL x_15728 -> h_RL x_15728
    2386 | RLC x_15729 -> h_RLC x_15729
    2387 | RR x_15730 -> h_RR x_15730
    2388 | RRC x_15731 -> h_RRC x_15731
    2389 | SWAP x_15732 -> h_SWAP x_15732
    2390 | MOV x_15733 -> h_MOV x_15733
    2391 | MOVX x_15734 -> h_MOVX x_15734
    2392 | SETB x_15735 -> h_SETB x_15735
    2393 | PUSH x_15736 -> h_PUSH x_15736
    2394 | POP x_15737 -> h_POP x_15737
    2395 | XCH (x_15739, x_15738) -> h_XCH x_15739 x_15738
    2396 | XCHD (x_15741, x_15740) -> h_XCHD x_15741 x_15740
     2355| ADD (x_1054, x_1053) -> h_ADD x_1054 x_1053
     2356| ADDC (x_1056, x_1055) -> h_ADDC x_1056 x_1055
     2357| SUBB (x_1058, x_1057) -> h_SUBB x_1058 x_1057
     2358| INC x_1059 -> h_INC x_1059
     2359| DEC x_1060 -> h_DEC x_1060
     2360| MUL (x_1062, x_1061) -> h_MUL x_1062 x_1061
     2361| DIV (x_1064, x_1063) -> h_DIV x_1064 x_1063
     2362| DA x_1065 -> h_DA x_1065
     2363| JC x_1066 -> h_JC x_1066
     2364| JNC x_1067 -> h_JNC x_1067
     2365| JB (x_1069, x_1068) -> h_JB x_1069 x_1068
     2366| JNB (x_1071, x_1070) -> h_JNB x_1071 x_1070
     2367| JBC (x_1073, x_1072) -> h_JBC x_1073 x_1072
     2368| JZ x_1074 -> h_JZ x_1074
     2369| JNZ x_1075 -> h_JNZ x_1075
     2370| CJNE (x_1077, x_1076) -> h_CJNE x_1077 x_1076
     2371| DJNZ (x_1079, x_1078) -> h_DJNZ x_1079 x_1078
     2372| ANL x_1080 -> h_ANL x_1080
     2373| ORL x_1081 -> h_ORL x_1081
     2374| XRL x_1082 -> h_XRL x_1082
     2375| CLR x_1083 -> h_CLR x_1083
     2376| CPL x_1084 -> h_CPL x_1084
     2377| RL x_1085 -> h_RL x_1085
     2378| RLC x_1086 -> h_RLC x_1086
     2379| RR x_1087 -> h_RR x_1087
     2380| RRC x_1088 -> h_RRC x_1088
     2381| SWAP x_1089 -> h_SWAP x_1089
     2382| MOV x_1090 -> h_MOV x_1090
     2383| MOVX x_1091 -> h_MOVX x_1091
     2384| SETB x_1092 -> h_SETB x_1092
     2385| PUSH x_1093 -> h_PUSH x_1093
     2386| POP x_1094 -> h_POP x_1094
     2387| XCH (x_1096, x_1095) -> h_XCH x_1096 x_1095
     2388| XCHD (x_1098, x_1097) -> h_XCHD x_1098 x_1097
    23972389| RET -> h_RET
    23982390| RETI -> h_RETI
     
    24352427    'a2 -> 'a2 -> 'a1 preinstruction -> 'a2 **)
    24362428let rec preinstruction_rect_Type1 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP = function
    2437 | ADD (x_15781, x_15780) -> h_ADD x_15781 x_15780
    2438 | ADDC (x_15783, x_15782) -> h_ADDC x_15783 x_15782
    2439 | SUBB (x_15785, x_15784) -> h_SUBB x_15785 x_15784
    2440 | INC x_15786 -> h_INC x_15786
    2441 | DEC x_15787 -> h_DEC x_15787
    2442 | MUL (x_15789, x_15788) -> h_MUL x_15789 x_15788
    2443 | DIV (x_15791, x_15790) -> h_DIV x_15791 x_15790
    2444 | DA x_15792 -> h_DA x_15792
    2445 | JC x_15793 -> h_JC x_15793
    2446 | JNC x_15794 -> h_JNC x_15794
    2447 | JB (x_15796, x_15795) -> h_JB x_15796 x_15795
    2448 | JNB (x_15798, x_15797) -> h_JNB x_15798 x_15797
    2449 | JBC (x_15800, x_15799) -> h_JBC x_15800 x_15799
    2450 | JZ x_15801 -> h_JZ x_15801
    2451 | JNZ x_15802 -> h_JNZ x_15802
    2452 | CJNE (x_15804, x_15803) -> h_CJNE x_15804 x_15803
    2453 | DJNZ (x_15806, x_15805) -> h_DJNZ x_15806 x_15805
    2454 | ANL x_15807 -> h_ANL x_15807
    2455 | ORL x_15808 -> h_ORL x_15808
    2456 | XRL x_15809 -> h_XRL x_15809
    2457 | CLR x_15810 -> h_CLR x_15810
    2458 | CPL x_15811 -> h_CPL x_15811
    2459 | RL x_15812 -> h_RL x_15812
    2460 | RLC x_15813 -> h_RLC x_15813
    2461 | RR x_15814 -> h_RR x_15814
    2462 | RRC x_15815 -> h_RRC x_15815
    2463 | SWAP x_15816 -> h_SWAP x_15816
    2464 | MOV x_15817 -> h_MOV x_15817
    2465 | MOVX x_15818 -> h_MOVX x_15818
    2466 | SETB x_15819 -> h_SETB x_15819
    2467 | PUSH x_15820 -> h_PUSH x_15820
    2468 | POP x_15821 -> h_POP x_15821
    2469 | XCH (x_15823, x_15822) -> h_XCH x_15823 x_15822
    2470 | XCHD (x_15825, x_15824) -> h_XCHD x_15825 x_15824
     2429| ADD (x_1138, x_1137) -> h_ADD x_1138 x_1137
     2430| ADDC (x_1140, x_1139) -> h_ADDC x_1140 x_1139
     2431| SUBB (x_1142, x_1141) -> h_SUBB x_1142 x_1141
     2432| INC x_1143 -> h_INC x_1143
     2433| DEC x_1144 -> h_DEC x_1144
     2434| MUL (x_1146, x_1145) -> h_MUL x_1146 x_1145
     2435| DIV (x_1148, x_1147) -> h_DIV x_1148 x_1147
     2436| DA x_1149 -> h_DA x_1149
     2437| JC x_1150 -> h_JC x_1150
     2438| JNC x_1151 -> h_JNC x_1151
     2439| JB (x_1153, x_1152) -> h_JB x_1153 x_1152
     2440| JNB (x_1155, x_1154) -> h_JNB x_1155 x_1154
     2441| JBC (x_1157, x_1156) -> h_JBC x_1157 x_1156
     2442| JZ x_1158 -> h_JZ x_1158
     2443| JNZ x_1159 -> h_JNZ x_1159
     2444| CJNE (x_1161, x_1160) -> h_CJNE x_1161 x_1160
     2445| DJNZ (x_1163, x_1162) -> h_DJNZ x_1163 x_1162
     2446| ANL x_1164 -> h_ANL x_1164
     2447| ORL x_1165 -> h_ORL x_1165
     2448| XRL x_1166 -> h_XRL x_1166
     2449| CLR x_1167 -> h_CLR x_1167
     2450| CPL x_1168 -> h_CPL x_1168
     2451| RL x_1169 -> h_RL x_1169
     2452| RLC x_1170 -> h_RLC x_1170
     2453| RR x_1171 -> h_RR x_1171
     2454| RRC x_1172 -> h_RRC x_1172
     2455| SWAP x_1173 -> h_SWAP x_1173
     2456| MOV x_1174 -> h_MOV x_1174
     2457| MOVX x_1175 -> h_MOVX x_1175
     2458| SETB x_1176 -> h_SETB x_1176
     2459| PUSH x_1177 -> h_PUSH x_1177
     2460| POP x_1178 -> h_POP x_1178
     2461| XCH (x_1180, x_1179) -> h_XCH x_1180 x_1179
     2462| XCHD (x_1182, x_1181) -> h_XCHD x_1182 x_1181
    24712463| RET -> h_RET
    24722464| RETI -> h_RETI
     
    25092501    'a2 -> 'a2 -> 'a1 preinstruction -> 'a2 **)
    25102502let rec preinstruction_rect_Type0 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP = function
    2511 | ADD (x_15865, x_15864) -> h_ADD x_15865 x_15864
    2512 | ADDC (x_15867, x_15866) -> h_ADDC x_15867 x_15866
    2513 | SUBB (x_15869, x_15868) -> h_SUBB x_15869 x_15868
    2514 | INC x_15870 -> h_INC x_15870
    2515 | DEC x_15871 -> h_DEC x_15871
    2516 | MUL (x_15873, x_15872) -> h_MUL x_15873 x_15872
    2517 | DIV (x_15875, x_15874) -> h_DIV x_15875 x_15874
    2518 | DA x_15876 -> h_DA x_15876
    2519 | JC x_15877 -> h_JC x_15877
    2520 | JNC x_15878 -> h_JNC x_15878
    2521 | JB (x_15880, x_15879) -> h_JB x_15880 x_15879
    2522 | JNB (x_15882, x_15881) -> h_JNB x_15882 x_15881
    2523 | JBC (x_15884, x_15883) -> h_JBC x_15884 x_15883
    2524 | JZ x_15885 -> h_JZ x_15885
    2525 | JNZ x_15886 -> h_JNZ x_15886
    2526 | CJNE (x_15888, x_15887) -> h_CJNE x_15888 x_15887
    2527 | DJNZ (x_15890, x_15889) -> h_DJNZ x_15890 x_15889
    2528 | ANL x_15891 -> h_ANL x_15891
    2529 | ORL x_15892 -> h_ORL x_15892
    2530 | XRL x_15893 -> h_XRL x_15893
    2531 | CLR x_15894 -> h_CLR x_15894
    2532 | CPL x_15895 -> h_CPL x_15895
    2533 | RL x_15896 -> h_RL x_15896
    2534 | RLC x_15897 -> h_RLC x_15897
    2535 | RR x_15898 -> h_RR x_15898
    2536 | RRC x_15899 -> h_RRC x_15899
    2537 | SWAP x_15900 -> h_SWAP x_15900
    2538 | MOV x_15901 -> h_MOV x_15901
    2539 | MOVX x_15902 -> h_MOVX x_15902
    2540 | SETB x_15903 -> h_SETB x_15903
    2541 | PUSH x_15904 -> h_PUSH x_15904
    2542 | POP x_15905 -> h_POP x_15905
    2543 | XCH (x_15907, x_15906) -> h_XCH x_15907 x_15906
    2544 | XCHD (x_15909, x_15908) -> h_XCHD x_15909 x_15908
     2503| ADD (x_1222, x_1221) -> h_ADD x_1222 x_1221
     2504| ADDC (x_1224, x_1223) -> h_ADDC x_1224 x_1223
     2505| SUBB (x_1226, x_1225) -> h_SUBB x_1226 x_1225
     2506| INC x_1227 -> h_INC x_1227
     2507| DEC x_1228 -> h_DEC x_1228
     2508| MUL (x_1230, x_1229) -> h_MUL x_1230 x_1229
     2509| DIV (x_1232, x_1231) -> h_DIV x_1232 x_1231
     2510| DA x_1233 -> h_DA x_1233
     2511| JC x_1234 -> h_JC x_1234
     2512| JNC x_1235 -> h_JNC x_1235
     2513| JB (x_1237, x_1236) -> h_JB x_1237 x_1236
     2514| JNB (x_1239, x_1238) -> h_JNB x_1239 x_1238
     2515| JBC (x_1241, x_1240) -> h_JBC x_1241 x_1240
     2516| JZ x_1242 -> h_JZ x_1242
     2517| JNZ x_1243 -> h_JNZ x_1243
     2518| CJNE (x_1245, x_1244) -> h_CJNE x_1245 x_1244
     2519| DJNZ (x_1247, x_1246) -> h_DJNZ x_1247 x_1246
     2520| ANL x_1248 -> h_ANL x_1248
     2521| ORL x_1249 -> h_ORL x_1249
     2522| XRL x_1250 -> h_XRL x_1250
     2523| CLR x_1251 -> h_CLR x_1251
     2524| CPL x_1252 -> h_CPL x_1252
     2525| RL x_1253 -> h_RL x_1253
     2526| RLC x_1254 -> h_RLC x_1254
     2527| RR x_1255 -> h_RR x_1255
     2528| RRC x_1256 -> h_RRC x_1256
     2529| SWAP x_1257 -> h_SWAP x_1257
     2530| MOV x_1258 -> h_MOV x_1258
     2531| MOVX x_1259 -> h_MOVX x_1259
     2532| SETB x_1260 -> h_SETB x_1260
     2533| PUSH x_1261 -> h_PUSH x_1261
     2534| POP x_1262 -> h_POP x_1262
     2535| XCH (x_1264, x_1263) -> h_XCH x_1264 x_1263
     2536| XCHD (x_1266, x_1265) -> h_XCHD x_1266 x_1265
    25452537| RET -> h_RET
    25462538| RETI -> h_RETI
     
    48664858    preinstruction -> 'a1) -> instruction -> 'a1 **)
    48674859let rec instruction_rect_Type4 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_JMP h_MOVC h_RealInstruction = function
    4868 | ACALL x_16470 -> h_ACALL x_16470
    4869 | LCALL x_16471 -> h_LCALL x_16471
    4870 | AJMP x_16472 -> h_AJMP x_16472
    4871 | LJMP x_16473 -> h_LJMP x_16473
    4872 | SJMP x_16474 -> h_SJMP x_16474
    4873 | JMP x_16475 -> h_JMP x_16475
    4874 | MOVC (x_16477, x_16476) -> h_MOVC x_16477 x_16476
    4875 | RealInstruction x_16478 -> h_RealInstruction x_16478
     4860| ACALL x_1827 -> h_ACALL x_1827
     4861| LCALL x_1828 -> h_LCALL x_1828
     4862| AJMP x_1829 -> h_AJMP x_1829
     4863| LJMP x_1830 -> h_LJMP x_1830
     4864| SJMP x_1831 -> h_SJMP x_1831
     4865| JMP x_1832 -> h_JMP x_1832
     4866| MOVC (x_1834, x_1833) -> h_MOVC x_1834 x_1833
     4867| RealInstruction x_1835 -> h_RealInstruction x_1835
    48764868
    48774869(** val instruction_rect_Type5 :
     
    48824874    preinstruction -> 'a1) -> instruction -> 'a1 **)
    48834875let rec instruction_rect_Type5 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_JMP h_MOVC h_RealInstruction = function
    4884 | ACALL x_16488 -> h_ACALL x_16488
    4885 | LCALL x_16489 -> h_LCALL x_16489
    4886 | AJMP x_16490 -> h_AJMP x_16490
    4887 | LJMP x_16491 -> h_LJMP x_16491
    4888 | SJMP x_16492 -> h_SJMP x_16492
    4889 | JMP x_16493 -> h_JMP x_16493
    4890 | MOVC (x_16495, x_16494) -> h_MOVC x_16495 x_16494
    4891 | RealInstruction x_16496 -> h_RealInstruction x_16496
     4876| ACALL x_1845 -> h_ACALL x_1845
     4877| LCALL x_1846 -> h_LCALL x_1846
     4878| AJMP x_1847 -> h_AJMP x_1847
     4879| LJMP x_1848 -> h_LJMP x_1848
     4880| SJMP x_1849 -> h_SJMP x_1849
     4881| JMP x_1850 -> h_JMP x_1850
     4882| MOVC (x_1852, x_1851) -> h_MOVC x_1852 x_1851
     4883| RealInstruction x_1853 -> h_RealInstruction x_1853
    48924884
    48934885(** val instruction_rect_Type3 :
     
    48984890    preinstruction -> 'a1) -> instruction -> 'a1 **)
    48994891let rec instruction_rect_Type3 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_JMP h_MOVC h_RealInstruction = function
    4900 | ACALL x_16506 -> h_ACALL x_16506
    4901 | LCALL x_16507 -> h_LCALL x_16507
    4902 | AJMP x_16508 -> h_AJMP x_16508
    4903 | LJMP x_16509 -> h_LJMP x_16509
    4904 | SJMP x_16510 -> h_SJMP x_16510
    4905 | JMP x_16511 -> h_JMP x_16511
    4906 | MOVC (x_16513, x_16512) -> h_MOVC x_16513 x_16512
    4907 | RealInstruction x_16514 -> h_RealInstruction x_16514
     4892| ACALL x_1863 -> h_ACALL x_1863
     4893| LCALL x_1864 -> h_LCALL x_1864
     4894| AJMP x_1865 -> h_AJMP x_1865
     4895| LJMP x_1866 -> h_LJMP x_1866
     4896| SJMP x_1867 -> h_SJMP x_1867
     4897| JMP x_1868 -> h_JMP x_1868
     4898| MOVC (x_1870, x_1869) -> h_MOVC x_1870 x_1869
     4899| RealInstruction x_1871 -> h_RealInstruction x_1871
    49084900
    49094901(** val instruction_rect_Type2 :
     
    49144906    preinstruction -> 'a1) -> instruction -> 'a1 **)
    49154907let rec instruction_rect_Type2 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_JMP h_MOVC h_RealInstruction = function
    4916 | ACALL x_16524 -> h_ACALL x_16524
    4917 | LCALL x_16525 -> h_LCALL x_16525
    4918 | AJMP x_16526 -> h_AJMP x_16526
    4919 | LJMP x_16527 -> h_LJMP x_16527
    4920 | SJMP x_16528 -> h_SJMP x_16528
    4921 | JMP x_16529 -> h_JMP x_16529
    4922 | MOVC (x_16531, x_16530) -> h_MOVC x_16531 x_16530
    4923 | RealInstruction x_16532 -> h_RealInstruction x_16532
     4908| ACALL x_1881 -> h_ACALL x_1881
     4909| LCALL x_1882 -> h_LCALL x_1882
     4910| AJMP x_1883 -> h_AJMP x_1883
     4911| LJMP x_1884 -> h_LJMP x_1884
     4912| SJMP x_1885 -> h_SJMP x_1885
     4913| JMP x_1886 -> h_JMP x_1886
     4914| MOVC (x_1888, x_1887) -> h_MOVC x_1888 x_1887
     4915| RealInstruction x_1889 -> h_RealInstruction x_1889
    49244916
    49254917(** val instruction_rect_Type1 :
     
    49304922    preinstruction -> 'a1) -> instruction -> 'a1 **)
    49314923let rec instruction_rect_Type1 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_JMP h_MOVC h_RealInstruction = function
    4932 | ACALL x_16542 -> h_ACALL x_16542
    4933 | LCALL x_16543 -> h_LCALL x_16543
    4934 | AJMP x_16544 -> h_AJMP x_16544
    4935 | LJMP x_16545 -> h_LJMP x_16545
    4936 | SJMP x_16546 -> h_SJMP x_16546
    4937 | JMP x_16547 -> h_JMP x_16547
    4938 | MOVC (x_16549, x_16548) -> h_MOVC x_16549 x_16548
    4939 | RealInstruction x_16550 -> h_RealInstruction x_16550
     4924| ACALL x_1899 -> h_ACALL x_1899
     4925| LCALL x_1900 -> h_LCALL x_1900
     4926| AJMP x_1901 -> h_AJMP x_1901
     4927| LJMP x_1902 -> h_LJMP x_1902
     4928| SJMP x_1903 -> h_SJMP x_1903
     4929| JMP x_1904 -> h_JMP x_1904
     4930| MOVC (x_1906, x_1905) -> h_MOVC x_1906 x_1905
     4931| RealInstruction x_1907 -> h_RealInstruction x_1907
    49404932
    49414933(** val instruction_rect_Type0 :
     
    49464938    preinstruction -> 'a1) -> instruction -> 'a1 **)
    49474939let rec instruction_rect_Type0 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_JMP h_MOVC h_RealInstruction = function
    4948 | ACALL x_16560 -> h_ACALL x_16560
    4949 | LCALL x_16561 -> h_LCALL x_16561
    4950 | AJMP x_16562 -> h_AJMP x_16562
    4951 | LJMP x_16563 -> h_LJMP x_16563
    4952 | SJMP x_16564 -> h_SJMP x_16564
    4953 | JMP x_16565 -> h_JMP x_16565
    4954 | MOVC (x_16567, x_16566) -> h_MOVC x_16567 x_16566
    4955 | RealInstruction x_16568 -> h_RealInstruction x_16568
     4940| ACALL x_1917 -> h_ACALL x_1917
     4941| LCALL x_1918 -> h_LCALL x_1918
     4942| AJMP x_1919 -> h_AJMP x_1919
     4943| LJMP x_1920 -> h_LJMP x_1920
     4944| SJMP x_1921 -> h_SJMP x_1921
     4945| JMP x_1922 -> h_JMP x_1922
     4946| MOVC (x_1924, x_1923) -> h_MOVC x_1924 x_1923
     4947| RealInstruction x_1925 -> h_RealInstruction x_1925
    49564948
    49574949(** val instruction_inv_rect_Type4 :
     
    51655157    -> 'a1 **)
    51665158let rec pseudo_instruction_rect_Type4 h_Instruction h_Comment h_Cost h_Jmp h_Call h_Mov = function
    5167 | Instruction x_16700 -> h_Instruction x_16700
    5168 | Comment x_16701 -> h_Comment x_16701
    5169 | Cost x_16702 -> h_Cost x_16702
    5170 | Jmp x_16703 -> h_Jmp x_16703
    5171 | Call x_16704 -> h_Call x_16704
    5172 | Mov (x_16706, x_16705) -> h_Mov x_16706 x_16705
     5159| Instruction x_2057 -> h_Instruction x_2057
     5160| Comment x_2058 -> h_Comment x_2058
     5161| Cost x_2059 -> h_Cost x_2059
     5162| Jmp x_2060 -> h_Jmp x_2060
     5163| Call x_2061 -> h_Call x_2061
     5164| Mov (x_2063, x_2062) -> h_Mov x_2063 x_2062
    51735165
    51745166(** val pseudo_instruction_rect_Type5 :
     
    51785170    -> 'a1 **)
    51795171let rec pseudo_instruction_rect_Type5 h_Instruction h_Comment h_Cost h_Jmp h_Call h_Mov = function
    5180 | Instruction x_16714 -> h_Instruction x_16714
    5181 | Comment x_16715 -> h_Comment x_16715
    5182 | Cost x_16716 -> h_Cost x_16716
    5183 | Jmp x_16717 -> h_Jmp x_16717
    5184 | Call x_16718 -> h_Call x_16718
    5185 | Mov (x_16720, x_16719) -> h_Mov x_16720 x_16719
     5172| Instruction x_2071 -> h_Instruction x_2071
     5173| Comment x_2072 -> h_Comment x_2072
     5174| Cost x_2073 -> h_Cost x_2073
     5175| Jmp x_2074 -> h_Jmp x_2074
     5176| Call x_2075 -> h_Call x_2075
     5177| Mov (x_2077, x_2076) -> h_Mov x_2077 x_2076
    51865178
    51875179(** val pseudo_instruction_rect_Type3 :
     
    51915183    -> 'a1 **)
    51925184let rec pseudo_instruction_rect_Type3 h_Instruction h_Comment h_Cost h_Jmp h_Call h_Mov = function
    5193 | Instruction x_16728 -> h_Instruction x_16728
    5194 | Comment x_16729 -> h_Comment x_16729
    5195 | Cost x_16730 -> h_Cost x_16730
    5196 | Jmp x_16731 -> h_Jmp x_16731
    5197 | Call x_16732 -> h_Call x_16732
    5198 | Mov (x_16734, x_16733) -> h_Mov x_16734 x_16733
     5185| Instruction x_2085 -> h_Instruction x_2085
     5186| Comment x_2086 -> h_Comment x_2086
     5187| Cost x_2087 -> h_Cost x_2087
     5188| Jmp x_2088 -> h_Jmp x_2088
     5189| Call x_2089 -> h_Call x_2089
     5190| Mov (x_2091, x_2090) -> h_Mov x_2091 x_2090
    51995191
    52005192(** val pseudo_instruction_rect_Type2 :
     
    52045196    -> 'a1 **)
    52055197let rec pseudo_instruction_rect_Type2 h_Instruction h_Comment h_Cost h_Jmp h_Call h_Mov = function
    5206 | Instruction x_16742 -> h_Instruction x_16742
    5207 | Comment x_16743 -> h_Comment x_16743
    5208 | Cost x_16744 -> h_Cost x_16744
    5209 | Jmp x_16745 -> h_Jmp x_16745
    5210 | Call x_16746 -> h_Call x_16746
    5211 | Mov (x_16748, x_16747) -> h_Mov x_16748 x_16747
     5198| Instruction x_2099 -> h_Instruction x_2099
     5199| Comment x_2100 -> h_Comment x_2100
     5200| Cost x_2101 -> h_Cost x_2101
     5201| Jmp x_2102 -> h_Jmp x_2102
     5202| Call x_2103 -> h_Call x_2103
     5203| Mov (x_2105, x_2104) -> h_Mov x_2105 x_2104
    52125204
    52135205(** val pseudo_instruction_rect_Type1 :
     
    52175209    -> 'a1 **)
    52185210let rec pseudo_instruction_rect_Type1 h_Instruction h_Comment h_Cost h_Jmp h_Call h_Mov = function
    5219 | Instruction x_16756 -> h_Instruction x_16756
    5220 | Comment x_16757 -> h_Comment x_16757
    5221 | Cost x_16758 -> h_Cost x_16758
    5222 | Jmp x_16759 -> h_Jmp x_16759
    5223 | Call x_16760 -> h_Call x_16760
    5224 | Mov (x_16762, x_16761) -> h_Mov x_16762 x_16761
     5211| Instruction x_2113 -> h_Instruction x_2113
     5212| Comment x_2114 -> h_Comment x_2114
     5213| Cost x_2115 -> h_Cost x_2115
     5214| Jmp x_2116 -> h_Jmp x_2116
     5215| Call x_2117 -> h_Call x_2117
     5216| Mov (x_2119, x_2118) -> h_Mov x_2119 x_2118
    52255217
    52265218(** val pseudo_instruction_rect_Type0 :
     
    52305222    -> 'a1 **)
    52315223let rec pseudo_instruction_rect_Type0 h_Instruction h_Comment h_Cost h_Jmp h_Call h_Mov = function
    5232 | Instruction x_16770 -> h_Instruction x_16770
    5233 | Comment x_16771 -> h_Comment x_16771
    5234 | Cost x_16772 -> h_Cost x_16772
    5235 | Jmp x_16773 -> h_Jmp x_16773
    5236 | Call x_16774 -> h_Call x_16774
    5237 | Mov (x_16776, x_16775) -> h_Mov x_16776 x_16775
     5224| Instruction x_2127 -> h_Instruction x_2127
     5225| Comment x_2128 -> h_Comment x_2128
     5226| Cost x_2129 -> h_Cost x_2129
     5227| Jmp x_2130 -> h_Jmp x_2130
     5228| Call x_2131 -> h_Call x_2131
     5229| Mov (x_2133, x_2132) -> h_Mov x_2133 x_2132
    52385230
    52395231(** val pseudo_instruction_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.