Changeset 3104


Ignore:
Timestamp:
Apr 6, 2013, 6:37:17 PM (4 years ago)
Author:
sacerdot
Message:

Performance improvement.

Files:
3 edited

Legend:

Unmodified
Added
Removed
  • driver/extracted/aSM.ml

    r3059 r3104  
    113113    -> 'a1) -> addressing_mode -> 'a1 **)
    114114let 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
    115 | DIRECT x_19160 -> h_DIRECT x_19160
    116 | INDIRECT x_19161 -> h_INDIRECT x_19161
    117 | EXT_INDIRECT x_19162 -> h_EXT_INDIRECT x_19162
    118 | REGISTER x_19163 -> h_REGISTER x_19163
     115| DIRECT x_33 -> h_DIRECT x_33
     116| INDIRECT x_34 -> h_INDIRECT x_34
     117| EXT_INDIRECT x_35 -> h_EXT_INDIRECT x_35
     118| REGISTER x_36 -> h_REGISTER x_36
    119119| ACC_A -> h_ACC_A
    120120| ACC_B -> h_ACC_B
    121121| DPTR -> h_DPTR
    122 | DATA x_19164 -> h_DATA x_19164
    123 | DATA16 x_19165 -> h_DATA16 x_19165
     122| DATA x_37 -> h_DATA x_37
     123| DATA16 x_38 -> h_DATA16 x_38
    124124| ACC_DPTR -> h_ACC_DPTR
    125125| ACC_PC -> h_ACC_PC
     
    127127| INDIRECT_DPTR -> h_INDIRECT_DPTR
    128128| CARRY -> h_CARRY
    129 | BIT_ADDR x_19166 -> h_BIT_ADDR x_19166
    130 | N_BIT_ADDR x_19167 -> h_N_BIT_ADDR x_19167
    131 | RELATIVE x_19168 -> h_RELATIVE x_19168
    132 | ADDR11 x_19169 -> h_ADDR11 x_19169
    133 | ADDR16 x_19170 -> h_ADDR16 x_19170
     129| BIT_ADDR x_39 -> h_BIT_ADDR x_39
     130| N_BIT_ADDR x_40 -> h_N_BIT_ADDR x_40
     131| RELATIVE x_41 -> h_RELATIVE x_41
     132| ADDR11 x_42 -> h_ADDR11 x_42
     133| ADDR16 x_43 -> h_ADDR16 x_43
    134134
    135135(** val addressing_mode_rect_Type5 :
     
    141141    -> 'a1) -> addressing_mode -> 'a1 **)
    142142let 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
    143 | DIRECT x_19191 -> h_DIRECT x_19191
    144 | INDIRECT x_19192 -> h_INDIRECT x_19192
    145 | EXT_INDIRECT x_19193 -> h_EXT_INDIRECT x_19193
    146 | REGISTER x_19194 -> h_REGISTER x_19194
     143| DIRECT x_64 -> h_DIRECT x_64
     144| INDIRECT x_65 -> h_INDIRECT x_65
     145| EXT_INDIRECT x_66 -> h_EXT_INDIRECT x_66
     146| REGISTER x_67 -> h_REGISTER x_67
    147147| ACC_A -> h_ACC_A
    148148| ACC_B -> h_ACC_B
    149149| DPTR -> h_DPTR
    150 | DATA x_19195 -> h_DATA x_19195
    151 | DATA16 x_19196 -> h_DATA16 x_19196
     150| DATA x_68 -> h_DATA x_68
     151| DATA16 x_69 -> h_DATA16 x_69
    152152| ACC_DPTR -> h_ACC_DPTR
    153153| ACC_PC -> h_ACC_PC
     
    155155| INDIRECT_DPTR -> h_INDIRECT_DPTR
    156156| CARRY -> h_CARRY
    157 | BIT_ADDR x_19197 -> h_BIT_ADDR x_19197
    158 | N_BIT_ADDR x_19198 -> h_N_BIT_ADDR x_19198
    159 | RELATIVE x_19199 -> h_RELATIVE x_19199
    160 | ADDR11 x_19200 -> h_ADDR11 x_19200
    161 | ADDR16 x_19201 -> h_ADDR16 x_19201
     157| BIT_ADDR x_70 -> h_BIT_ADDR x_70
     158| N_BIT_ADDR x_71 -> h_N_BIT_ADDR x_71
     159| RELATIVE x_72 -> h_RELATIVE x_72
     160| ADDR11 x_73 -> h_ADDR11 x_73
     161| ADDR16 x_74 -> h_ADDR16 x_74
    162162
    163163(** val addressing_mode_rect_Type3 :
     
    169169    -> 'a1) -> addressing_mode -> 'a1 **)
    170170let 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
    171 | DIRECT x_19222 -> h_DIRECT x_19222
    172 | INDIRECT x_19223 -> h_INDIRECT x_19223
    173 | EXT_INDIRECT x_19224 -> h_EXT_INDIRECT x_19224
    174 | REGISTER x_19225 -> h_REGISTER x_19225
     171| DIRECT x_95 -> h_DIRECT x_95
     172| INDIRECT x_96 -> h_INDIRECT x_96
     173| EXT_INDIRECT x_97 -> h_EXT_INDIRECT x_97
     174| REGISTER x_98 -> h_REGISTER x_98
    175175| ACC_A -> h_ACC_A
    176176| ACC_B -> h_ACC_B
    177177| DPTR -> h_DPTR
    178 | DATA x_19226 -> h_DATA x_19226
    179 | DATA16 x_19227 -> h_DATA16 x_19227
     178| DATA x_99 -> h_DATA x_99
     179| DATA16 x_100 -> h_DATA16 x_100
    180180| ACC_DPTR -> h_ACC_DPTR
    181181| ACC_PC -> h_ACC_PC
     
    183183| INDIRECT_DPTR -> h_INDIRECT_DPTR
    184184| CARRY -> h_CARRY
    185 | BIT_ADDR x_19228 -> h_BIT_ADDR x_19228
    186 | N_BIT_ADDR x_19229 -> h_N_BIT_ADDR x_19229
    187 | RELATIVE x_19230 -> h_RELATIVE x_19230
    188 | ADDR11 x_19231 -> h_ADDR11 x_19231
    189 | ADDR16 x_19232 -> h_ADDR16 x_19232
     185| BIT_ADDR x_101 -> h_BIT_ADDR x_101
     186| N_BIT_ADDR x_102 -> h_N_BIT_ADDR x_102
     187| RELATIVE x_103 -> h_RELATIVE x_103
     188| ADDR11 x_104 -> h_ADDR11 x_104
     189| ADDR16 x_105 -> h_ADDR16 x_105
    190190
    191191(** val addressing_mode_rect_Type2 :
     
    197197    -> 'a1) -> addressing_mode -> 'a1 **)
    198198let 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
    199 | DIRECT x_19253 -> h_DIRECT x_19253
    200 | INDIRECT x_19254 -> h_INDIRECT x_19254
    201 | EXT_INDIRECT x_19255 -> h_EXT_INDIRECT x_19255
    202 | REGISTER x_19256 -> h_REGISTER x_19256
     199| DIRECT x_126 -> h_DIRECT x_126
     200| INDIRECT x_127 -> h_INDIRECT x_127
     201| EXT_INDIRECT x_128 -> h_EXT_INDIRECT x_128
     202| REGISTER x_129 -> h_REGISTER x_129
    203203| ACC_A -> h_ACC_A
    204204| ACC_B -> h_ACC_B
    205205| DPTR -> h_DPTR
    206 | DATA x_19257 -> h_DATA x_19257
    207 | DATA16 x_19258 -> h_DATA16 x_19258
     206| DATA x_130 -> h_DATA x_130
     207| DATA16 x_131 -> h_DATA16 x_131
    208208| ACC_DPTR -> h_ACC_DPTR
    209209| ACC_PC -> h_ACC_PC
     
    211211| INDIRECT_DPTR -> h_INDIRECT_DPTR
    212212| CARRY -> h_CARRY
    213 | BIT_ADDR x_19259 -> h_BIT_ADDR x_19259
    214 | N_BIT_ADDR x_19260 -> h_N_BIT_ADDR x_19260
    215 | RELATIVE x_19261 -> h_RELATIVE x_19261
    216 | ADDR11 x_19262 -> h_ADDR11 x_19262
    217 | ADDR16 x_19263 -> h_ADDR16 x_19263
     213| BIT_ADDR x_132 -> h_BIT_ADDR x_132
     214| N_BIT_ADDR x_133 -> h_N_BIT_ADDR x_133
     215| RELATIVE x_134 -> h_RELATIVE x_134
     216| ADDR11 x_135 -> h_ADDR11 x_135
     217| ADDR16 x_136 -> h_ADDR16 x_136
    218218
    219219(** val addressing_mode_rect_Type1 :
     
    225225    -> 'a1) -> addressing_mode -> 'a1 **)
    226226let 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
    227 | DIRECT x_19284 -> h_DIRECT x_19284
    228 | INDIRECT x_19285 -> h_INDIRECT x_19285
    229 | EXT_INDIRECT x_19286 -> h_EXT_INDIRECT x_19286
    230 | REGISTER x_19287 -> h_REGISTER x_19287
     227| DIRECT x_157 -> h_DIRECT x_157
     228| INDIRECT x_158 -> h_INDIRECT x_158
     229| EXT_INDIRECT x_159 -> h_EXT_INDIRECT x_159
     230| REGISTER x_160 -> h_REGISTER x_160
    231231| ACC_A -> h_ACC_A
    232232| ACC_B -> h_ACC_B
    233233| DPTR -> h_DPTR
    234 | DATA x_19288 -> h_DATA x_19288
    235 | DATA16 x_19289 -> h_DATA16 x_19289
     234| DATA x_161 -> h_DATA x_161
     235| DATA16 x_162 -> h_DATA16 x_162
    236236| ACC_DPTR -> h_ACC_DPTR
    237237| ACC_PC -> h_ACC_PC
     
    239239| INDIRECT_DPTR -> h_INDIRECT_DPTR
    240240| CARRY -> h_CARRY
    241 | BIT_ADDR x_19290 -> h_BIT_ADDR x_19290
    242 | N_BIT_ADDR x_19291 -> h_N_BIT_ADDR x_19291
    243 | RELATIVE x_19292 -> h_RELATIVE x_19292
    244 | ADDR11 x_19293 -> h_ADDR11 x_19293
    245 | ADDR16 x_19294 -> h_ADDR16 x_19294
     241| BIT_ADDR x_163 -> h_BIT_ADDR x_163
     242| N_BIT_ADDR x_164 -> h_N_BIT_ADDR x_164
     243| RELATIVE x_165 -> h_RELATIVE x_165
     244| ADDR11 x_166 -> h_ADDR11 x_166
     245| ADDR16 x_167 -> h_ADDR16 x_167
    246246
    247247(** val addressing_mode_rect_Type0 :
     
    253253    -> 'a1) -> addressing_mode -> 'a1 **)
    254254let 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
    255 | DIRECT x_19315 -> h_DIRECT x_19315
    256 | INDIRECT x_19316 -> h_INDIRECT x_19316
    257 | EXT_INDIRECT x_19317 -> h_EXT_INDIRECT x_19317
    258 | REGISTER x_19318 -> h_REGISTER x_19318
     255| DIRECT x_188 -> h_DIRECT x_188
     256| INDIRECT x_189 -> h_INDIRECT x_189
     257| EXT_INDIRECT x_190 -> h_EXT_INDIRECT x_190
     258| REGISTER x_191 -> h_REGISTER x_191
    259259| ACC_A -> h_ACC_A
    260260| ACC_B -> h_ACC_B
    261261| DPTR -> h_DPTR
    262 | DATA x_19319 -> h_DATA x_19319
    263 | DATA16 x_19320 -> h_DATA16 x_19320
     262| DATA x_192 -> h_DATA x_192
     263| DATA16 x_193 -> h_DATA16 x_193
    264264| ACC_DPTR -> h_ACC_DPTR
    265265| ACC_PC -> h_ACC_PC
     
    267267| INDIRECT_DPTR -> h_INDIRECT_DPTR
    268268| CARRY -> h_CARRY
    269 | BIT_ADDR x_19321 -> h_BIT_ADDR x_19321
    270 | N_BIT_ADDR x_19322 -> h_N_BIT_ADDR x_19322
    271 | RELATIVE x_19323 -> h_RELATIVE x_19323
    272 | ADDR11 x_19324 -> h_ADDR11 x_19324
    273 | ADDR16 x_19325 -> h_ADDR16 x_19325
     269| BIT_ADDR x_194 -> h_BIT_ADDR x_194
     270| N_BIT_ADDR x_195 -> h_N_BIT_ADDR x_195
     271| RELATIVE x_196 -> h_RELATIVE x_196
     272| ADDR11 x_197 -> h_ADDR11 x_197
     273| ADDR16 x_198 -> h_ADDR16 x_198
    274274
    275275(** val addressing_mode_inv_rect_Type4 :
     
    19261926    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19271927    'a1) -> subaddressing_mode -> 'a1 **)
    1928 let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_19793 =
    1929   let subaddressing_modeel = x_19793 in
     1928let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_666 =
     1929  let subaddressing_modeel = x_666 in
    19301930  h_mk_subaddressing_mode subaddressing_modeel __
    19311931
     
    19331933    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19341934    'a1) -> subaddressing_mode -> 'a1 **)
    1935 let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_19795 =
    1936   let subaddressing_modeel = x_19795 in
     1935let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_668 =
     1936  let subaddressing_modeel = x_668 in
    19371937  h_mk_subaddressing_mode subaddressing_modeel __
    19381938
     
    19401940    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19411941    'a1) -> subaddressing_mode -> 'a1 **)
    1942 let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_19797 =
    1943   let subaddressing_modeel = x_19797 in
     1942let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_670 =
     1943  let subaddressing_modeel = x_670 in
    19441944  h_mk_subaddressing_mode subaddressing_modeel __
    19451945
     
    19471947    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19481948    'a1) -> subaddressing_mode -> 'a1 **)
    1949 let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_19799 =
    1950   let subaddressing_modeel = x_19799 in
     1949let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_672 =
     1950  let subaddressing_modeel = x_672 in
    19511951  h_mk_subaddressing_mode subaddressing_modeel __
    19521952
     
    19541954    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19551955    'a1) -> subaddressing_mode -> 'a1 **)
    1956 let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_19801 =
    1957   let subaddressing_modeel = x_19801 in
     1956let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_674 =
     1957  let subaddressing_modeel = x_674 in
    19581958  h_mk_subaddressing_mode subaddressing_modeel __
    19591959
     
    19611961    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19621962    'a1) -> subaddressing_mode -> 'a1 **)
    1963 let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_19803 =
    1964   let subaddressing_modeel = x_19803 in
     1963let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_676 =
     1964  let subaddressing_modeel = x_676 in
    19651965  h_mk_subaddressing_mode subaddressing_modeel __
    19661966
     
    22882288    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    22892289let 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
    2290 | ADD (x_19905, x_19904) -> h_ADD x_19905 x_19904
    2291 | ADDC (x_19907, x_19906) -> h_ADDC x_19907 x_19906
    2292 | SUBB (x_19909, x_19908) -> h_SUBB x_19909 x_19908
    2293 | INC x_19910 -> h_INC x_19910
    2294 | DEC x_19911 -> h_DEC x_19911
    2295 | MUL (x_19913, x_19912) -> h_MUL x_19913 x_19912
    2296 | DIV (x_19915, x_19914) -> h_DIV x_19915 x_19914
    2297 | DA x_19916 -> h_DA x_19916
    2298 | JC x_19917 -> h_JC x_19917
    2299 | JNC x_19918 -> h_JNC x_19918
    2300 | JB (x_19920, x_19919) -> h_JB x_19920 x_19919
    2301 | JNB (x_19922, x_19921) -> h_JNB x_19922 x_19921
    2302 | JBC (x_19924, x_19923) -> h_JBC x_19924 x_19923
    2303 | JZ x_19925 -> h_JZ x_19925
    2304 | JNZ x_19926 -> h_JNZ x_19926
    2305 | CJNE (x_19928, x_19927) -> h_CJNE x_19928 x_19927
    2306 | DJNZ (x_19930, x_19929) -> h_DJNZ x_19930 x_19929
    2307 | ANL x_19931 -> h_ANL x_19931
    2308 | ORL x_19932 -> h_ORL x_19932
    2309 | XRL x_19933 -> h_XRL x_19933
    2310 | CLR x_19934 -> h_CLR x_19934
    2311 | CPL x_19935 -> h_CPL x_19935
    2312 | RL x_19936 -> h_RL x_19936
    2313 | RLC x_19937 -> h_RLC x_19937
    2314 | RR x_19938 -> h_RR x_19938
    2315 | RRC x_19939 -> h_RRC x_19939
    2316 | SWAP x_19940 -> h_SWAP x_19940
    2317 | MOV x_19941 -> h_MOV x_19941
    2318 | MOVX x_19942 -> h_MOVX x_19942
    2319 | SETB x_19943 -> h_SETB x_19943
    2320 | PUSH x_19944 -> h_PUSH x_19944
    2321 | POP x_19945 -> h_POP x_19945
    2322 | XCH (x_19947, x_19946) -> h_XCH x_19947 x_19946
    2323 | XCHD (x_19949, x_19948) -> h_XCHD x_19949 x_19948
     2290| ADD (x_778, x_777) -> h_ADD x_778 x_777
     2291| ADDC (x_780, x_779) -> h_ADDC x_780 x_779
     2292| SUBB (x_782, x_781) -> h_SUBB x_782 x_781
     2293| INC x_783 -> h_INC x_783
     2294| DEC x_784 -> h_DEC x_784
     2295| MUL (x_786, x_785) -> h_MUL x_786 x_785
     2296| DIV (x_788, x_787) -> h_DIV x_788 x_787
     2297| DA x_789 -> h_DA x_789
     2298| JC x_790 -> h_JC x_790
     2299| JNC x_791 -> h_JNC x_791
     2300| JB (x_793, x_792) -> h_JB x_793 x_792
     2301| JNB (x_795, x_794) -> h_JNB x_795 x_794
     2302| JBC (x_797, x_796) -> h_JBC x_797 x_796
     2303| JZ x_798 -> h_JZ x_798
     2304| JNZ x_799 -> h_JNZ x_799
     2305| CJNE (x_801, x_800) -> h_CJNE x_801 x_800
     2306| DJNZ (x_803, x_802) -> h_DJNZ x_803 x_802
     2307| ANL x_804 -> h_ANL x_804
     2308| ORL x_805 -> h_ORL x_805
     2309| XRL x_806 -> h_XRL x_806
     2310| CLR x_807 -> h_CLR x_807
     2311| CPL x_808 -> h_CPL x_808
     2312| RL x_809 -> h_RL x_809
     2313| RLC x_810 -> h_RLC x_810
     2314| RR x_811 -> h_RR x_811
     2315| RRC x_812 -> h_RRC x_812
     2316| SWAP x_813 -> h_SWAP x_813
     2317| MOV x_814 -> h_MOV x_814
     2318| MOVX x_815 -> h_MOVX x_815
     2319| SETB x_816 -> h_SETB x_816
     2320| PUSH x_817 -> h_PUSH x_817
     2321| POP x_818 -> h_POP x_818
     2322| XCH (x_820, x_819) -> h_XCH x_820 x_819
     2323| XCHD (x_822, x_821) -> h_XCHD x_822 x_821
    23242324| RET -> h_RET
    23252325| RETI -> h_RETI
    23262326| NOP -> h_NOP
    2327 | JMP x_19950 -> h_JMP x_19950
     2327| JMP x_823 -> h_JMP x_823
    23282328
    23292329(** val preinstruction_rect_Type5 :
     
    23632363    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    23642364let 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
    2365 | ADD (x_19991, x_19990) -> h_ADD x_19991 x_19990
    2366 | ADDC (x_19993, x_19992) -> h_ADDC x_19993 x_19992
    2367 | SUBB (x_19995, x_19994) -> h_SUBB x_19995 x_19994
    2368 | INC x_19996 -> h_INC x_19996
    2369 | DEC x_19997 -> h_DEC x_19997
    2370 | MUL (x_19999, x_19998) -> h_MUL x_19999 x_19998
    2371 | DIV (x_20001, x_20000) -> h_DIV x_20001 x_20000
    2372 | DA x_20002 -> h_DA x_20002
    2373 | JC x_20003 -> h_JC x_20003
    2374 | JNC x_20004 -> h_JNC x_20004
    2375 | JB (x_20006, x_20005) -> h_JB x_20006 x_20005
    2376 | JNB (x_20008, x_20007) -> h_JNB x_20008 x_20007
    2377 | JBC (x_20010, x_20009) -> h_JBC x_20010 x_20009
    2378 | JZ x_20011 -> h_JZ x_20011
    2379 | JNZ x_20012 -> h_JNZ x_20012
    2380 | CJNE (x_20014, x_20013) -> h_CJNE x_20014 x_20013
    2381 | DJNZ (x_20016, x_20015) -> h_DJNZ x_20016 x_20015
    2382 | ANL x_20017 -> h_ANL x_20017
    2383 | ORL x_20018 -> h_ORL x_20018
    2384 | XRL x_20019 -> h_XRL x_20019
    2385 | CLR x_20020 -> h_CLR x_20020
    2386 | CPL x_20021 -> h_CPL x_20021
    2387 | RL x_20022 -> h_RL x_20022
    2388 | RLC x_20023 -> h_RLC x_20023
    2389 | RR x_20024 -> h_RR x_20024
    2390 | RRC x_20025 -> h_RRC x_20025
    2391 | SWAP x_20026 -> h_SWAP x_20026
    2392 | MOV x_20027 -> h_MOV x_20027
    2393 | MOVX x_20028 -> h_MOVX x_20028
    2394 | SETB x_20029 -> h_SETB x_20029
    2395 | PUSH x_20030 -> h_PUSH x_20030
    2396 | POP x_20031 -> h_POP x_20031
    2397 | XCH (x_20033, x_20032) -> h_XCH x_20033 x_20032
    2398 | XCHD (x_20035, x_20034) -> h_XCHD x_20035 x_20034
     2365| ADD (x_864, x_863) -> h_ADD x_864 x_863
     2366| ADDC (x_866, x_865) -> h_ADDC x_866 x_865
     2367| SUBB (x_868, x_867) -> h_SUBB x_868 x_867
     2368| INC x_869 -> h_INC x_869
     2369| DEC x_870 -> h_DEC x_870
     2370| MUL (x_872, x_871) -> h_MUL x_872 x_871
     2371| DIV (x_874, x_873) -> h_DIV x_874 x_873
     2372| DA x_875 -> h_DA x_875
     2373| JC x_876 -> h_JC x_876
     2374| JNC x_877 -> h_JNC x_877
     2375| JB (x_879, x_878) -> h_JB x_879 x_878
     2376| JNB (x_881, x_880) -> h_JNB x_881 x_880
     2377| JBC (x_883, x_882) -> h_JBC x_883 x_882
     2378| JZ x_884 -> h_JZ x_884
     2379| JNZ x_885 -> h_JNZ x_885
     2380| CJNE (x_887, x_886) -> h_CJNE x_887 x_886
     2381| DJNZ (x_889, x_888) -> h_DJNZ x_889 x_888
     2382| ANL x_890 -> h_ANL x_890
     2383| ORL x_891 -> h_ORL x_891
     2384| XRL x_892 -> h_XRL x_892
     2385| CLR x_893 -> h_CLR x_893
     2386| CPL x_894 -> h_CPL x_894
     2387| RL x_895 -> h_RL x_895
     2388| RLC x_896 -> h_RLC x_896
     2389| RR x_897 -> h_RR x_897
     2390| RRC x_898 -> h_RRC x_898
     2391| SWAP x_899 -> h_SWAP x_899
     2392| MOV x_900 -> h_MOV x_900
     2393| MOVX x_901 -> h_MOVX x_901
     2394| SETB x_902 -> h_SETB x_902
     2395| PUSH x_903 -> h_PUSH x_903
     2396| POP x_904 -> h_POP x_904
     2397| XCH (x_906, x_905) -> h_XCH x_906 x_905
     2398| XCHD (x_908, x_907) -> h_XCHD x_908 x_907
    23992399| RET -> h_RET
    24002400| RETI -> h_RETI
    24012401| NOP -> h_NOP
    2402 | JMP x_20036 -> h_JMP x_20036
     2402| JMP x_909 -> h_JMP x_909
    24032403
    24042404(** val preinstruction_rect_Type3 :
     
    24382438    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    24392439let 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
    2440 | ADD (x_20077, x_20076) -> h_ADD x_20077 x_20076
    2441 | ADDC (x_20079, x_20078) -> h_ADDC x_20079 x_20078
    2442 | SUBB (x_20081, x_20080) -> h_SUBB x_20081 x_20080
    2443 | INC x_20082 -> h_INC x_20082
    2444 | DEC x_20083 -> h_DEC x_20083
    2445 | MUL (x_20085, x_20084) -> h_MUL x_20085 x_20084
    2446 | DIV (x_20087, x_20086) -> h_DIV x_20087 x_20086
    2447 | DA x_20088 -> h_DA x_20088
    2448 | JC x_20089 -> h_JC x_20089
    2449 | JNC x_20090 -> h_JNC x_20090
    2450 | JB (x_20092, x_20091) -> h_JB x_20092 x_20091
    2451 | JNB (x_20094, x_20093) -> h_JNB x_20094 x_20093
    2452 | JBC (x_20096, x_20095) -> h_JBC x_20096 x_20095
    2453 | JZ x_20097 -> h_JZ x_20097
    2454 | JNZ x_20098 -> h_JNZ x_20098
    2455 | CJNE (x_20100, x_20099) -> h_CJNE x_20100 x_20099
    2456 | DJNZ (x_20102, x_20101) -> h_DJNZ x_20102 x_20101
    2457 | ANL x_20103 -> h_ANL x_20103
    2458 | ORL x_20104 -> h_ORL x_20104
    2459 | XRL x_20105 -> h_XRL x_20105
    2460 | CLR x_20106 -> h_CLR x_20106
    2461 | CPL x_20107 -> h_CPL x_20107
    2462 | RL x_20108 -> h_RL x_20108
    2463 | RLC x_20109 -> h_RLC x_20109
    2464 | RR x_20110 -> h_RR x_20110
    2465 | RRC x_20111 -> h_RRC x_20111
    2466 | SWAP x_20112 -> h_SWAP x_20112
    2467 | MOV x_20113 -> h_MOV x_20113
    2468 | MOVX x_20114 -> h_MOVX x_20114
    2469 | SETB x_20115 -> h_SETB x_20115
    2470 | PUSH x_20116 -> h_PUSH x_20116
    2471 | POP x_20117 -> h_POP x_20117
    2472 | XCH (x_20119, x_20118) -> h_XCH x_20119 x_20118
    2473 | XCHD (x_20121, x_20120) -> h_XCHD x_20121 x_20120
     2440| ADD (x_950, x_949) -> h_ADD x_950 x_949
     2441| ADDC (x_952, x_951) -> h_ADDC x_952 x_951
     2442| SUBB (x_954, x_953) -> h_SUBB x_954 x_953
     2443| INC x_955 -> h_INC x_955
     2444| DEC x_956 -> h_DEC x_956
     2445| MUL (x_958, x_957) -> h_MUL x_958 x_957
     2446| DIV (x_960, x_959) -> h_DIV x_960 x_959
     2447| DA x_961 -> h_DA x_961
     2448| JC x_962 -> h_JC x_962
     2449| JNC x_963 -> h_JNC x_963
     2450| JB (x_965, x_964) -> h_JB x_965 x_964
     2451| JNB (x_967, x_966) -> h_JNB x_967 x_966
     2452| JBC (x_969, x_968) -> h_JBC x_969 x_968
     2453| JZ x_970 -> h_JZ x_970
     2454| JNZ x_971 -> h_JNZ x_971
     2455| CJNE (x_973, x_972) -> h_CJNE x_973 x_972
     2456| DJNZ (x_975, x_974) -> h_DJNZ x_975 x_974
     2457| ANL x_976 -> h_ANL x_976
     2458| ORL x_977 -> h_ORL x_977
     2459| XRL x_978 -> h_XRL x_978
     2460| CLR x_979 -> h_CLR x_979
     2461| CPL x_980 -> h_CPL x_980
     2462| RL x_981 -> h_RL x_981
     2463| RLC x_982 -> h_RLC x_982
     2464| RR x_983 -> h_RR x_983
     2465| RRC x_984 -> h_RRC x_984
     2466| SWAP x_985 -> h_SWAP x_985
     2467| MOV x_986 -> h_MOV x_986
     2468| MOVX x_987 -> h_MOVX x_987
     2469| SETB x_988 -> h_SETB x_988
     2470| PUSH x_989 -> h_PUSH x_989
     2471| POP x_990 -> h_POP x_990
     2472| XCH (x_992, x_991) -> h_XCH x_992 x_991
     2473| XCHD (x_994, x_993) -> h_XCHD x_994 x_993
    24742474| RET -> h_RET
    24752475| RETI -> h_RETI
    24762476| NOP -> h_NOP
    2477 | JMP x_20122 -> h_JMP x_20122
     2477| JMP x_995 -> h_JMP x_995
    24782478
    24792479(** val preinstruction_rect_Type2 :
     
    25132513    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    25142514let 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
    2515 | ADD (x_20163, x_20162) -> h_ADD x_20163 x_20162
    2516 | ADDC (x_20165, x_20164) -> h_ADDC x_20165 x_20164
    2517 | SUBB (x_20167, x_20166) -> h_SUBB x_20167 x_20166
    2518 | INC x_20168 -> h_INC x_20168
    2519 | DEC x_20169 -> h_DEC x_20169
    2520 | MUL (x_20171, x_20170) -> h_MUL x_20171 x_20170
    2521 | DIV (x_20173, x_20172) -> h_DIV x_20173 x_20172
    2522 | DA x_20174 -> h_DA x_20174
    2523 | JC x_20175 -> h_JC x_20175
    2524 | JNC x_20176 -> h_JNC x_20176
    2525 | JB (x_20178, x_20177) -> h_JB x_20178 x_20177
    2526 | JNB (x_20180, x_20179) -> h_JNB x_20180 x_20179
    2527 | JBC (x_20182, x_20181) -> h_JBC x_20182 x_20181
    2528 | JZ x_20183 -> h_JZ x_20183
    2529 | JNZ x_20184 -> h_JNZ x_20184
    2530 | CJNE (x_20186, x_20185) -> h_CJNE x_20186 x_20185
    2531 | DJNZ (x_20188, x_20187) -> h_DJNZ x_20188 x_20187
    2532 | ANL x_20189 -> h_ANL x_20189
    2533 | ORL x_20190 -> h_ORL x_20190
    2534 | XRL x_20191 -> h_XRL x_20191
    2535 | CLR x_20192 -> h_CLR x_20192
    2536 | CPL x_20193 -> h_CPL x_20193
    2537 | RL x_20194 -> h_RL x_20194
    2538 | RLC x_20195 -> h_RLC x_20195
    2539 | RR x_20196 -> h_RR x_20196
    2540 | RRC x_20197 -> h_RRC x_20197
    2541 | SWAP x_20198 -> h_SWAP x_20198
    2542 | MOV x_20199 -> h_MOV x_20199
    2543 | MOVX x_20200 -> h_MOVX x_20200
    2544 | SETB x_20201 -> h_SETB x_20201
    2545 | PUSH x_20202 -> h_PUSH x_20202
    2546 | POP x_20203 -> h_POP x_20203
    2547 | XCH (x_20205, x_20204) -> h_XCH x_20205 x_20204
    2548 | XCHD (x_20207, x_20206) -> h_XCHD x_20207 x_20206
     2515| ADD (x_1036, x_1035) -> h_ADD x_1036 x_1035
     2516| ADDC (x_1038, x_1037) -> h_ADDC x_1038 x_1037
     2517| SUBB (x_1040, x_1039) -> h_SUBB x_1040 x_1039
     2518| INC x_1041 -> h_INC x_1041
     2519| DEC x_1042 -> h_DEC x_1042
     2520| MUL (x_1044, x_1043) -> h_MUL x_1044 x_1043
     2521| DIV (x_1046, x_1045) -> h_DIV x_1046 x_1045
     2522| DA x_1047 -> h_DA x_1047
     2523| JC x_1048 -> h_JC x_1048
     2524| JNC x_1049 -> h_JNC x_1049
     2525| JB (x_1051, x_1050) -> h_JB x_1051 x_1050
     2526| JNB (x_1053, x_1052) -> h_JNB x_1053 x_1052
     2527| JBC (x_1055, x_1054) -> h_JBC x_1055 x_1054
     2528| JZ x_1056 -> h_JZ x_1056
     2529| JNZ x_1057 -> h_JNZ x_1057
     2530| CJNE (x_1059, x_1058) -> h_CJNE x_1059 x_1058
     2531| DJNZ (x_1061, x_1060) -> h_DJNZ x_1061 x_1060
     2532| ANL x_1062 -> h_ANL x_1062
     2533| ORL x_1063 -> h_ORL x_1063
     2534| XRL x_1064 -> h_XRL x_1064
     2535| CLR x_1065 -> h_CLR x_1065
     2536| CPL x_1066 -> h_CPL x_1066
     2537| RL x_1067 -> h_RL x_1067
     2538| RLC x_1068 -> h_RLC x_1068
     2539| RR x_1069 -> h_RR x_1069
     2540| RRC x_1070 -> h_RRC x_1070
     2541| SWAP x_1071 -> h_SWAP x_1071
     2542| MOV x_1072 -> h_MOV x_1072
     2543| MOVX x_1073 -> h_MOVX x_1073
     2544| SETB x_1074 -> h_SETB x_1074
     2545| PUSH x_1075 -> h_PUSH x_1075
     2546| POP x_1076 -> h_POP x_1076
     2547| XCH (x_1078, x_1077) -> h_XCH x_1078 x_1077
     2548| XCHD (x_1080, x_1079) -> h_XCHD x_1080 x_1079
    25492549| RET -> h_RET
    25502550| RETI -> h_RETI
    25512551| NOP -> h_NOP
    2552 | JMP x_20208 -> h_JMP x_20208
     2552| JMP x_1081 -> h_JMP x_1081
    25532553
    25542554(** val preinstruction_rect_Type1 :
     
    25882588    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    25892589let 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
    2590 | ADD (x_20249, x_20248) -> h_ADD x_20249 x_20248
    2591 | ADDC (x_20251, x_20250) -> h_ADDC x_20251 x_20250
    2592 | SUBB (x_20253, x_20252) -> h_SUBB x_20253 x_20252
    2593 | INC x_20254 -> h_INC x_20254
    2594 | DEC x_20255 -> h_DEC x_20255
    2595 | MUL (x_20257, x_20256) -> h_MUL x_20257 x_20256
    2596 | DIV (x_20259, x_20258) -> h_DIV x_20259 x_20258
    2597 | DA x_20260 -> h_DA x_20260
    2598 | JC x_20261 -> h_JC x_20261
    2599 | JNC x_20262 -> h_JNC x_20262
    2600 | JB (x_20264, x_20263) -> h_JB x_20264 x_20263
    2601 | JNB (x_20266, x_20265) -> h_JNB x_20266 x_20265
    2602 | JBC (x_20268, x_20267) -> h_JBC x_20268 x_20267
    2603 | JZ x_20269 -> h_JZ x_20269
    2604 | JNZ x_20270 -> h_JNZ x_20270
    2605 | CJNE (x_20272, x_20271) -> h_CJNE x_20272 x_20271
    2606 | DJNZ (x_20274, x_20273) -> h_DJNZ x_20274 x_20273
    2607 | ANL x_20275 -> h_ANL x_20275
    2608 | ORL x_20276 -> h_ORL x_20276
    2609 | XRL x_20277 -> h_XRL x_20277
    2610 | CLR x_20278 -> h_CLR x_20278
    2611 | CPL x_20279 -> h_CPL x_20279
    2612 | RL x_20280 -> h_RL x_20280
    2613 | RLC x_20281 -> h_RLC x_20281
    2614 | RR x_20282 -> h_RR x_20282
    2615 | RRC x_20283 -> h_RRC x_20283
    2616 | SWAP x_20284 -> h_SWAP x_20284
    2617 | MOV x_20285 -> h_MOV x_20285
    2618 | MOVX x_20286 -> h_MOVX x_20286
    2619 | SETB x_20287 -> h_SETB x_20287
    2620 | PUSH x_20288 -> h_PUSH x_20288
    2621 | POP x_20289 -> h_POP x_20289
    2622 | XCH (x_20291, x_20290) -> h_XCH x_20291 x_20290
    2623 | XCHD (x_20293, x_20292) -> h_XCHD x_20293 x_20292
     2590| ADD (x_1122, x_1121) -> h_ADD x_1122 x_1121
     2591| ADDC (x_1124, x_1123) -> h_ADDC x_1124 x_1123
     2592| SUBB (x_1126, x_1125) -> h_SUBB x_1126 x_1125
     2593| INC x_1127 -> h_INC x_1127
     2594| DEC x_1128 -> h_DEC x_1128
     2595| MUL (x_1130, x_1129) -> h_MUL x_1130 x_1129
     2596| DIV (x_1132, x_1131) -> h_DIV x_1132 x_1131
     2597| DA x_1133 -> h_DA x_1133
     2598| JC x_1134 -> h_JC x_1134
     2599| JNC x_1135 -> h_JNC x_1135
     2600| JB (x_1137, x_1136) -> h_JB x_1137 x_1136
     2601| JNB (x_1139, x_1138) -> h_JNB x_1139 x_1138
     2602| JBC (x_1141, x_1140) -> h_JBC x_1141 x_1140
     2603| JZ x_1142 -> h_JZ x_1142
     2604| JNZ x_1143 -> h_JNZ x_1143
     2605| CJNE (x_1145, x_1144) -> h_CJNE x_1145 x_1144
     2606| DJNZ (x_1147, x_1146) -> h_DJNZ x_1147 x_1146
     2607| ANL x_1148 -> h_ANL x_1148
     2608| ORL x_1149 -> h_ORL x_1149
     2609| XRL x_1150 -> h_XRL x_1150
     2610| CLR x_1151 -> h_CLR x_1151
     2611| CPL x_1152 -> h_CPL x_1152
     2612| RL x_1153 -> h_RL x_1153
     2613| RLC x_1154 -> h_RLC x_1154
     2614| RR x_1155 -> h_RR x_1155
     2615| RRC x_1156 -> h_RRC x_1156
     2616| SWAP x_1157 -> h_SWAP x_1157
     2617| MOV x_1158 -> h_MOV x_1158
     2618| MOVX x_1159 -> h_MOVX x_1159
     2619| SETB x_1160 -> h_SETB x_1160
     2620| PUSH x_1161 -> h_PUSH x_1161
     2621| POP x_1162 -> h_POP x_1162
     2622| XCH (x_1164, x_1163) -> h_XCH x_1164 x_1163
     2623| XCHD (x_1166, x_1165) -> h_XCHD x_1166 x_1165
    26242624| RET -> h_RET
    26252625| RETI -> h_RETI
    26262626| NOP -> h_NOP
    2627 | JMP x_20294 -> h_JMP x_20294
     2627| JMP x_1167 -> h_JMP x_1167
    26282628
    26292629(** val preinstruction_rect_Type0 :
     
    26632663    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    26642664let 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
    2665 | ADD (x_20335, x_20334) -> h_ADD x_20335 x_20334
    2666 | ADDC (x_20337, x_20336) -> h_ADDC x_20337 x_20336
    2667 | SUBB (x_20339, x_20338) -> h_SUBB x_20339 x_20338
    2668 | INC x_20340 -> h_INC x_20340
    2669 | DEC x_20341 -> h_DEC x_20341
    2670 | MUL (x_20343, x_20342) -> h_MUL x_20343 x_20342
    2671 | DIV (x_20345, x_20344) -> h_DIV x_20345 x_20344
    2672 | DA x_20346 -> h_DA x_20346
    2673 | JC x_20347 -> h_JC x_20347
    2674 | JNC x_20348 -> h_JNC x_20348
    2675 | JB (x_20350, x_20349) -> h_JB x_20350 x_20349
    2676 | JNB (x_20352, x_20351) -> h_JNB x_20352 x_20351
    2677 | JBC (x_20354, x_20353) -> h_JBC x_20354 x_20353
    2678 | JZ x_20355 -> h_JZ x_20355
    2679 | JNZ x_20356 -> h_JNZ x_20356
    2680 | CJNE (x_20358, x_20357) -> h_CJNE x_20358 x_20357
    2681 | DJNZ (x_20360, x_20359) -> h_DJNZ x_20360 x_20359
    2682 | ANL x_20361 -> h_ANL x_20361
    2683 | ORL x_20362 -> h_ORL x_20362
    2684 | XRL x_20363 -> h_XRL x_20363
    2685 | CLR x_20364 -> h_CLR x_20364
    2686 | CPL x_20365 -> h_CPL x_20365
    2687 | RL x_20366 -> h_RL x_20366
    2688 | RLC x_20367 -> h_RLC x_20367
    2689 | RR x_20368 -> h_RR x_20368
    2690 | RRC x_20369 -> h_RRC x_20369
    2691 | SWAP x_20370 -> h_SWAP x_20370
    2692 | MOV x_20371 -> h_MOV x_20371
    2693 | MOVX x_20372 -> h_MOVX x_20372
    2694 | SETB x_20373 -> h_SETB x_20373
    2695 | PUSH x_20374 -> h_PUSH x_20374
    2696 | POP x_20375 -> h_POP x_20375
    2697 | XCH (x_20377, x_20376) -> h_XCH x_20377 x_20376
    2698 | XCHD (x_20379, x_20378) -> h_XCHD x_20379 x_20378
     2665| ADD (x_1208, x_1207) -> h_ADD x_1208 x_1207
     2666| ADDC (x_1210, x_1209) -> h_ADDC x_1210 x_1209
     2667| SUBB (x_1212, x_1211) -> h_SUBB x_1212 x_1211
     2668| INC x_1213 -> h_INC x_1213
     2669| DEC x_1214 -> h_DEC x_1214
     2670| MUL (x_1216, x_1215) -> h_MUL x_1216 x_1215
     2671| DIV (x_1218, x_1217) -> h_DIV x_1218 x_1217
     2672| DA x_1219 -> h_DA x_1219
     2673| JC x_1220 -> h_JC x_1220
     2674| JNC x_1221 -> h_JNC x_1221
     2675| JB (x_1223, x_1222) -> h_JB x_1223 x_1222
     2676| JNB (x_1225, x_1224) -> h_JNB x_1225 x_1224
     2677| JBC (x_1227, x_1226) -> h_JBC x_1227 x_1226
     2678| JZ x_1228 -> h_JZ x_1228
     2679| JNZ x_1229 -> h_JNZ x_1229
     2680| CJNE (x_1231, x_1230) -> h_CJNE x_1231 x_1230
     2681| DJNZ (x_1233, x_1232) -> h_DJNZ x_1233 x_1232
     2682| ANL x_1234 -> h_ANL x_1234
     2683| ORL x_1235 -> h_ORL x_1235
     2684| XRL x_1236 -> h_XRL x_1236
     2685| CLR x_1237 -> h_CLR x_1237
     2686| CPL x_1238 -> h_CPL x_1238
     2687| RL x_1239 -> h_RL x_1239
     2688| RLC x_1240 -> h_RLC x_1240
     2689| RR x_1241 -> h_RR x_1241
     2690| RRC x_1242 -> h_RRC x_1242
     2691| SWAP x_1243 -> h_SWAP x_1243
     2692| MOV x_1244 -> h_MOV x_1244
     2693| MOVX x_1245 -> h_MOVX x_1245
     2694| SETB x_1246 -> h_SETB x_1246
     2695| PUSH x_1247 -> h_PUSH x_1247
     2696| POP x_1248 -> h_POP x_1248
     2697| XCH (x_1250, x_1249) -> h_XCH x_1250 x_1249
     2698| XCHD (x_1252, x_1251) -> h_XCHD x_1252 x_1251
    26992699| RET -> h_RET
    27002700| RETI -> h_RETI
    27012701| NOP -> h_NOP
    2702 | JMP x_20380 -> h_JMP x_20380
     2702| JMP x_1253 -> h_JMP x_1253
    27032703
    27042704(** val preinstruction_inv_rect_Type4 :
     
    51045104    'a1 **)
    51055105let rec instruction_rect_Type4 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    5106 | ACALL x_20952 -> h_ACALL x_20952
    5107 | LCALL x_20953 -> h_LCALL x_20953
    5108 | AJMP x_20954 -> h_AJMP x_20954
    5109 | LJMP x_20955 -> h_LJMP x_20955
    5110 | SJMP x_20956 -> h_SJMP x_20956
    5111 | MOVC (x_20958, x_20957) -> h_MOVC x_20958 x_20957
    5112 | RealInstruction x_20959 -> h_RealInstruction x_20959
     5106| ACALL x_1825 -> h_ACALL x_1825
     5107| LCALL x_1826 -> h_LCALL x_1826
     5108| AJMP x_1827 -> h_AJMP x_1827
     5109| LJMP x_1828 -> h_LJMP x_1828
     5110| SJMP x_1829 -> h_SJMP x_1829
     5111| MOVC (x_1831, x_1830) -> h_MOVC x_1831 x_1830
     5112| RealInstruction x_1832 -> h_RealInstruction x_1832
    51135113
    51145114(** val instruction_rect_Type5 :
     
    51195119    'a1 **)
    51205120let rec instruction_rect_Type5 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    5121 | ACALL x_20968 -> h_ACALL x_20968
    5122 | LCALL x_20969 -> h_LCALL x_20969
    5123 | AJMP x_20970 -> h_AJMP x_20970
    5124 | LJMP x_20971 -> h_LJMP x_20971
    5125 | SJMP x_20972 -> h_SJMP x_20972
    5126 | MOVC (x_20974, x_20973) -> h_MOVC x_20974 x_20973
    5127 | RealInstruction x_20975 -> h_RealInstruction x_20975
     5121| ACALL x_1841 -> h_ACALL x_1841
     5122| LCALL x_1842 -> h_LCALL x_1842
     5123| AJMP x_1843 -> h_AJMP x_1843
     5124| LJMP x_1844 -> h_LJMP x_1844
     5125| SJMP x_1845 -> h_SJMP x_1845
     5126| MOVC (x_1847, x_1846) -> h_MOVC x_1847 x_1846
     5127| RealInstruction x_1848 -> h_RealInstruction x_1848
    51285128
    51295129(** val instruction_rect_Type3 :
     
    51345134    'a1 **)
    51355135let rec instruction_rect_Type3 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    5136 | ACALL x_20984 -> h_ACALL x_20984
    5137 | LCALL x_20985 -> h_LCALL x_20985
    5138 | AJMP x_20986 -> h_AJMP x_20986
    5139 | LJMP x_20987 -> h_LJMP x_20987
    5140 | SJMP x_20988 -> h_SJMP x_20988
    5141 | MOVC (x_20990, x_20989) -> h_MOVC x_20990 x_20989
    5142 | RealInstruction x_20991 -> h_RealInstruction x_20991
     5136| ACALL x_1857 -> h_ACALL x_1857
     5137| LCALL x_1858 -> h_LCALL x_1858
     5138| AJMP x_1859 -> h_AJMP x_1859
     5139| LJMP x_1860 -> h_LJMP x_1860
     5140| SJMP x_1861 -> h_SJMP x_1861
     5141| MOVC (x_1863, x_1862) -> h_MOVC x_1863 x_1862
     5142| RealInstruction x_1864 -> h_RealInstruction x_1864
    51435143
    51445144(** val instruction_rect_Type2 :
     
    51495149    'a1 **)
    51505150let rec instruction_rect_Type2 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    5151 | ACALL x_21000 -> h_ACALL x_21000
    5152 | LCALL x_21001 -> h_LCALL x_21001
    5153 | AJMP x_21002 -> h_AJMP x_21002
    5154 | LJMP x_21003 -> h_LJMP x_21003
    5155 | SJMP x_21004 -> h_SJMP x_21004
    5156 | MOVC (x_21006, x_21005) -> h_MOVC x_21006 x_21005
    5157 | RealInstruction x_21007 -> h_RealInstruction x_21007
     5151| ACALL x_1873 -> h_ACALL x_1873
     5152| LCALL x_1874 -> h_LCALL x_1874
     5153| AJMP x_1875 -> h_AJMP x_1875
     5154| LJMP x_1876 -> h_LJMP x_1876
     5155| SJMP x_1877 -> h_SJMP x_1877
     5156| MOVC (x_1879, x_1878) -> h_MOVC x_1879 x_1878
     5157| RealInstruction x_1880 -> h_RealInstruction x_1880
    51585158
    51595159(** val instruction_rect_Type1 :
     
    51645164    'a1 **)
    51655165let rec instruction_rect_Type1 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    5166 | ACALL x_21016 -> h_ACALL x_21016
    5167 | LCALL x_21017 -> h_LCALL x_21017
    5168 | AJMP x_21018 -> h_AJMP x_21018
    5169 | LJMP x_21019 -> h_LJMP x_21019
    5170 | SJMP x_21020 -> h_SJMP x_21020
    5171 | MOVC (x_21022, x_21021) -> h_MOVC x_21022 x_21021
    5172 | RealInstruction x_21023 -> h_RealInstruction x_21023
     5166| ACALL x_1889 -> h_ACALL x_1889
     5167| LCALL x_1890 -> h_LCALL x_1890
     5168| AJMP x_1891 -> h_AJMP x_1891
     5169| LJMP x_1892 -> h_LJMP x_1892
     5170| SJMP x_1893 -> h_SJMP x_1893
     5171| MOVC (x_1895, x_1894) -> h_MOVC x_1895 x_1894
     5172| RealInstruction x_1896 -> h_RealInstruction x_1896
    51735173
    51745174(** val instruction_rect_Type0 :
     
    51795179    'a1 **)
    51805180let rec instruction_rect_Type0 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    5181 | ACALL x_21032 -> h_ACALL x_21032
    5182 | LCALL x_21033 -> h_LCALL x_21033
    5183 | AJMP x_21034 -> h_AJMP x_21034
    5184 | LJMP x_21035 -> h_LJMP x_21035
    5185 | SJMP x_21036 -> h_SJMP x_21036
    5186 | MOVC (x_21038, x_21037) -> h_MOVC x_21038 x_21037
    5187 | RealInstruction x_21039 -> h_RealInstruction x_21039
     5181| ACALL x_1905 -> h_ACALL x_1905
     5182| LCALL x_1906 -> h_LCALL x_1906
     5183| AJMP x_1907 -> h_AJMP x_1907
     5184| LJMP x_1908 -> h_LJMP x_1908
     5185| SJMP x_1909 -> h_SJMP x_1909
     5186| MOVC (x_1911, x_1910) -> h_MOVC x_1911 x_1910
     5187| RealInstruction x_1912 -> h_RealInstruction x_1912
    51885188
    51895189(** val instruction_inv_rect_Type4 :
     
    54765476    -> 'a1 **)
    54775477let rec pseudo_instruction_rect_Type4 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function
    5478 | Instruction x_21202 -> h_Instruction x_21202
    5479 | Comment x_21203 -> h_Comment x_21203
    5480 | Cost x_21204 -> h_Cost x_21204
    5481 | Jmp x_21205 -> h_Jmp x_21205
    5482 | Jnz (x_21208, x_21207, x_21206) -> h_Jnz x_21208 x_21207 x_21206
    5483 | Call x_21209 -> h_Call x_21209
    5484 | Mov (x_21212, x_21211, x_21210) -> h_Mov x_21212 x_21211 x_21210
     5478| Instruction x_2075 -> h_Instruction x_2075
     5479| Comment x_2076 -> h_Comment x_2076
     5480| Cost x_2077 -> h_Cost x_2077
     5481| Jmp x_2078 -> h_Jmp x_2078
     5482| Jnz (x_2081, x_2080, x_2079) -> h_Jnz x_2081 x_2080 x_2079
     5483| Call x_2082 -> h_Call x_2082
     5484| Mov (x_2085, x_2084, x_2083) -> h_Mov x_2085 x_2084 x_2083
    54855485
    54865486(** val pseudo_instruction_rect_Type5 :
     
    54925492    -> 'a1 **)
    54935493let rec pseudo_instruction_rect_Type5 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function
    5494 | Instruction x_21221 -> h_Instruction x_21221
    5495 | Comment x_21222 -> h_Comment x_21222
    5496 | Cost x_21223 -> h_Cost x_21223
    5497 | Jmp x_21224 -> h_Jmp x_21224
    5498 | Jnz (x_21227, x_21226, x_21225) -> h_Jnz x_21227 x_21226 x_21225
    5499 | Call x_21228 -> h_Call x_21228
    5500 | Mov (x_21231, x_21230, x_21229) -> h_Mov x_21231 x_21230 x_21229
     5494| Instruction x_2094 -> h_Instruction x_2094
     5495| Comment x_2095 -> h_Comment x_2095
     5496| Cost x_2096 -> h_Cost x_2096
     5497| Jmp x_2097 -> h_Jmp x_2097
     5498| Jnz (x_2100, x_2099, x_2098) -> h_Jnz x_2100 x_2099 x_2098
     5499| Call x_2101 -> h_Call x_2101
     5500| Mov (x_2104, x_2103, x_2102) -> h_Mov x_2104 x_2103 x_2102
    55015501
    55025502(** val pseudo_instruction_rect_Type3 :
     
    55085508    -> 'a1 **)
    55095509let rec pseudo_instruction_rect_Type3 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function
    5510 | Instruction x_21240 -> h_Instruction x_21240
    5511 | Comment x_21241 -> h_Comment x_21241
    5512 | Cost x_21242 -> h_Cost x_21242
    5513 | Jmp x_21243 -> h_Jmp x_21243
    5514 | Jnz (x_21246, x_21245, x_21244) -> h_Jnz x_21246 x_21245 x_21244
    5515 | Call x_21247 -> h_Call x_21247
    5516 | Mov (x_21250, x_21249, x_21248) -> h_Mov x_21250 x_21249 x_21248
     5510| Instruction x_2113 -> h_Instruction x_2113
     5511| Comment x_2114 -> h_Comment x_2114
     5512| Cost x_2115 -> h_Cost x_2115
     5513| Jmp x_2116 -> h_Jmp x_2116
     5514| Jnz (x_2119, x_2118, x_2117) -> h_Jnz x_2119 x_2118 x_2117
     5515| Call x_2120 -> h_Call x_2120
     5516| Mov (x_2123, x_2122, x_2121) -> h_Mov x_2123 x_2122 x_2121
    55175517
    55185518(** val pseudo_instruction_rect_Type2 :
     
    55245524    -> 'a1 **)
    55255525let rec pseudo_instruction_rect_Type2 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function
    5526 | Instruction x_21259 -> h_Instruction x_21259
    5527 | Comment x_21260 -> h_Comment x_21260
    5528 | Cost x_21261 -> h_Cost x_21261
    5529 | Jmp x_21262 -> h_Jmp x_21262
    5530 | Jnz (x_21265, x_21264, x_21263) -> h_Jnz x_21265 x_21264 x_21263
    5531 | Call x_21266 -> h_Call x_21266
    5532 | Mov (x_21269, x_21268, x_21267) -> h_Mov x_21269 x_21268 x_21267
     5526| Instruction x_2132 -> h_Instruction x_2132
     5527| Comment x_2133 -> h_Comment x_2133
     5528| Cost x_2134 -> h_Cost x_2134
     5529| Jmp x_2135 -> h_Jmp x_2135
     5530| Jnz (x_2138, x_2137, x_2136) -> h_Jnz x_2138 x_2137 x_2136
     5531| Call x_2139 -> h_Call x_2139
     5532| Mov (x_2142, x_2141, x_2140) -> h_Mov x_2142 x_2141 x_2140
    55335533
    55345534(** val pseudo_instruction_rect_Type1 :
     
    55405540    -> 'a1 **)
    55415541let rec pseudo_instruction_rect_Type1 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function
    5542 | Instruction x_21278 -> h_Instruction x_21278
    5543 | Comment x_21279 -> h_Comment x_21279
    5544 | Cost x_21280 -> h_Cost x_21280
    5545 | Jmp x_21281 -> h_Jmp x_21281
    5546 | Jnz (x_21284, x_21283, x_21282) -> h_Jnz x_21284 x_21283 x_21282
    5547 | Call x_21285 -> h_Call x_21285
    5548 | Mov (x_21288, x_21287, x_21286) -> h_Mov x_21288 x_21287 x_21286
     5542| Instruction x_2151 -> h_Instruction x_2151
     5543| Comment x_2152 -> h_Comment x_2152
     5544| Cost x_2153 -> h_Cost x_2153
     5545| Jmp x_2154 -> h_Jmp x_2154
     5546| Jnz (x_2157, x_2156, x_2155) -> h_Jnz x_2157 x_2156 x_2155
     5547| Call x_2158 -> h_Call x_2158
     5548| Mov (x_2161, x_2160, x_2159) -> h_Mov x_2161 x_2160 x_2159
    55495549
    55505550(** val pseudo_instruction_rect_Type0 :
     
    55565556    -> 'a1 **)
    55575557let rec pseudo_instruction_rect_Type0 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function
    5558 | Instruction x_21297 -> h_Instruction x_21297
    5559 | Comment x_21298 -> h_Comment x_21298
    5560 | Cost x_21299 -> h_Cost x_21299
    5561 | Jmp x_21300 -> h_Jmp x_21300
    5562 | Jnz (x_21303, x_21302, x_21301) -> h_Jnz x_21303 x_21302 x_21301
    5563 | Call x_21304 -> h_Call x_21304
    5564 | Mov (x_21307, x_21306, x_21305) -> h_Mov x_21307 x_21306 x_21305
     5558| Instruction x_2170 -> h_Instruction x_2170
     5559| Comment x_2171 -> h_Comment x_2171
     5560| Cost x_2172 -> h_Cost x_2172
     5561| Jmp x_2173 -> h_Jmp x_2173
     5562| Jnz (x_2176, x_2175, x_2174) -> h_Jnz x_2176 x_2175 x_2174
     5563| Call x_2177 -> h_Call x_2177
     5564| Mov (x_2180, x_2179, x_2178) -> h_Mov x_2180 x_2179 x_2178
    55655565
    55665566(** val pseudo_instruction_inv_rect_Type4 :
     
    57785778    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
    57795779    pseudo_assembly_program -> 'a1 **)
    5780 let rec pseudo_assembly_program_rect_Type4 h_mk_pseudo_assembly_program x_21431 =
     5780let rec pseudo_assembly_program_rect_Type4 h_mk_pseudo_assembly_program x_2304 =
    57815781  let { preamble = preamble0; code = code0; renamed_symbols =
    5782     renamed_symbols0; final_label = final_label0 } = x_21431
     5782    renamed_symbols0; final_label = final_label0 } = x_2304
    57835783  in
    57845784  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     
    57905790    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
    57915791    pseudo_assembly_program -> 'a1 **)
    5792 let rec pseudo_assembly_program_rect_Type5 h_mk_pseudo_assembly_program x_21433 =
     5792let rec pseudo_assembly_program_rect_Type5 h_mk_pseudo_assembly_program x_2306 =
    57935793  let { preamble = preamble0; code = code0; renamed_symbols =
    5794     renamed_symbols0; final_label = final_label0 } = x_21433
     5794    renamed_symbols0; final_label = final_label0 } = x_2306
    57955795  in
    57965796  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     
    58025802    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
    58035803    pseudo_assembly_program -> 'a1 **)
    5804 let rec pseudo_assembly_program_rect_Type3 h_mk_pseudo_assembly_program x_21435 =
     5804let rec pseudo_assembly_program_rect_Type3 h_mk_pseudo_assembly_program x_2308 =
    58055805  let { preamble = preamble0; code = code0; renamed_symbols =
    5806     renamed_symbols0; final_label = final_label0 } = x_21435
     5806    renamed_symbols0; final_label = final_label0 } = x_2308
    58075807  in
    58085808  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     
    58145814    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
    58155815    pseudo_assembly_program -> 'a1 **)
    5816 let rec pseudo_assembly_program_rect_Type2 h_mk_pseudo_assembly_program x_21437 =
     5816let rec pseudo_assembly_program_rect_Type2 h_mk_pseudo_assembly_program x_2310 =
    58175817  let { preamble = preamble0; code = code0; renamed_symbols =
    5818     renamed_symbols0; final_label = final_label0 } = x_21437
     5818    renamed_symbols0; final_label = final_label0 } = x_2310
    58195819  in
    58205820  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     
    58265826    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
    58275827    pseudo_assembly_program -> 'a1 **)
    5828 let rec pseudo_assembly_program_rect_Type1 h_mk_pseudo_assembly_program x_21439 =
     5828let rec pseudo_assembly_program_rect_Type1 h_mk_pseudo_assembly_program x_2312 =
    58295829  let { preamble = preamble0; code = code0; renamed_symbols =
    5830     renamed_symbols0; final_label = final_label0 } = x_21439
     5830    renamed_symbols0; final_label = final_label0 } = x_2312
    58315831  in
    58325832  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     
    58385838    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
    58395839    pseudo_assembly_program -> 'a1 **)
    5840 let rec pseudo_assembly_program_rect_Type0 h_mk_pseudo_assembly_program x_21441 =
     5840let rec pseudo_assembly_program_rect_Type0 h_mk_pseudo_assembly_program x_2314 =
    58415841  let { preamble = preamble0; code = code0; renamed_symbols =
    5842     renamed_symbols0; final_label = final_label0 } = x_21441
     5842    renamed_symbols0; final_label = final_label0 } = x_2314
    58435843  in
    58445844  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     
    59375937  (Types.pi1
    59385938    (FoldStuff.foldl_strong program (fun prefix v tl _ i_mem ->
    5939       (let { Types.fst = i; Types.snd = mem } = Types.pi1 i_mem in
    5940       (fun _ -> { Types.fst = (Nat.S i); Types.snd =
     5939      (let { Types.fst = eta24568; Types.snd = mem } = Types.pi1 i_mem in
     5940      (fun _ ->
     5941      (let { Types.fst = i; Types.snd = bvi } = eta24568 in
     5942      (fun _ -> { Types.fst = { Types.fst = (Nat.S i); Types.snd =
     5943      (Arithmetic.increment (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5944        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5945        Nat.O)))))))))))))))) bvi) }; Types.snd =
    59415946      (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    59425947        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    5943         Nat.O))))))))))))))))
    5944         (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    5945           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    5946           (Nat.S (Nat.S Nat.O)))))))))))))))) i) v mem) })) __) { Types.fst =
    5947       Nat.O; Types.snd = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S
     5948        Nat.O)))))))))))))))) bvi v mem) })) __)) __) { Types.fst =
     5949      { Types.fst = Nat.O; Types.snd =
     5950      (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5951        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5952        Nat.O))))))))))))))))) }; Types.snd = (BitVectorTrie.Stub (Nat.S
    59485953      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    5949       (Nat.S (Nat.S Nat.O))))))))))))))))) })).Types.snd
     5954      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))) })).Types.snd
    59505955
    59515956(** val load_code_memory :
     
    59685973    costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
    59695974    labelled_object_code -> 'a1 **)
    5970 let rec labelled_object_code_rect_Type4 h_mk_labelled_object_code x_21457 =
     5975let rec labelled_object_code_rect_Type4 h_mk_labelled_object_code x_2330 =
    59715976  let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
    5972     symboltable0; final_pc = final_pc0 } = x_21457
     5977    symboltable0; final_pc = final_pc0 } = x_2330
    59735978  in
    59745979  h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __
     
    59785983    costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
    59795984    labelled_object_code -> 'a1 **)
    5980 let rec labelled_object_code_rect_Type5 h_mk_labelled_object_code x_21459 =
     5985let rec labelled_object_code_rect_Type5 h_mk_labelled_object_code x_2332 =
    59815986  let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
    5982     symboltable0; final_pc = final_pc0 } = x_21459
     5987    symboltable0; final_pc = final_pc0 } = x_2332
    59835988  in
    59845989  h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __
     
    59885993    costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
    59895994    labelled_object_code -> 'a1 **)
    5990 let rec labelled_object_code_rect_Type3 h_mk_labelled_object_code x_21461 =
     5995let rec labelled_object_code_rect_Type3 h_mk_labelled_object_code x_2334 =
    59915996  let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
    5992     symboltable0; final_pc = final_pc0 } = x_21461
     5997    symboltable0; final_pc = final_pc0 } = x_2334
    59935998  in
    59945999  h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __
     
    59986003    costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
    59996004    labelled_object_code -> 'a1 **)
    6000 let rec labelled_object_code_rect_Type2 h_mk_labelled_object_code x_21463 =
     6005let rec labelled_object_code_rect_Type2 h_mk_labelled_object_code x_2336 =
    60016006  let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
    6002     symboltable0; final_pc = final_pc0 } = x_21463
     6007    symboltable0; final_pc = final_pc0 } = x_2336
    60036008  in
    60046009  h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __
     
    60086013    costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
    60096014    labelled_object_code -> 'a1 **)
    6010 let rec labelled_object_code_rect_Type1 h_mk_labelled_object_code x_21465 =
     6015let rec labelled_object_code_rect_Type1 h_mk_labelled_object_code x_2338 =
    60116016  let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
    6012     symboltable0; final_pc = final_pc0 } = x_21465
     6017    symboltable0; final_pc = final_pc0 } = x_2338
    60136018  in
    60146019  h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __
     
    60186023    costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
    60196024    labelled_object_code -> 'a1 **)
    6020 let rec labelled_object_code_rect_Type0 h_mk_labelled_object_code x_21467 =
     6025let rec labelled_object_code_rect_Type0 h_mk_labelled_object_code x_2340 =
    60216026  let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
    6022     symboltable0; final_pc = final_pc0 } = x_21467
     6027    symboltable0; final_pc = final_pc0 } = x_2340
    60236028  in
    60246029  h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __
  • src/ASM/ASM.ma

    r3082 r3104  
    11771177  (foldl_strong ?
    11781178   (λprefix.
    1179      Σres: nat × (BitVectorTrie Byte 16).
    1180       let 〈i,mem〉 ≝ res in
    1181       i = |prefix| ∧
     1179     Σres: nat × Word × (BitVectorTrie Byte 16).
     1180      let 〈i,bvi,mem〉 ≝ res in
     1181      i = |prefix| ∧ bvi = bitvector_of_nat … i ∧
    11821182      (i ≤ 2^16 →
    11831183        ∀pc. ∀pc_ok: pc < |prefix|.
     
    11851185   program
    11861186   (λprefix,v,tl,prf,i_mem.
    1187      let 〈i,mem〉 ≝ i_mem in
    1188       〈S i,insert … (bitvector_of_nat … i) v mem〉)
    1189   〈0,Stub Byte 16〉).
    1190 [3: cases (foldl_strong ? (λprefix.Σres.?) ???) * #i #mem * #H1 >H1 #H2 @H2
    1191 | % // #_ #pc #abs @⊥ @(absurd … abs (not_le_Sn_O …))
    1192 | cases i_mem in p; * #i' #mem' #H #EQ destruct(EQ) cases H -H #H1 #H2 %
    1193   [ >length_append >H1 normalize //
     1187     let 〈i,bvi,mem〉 ≝ i_mem in
     1188      〈S i,increment … bvi,insert … bvi v mem〉)
     1189  〈0,zero ?,Stub Byte 16〉).
     1190[3: cases (foldl_strong ? (λprefix.Σres.?) ???) ** #i #bvi #mem ** #H1 #H3 >H1 #H2 @H2
     1191| % // % // (*#_ #pc #abs @⊥ @(absurd … abs (not_le_Sn_O …))*)
     1192| cases i_mem in p; ** #i' #bvi' #mem' normalize nodelta #H #EQ destruct(EQ)
     1193  cases H -H * #H1 #H3 #H2 destruct (p1) %
     1194  [ % [ >length_append >H1 normalize //
     1195      | >increment_zero_bitvector_of_nat_1 >H3 <add_bitvector_of_nat % ]
    11941196  | #LE #pc #pc_ok
    11951197    cases (le_to_or_lt_eq … pc_ok)
     
    11981200      #pc_ok <nth_safe_prepend [2: //] whd in ⊢ (??%?);
    11991201      <H1 <plus_n_O whd in ⊢ (???%); //
    1200     | >length_append <plus_n_Sm <plus_n_O #LT <shift_nth_prefix [2: /2/]
     1202    | >length_append <plus_n_Sm <plus_n_O #LT <shift_nth_prefix
     1203      [2: /2 by lt_plus_to_lt_l/]
    12011204      >H2 [2: @(transitive_le … LE) //]
    12021205      cut (pc ≠ i) [ >H1 @lt_to_not_eq @lt_S_S_to_lt //] #NEQ
    1203       whd in ⊢ (??%%); @sym_eq @lookup_insert_miss >eq_bv_false %
     1206      whd in ⊢ (??%%); @sym_eq @lookup_insert_miss >eq_bv_false % >H3
    12041207      #EQ @(absurd ?? NEQ) @(eq_bitvector_of_nat_to_eq … EQ) try assumption
    12051208      @(transitive_lt … LE) >H1 @lt_S_S_to_lt //]]
  • src/ASM/Assembly.ma

    r3076 r3104  
    855855       let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in
    856856       let lookup_datalabels ≝ λx.
    857          match lookup ASMTag … (construct_datalabels preamble) x with
     857         match lookup ASMTag … datalabels x with
    858858         [ Some addr ⇒ 〈XData, addr〉
    859859         | None ⇒ 〈Code, lookup_labels x〉
Note: See TracChangeset for help on using the changeset viewer.