Changeset 2717 for extracted/aSM.ml


Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (7 years ago)
Author:
sacerdot
Message:

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/aSM.ml

    r2649 r2717  
    6060
    6161open Identifiers
     62
     63open BitVectorTrie
     64
     65open Exp
    6266
    6367open Arithmetic
     
    109113    -> 'a1) -> addressing_mode -> 'a1 **)
    110114let 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
    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
     115| DIRECT x_18716 -> h_DIRECT x_18716
     116| INDIRECT x_18717 -> h_INDIRECT x_18717
     117| EXT_INDIRECT x_18718 -> h_EXT_INDIRECT x_18718
     118| REGISTER x_18719 -> h_REGISTER x_18719
    115119| ACC_A -> h_ACC_A
    116120| ACC_B -> h_ACC_B
    117121| DPTR -> h_DPTR
    118 | DATA x_63 -> h_DATA x_63
    119 | DATA16 x_64 -> h_DATA16 x_64
     122| DATA x_18720 -> h_DATA x_18720
     123| DATA16 x_18721 -> h_DATA16 x_18721
    120124| ACC_DPTR -> h_ACC_DPTR
    121125| ACC_PC -> h_ACC_PC
     
    123127| INDIRECT_DPTR -> h_INDIRECT_DPTR
    124128| CARRY -> h_CARRY
    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
     129| BIT_ADDR x_18722 -> h_BIT_ADDR x_18722
     130| N_BIT_ADDR x_18723 -> h_N_BIT_ADDR x_18723
     131| RELATIVE x_18724 -> h_RELATIVE x_18724
     132| ADDR11 x_18725 -> h_ADDR11 x_18725
     133| ADDR16 x_18726 -> h_ADDR16 x_18726
    130134
    131135(** val addressing_mode_rect_Type5 :
     
    137141    -> 'a1) -> addressing_mode -> 'a1 **)
    138142let 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
    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
     143| DIRECT x_18747 -> h_DIRECT x_18747
     144| INDIRECT x_18748 -> h_INDIRECT x_18748
     145| EXT_INDIRECT x_18749 -> h_EXT_INDIRECT x_18749
     146| REGISTER x_18750 -> h_REGISTER x_18750
    143147| ACC_A -> h_ACC_A
    144148| ACC_B -> h_ACC_B
    145149| DPTR -> h_DPTR
    146 | DATA x_94 -> h_DATA x_94
    147 | DATA16 x_95 -> h_DATA16 x_95
     150| DATA x_18751 -> h_DATA x_18751
     151| DATA16 x_18752 -> h_DATA16 x_18752
    148152| ACC_DPTR -> h_ACC_DPTR
    149153| ACC_PC -> h_ACC_PC
     
    151155| INDIRECT_DPTR -> h_INDIRECT_DPTR
    152156| CARRY -> h_CARRY
    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
     157| BIT_ADDR x_18753 -> h_BIT_ADDR x_18753
     158| N_BIT_ADDR x_18754 -> h_N_BIT_ADDR x_18754
     159| RELATIVE x_18755 -> h_RELATIVE x_18755
     160| ADDR11 x_18756 -> h_ADDR11 x_18756
     161| ADDR16 x_18757 -> h_ADDR16 x_18757
    158162
    159163(** val addressing_mode_rect_Type3 :
     
    165169    -> 'a1) -> addressing_mode -> 'a1 **)
    166170let 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
    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
     171| DIRECT x_18778 -> h_DIRECT x_18778
     172| INDIRECT x_18779 -> h_INDIRECT x_18779
     173| EXT_INDIRECT x_18780 -> h_EXT_INDIRECT x_18780
     174| REGISTER x_18781 -> h_REGISTER x_18781
    171175| ACC_A -> h_ACC_A
    172176| ACC_B -> h_ACC_B
    173177| DPTR -> h_DPTR
    174 | DATA x_125 -> h_DATA x_125
    175 | DATA16 x_126 -> h_DATA16 x_126
     178| DATA x_18782 -> h_DATA x_18782
     179| DATA16 x_18783 -> h_DATA16 x_18783
    176180| ACC_DPTR -> h_ACC_DPTR
    177181| ACC_PC -> h_ACC_PC
     
    179183| INDIRECT_DPTR -> h_INDIRECT_DPTR
    180184| CARRY -> h_CARRY
    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
     185| BIT_ADDR x_18784 -> h_BIT_ADDR x_18784
     186| N_BIT_ADDR x_18785 -> h_N_BIT_ADDR x_18785
     187| RELATIVE x_18786 -> h_RELATIVE x_18786
     188| ADDR11 x_18787 -> h_ADDR11 x_18787
     189| ADDR16 x_18788 -> h_ADDR16 x_18788
    186190
    187191(** val addressing_mode_rect_Type2 :
     
    193197    -> 'a1) -> addressing_mode -> 'a1 **)
    194198let 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
    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
     199| DIRECT x_18809 -> h_DIRECT x_18809
     200| INDIRECT x_18810 -> h_INDIRECT x_18810
     201| EXT_INDIRECT x_18811 -> h_EXT_INDIRECT x_18811
     202| REGISTER x_18812 -> h_REGISTER x_18812
    199203| ACC_A -> h_ACC_A
    200204| ACC_B -> h_ACC_B
    201205| DPTR -> h_DPTR
    202 | DATA x_156 -> h_DATA x_156
    203 | DATA16 x_157 -> h_DATA16 x_157
     206| DATA x_18813 -> h_DATA x_18813
     207| DATA16 x_18814 -> h_DATA16 x_18814
    204208| ACC_DPTR -> h_ACC_DPTR
    205209| ACC_PC -> h_ACC_PC
     
    207211| INDIRECT_DPTR -> h_INDIRECT_DPTR
    208212| CARRY -> h_CARRY
    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
     213| BIT_ADDR x_18815 -> h_BIT_ADDR x_18815
     214| N_BIT_ADDR x_18816 -> h_N_BIT_ADDR x_18816
     215| RELATIVE x_18817 -> h_RELATIVE x_18817
     216| ADDR11 x_18818 -> h_ADDR11 x_18818
     217| ADDR16 x_18819 -> h_ADDR16 x_18819
    214218
    215219(** val addressing_mode_rect_Type1 :
     
    221225    -> 'a1) -> addressing_mode -> 'a1 **)
    222226let 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
    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
     227| DIRECT x_18840 -> h_DIRECT x_18840
     228| INDIRECT x_18841 -> h_INDIRECT x_18841
     229| EXT_INDIRECT x_18842 -> h_EXT_INDIRECT x_18842
     230| REGISTER x_18843 -> h_REGISTER x_18843
    227231| ACC_A -> h_ACC_A
    228232| ACC_B -> h_ACC_B
    229233| DPTR -> h_DPTR
    230 | DATA x_187 -> h_DATA x_187
    231 | DATA16 x_188 -> h_DATA16 x_188
     234| DATA x_18844 -> h_DATA x_18844
     235| DATA16 x_18845 -> h_DATA16 x_18845
    232236| ACC_DPTR -> h_ACC_DPTR
    233237| ACC_PC -> h_ACC_PC
     
    235239| INDIRECT_DPTR -> h_INDIRECT_DPTR
    236240| CARRY -> h_CARRY
    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
     241| BIT_ADDR x_18846 -> h_BIT_ADDR x_18846
     242| N_BIT_ADDR x_18847 -> h_N_BIT_ADDR x_18847
     243| RELATIVE x_18848 -> h_RELATIVE x_18848
     244| ADDR11 x_18849 -> h_ADDR11 x_18849
     245| ADDR16 x_18850 -> h_ADDR16 x_18850
    242246
    243247(** val addressing_mode_rect_Type0 :
     
    249253    -> 'a1) -> addressing_mode -> 'a1 **)
    250254let 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
    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
     255| DIRECT x_18871 -> h_DIRECT x_18871
     256| INDIRECT x_18872 -> h_INDIRECT x_18872
     257| EXT_INDIRECT x_18873 -> h_EXT_INDIRECT x_18873
     258| REGISTER x_18874 -> h_REGISTER x_18874
    255259| ACC_A -> h_ACC_A
    256260| ACC_B -> h_ACC_B
    257261| DPTR -> h_DPTR
    258 | DATA x_218 -> h_DATA x_218
    259 | DATA16 x_219 -> h_DATA16 x_219
     262| DATA x_18875 -> h_DATA x_18875
     263| DATA16 x_18876 -> h_DATA16 x_18876
    260264| ACC_DPTR -> h_ACC_DPTR
    261265| ACC_PC -> h_ACC_PC
     
    263267| INDIRECT_DPTR -> h_INDIRECT_DPTR
    264268| CARRY -> h_CARRY
    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
     269| BIT_ADDR x_18877 -> h_BIT_ADDR x_18877
     270| N_BIT_ADDR x_18878 -> h_N_BIT_ADDR x_18878
     271| RELATIVE x_18879 -> h_RELATIVE x_18879
     272| ADDR11 x_18880 -> h_ADDR11 x_18880
     273| ADDR16 x_18881 -> h_ADDR16 x_18881
    270274
    271275(** val addressing_mode_inv_rect_Type4 :
     
    19241928    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19251929    'a1) -> subaddressing_mode -> 'a1 **)
    1926 let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_692 =
    1927   let subaddressing_modeel = x_692 in
     1930let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_19349 =
     1931  let subaddressing_modeel = x_19349 in
    19281932  h_mk_subaddressing_mode subaddressing_modeel __
    19291933
     
    19311935    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19321936    'a1) -> subaddressing_mode -> 'a1 **)
    1933 let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_694 =
    1934   let subaddressing_modeel = x_694 in
     1937let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_19351 =
     1938  let subaddressing_modeel = x_19351 in
    19351939  h_mk_subaddressing_mode subaddressing_modeel __
    19361940
     
    19381942    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19391943    'a1) -> subaddressing_mode -> 'a1 **)
    1940 let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_696 =
    1941   let subaddressing_modeel = x_696 in
     1944let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_19353 =
     1945  let subaddressing_modeel = x_19353 in
    19421946  h_mk_subaddressing_mode subaddressing_modeel __
    19431947
     
    19451949    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19461950    'a1) -> subaddressing_mode -> 'a1 **)
    1947 let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_698 =
    1948   let subaddressing_modeel = x_698 in
     1951let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_19355 =
     1952  let subaddressing_modeel = x_19355 in
    19491953  h_mk_subaddressing_mode subaddressing_modeel __
    19501954
     
    19521956    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19531957    'a1) -> subaddressing_mode -> 'a1 **)
    1954 let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_700 =
    1955   let subaddressing_modeel = x_700 in
     1958let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_19357 =
     1959  let subaddressing_modeel = x_19357 in
    19561960  h_mk_subaddressing_mode subaddressing_modeel __
    19571961
     
    19591963    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19601964    'a1) -> subaddressing_mode -> 'a1 **)
    1961 let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_702 =
    1962   let subaddressing_modeel = x_702 in
     1965let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_19359 =
     1966  let subaddressing_modeel = x_19359 in
    19631967  h_mk_subaddressing_mode subaddressing_modeel __
    19641968
     
    20942098| RETI
    20952099| NOP
     2100| JMP of subaddressing_mode
    20962101
    20972102(** val preinstruction_rect_Type4 :
     
    21292134    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
    21302135    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 ->
    2131     'a2 -> 'a2 -> 'a1 preinstruction -> 'a2 **)
    2132 let 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
    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
     2136    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
     2137let 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 h_JMP = function
     2138| ADD (x_19461, x_19460) -> h_ADD x_19461 x_19460
     2139| ADDC (x_19463, x_19462) -> h_ADDC x_19463 x_19462
     2140| SUBB (x_19465, x_19464) -> h_SUBB x_19465 x_19464
     2141| INC x_19466 -> h_INC x_19466
     2142| DEC x_19467 -> h_DEC x_19467
     2143| MUL (x_19469, x_19468) -> h_MUL x_19469 x_19468
     2144| DIV (x_19471, x_19470) -> h_DIV x_19471 x_19470
     2145| DA x_19472 -> h_DA x_19472
     2146| JC x_19473 -> h_JC x_19473
     2147| JNC x_19474 -> h_JNC x_19474
     2148| JB (x_19476, x_19475) -> h_JB x_19476 x_19475
     2149| JNB (x_19478, x_19477) -> h_JNB x_19478 x_19477
     2150| JBC (x_19480, x_19479) -> h_JBC x_19480 x_19479
     2151| JZ x_19481 -> h_JZ x_19481
     2152| JNZ x_19482 -> h_JNZ x_19482
     2153| CJNE (x_19484, x_19483) -> h_CJNE x_19484 x_19483
     2154| DJNZ (x_19486, x_19485) -> h_DJNZ x_19486 x_19485
     2155| ANL x_19487 -> h_ANL x_19487
     2156| ORL x_19488 -> h_ORL x_19488
     2157| XRL x_19489 -> h_XRL x_19489
     2158| CLR x_19490 -> h_CLR x_19490
     2159| CPL x_19491 -> h_CPL x_19491
     2160| RL x_19492 -> h_RL x_19492
     2161| RLC x_19493 -> h_RLC x_19493
     2162| RR x_19494 -> h_RR x_19494
     2163| RRC x_19495 -> h_RRC x_19495
     2164| SWAP x_19496 -> h_SWAP x_19496
     2165| MOV x_19497 -> h_MOV x_19497
     2166| MOVX x_19498 -> h_MOVX x_19498
     2167| SETB x_19499 -> h_SETB x_19499
     2168| PUSH x_19500 -> h_PUSH x_19500
     2169| POP x_19501 -> h_POP x_19501
     2170| XCH (x_19503, x_19502) -> h_XCH x_19503 x_19502
     2171| XCHD (x_19505, x_19504) -> h_XCHD x_19505 x_19504
    21672172| RET -> h_RET
    21682173| RETI -> h_RETI
    21692174| NOP -> h_NOP
     2175| JMP x_19506 -> h_JMP x_19506
    21702176
    21712177(** val preinstruction_rect_Type5 :
     
    22032209    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
    22042210    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 ->
    2205     'a2 -> 'a2 -> 'a1 preinstruction -> 'a2 **)
    2206 let 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
    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
     2211    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
     2212let 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 h_JMP = function
     2213| ADD (x_19547, x_19546) -> h_ADD x_19547 x_19546
     2214| ADDC (x_19549, x_19548) -> h_ADDC x_19549 x_19548
     2215| SUBB (x_19551, x_19550) -> h_SUBB x_19551 x_19550
     2216| INC x_19552 -> h_INC x_19552
     2217| DEC x_19553 -> h_DEC x_19553
     2218| MUL (x_19555, x_19554) -> h_MUL x_19555 x_19554
     2219| DIV (x_19557, x_19556) -> h_DIV x_19557 x_19556
     2220| DA x_19558 -> h_DA x_19558
     2221| JC x_19559 -> h_JC x_19559
     2222| JNC x_19560 -> h_JNC x_19560
     2223| JB (x_19562, x_19561) -> h_JB x_19562 x_19561
     2224| JNB (x_19564, x_19563) -> h_JNB x_19564 x_19563
     2225| JBC (x_19566, x_19565) -> h_JBC x_19566 x_19565
     2226| JZ x_19567 -> h_JZ x_19567
     2227| JNZ x_19568 -> h_JNZ x_19568
     2228| CJNE (x_19570, x_19569) -> h_CJNE x_19570 x_19569
     2229| DJNZ (x_19572, x_19571) -> h_DJNZ x_19572 x_19571
     2230| ANL x_19573 -> h_ANL x_19573
     2231| ORL x_19574 -> h_ORL x_19574
     2232| XRL x_19575 -> h_XRL x_19575
     2233| CLR x_19576 -> h_CLR x_19576
     2234| CPL x_19577 -> h_CPL x_19577
     2235| RL x_19578 -> h_RL x_19578
     2236| RLC x_19579 -> h_RLC x_19579
     2237| RR x_19580 -> h_RR x_19580
     2238| RRC x_19581 -> h_RRC x_19581
     2239| SWAP x_19582 -> h_SWAP x_19582
     2240| MOV x_19583 -> h_MOV x_19583
     2241| MOVX x_19584 -> h_MOVX x_19584
     2242| SETB x_19585 -> h_SETB x_19585
     2243| PUSH x_19586 -> h_PUSH x_19586
     2244| POP x_19587 -> h_POP x_19587
     2245| XCH (x_19589, x_19588) -> h_XCH x_19589 x_19588
     2246| XCHD (x_19591, x_19590) -> h_XCHD x_19591 x_19590
    22412247| RET -> h_RET
    22422248| RETI -> h_RETI
    22432249| NOP -> h_NOP
     2250| JMP x_19592 -> h_JMP x_19592
    22442251
    22452252(** val preinstruction_rect_Type3 :
     
    22772284    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
    22782285    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 ->
    2279     'a2 -> 'a2 -> 'a1 preinstruction -> 'a2 **)
    2280 let 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
    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
     2286    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
     2287let 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 h_JMP = function
     2288| ADD (x_19633, x_19632) -> h_ADD x_19633 x_19632
     2289| ADDC (x_19635, x_19634) -> h_ADDC x_19635 x_19634
     2290| SUBB (x_19637, x_19636) -> h_SUBB x_19637 x_19636
     2291| INC x_19638 -> h_INC x_19638
     2292| DEC x_19639 -> h_DEC x_19639
     2293| MUL (x_19641, x_19640) -> h_MUL x_19641 x_19640
     2294| DIV (x_19643, x_19642) -> h_DIV x_19643 x_19642
     2295| DA x_19644 -> h_DA x_19644
     2296| JC x_19645 -> h_JC x_19645
     2297| JNC x_19646 -> h_JNC x_19646
     2298| JB (x_19648, x_19647) -> h_JB x_19648 x_19647
     2299| JNB (x_19650, x_19649) -> h_JNB x_19650 x_19649
     2300| JBC (x_19652, x_19651) -> h_JBC x_19652 x_19651
     2301| JZ x_19653 -> h_JZ x_19653
     2302| JNZ x_19654 -> h_JNZ x_19654
     2303| CJNE (x_19656, x_19655) -> h_CJNE x_19656 x_19655
     2304| DJNZ (x_19658, x_19657) -> h_DJNZ x_19658 x_19657
     2305| ANL x_19659 -> h_ANL x_19659
     2306| ORL x_19660 -> h_ORL x_19660
     2307| XRL x_19661 -> h_XRL x_19661
     2308| CLR x_19662 -> h_CLR x_19662
     2309| CPL x_19663 -> h_CPL x_19663
     2310| RL x_19664 -> h_RL x_19664
     2311| RLC x_19665 -> h_RLC x_19665
     2312| RR x_19666 -> h_RR x_19666
     2313| RRC x_19667 -> h_RRC x_19667
     2314| SWAP x_19668 -> h_SWAP x_19668
     2315| MOV x_19669 -> h_MOV x_19669
     2316| MOVX x_19670 -> h_MOVX x_19670
     2317| SETB x_19671 -> h_SETB x_19671
     2318| PUSH x_19672 -> h_PUSH x_19672
     2319| POP x_19673 -> h_POP x_19673
     2320| XCH (x_19675, x_19674) -> h_XCH x_19675 x_19674
     2321| XCHD (x_19677, x_19676) -> h_XCHD x_19677 x_19676
    23152322| RET -> h_RET
    23162323| RETI -> h_RETI
    23172324| NOP -> h_NOP
     2325| JMP x_19678 -> h_JMP x_19678
    23182326
    23192327(** val preinstruction_rect_Type2 :
     
    23512359    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
    23522360    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 ->
    2353     'a2 -> 'a2 -> 'a1 preinstruction -> 'a2 **)
    2354 let 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
    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
     2361    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
     2362let 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 h_JMP = function
     2363| ADD (x_19719, x_19718) -> h_ADD x_19719 x_19718
     2364| ADDC (x_19721, x_19720) -> h_ADDC x_19721 x_19720
     2365| SUBB (x_19723, x_19722) -> h_SUBB x_19723 x_19722
     2366| INC x_19724 -> h_INC x_19724
     2367| DEC x_19725 -> h_DEC x_19725
     2368| MUL (x_19727, x_19726) -> h_MUL x_19727 x_19726
     2369| DIV (x_19729, x_19728) -> h_DIV x_19729 x_19728
     2370| DA x_19730 -> h_DA x_19730
     2371| JC x_19731 -> h_JC x_19731
     2372| JNC x_19732 -> h_JNC x_19732
     2373| JB (x_19734, x_19733) -> h_JB x_19734 x_19733
     2374| JNB (x_19736, x_19735) -> h_JNB x_19736 x_19735
     2375| JBC (x_19738, x_19737) -> h_JBC x_19738 x_19737
     2376| JZ x_19739 -> h_JZ x_19739
     2377| JNZ x_19740 -> h_JNZ x_19740
     2378| CJNE (x_19742, x_19741) -> h_CJNE x_19742 x_19741
     2379| DJNZ (x_19744, x_19743) -> h_DJNZ x_19744 x_19743
     2380| ANL x_19745 -> h_ANL x_19745
     2381| ORL x_19746 -> h_ORL x_19746
     2382| XRL x_19747 -> h_XRL x_19747
     2383| CLR x_19748 -> h_CLR x_19748
     2384| CPL x_19749 -> h_CPL x_19749
     2385| RL x_19750 -> h_RL x_19750
     2386| RLC x_19751 -> h_RLC x_19751
     2387| RR x_19752 -> h_RR x_19752
     2388| RRC x_19753 -> h_RRC x_19753
     2389| SWAP x_19754 -> h_SWAP x_19754
     2390| MOV x_19755 -> h_MOV x_19755
     2391| MOVX x_19756 -> h_MOVX x_19756
     2392| SETB x_19757 -> h_SETB x_19757
     2393| PUSH x_19758 -> h_PUSH x_19758
     2394| POP x_19759 -> h_POP x_19759
     2395| XCH (x_19761, x_19760) -> h_XCH x_19761 x_19760
     2396| XCHD (x_19763, x_19762) -> h_XCHD x_19763 x_19762
    23892397| RET -> h_RET
    23902398| RETI -> h_RETI
    23912399| NOP -> h_NOP
     2400| JMP x_19764 -> h_JMP x_19764
    23922401
    23932402(** val preinstruction_rect_Type1 :
     
    24252434    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
    24262435    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 ->
    2427     'a2 -> 'a2 -> 'a1 preinstruction -> 'a2 **)
    2428 let 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
    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
     2436    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
     2437let 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 h_JMP = function
     2438| ADD (x_19805, x_19804) -> h_ADD x_19805 x_19804
     2439| ADDC (x_19807, x_19806) -> h_ADDC x_19807 x_19806
     2440| SUBB (x_19809, x_19808) -> h_SUBB x_19809 x_19808
     2441| INC x_19810 -> h_INC x_19810
     2442| DEC x_19811 -> h_DEC x_19811
     2443| MUL (x_19813, x_19812) -> h_MUL x_19813 x_19812
     2444| DIV (x_19815, x_19814) -> h_DIV x_19815 x_19814
     2445| DA x_19816 -> h_DA x_19816
     2446| JC x_19817 -> h_JC x_19817
     2447| JNC x_19818 -> h_JNC x_19818
     2448| JB (x_19820, x_19819) -> h_JB x_19820 x_19819
     2449| JNB (x_19822, x_19821) -> h_JNB x_19822 x_19821
     2450| JBC (x_19824, x_19823) -> h_JBC x_19824 x_19823
     2451| JZ x_19825 -> h_JZ x_19825
     2452| JNZ x_19826 -> h_JNZ x_19826
     2453| CJNE (x_19828, x_19827) -> h_CJNE x_19828 x_19827
     2454| DJNZ (x_19830, x_19829) -> h_DJNZ x_19830 x_19829
     2455| ANL x_19831 -> h_ANL x_19831
     2456| ORL x_19832 -> h_ORL x_19832
     2457| XRL x_19833 -> h_XRL x_19833
     2458| CLR x_19834 -> h_CLR x_19834
     2459| CPL x_19835 -> h_CPL x_19835
     2460| RL x_19836 -> h_RL x_19836
     2461| RLC x_19837 -> h_RLC x_19837
     2462| RR x_19838 -> h_RR x_19838
     2463| RRC x_19839 -> h_RRC x_19839
     2464| SWAP x_19840 -> h_SWAP x_19840
     2465| MOV x_19841 -> h_MOV x_19841
     2466| MOVX x_19842 -> h_MOVX x_19842
     2467| SETB x_19843 -> h_SETB x_19843
     2468| PUSH x_19844 -> h_PUSH x_19844
     2469| POP x_19845 -> h_POP x_19845
     2470| XCH (x_19847, x_19846) -> h_XCH x_19847 x_19846
     2471| XCHD (x_19849, x_19848) -> h_XCHD x_19849 x_19848
    24632472| RET -> h_RET
    24642473| RETI -> h_RETI
    24652474| NOP -> h_NOP
     2475| JMP x_19850 -> h_JMP x_19850
    24662476
    24672477(** val preinstruction_rect_Type0 :
     
    24992509    (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode
    25002510    -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 ->
    2501     'a2 -> 'a2 -> 'a1 preinstruction -> 'a2 **)
    2502 let 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
    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
     2511    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
     2512let 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 h_JMP = function
     2513| ADD (x_19891, x_19890) -> h_ADD x_19891 x_19890
     2514| ADDC (x_19893, x_19892) -> h_ADDC x_19893 x_19892
     2515| SUBB (x_19895, x_19894) -> h_SUBB x_19895 x_19894
     2516| INC x_19896 -> h_INC x_19896
     2517| DEC x_19897 -> h_DEC x_19897
     2518| MUL (x_19899, x_19898) -> h_MUL x_19899 x_19898
     2519| DIV (x_19901, x_19900) -> h_DIV x_19901 x_19900
     2520| DA x_19902 -> h_DA x_19902
     2521| JC x_19903 -> h_JC x_19903
     2522| JNC x_19904 -> h_JNC x_19904
     2523| JB (x_19906, x_19905) -> h_JB x_19906 x_19905
     2524| JNB (x_19908, x_19907) -> h_JNB x_19908 x_19907
     2525| JBC (x_19910, x_19909) -> h_JBC x_19910 x_19909
     2526| JZ x_19911 -> h_JZ x_19911
     2527| JNZ x_19912 -> h_JNZ x_19912
     2528| CJNE (x_19914, x_19913) -> h_CJNE x_19914 x_19913
     2529| DJNZ (x_19916, x_19915) -> h_DJNZ x_19916 x_19915
     2530| ANL x_19917 -> h_ANL x_19917
     2531| ORL x_19918 -> h_ORL x_19918
     2532| XRL x_19919 -> h_XRL x_19919
     2533| CLR x_19920 -> h_CLR x_19920
     2534| CPL x_19921 -> h_CPL x_19921
     2535| RL x_19922 -> h_RL x_19922
     2536| RLC x_19923 -> h_RLC x_19923
     2537| RR x_19924 -> h_RR x_19924
     2538| RRC x_19925 -> h_RRC x_19925
     2539| SWAP x_19926 -> h_SWAP x_19926
     2540| MOV x_19927 -> h_MOV x_19927
     2541| MOVX x_19928 -> h_MOVX x_19928
     2542| SETB x_19929 -> h_SETB x_19929
     2543| PUSH x_19930 -> h_PUSH x_19930
     2544| POP x_19931 -> h_POP x_19931
     2545| XCH (x_19933, x_19932) -> h_XCH x_19933 x_19932
     2546| XCHD (x_19935, x_19934) -> h_XCHD x_19935 x_19934
    25372547| RET -> h_RET
    25382548| RETI -> h_RETI
    25392549| NOP -> h_NOP
     2550| JMP x_19936 -> h_JMP x_19936
    25402551
    25412552(** val preinstruction_inv_rect_Type4 :
     
    25752586    -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
    25762587    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) ->
    2577     (__ -> 'a2) -> (__ -> 'a2) -> 'a2 **)
    2578 let preinstruction_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 =
     2588    (__ -> 'a2) -> (__ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2 **)
     2589let preinstruction_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 h38 =
    25792590  let hcut =
    25802591    preinstruction_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
    25812592      h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32
    2582       h33 h34 h35 h36 h37 hterm
     2593      h33 h34 h35 h36 h37 h38 hterm
    25832594  in
    25842595  hcut __
     
    26202631    -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
    26212632    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) ->
    2622     (__ -> 'a2) -> (__ -> 'a2) -> 'a2 **)
    2623 let preinstruction_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 =
     2633    (__ -> 'a2) -> (__ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2 **)
     2634let preinstruction_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 h38 =
    26242635  let hcut =
    26252636    preinstruction_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
    26262637      h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32
    2627       h33 h34 h35 h36 h37 hterm
     2638      h33 h34 h35 h36 h37 h38 hterm
    26282639  in
    26292640  hcut __
     
    26652676    -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
    26662677    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) ->
    2667     (__ -> 'a2) -> (__ -> 'a2) -> 'a2 **)
    2668 let preinstruction_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 =
     2678    (__ -> 'a2) -> (__ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2 **)
     2679let preinstruction_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 h38 =
    26692680  let hcut =
    26702681    preinstruction_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
    26712682      h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32
    2672       h33 h34 h35 h36 h37 hterm
     2683      h33 h34 h35 h36 h37 h38 hterm
    26732684  in
    26742685  hcut __
     
    27102721    -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
    27112722    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) ->
    2712     (__ -> 'a2) -> (__ -> 'a2) -> 'a2 **)
    2713 let preinstruction_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 =
     2723    (__ -> 'a2) -> (__ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2 **)
     2724let preinstruction_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 h38 =
    27142725  let hcut =
    27152726    preinstruction_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
    27162727      h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32
    2717       h33 h34 h35 h36 h37 hterm
     2728      h33 h34 h35 h36 h37 h38 hterm
    27182729  in
    27192730  hcut __
     
    27552766    -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
    27562767    (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) ->
    2757     (__ -> 'a2) -> (__ -> 'a2) -> 'a2 **)
    2758 let preinstruction_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 =
     2768    (__ -> 'a2) -> (__ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2 **)
     2769let preinstruction_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 h38 =
    27592770  let hcut =
    27602771    preinstruction_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14
    27612772      h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32
    2762       h33 h34 h35 h36 h37 hterm
     2773      h33 h34 h35 h36 h37 h38 hterm
    27632774  in
    27642775  hcut __
     
    28052816     | RET -> Obj.magic (fun _ dH -> dH)
    28062817     | RETI -> Obj.magic (fun _ dH -> dH)
    2807      | NOP -> Obj.magic (fun _ dH -> dH)) y
     2818     | NOP -> Obj.magic (fun _ dH -> dH)
     2819     | JMP a0 -> Obj.magic (fun _ dH -> dH __)) y
    28082820
    28092821(** val preinstruction_jmdiscr :
     
    28482860     | RET -> Obj.magic (fun _ dH -> dH)
    28492861     | RETI -> Obj.magic (fun _ dH -> dH)
    2850      | NOP -> Obj.magic (fun _ dH -> dH)) y
     2862     | NOP -> Obj.magic (fun _ dH -> dH)
     2863     | JMP a0 -> Obj.magic (fun _ dH -> dH __)) y
    28512864
    28522865(** val eq_preinstruction :
     
    29082921     | RET -> Bool.False
    29092922     | RETI -> Bool.False
    2910      | NOP -> Bool.False)
     2923     | NOP -> Bool.False
     2924     | JMP x -> Bool.False)
    29112925  | ADDC (arg1, arg2) ->
    29122926    (match j with
     
    29622976     | RET -> Bool.False
    29632977     | RETI -> Bool.False
    2964      | NOP -> Bool.False)
     2978     | NOP -> Bool.False
     2979     | JMP x -> Bool.False)
    29652980  | SUBB (arg1, arg2) ->
    29662981    (match j with
     
    30163031     | RET -> Bool.False
    30173032     | RETI -> Bool.False
    3018      | NOP -> Bool.False)
     3033     | NOP -> Bool.False
     3034     | JMP x -> Bool.False)
    30193035  | INC arg ->
    30203036    (match j with
     
    30683084     | RET -> Bool.False
    30693085     | RETI -> Bool.False
    3070      | NOP -> Bool.False)
     3086     | NOP -> Bool.False
     3087     | JMP x -> Bool.False)
    30713088  | DEC arg ->
    30723089    (match j with
     
    31163133     | RET -> Bool.False
    31173134     | RETI -> Bool.False
    3118      | NOP -> Bool.False)
     3135     | NOP -> Bool.False
     3136     | JMP x -> Bool.False)
    31193137  | MUL (arg1, arg2) ->
    31203138    (match j with
     
    31663184     | RET -> Bool.False
    31673185     | RETI -> Bool.False
    3168      | NOP -> Bool.False)
     3186     | NOP -> Bool.False
     3187     | JMP x -> Bool.False)
    31693188  | DIV (arg1, arg2) ->
    31703189    (match j with
     
    32163235     | RET -> Bool.False
    32173236     | RETI -> Bool.False
    3218      | NOP -> Bool.False)
     3237     | NOP -> Bool.False
     3238     | JMP x -> Bool.False)
    32193239  | DA arg ->
    32203240    (match j with
     
    32603280     | RET -> Bool.False
    32613281     | RETI -> Bool.False
    3262      | NOP -> Bool.False)
     3282     | NOP -> Bool.False
     3283     | JMP x -> Bool.False)
    32633284  | JC arg ->
    32643285    (match j with
     
    33043325     | RET -> Bool.False
    33053326     | RETI -> Bool.False
    3306      | NOP -> Bool.False)
     3327     | NOP -> Bool.False
     3328     | JMP x -> Bool.False)
    33073329  | JNC arg ->
    33083330    (match j with
     
    33483370     | RET -> Bool.False
    33493371     | RETI -> Bool.False
    3350      | NOP -> Bool.False)
     3372     | NOP -> Bool.False
     3373     | JMP x -> Bool.False)
    33513374  | JB (arg1, arg2) ->
    33523375    (match j with
     
    33983421     | RET -> Bool.False
    33993422     | RETI -> Bool.False
    3400      | NOP -> Bool.False)
     3423     | NOP -> Bool.False
     3424     | JMP x -> Bool.False)
    34013425  | JNB (arg1, arg2) ->
    34023426    (match j with
     
    34483472     | RET -> Bool.False
    34493473     | RETI -> Bool.False
    3450      | NOP -> Bool.False)
     3474     | NOP -> Bool.False
     3475     | JMP x -> Bool.False)
    34513476  | JBC (arg1, arg2) ->
    34523477    (match j with
     
    34983523     | RET -> Bool.False
    34993524     | RETI -> Bool.False
    3500      | NOP -> Bool.False)
     3525     | NOP -> Bool.False
     3526     | JMP x -> Bool.False)
    35013527  | JZ arg ->
    35023528    (match j with
     
    35423568     | RET -> Bool.False
    35433569     | RETI -> Bool.False
    3544      | NOP -> Bool.False)
     3570     | NOP -> Bool.False
     3571     | JMP x -> Bool.False)
    35453572  | JNZ arg ->
    35463573    (match j with
     
    35863613     | RET -> Bool.False
    35873614     | RETI -> Bool.False
    3588      | NOP -> Bool.False)
     3615     | NOP -> Bool.False
     3616     | JMP x -> Bool.False)
    35893617  | CJNE (arg1, arg2) ->
    35903618    (match j with
     
    36623690     | RET -> Bool.False
    36633691     | RETI -> Bool.False
    3664      | NOP -> Bool.False)
     3692     | NOP -> Bool.False
     3693     | JMP x -> Bool.False)
    36653694  | DJNZ (arg1, arg2) ->
    36663695    (match j with
     
    37123741     | RET -> Bool.False
    37133742     | RETI -> Bool.False
    3714      | NOP -> Bool.False)
     3743     | NOP -> Bool.False
     3744     | JMP x -> Bool.False)
    37153745  | ANL arg ->
    37163746    (match j with
     
    38023832     | RET -> Bool.False
    38033833     | RETI -> Bool.False
    3804      | NOP -> Bool.False)
     3834     | NOP -> Bool.False
     3835     | JMP x -> Bool.False)
    38053836  | ORL arg ->
    38063837    (match j with
     
    38923923     | RET -> Bool.False
    38933924     | RETI -> Bool.False
    3894      | NOP -> Bool.False)
     3925     | NOP -> Bool.False
     3926     | JMP x -> Bool.False)
    38953927  | XRL arg ->
    38963928    (match j with
     
    39663998     | RET -> Bool.False
    39673999     | RETI -> Bool.False
    3968      | NOP -> Bool.False)
     4000     | NOP -> Bool.False
     4001     | JMP x -> Bool.False)
    39694002  | CLR arg ->
    39704003    (match j with
     
    40124045     | RET -> Bool.False
    40134046     | RETI -> Bool.False
    4014      | NOP -> Bool.False)
     4047     | NOP -> Bool.False
     4048     | JMP x -> Bool.False)
    40154049  | CPL arg ->
    40164050    (match j with
     
    40584092     | RET -> Bool.False
    40594093     | RETI -> Bool.False
    4060      | NOP -> Bool.False)
     4094     | NOP -> Bool.False
     4095     | JMP x -> Bool.False)
    40614096  | RL arg ->
    40624097    (match j with
     
    41024137     | RET -> Bool.False
    41034138     | RETI -> Bool.False
    4104      | NOP -> Bool.False)
     4139     | NOP -> Bool.False
     4140     | JMP x -> Bool.False)
    41054141  | RLC arg ->
    41064142    (match j with
     
    41464182     | RET -> Bool.False
    41474183     | RETI -> Bool.False
    4148      | NOP -> Bool.False)
     4184     | NOP -> Bool.False
     4185     | JMP x -> Bool.False)
    41494186  | RR arg ->
    41504187    (match j with
     
    41904227     | RET -> Bool.False
    41914228     | RETI -> Bool.False
    4192      | NOP -> Bool.False)
     4229     | NOP -> Bool.False
     4230     | JMP x -> Bool.False)
    41934231  | RRC arg ->
    41944232    (match j with
     
    42344272     | RET -> Bool.False
    42354273     | RETI -> Bool.False
    4236      | NOP -> Bool.False)
     4274     | NOP -> Bool.False
     4275     | JMP x -> Bool.False)
    42374276  | SWAP arg ->
    42384277    (match j with
     
    42784317     | RET -> Bool.False
    42794318     | RETI -> Bool.False
    4280      | NOP -> Bool.False)
     4319     | NOP -> Bool.False
     4320     | JMP x -> Bool.False)
    42814321  | MOV arg ->
    42824322    (match j with
     
    44184458     | RET -> Bool.False
    44194459     | RETI -> Bool.False
    4420      | NOP -> Bool.False)
     4460     | NOP -> Bool.False
     4461     | JMP x -> Bool.False)
    44214462  | MOVX arg ->
    44224463    (match j with
     
    44884529     | RET -> Bool.False
    44894530     | RETI -> Bool.False
    4490      | NOP -> Bool.False)
     4531     | NOP -> Bool.False
     4532     | JMP x -> Bool.False)
    44914533  | SETB arg ->
    44924534    (match j with
     
    45324574     | RET -> Bool.False
    45334575     | RETI -> Bool.False
    4534      | NOP -> Bool.False)
     4576     | NOP -> Bool.False
     4577     | JMP x -> Bool.False)
    45354578  | PUSH arg ->
    45364579    (match j with
     
    45764619     | RET -> Bool.False
    45774620     | RETI -> Bool.False
    4578      | NOP -> Bool.False)
     4621     | NOP -> Bool.False
     4622     | JMP x -> Bool.False)
    45794623  | POP arg ->
    45804624    (match j with
     
    46204664     | RET -> Bool.False
    46214665     | RETI -> Bool.False
    4622      | NOP -> Bool.False)
     4666     | NOP -> Bool.False
     4667     | JMP x -> Bool.False)
    46234668  | XCH (arg1, arg2) ->
    46244669    (match j with
     
    46724717     | RET -> Bool.False
    46734718     | RETI -> Bool.False
    4674      | NOP -> Bool.False)
     4719     | NOP -> Bool.False
     4720     | JMP x -> Bool.False)
    46754721  | XCHD (arg1, arg2) ->
    46764722    (match j with
     
    47224768     | RET -> Bool.False
    47234769     | RETI -> Bool.False
    4724      | NOP -> Bool.False)
     4770     | NOP -> Bool.False
     4771     | JMP x -> Bool.False)
    47254772  | RET ->
    47264773    (match j with
     
    47614808     | RET -> Bool.True
    47624809     | RETI -> Bool.False
    4763      | NOP -> Bool.False)
     4810     | NOP -> Bool.False
     4811     | JMP x -> Bool.False)
    47644812  | RETI ->
    47654813    (match j with
     
    48004848     | RET -> Bool.False
    48014849     | RETI -> Bool.True
    4802      | NOP -> Bool.False)
     4850     | NOP -> Bool.False
     4851     | JMP x -> Bool.False)
    48034852  | NOP ->
    48044853    (match j with
     
    48394888     | RET -> Bool.False
    48404889     | RETI -> Bool.False
    4841      | NOP -> Bool.True)
     4890     | NOP -> Bool.True
     4891     | JMP x -> Bool.False)
     4892  | JMP arg ->
     4893    (match j with
     4894     | ADD (x, x0) -> Bool.False
     4895     | ADDC (x, x0) -> Bool.False
     4896     | SUBB (x, x0) -> Bool.False
     4897     | INC x -> Bool.False
     4898     | DEC x -> Bool.False
     4899     | MUL (x, x0) -> Bool.False
     4900     | DIV (x, x0) -> Bool.False
     4901     | DA x -> Bool.False
     4902     | JC x -> Bool.False
     4903     | JNC x -> Bool.False
     4904     | JB (x, x0) -> Bool.False
     4905     | JNB (x, x0) -> Bool.False
     4906     | JBC (x, x0) -> Bool.False
     4907     | JZ x -> Bool.False
     4908     | JNZ x -> Bool.False
     4909     | CJNE (x, x0) -> Bool.False
     4910     | DJNZ (x, x0) -> Bool.False
     4911     | ANL x -> Bool.False
     4912     | ORL x -> Bool.False
     4913     | XRL x -> Bool.False
     4914     | CLR x -> Bool.False
     4915     | CPL x -> Bool.False
     4916     | RL x -> Bool.False
     4917     | RLC x -> Bool.False
     4918     | RR x -> Bool.False
     4919     | RRC x -> Bool.False
     4920     | SWAP x -> Bool.False
     4921     | MOV x -> Bool.False
     4922     | MOVX x -> Bool.False
     4923     | SETB x -> Bool.False
     4924     | PUSH x -> Bool.False
     4925     | POP x -> Bool.False
     4926     | XCH (x, x0) -> Bool.False
     4927     | XCHD (x, x0) -> Bool.False
     4928     | RET -> Bool.False
     4929     | RETI -> Bool.False
     4930     | NOP -> Bool.False
     4931     | JMP arg' ->
     4932       eq_addressing_mode
     4933         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Indirect_dptr,
     4934           Vector.VEmpty)) arg)
     4935         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Indirect_dptr,
     4936           Vector.VEmpty)) arg'))
    48424937
    48434938type instruction =
     
    48474942| LJMP of subaddressing_mode
    48484943| SJMP of subaddressing_mode
    4849 | JMP of subaddressing_mode
    48504944| MOVC of subaddressing_mode * subaddressing_mode
    48514945| RealInstruction of subaddressing_mode preinstruction
     
    48544948    (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    48554949    (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    4856     (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    4857     (subaddressing_mode -> subaddressing_mode -> 'a1) -> (subaddressing_mode
    4858     preinstruction -> 'a1) -> instruction -> 'a1 **)
    4859 let rec instruction_rect_Type4 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_JMP h_MOVC h_RealInstruction = function
    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
     4950    (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode
     4951    -> 'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction ->
     4952    'a1 **)
     4953let rec instruction_rect_Type4 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
     4954| ACALL x_20508 -> h_ACALL x_20508
     4955| LCALL x_20509 -> h_LCALL x_20509
     4956| AJMP x_20510 -> h_AJMP x_20510
     4957| LJMP x_20511 -> h_LJMP x_20511
     4958| SJMP x_20512 -> h_SJMP x_20512
     4959| MOVC (x_20514, x_20513) -> h_MOVC x_20514 x_20513
     4960| RealInstruction x_20515 -> h_RealInstruction x_20515
    48684961
    48694962(** val instruction_rect_Type5 :
    48704963    (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    48714964    (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    4872     (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    4873     (subaddressing_mode -> subaddressing_mode -> 'a1) -> (subaddressing_mode
    4874     preinstruction -> 'a1) -> instruction -> 'a1 **)
    4875 let rec instruction_rect_Type5 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_JMP h_MOVC h_RealInstruction = function
    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
     4965    (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode
     4966    -> 'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction ->
     4967    'a1 **)
     4968let rec instruction_rect_Type5 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
     4969| ACALL x_20524 -> h_ACALL x_20524
     4970| LCALL x_20525 -> h_LCALL x_20525
     4971| AJMP x_20526 -> h_AJMP x_20526
     4972| LJMP x_20527 -> h_LJMP x_20527
     4973| SJMP x_20528 -> h_SJMP x_20528
     4974| MOVC (x_20530, x_20529) -> h_MOVC x_20530 x_20529
     4975| RealInstruction x_20531 -> h_RealInstruction x_20531
    48844976
    48854977(** val instruction_rect_Type3 :
    48864978    (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    48874979    (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    4888     (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    4889     (subaddressing_mode -> subaddressing_mode -> 'a1) -> (subaddressing_mode
    4890     preinstruction -> 'a1) -> instruction -> 'a1 **)
    4891 let rec instruction_rect_Type3 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_JMP h_MOVC h_RealInstruction = function
    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
     4980    (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode
     4981    -> 'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction ->
     4982    'a1 **)
     4983let rec instruction_rect_Type3 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
     4984| ACALL x_20540 -> h_ACALL x_20540
     4985| LCALL x_20541 -> h_LCALL x_20541
     4986| AJMP x_20542 -> h_AJMP x_20542
     4987| LJMP x_20543 -> h_LJMP x_20543
     4988| SJMP x_20544 -> h_SJMP x_20544
     4989| MOVC (x_20546, x_20545) -> h_MOVC x_20546 x_20545
     4990| RealInstruction x_20547 -> h_RealInstruction x_20547
    49004991
    49014992(** val instruction_rect_Type2 :
    49024993    (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    49034994    (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    4904     (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    4905     (subaddressing_mode -> subaddressing_mode -> 'a1) -> (subaddressing_mode
    4906     preinstruction -> 'a1) -> instruction -> 'a1 **)
    4907 let rec instruction_rect_Type2 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_JMP h_MOVC h_RealInstruction = function
    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
     4995    (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode
     4996    -> 'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction ->
     4997    'a1 **)
     4998let rec instruction_rect_Type2 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
     4999| ACALL x_20556 -> h_ACALL x_20556
     5000| LCALL x_20557 -> h_LCALL x_20557
     5001| AJMP x_20558 -> h_AJMP x_20558
     5002| LJMP x_20559 -> h_LJMP x_20559
     5003| SJMP x_20560 -> h_SJMP x_20560
     5004| MOVC (x_20562, x_20561) -> h_MOVC x_20562 x_20561
     5005| RealInstruction x_20563 -> h_RealInstruction x_20563
    49165006
    49175007(** val instruction_rect_Type1 :
    49185008    (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    49195009    (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    4920     (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    4921     (subaddressing_mode -> subaddressing_mode -> 'a1) -> (subaddressing_mode
    4922     preinstruction -> 'a1) -> instruction -> 'a1 **)
    4923 let rec instruction_rect_Type1 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_JMP h_MOVC h_RealInstruction = function
    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
     5010    (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode
     5011    -> 'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction ->
     5012    'a1 **)
     5013let rec instruction_rect_Type1 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
     5014| ACALL x_20572 -> h_ACALL x_20572
     5015| LCALL x_20573 -> h_LCALL x_20573
     5016| AJMP x_20574 -> h_AJMP x_20574
     5017| LJMP x_20575 -> h_LJMP x_20575
     5018| SJMP x_20576 -> h_SJMP x_20576
     5019| MOVC (x_20578, x_20577) -> h_MOVC x_20578 x_20577
     5020| RealInstruction x_20579 -> h_RealInstruction x_20579
    49325021
    49335022(** val instruction_rect_Type0 :
    49345023    (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    49355024    (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    4936     (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    4937     (subaddressing_mode -> subaddressing_mode -> 'a1) -> (subaddressing_mode
    4938     preinstruction -> 'a1) -> instruction -> 'a1 **)
    4939 let rec instruction_rect_Type0 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_JMP h_MOVC h_RealInstruction = function
    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
     5025    (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode
     5026    -> 'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction ->
     5027    'a1 **)
     5028let rec instruction_rect_Type0 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
     5029| ACALL x_20588 -> h_ACALL x_20588
     5030| LCALL x_20589 -> h_LCALL x_20589
     5031| AJMP x_20590 -> h_AJMP x_20590
     5032| LJMP x_20591 -> h_LJMP x_20591
     5033| SJMP x_20592 -> h_SJMP x_20592
     5034| MOVC (x_20594, x_20593) -> h_MOVC x_20594 x_20593
     5035| RealInstruction x_20595 -> h_RealInstruction x_20595
    49485036
    49495037(** val instruction_inv_rect_Type4 :
     
    49515039    -> __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode
    49525040    -> __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode
    4953     -> __ -> 'a1) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a1)
    4954     -> (subaddressing_mode preinstruction -> __ -> 'a1) -> 'a1 **)
    4955 let instruction_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
    4956   let hcut = instruction_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
     5041    -> subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction
     5042    -> __ -> 'a1) -> 'a1 **)
     5043let instruction_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 =
     5044  let hcut = instruction_rect_Type4 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __
    49575045
    49585046(** val instruction_inv_rect_Type3 :
     
    49605048    -> __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode
    49615049    -> __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode
    4962     -> __ -> 'a1) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a1)
    4963     -> (subaddressing_mode preinstruction -> __ -> 'a1) -> 'a1 **)
    4964 let instruction_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
    4965   let hcut = instruction_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
     5050    -> subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction
     5051    -> __ -> 'a1) -> 'a1 **)
     5052let instruction_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 =
     5053  let hcut = instruction_rect_Type3 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __
    49665054
    49675055(** val instruction_inv_rect_Type2 :
     
    49695057    -> __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode
    49705058    -> __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode
    4971     -> __ -> 'a1) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a1)
    4972     -> (subaddressing_mode preinstruction -> __ -> 'a1) -> 'a1 **)
    4973 let instruction_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
    4974   let hcut = instruction_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
     5059    -> subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction
     5060    -> __ -> 'a1) -> 'a1 **)
     5061let instruction_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 =
     5062  let hcut = instruction_rect_Type2 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __
    49755063
    49765064(** val instruction_inv_rect_Type1 :
     
    49785066    -> __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode
    49795067    -> __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode
    4980     -> __ -> 'a1) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a1)
    4981     -> (subaddressing_mode preinstruction -> __ -> 'a1) -> 'a1 **)
    4982 let instruction_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
    4983   let hcut = instruction_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
     5068    -> subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction
     5069    -> __ -> 'a1) -> 'a1 **)
     5070let instruction_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 =
     5071  let hcut = instruction_rect_Type1 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __
    49845072
    49855073(** val instruction_inv_rect_Type0 :
     
    49875075    -> __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode
    49885076    -> __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode
    4989     -> __ -> 'a1) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a1)
    4990     -> (subaddressing_mode preinstruction -> __ -> 'a1) -> 'a1 **)
    4991 let instruction_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
    4992   let hcut = instruction_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
     5077    -> subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction
     5078    -> __ -> 'a1) -> 'a1 **)
     5079let instruction_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 =
     5080  let hcut = instruction_rect_Type0 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __
    49935081
    49945082(** val instruction_discr : instruction -> instruction -> __ **)
     
    50015089     | LJMP a0 -> Obj.magic (fun _ dH -> dH __)
    50025090     | SJMP a0 -> Obj.magic (fun _ dH -> dH __)
    5003      | JMP a0 -> Obj.magic (fun _ dH -> dH __)
    50045091     | MOVC (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
    50055092     | RealInstruction a0 -> Obj.magic (fun _ dH -> dH __)) y
     
    50145101     | LJMP a0 -> Obj.magic (fun _ dH -> dH __)
    50155102     | SJMP a0 -> Obj.magic (fun _ dH -> dH __)
    5016      | JMP a0 -> Obj.magic (fun _ dH -> dH __)
    50175103     | MOVC (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
    50185104     | RealInstruction a0 -> Obj.magic (fun _ dH -> dH __)) y
     
    50335119     | LJMP x -> Bool.False
    50345120     | SJMP x -> Bool.False
    5035      | JMP x -> Bool.False
    50365121     | MOVC (x, x0) -> Bool.False
    50375122     | RealInstruction x -> Bool.False)
     
    50485133     | LJMP x -> Bool.False
    50495134     | SJMP x -> Bool.False
    5050      | JMP x -> Bool.False
    50515135     | MOVC (x, x0) -> Bool.False
    50525136     | RealInstruction x -> Bool.False)
     
    50635147     | LJMP x -> Bool.False
    50645148     | SJMP x -> Bool.False
    5065      | JMP x -> Bool.False
    50665149     | MOVC (x, x0) -> Bool.False
    50675150     | RealInstruction x -> Bool.False)
     
    50785161           Vector.VEmpty)) arg')
    50795162     | SJMP x -> Bool.False
    5080      | JMP x -> Bool.False
    50815163     | MOVC (x, x0) -> Bool.False
    50825164     | RealInstruction x -> Bool.False)
     
    50935175         (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative,
    50945176           Vector.VEmpty)) arg')
    5095      | JMP x -> Bool.False
    5096      | MOVC (x, x0) -> Bool.False
    5097      | RealInstruction x -> Bool.False)
    5098   | JMP arg ->
    5099     (match j with
    5100      | ACALL x -> Bool.False
    5101      | LCALL x -> Bool.False
    5102      | AJMP x -> Bool.False
    5103      | LJMP x -> Bool.False
    5104      | SJMP x -> Bool.False
    5105      | JMP arg' ->
    5106        eq_addressing_mode
    5107          (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Indirect_dptr,
    5108            Vector.VEmpty)) arg)
    5109          (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Indirect_dptr,
    5110            Vector.VEmpty)) arg')
    51115177     | MOVC (x, x0) -> Bool.False
    51125178     | RealInstruction x -> Bool.False)
     
    51185184     | LJMP x -> Bool.False
    51195185     | SJMP x -> Bool.False
    5120      | JMP x -> Bool.False
    51215186     | MOVC (arg1', arg2') ->
    51225187       Bool.andb
     
    51395204     | LJMP x -> Bool.False
    51405205     | SJMP x -> Bool.False
    5141      | JMP x -> Bool.False
    51425206     | MOVC (x, x0) -> Bool.False
    51435207     | RealInstruction instr' -> eq_preinstruction instr instr')
     5208
     5209type word_side =
     5210| HIGH
     5211| LOW
     5212
     5213(** val word_side_rect_Type4 : 'a1 -> 'a1 -> word_side -> 'a1 **)
     5214let rec word_side_rect_Type4 h_HIGH h_LOW = function
     5215| HIGH -> h_HIGH
     5216| LOW -> h_LOW
     5217
     5218(** val word_side_rect_Type5 : 'a1 -> 'a1 -> word_side -> 'a1 **)
     5219let rec word_side_rect_Type5 h_HIGH h_LOW = function
     5220| HIGH -> h_HIGH
     5221| LOW -> h_LOW
     5222
     5223(** val word_side_rect_Type3 : 'a1 -> 'a1 -> word_side -> 'a1 **)
     5224let rec word_side_rect_Type3 h_HIGH h_LOW = function
     5225| HIGH -> h_HIGH
     5226| LOW -> h_LOW
     5227
     5228(** val word_side_rect_Type2 : 'a1 -> 'a1 -> word_side -> 'a1 **)
     5229let rec word_side_rect_Type2 h_HIGH h_LOW = function
     5230| HIGH -> h_HIGH
     5231| LOW -> h_LOW
     5232
     5233(** val word_side_rect_Type1 : 'a1 -> 'a1 -> word_side -> 'a1 **)
     5234let rec word_side_rect_Type1 h_HIGH h_LOW = function
     5235| HIGH -> h_HIGH
     5236| LOW -> h_LOW
     5237
     5238(** val word_side_rect_Type0 : 'a1 -> 'a1 -> word_side -> 'a1 **)
     5239let rec word_side_rect_Type0 h_HIGH h_LOW = function
     5240| HIGH -> h_HIGH
     5241| LOW -> h_LOW
     5242
     5243(** val word_side_inv_rect_Type4 :
     5244    word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
     5245let word_side_inv_rect_Type4 hterm h1 h2 =
     5246  let hcut = word_side_rect_Type4 h1 h2 hterm in hcut __
     5247
     5248(** val word_side_inv_rect_Type3 :
     5249    word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
     5250let word_side_inv_rect_Type3 hterm h1 h2 =
     5251  let hcut = word_side_rect_Type3 h1 h2 hterm in hcut __
     5252
     5253(** val word_side_inv_rect_Type2 :
     5254    word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
     5255let word_side_inv_rect_Type2 hterm h1 h2 =
     5256  let hcut = word_side_rect_Type2 h1 h2 hterm in hcut __
     5257
     5258(** val word_side_inv_rect_Type1 :
     5259    word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
     5260let word_side_inv_rect_Type1 hterm h1 h2 =
     5261  let hcut = word_side_rect_Type1 h1 h2 hterm in hcut __
     5262
     5263(** val word_side_inv_rect_Type0 :
     5264    word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
     5265let word_side_inv_rect_Type0 hterm h1 h2 =
     5266  let hcut = word_side_rect_Type0 h1 h2 hterm in hcut __
     5267
     5268(** val word_side_discr : word_side -> word_side -> __ **)
     5269let word_side_discr x y =
     5270  Logic.eq_rect_Type2 x
     5271    (match x with
     5272     | HIGH -> Obj.magic (fun _ dH -> dH)
     5273     | LOW -> Obj.magic (fun _ dH -> dH)) y
     5274
     5275(** val word_side_jmdiscr : word_side -> word_side -> __ **)
     5276let word_side_jmdiscr x y =
     5277  Logic.eq_rect_Type2 x
     5278    (match x with
     5279     | HIGH -> Obj.magic (fun _ dH -> dH)
     5280     | LOW -> Obj.magic (fun _ dH -> dH)) y
    51445281
    51455282type pseudo_instruction =
     
    51485285| Cost of CostLabel.costlabel
    51495286| Jmp of identifier0
     5287| Jnz of subaddressing_mode * identifier0 * identifier0
     5288| MovSuccessor of subaddressing_mode * word_side * identifier0
    51505289| Call of identifier0
    51515290| Mov of subaddressing_mode * identifier0
     
    51535292(** val pseudo_instruction_rect_Type4 :
    51545293    (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    5155     (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (identifier0 ->
    5156     'a1) -> (subaddressing_mode -> identifier0 -> 'a1) -> pseudo_instruction
    5157     -> 'a1 **)
    5158 let rec pseudo_instruction_rect_Type4 h_Instruction h_Comment h_Cost h_Jmp h_Call h_Mov = function
    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
     5294    (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) ->
     5295    (subaddressing_mode -> identifier0 -> identifier0 -> 'a1) ->
     5296    (subaddressing_mode -> word_side -> identifier0 -> 'a1) -> (identifier0
     5297    -> 'a1) -> (subaddressing_mode -> identifier0 -> 'a1) ->
     5298    pseudo_instruction -> 'a1 **)
     5299let rec pseudo_instruction_rect_Type4 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
     5300| Instruction x_20761 -> h_Instruction x_20761
     5301| Comment x_20762 -> h_Comment x_20762
     5302| Cost x_20763 -> h_Cost x_20763
     5303| Jmp x_20764 -> h_Jmp x_20764
     5304| Jnz (x_20767, x_20766, x_20765) -> h_Jnz x_20767 x_20766 x_20765
     5305| MovSuccessor (x_20770, x_20769, x_20768) ->
     5306  h_MovSuccessor x_20770 x_20769 x_20768
     5307| Call x_20771 -> h_Call x_20771
     5308| Mov (x_20773, x_20772) -> h_Mov x_20773 x_20772
    51655309
    51665310(** val pseudo_instruction_rect_Type5 :
    51675311    (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    5168     (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (identifier0 ->
    5169     'a1) -> (subaddressing_mode -> identifier0 -> 'a1) -> pseudo_instruction
    5170     -> 'a1 **)
    5171 let rec pseudo_instruction_rect_Type5 h_Instruction h_Comment h_Cost h_Jmp h_Call h_Mov = function
    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
     5312    (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) ->
     5313    (subaddressing_mode -> identifier0 -> identifier0 -> 'a1) ->
     5314    (subaddressing_mode -> word_side -> identifier0 -> 'a1) -> (identifier0
     5315    -> 'a1) -> (subaddressing_mode -> identifier0 -> 'a1) ->
     5316    pseudo_instruction -> 'a1 **)
     5317let rec pseudo_instruction_rect_Type5 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
     5318| Instruction x_20783 -> h_Instruction x_20783
     5319| Comment x_20784 -> h_Comment x_20784
     5320| Cost x_20785 -> h_Cost x_20785
     5321| Jmp x_20786 -> h_Jmp x_20786
     5322| Jnz (x_20789, x_20788, x_20787) -> h_Jnz x_20789 x_20788 x_20787
     5323| MovSuccessor (x_20792, x_20791, x_20790) ->
     5324  h_MovSuccessor x_20792 x_20791 x_20790
     5325| Call x_20793 -> h_Call x_20793
     5326| Mov (x_20795, x_20794) -> h_Mov x_20795 x_20794
    51785327
    51795328(** val pseudo_instruction_rect_Type3 :
    51805329    (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    5181     (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (identifier0 ->
    5182     'a1) -> (subaddressing_mode -> identifier0 -> 'a1) -> pseudo_instruction
    5183     -> 'a1 **)
    5184 let rec pseudo_instruction_rect_Type3 h_Instruction h_Comment h_Cost h_Jmp h_Call h_Mov = function
    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
     5330    (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) ->
     5331    (subaddressing_mode -> identifier0 -> identifier0 -> 'a1) ->
     5332    (subaddressing_mode -> word_side -> identifier0 -> 'a1) -> (identifier0
     5333    -> 'a1) -> (subaddressing_mode -> identifier0 -> 'a1) ->
     5334    pseudo_instruction -> 'a1 **)
     5335let rec pseudo_instruction_rect_Type3 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
     5336| Instruction x_20805 -> h_Instruction x_20805
     5337| Comment x_20806 -> h_Comment x_20806
     5338| Cost x_20807 -> h_Cost x_20807
     5339| Jmp x_20808 -> h_Jmp x_20808
     5340| Jnz (x_20811, x_20810, x_20809) -> h_Jnz x_20811 x_20810 x_20809
     5341| MovSuccessor (x_20814, x_20813, x_20812) ->
     5342  h_MovSuccessor x_20814 x_20813 x_20812
     5343| Call x_20815 -> h_Call x_20815
     5344| Mov (x_20817, x_20816) -> h_Mov x_20817 x_20816
    51915345
    51925346(** val pseudo_instruction_rect_Type2 :
    51935347    (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    5194     (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (identifier0 ->
    5195     'a1) -> (subaddressing_mode -> identifier0 -> 'a1) -> pseudo_instruction
    5196     -> 'a1 **)
    5197 let rec pseudo_instruction_rect_Type2 h_Instruction h_Comment h_Cost h_Jmp h_Call h_Mov = function
    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
     5348    (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) ->
     5349    (subaddressing_mode -> identifier0 -> identifier0 -> 'a1) ->
     5350    (subaddressing_mode -> word_side -> identifier0 -> 'a1) -> (identifier0
     5351    -> 'a1) -> (subaddressing_mode -> identifier0 -> 'a1) ->
     5352    pseudo_instruction -> 'a1 **)
     5353let rec pseudo_instruction_rect_Type2 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
     5354| Instruction x_20827 -> h_Instruction x_20827
     5355| Comment x_20828 -> h_Comment x_20828
     5356| Cost x_20829 -> h_Cost x_20829
     5357| Jmp x_20830 -> h_Jmp x_20830
     5358| Jnz (x_20833, x_20832, x_20831) -> h_Jnz x_20833 x_20832 x_20831
     5359| MovSuccessor (x_20836, x_20835, x_20834) ->
     5360  h_MovSuccessor x_20836 x_20835 x_20834
     5361| Call x_20837 -> h_Call x_20837
     5362| Mov (x_20839, x_20838) -> h_Mov x_20839 x_20838
    52045363
    52055364(** val pseudo_instruction_rect_Type1 :
    52065365    (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    5207     (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (identifier0 ->
    5208     'a1) -> (subaddressing_mode -> identifier0 -> 'a1) -> pseudo_instruction
    5209     -> 'a1 **)
    5210 let rec pseudo_instruction_rect_Type1 h_Instruction h_Comment h_Cost h_Jmp h_Call h_Mov = function
    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
     5366    (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) ->
     5367    (subaddressing_mode -> identifier0 -> identifier0 -> 'a1) ->
     5368    (subaddressing_mode -> word_side -> identifier0 -> 'a1) -> (identifier0
     5369    -> 'a1) -> (subaddressing_mode -> identifier0 -> 'a1) ->
     5370    pseudo_instruction -> 'a1 **)
     5371let rec pseudo_instruction_rect_Type1 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
     5372| Instruction x_20849 -> h_Instruction x_20849
     5373| Comment x_20850 -> h_Comment x_20850
     5374| Cost x_20851 -> h_Cost x_20851
     5375| Jmp x_20852 -> h_Jmp x_20852
     5376| Jnz (x_20855, x_20854, x_20853) -> h_Jnz x_20855 x_20854 x_20853
     5377| MovSuccessor (x_20858, x_20857, x_20856) ->
     5378  h_MovSuccessor x_20858 x_20857 x_20856
     5379| Call x_20859 -> h_Call x_20859
     5380| Mov (x_20861, x_20860) -> h_Mov x_20861 x_20860
    52175381
    52185382(** val pseudo_instruction_rect_Type0 :
    52195383    (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    5220     (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (identifier0 ->
    5221     'a1) -> (subaddressing_mode -> identifier0 -> 'a1) -> pseudo_instruction
    5222     -> 'a1 **)
    5223 let rec pseudo_instruction_rect_Type0 h_Instruction h_Comment h_Cost h_Jmp h_Call h_Mov = function
    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
     5384    (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) ->
     5385    (subaddressing_mode -> identifier0 -> identifier0 -> 'a1) ->
     5386    (subaddressing_mode -> word_side -> identifier0 -> 'a1) -> (identifier0
     5387    -> 'a1) -> (subaddressing_mode -> identifier0 -> 'a1) ->
     5388    pseudo_instruction -> 'a1 **)
     5389let rec pseudo_instruction_rect_Type0 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
     5390| Instruction x_20871 -> h_Instruction x_20871
     5391| Comment x_20872 -> h_Comment x_20872
     5392| Cost x_20873 -> h_Cost x_20873
     5393| Jmp x_20874 -> h_Jmp x_20874
     5394| Jnz (x_20877, x_20876, x_20875) -> h_Jnz x_20877 x_20876 x_20875
     5395| MovSuccessor (x_20880, x_20879, x_20878) ->
     5396  h_MovSuccessor x_20880 x_20879 x_20878
     5397| Call x_20881 -> h_Call x_20881
     5398| Mov (x_20883, x_20882) -> h_Mov x_20883 x_20882
    52305399
    52315400(** val pseudo_instruction_inv_rect_Type4 :
    52325401    pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
    52335402    (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
    5234     (identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
     5403    (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
     5404    identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
     5405    identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
    52355406    (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1 **)
    5236 let pseudo_instruction_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 =
    5237   let hcut = pseudo_instruction_rect_Type4 h1 h2 h3 h4 h5 h6 hterm in hcut __
     5407let pseudo_instruction_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
     5408  let hcut = pseudo_instruction_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 hterm in
     5409  hcut __
    52385410
    52395411(** val pseudo_instruction_inv_rect_Type3 :
    52405412    pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
    52415413    (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
    5242     (identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
     5414    (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
     5415    identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
     5416    identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
    52435417    (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1 **)
    5244 let pseudo_instruction_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 =
    5245   let hcut = pseudo_instruction_rect_Type3 h1 h2 h3 h4 h5 h6 hterm in hcut __
     5418let pseudo_instruction_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
     5419  let hcut = pseudo_instruction_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 hterm in
     5420  hcut __
    52465421
    52475422(** val pseudo_instruction_inv_rect_Type2 :
    52485423    pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
    52495424    (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
    5250     (identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
     5425    (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
     5426    identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
     5427    identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
    52515428    (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1 **)
    5252 let pseudo_instruction_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 =
    5253   let hcut = pseudo_instruction_rect_Type2 h1 h2 h3 h4 h5 h6 hterm in hcut __
     5429let pseudo_instruction_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
     5430  let hcut = pseudo_instruction_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 hterm in
     5431  hcut __
    52545432
    52555433(** val pseudo_instruction_inv_rect_Type1 :
    52565434    pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
    52575435    (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
    5258     (identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
     5436    (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
     5437    identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
     5438    identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
    52595439    (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1 **)
    5260 let pseudo_instruction_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 =
    5261   let hcut = pseudo_instruction_rect_Type1 h1 h2 h3 h4 h5 h6 hterm in hcut __
     5440let pseudo_instruction_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
     5441  let hcut = pseudo_instruction_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 hterm in
     5442  hcut __
    52625443
    52635444(** val pseudo_instruction_inv_rect_Type0 :
    52645445    pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
    52655446    (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
    5266     (identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
     5447    (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
     5448    identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
     5449    identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
    52675450    (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1 **)
    5268 let pseudo_instruction_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 =
    5269   let hcut = pseudo_instruction_rect_Type0 h1 h2 h3 h4 h5 h6 hterm in hcut __
     5451let pseudo_instruction_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
     5452  let hcut = pseudo_instruction_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 hterm in
     5453  hcut __
    52705454
    52715455(** val pseudo_instruction_discr :
     
    52785462     | Cost a0 -> Obj.magic (fun _ dH -> dH __)
    52795463     | Jmp a0 -> Obj.magic (fun _ dH -> dH __)
     5464     | Jnz (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     5465     | MovSuccessor (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
    52805466     | Call a0 -> Obj.magic (fun _ dH -> dH __)
    52815467     | Mov (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
     
    52905476     | Cost a0 -> Obj.magic (fun _ dH -> dH __)
    52915477     | Jmp a0 -> Obj.magic (fun _ dH -> dH __)
     5478     | Jnz (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     5479     | MovSuccessor (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
    52925480     | Call a0 -> Obj.magic (fun _ dH -> dH __)
    52935481     | Mov (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
     
    52955483type labelled_instruction = pseudo_instruction LabelledObjects.labelled_obj
    52965484
    5297 type preamble =
    5298   (Nat.nat Identifiers.identifier_map, (identifier0, BitVector.word)
    5299   Types.prod List.list) Types.prod
     5485type preamble = (identifier0, BitVector.word) Types.prod List.list
    53005486
    53015487type assembly_program = instruction List.list
     
    53435529| RETI -> Bool.False
    53445530| NOP -> Bool.False
     5531| JMP x0 -> Bool.False
    53455532
    53465533(** val is_relative_jump : pseudo_instruction -> Bool.bool **)
     
    53505537| Cost x -> Bool.False
    53515538| Jmp x -> Bool.False
     5539| Jnz (x, x0, x1) -> Bool.False
     5540| MovSuccessor (x, x0, x1) -> Bool.False
    53525541| Call x -> Bool.False
    53535542| Mov (x, x0) -> Bool.False
     
    53595548| Cost x -> Bool.False
    53605549| Jmp x -> Bool.True
     5550| Jnz (x, x0, x1) -> Bool.False
     5551| MovSuccessor (x, x0, x1) -> Bool.False
    53615552| Call x -> Bool.True
    53625553| Mov (x, x0) -> Bool.False
     
    53685559| Cost x -> Bool.False
    53695560| Jmp x -> Bool.False
     5561| Jnz (x, x0, x1) -> Bool.False
     5562| MovSuccessor (x, x0, x1) -> Bool.False
    53705563| Call x -> Bool.True
    53715564| Mov (x, x0) -> Bool.False
Note: See TracChangeset for help on using the changeset viewer.