Changeset 2951 for extracted/aSM.ml


Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (7 years ago)
Author:
sacerdot
Message:

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/aSM.ml

    r2873 r2951  
    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_22221 -> h_DIRECT x_22221
    116 | INDIRECT x_22222 -> h_INDIRECT x_22222
    117 | EXT_INDIRECT x_22223 -> h_EXT_INDIRECT x_22223
    118 | REGISTER x_22224 -> h_REGISTER x_22224
     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_22225 -> h_DATA x_22225
    123 | DATA16 x_22226 -> h_DATA16 x_22226
     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_22227 -> h_BIT_ADDR x_22227
    130 | N_BIT_ADDR x_22228 -> h_N_BIT_ADDR x_22228
    131 | RELATIVE x_22229 -> h_RELATIVE x_22229
    132 | ADDR11 x_22230 -> h_ADDR11 x_22230
    133 | ADDR16 x_22231 -> h_ADDR16 x_22231
     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_22252 -> h_DIRECT x_22252
    144 | INDIRECT x_22253 -> h_INDIRECT x_22253
    145 | EXT_INDIRECT x_22254 -> h_EXT_INDIRECT x_22254
    146 | REGISTER x_22255 -> h_REGISTER x_22255
     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_22256 -> h_DATA x_22256
    151 | DATA16 x_22257 -> h_DATA16 x_22257
     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_22258 -> h_BIT_ADDR x_22258
    158 | N_BIT_ADDR x_22259 -> h_N_BIT_ADDR x_22259
    159 | RELATIVE x_22260 -> h_RELATIVE x_22260
    160 | ADDR11 x_22261 -> h_ADDR11 x_22261
    161 | ADDR16 x_22262 -> h_ADDR16 x_22262
     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_22283 -> h_DIRECT x_22283
    172 | INDIRECT x_22284 -> h_INDIRECT x_22284
    173 | EXT_INDIRECT x_22285 -> h_EXT_INDIRECT x_22285
    174 | REGISTER x_22286 -> h_REGISTER x_22286
     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_22287 -> h_DATA x_22287
    179 | DATA16 x_22288 -> h_DATA16 x_22288
     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_22289 -> h_BIT_ADDR x_22289
    186 | N_BIT_ADDR x_22290 -> h_N_BIT_ADDR x_22290
    187 | RELATIVE x_22291 -> h_RELATIVE x_22291
    188 | ADDR11 x_22292 -> h_ADDR11 x_22292
    189 | ADDR16 x_22293 -> h_ADDR16 x_22293
     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_22314 -> h_DIRECT x_22314
    200 | INDIRECT x_22315 -> h_INDIRECT x_22315
    201 | EXT_INDIRECT x_22316 -> h_EXT_INDIRECT x_22316
    202 | REGISTER x_22317 -> h_REGISTER x_22317
     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_22318 -> h_DATA x_22318
    207 | DATA16 x_22319 -> h_DATA16 x_22319
     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_22320 -> h_BIT_ADDR x_22320
    214 | N_BIT_ADDR x_22321 -> h_N_BIT_ADDR x_22321
    215 | RELATIVE x_22322 -> h_RELATIVE x_22322
    216 | ADDR11 x_22323 -> h_ADDR11 x_22323
    217 | ADDR16 x_22324 -> h_ADDR16 x_22324
     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_22345 -> h_DIRECT x_22345
    228 | INDIRECT x_22346 -> h_INDIRECT x_22346
    229 | EXT_INDIRECT x_22347 -> h_EXT_INDIRECT x_22347
    230 | REGISTER x_22348 -> h_REGISTER x_22348
     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_22349 -> h_DATA x_22349
    235 | DATA16 x_22350 -> h_DATA16 x_22350
     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_22351 -> h_BIT_ADDR x_22351
    242 | N_BIT_ADDR x_22352 -> h_N_BIT_ADDR x_22352
    243 | RELATIVE x_22353 -> h_RELATIVE x_22353
    244 | ADDR11 x_22354 -> h_ADDR11 x_22354
    245 | ADDR16 x_22355 -> h_ADDR16 x_22355
     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_22376 -> h_DIRECT x_22376
    256 | INDIRECT x_22377 -> h_INDIRECT x_22377
    257 | EXT_INDIRECT x_22378 -> h_EXT_INDIRECT x_22378
    258 | REGISTER x_22379 -> h_REGISTER x_22379
     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_22380 -> h_DATA x_22380
    263 | DATA16 x_22381 -> h_DATA16 x_22381
     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_22382 -> h_BIT_ADDR x_22382
    270 | N_BIT_ADDR x_22383 -> h_N_BIT_ADDR x_22383
    271 | RELATIVE x_22384 -> h_RELATIVE x_22384
    272 | ADDR11 x_22385 -> h_ADDR11 x_22385
    273 | ADDR16 x_22386 -> h_ADDR16 x_22386
     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_22854 =
    1929   let subaddressing_modeel = x_22854 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_22856 =
    1936   let subaddressing_modeel = x_22856 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_22858 =
    1943   let subaddressing_modeel = x_22858 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_22860 =
    1950   let subaddressing_modeel = x_22860 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_22862 =
    1957   let subaddressing_modeel = x_22862 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_22864 =
    1964   let subaddressing_modeel = x_22864 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_22966, x_22965) -> h_ADD x_22966 x_22965
    2291 | ADDC (x_22968, x_22967) -> h_ADDC x_22968 x_22967
    2292 | SUBB (x_22970, x_22969) -> h_SUBB x_22970 x_22969
    2293 | INC x_22971 -> h_INC x_22971
    2294 | DEC x_22972 -> h_DEC x_22972
    2295 | MUL (x_22974, x_22973) -> h_MUL x_22974 x_22973
    2296 | DIV (x_22976, x_22975) -> h_DIV x_22976 x_22975
    2297 | DA x_22977 -> h_DA x_22977
    2298 | JC x_22978 -> h_JC x_22978
    2299 | JNC x_22979 -> h_JNC x_22979
    2300 | JB (x_22981, x_22980) -> h_JB x_22981 x_22980
    2301 | JNB (x_22983, x_22982) -> h_JNB x_22983 x_22982
    2302 | JBC (x_22985, x_22984) -> h_JBC x_22985 x_22984
    2303 | JZ x_22986 -> h_JZ x_22986
    2304 | JNZ x_22987 -> h_JNZ x_22987
    2305 | CJNE (x_22989, x_22988) -> h_CJNE x_22989 x_22988
    2306 | DJNZ (x_22991, x_22990) -> h_DJNZ x_22991 x_22990
    2307 | ANL x_22992 -> h_ANL x_22992
    2308 | ORL x_22993 -> h_ORL x_22993
    2309 | XRL x_22994 -> h_XRL x_22994
    2310 | CLR x_22995 -> h_CLR x_22995
    2311 | CPL x_22996 -> h_CPL x_22996
    2312 | RL x_22997 -> h_RL x_22997
    2313 | RLC x_22998 -> h_RLC x_22998
    2314 | RR x_22999 -> h_RR x_22999
    2315 | RRC x_23000 -> h_RRC x_23000
    2316 | SWAP x_23001 -> h_SWAP x_23001
    2317 | MOV x_23002 -> h_MOV x_23002
    2318 | MOVX x_23003 -> h_MOVX x_23003
    2319 | SETB x_23004 -> h_SETB x_23004
    2320 | PUSH x_23005 -> h_PUSH x_23005
    2321 | POP x_23006 -> h_POP x_23006
    2322 | XCH (x_23008, x_23007) -> h_XCH x_23008 x_23007
    2323 | XCHD (x_23010, x_23009) -> h_XCHD x_23010 x_23009
     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_23011 -> h_JMP x_23011
     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_23052, x_23051) -> h_ADD x_23052 x_23051
    2366 | ADDC (x_23054, x_23053) -> h_ADDC x_23054 x_23053
    2367 | SUBB (x_23056, x_23055) -> h_SUBB x_23056 x_23055
    2368 | INC x_23057 -> h_INC x_23057
    2369 | DEC x_23058 -> h_DEC x_23058
    2370 | MUL (x_23060, x_23059) -> h_MUL x_23060 x_23059
    2371 | DIV (x_23062, x_23061) -> h_DIV x_23062 x_23061
    2372 | DA x_23063 -> h_DA x_23063
    2373 | JC x_23064 -> h_JC x_23064
    2374 | JNC x_23065 -> h_JNC x_23065
    2375 | JB (x_23067, x_23066) -> h_JB x_23067 x_23066
    2376 | JNB (x_23069, x_23068) -> h_JNB x_23069 x_23068
    2377 | JBC (x_23071, x_23070) -> h_JBC x_23071 x_23070
    2378 | JZ x_23072 -> h_JZ x_23072
    2379 | JNZ x_23073 -> h_JNZ x_23073
    2380 | CJNE (x_23075, x_23074) -> h_CJNE x_23075 x_23074
    2381 | DJNZ (x_23077, x_23076) -> h_DJNZ x_23077 x_23076
    2382 | ANL x_23078 -> h_ANL x_23078
    2383 | ORL x_23079 -> h_ORL x_23079
    2384 | XRL x_23080 -> h_XRL x_23080
    2385 | CLR x_23081 -> h_CLR x_23081
    2386 | CPL x_23082 -> h_CPL x_23082
    2387 | RL x_23083 -> h_RL x_23083
    2388 | RLC x_23084 -> h_RLC x_23084
    2389 | RR x_23085 -> h_RR x_23085
    2390 | RRC x_23086 -> h_RRC x_23086
    2391 | SWAP x_23087 -> h_SWAP x_23087
    2392 | MOV x_23088 -> h_MOV x_23088
    2393 | MOVX x_23089 -> h_MOVX x_23089
    2394 | SETB x_23090 -> h_SETB x_23090
    2395 | PUSH x_23091 -> h_PUSH x_23091
    2396 | POP x_23092 -> h_POP x_23092
    2397 | XCH (x_23094, x_23093) -> h_XCH x_23094 x_23093
    2398 | XCHD (x_23096, x_23095) -> h_XCHD x_23096 x_23095
     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_23097 -> h_JMP x_23097
     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_23138, x_23137) -> h_ADD x_23138 x_23137
    2441 | ADDC (x_23140, x_23139) -> h_ADDC x_23140 x_23139
    2442 | SUBB (x_23142, x_23141) -> h_SUBB x_23142 x_23141
    2443 | INC x_23143 -> h_INC x_23143
    2444 | DEC x_23144 -> h_DEC x_23144
    2445 | MUL (x_23146, x_23145) -> h_MUL x_23146 x_23145
    2446 | DIV (x_23148, x_23147) -> h_DIV x_23148 x_23147
    2447 | DA x_23149 -> h_DA x_23149
    2448 | JC x_23150 -> h_JC x_23150
    2449 | JNC x_23151 -> h_JNC x_23151
    2450 | JB (x_23153, x_23152) -> h_JB x_23153 x_23152
    2451 | JNB (x_23155, x_23154) -> h_JNB x_23155 x_23154
    2452 | JBC (x_23157, x_23156) -> h_JBC x_23157 x_23156
    2453 | JZ x_23158 -> h_JZ x_23158
    2454 | JNZ x_23159 -> h_JNZ x_23159
    2455 | CJNE (x_23161, x_23160) -> h_CJNE x_23161 x_23160
    2456 | DJNZ (x_23163, x_23162) -> h_DJNZ x_23163 x_23162
    2457 | ANL x_23164 -> h_ANL x_23164
    2458 | ORL x_23165 -> h_ORL x_23165
    2459 | XRL x_23166 -> h_XRL x_23166
    2460 | CLR x_23167 -> h_CLR x_23167
    2461 | CPL x_23168 -> h_CPL x_23168
    2462 | RL x_23169 -> h_RL x_23169
    2463 | RLC x_23170 -> h_RLC x_23170
    2464 | RR x_23171 -> h_RR x_23171
    2465 | RRC x_23172 -> h_RRC x_23172
    2466 | SWAP x_23173 -> h_SWAP x_23173
    2467 | MOV x_23174 -> h_MOV x_23174
    2468 | MOVX x_23175 -> h_MOVX x_23175
    2469 | SETB x_23176 -> h_SETB x_23176
    2470 | PUSH x_23177 -> h_PUSH x_23177
    2471 | POP x_23178 -> h_POP x_23178
    2472 | XCH (x_23180, x_23179) -> h_XCH x_23180 x_23179
    2473 | XCHD (x_23182, x_23181) -> h_XCHD x_23182 x_23181
     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_23183 -> h_JMP x_23183
     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_23224, x_23223) -> h_ADD x_23224 x_23223
    2516 | ADDC (x_23226, x_23225) -> h_ADDC x_23226 x_23225
    2517 | SUBB (x_23228, x_23227) -> h_SUBB x_23228 x_23227
    2518 | INC x_23229 -> h_INC x_23229
    2519 | DEC x_23230 -> h_DEC x_23230
    2520 | MUL (x_23232, x_23231) -> h_MUL x_23232 x_23231
    2521 | DIV (x_23234, x_23233) -> h_DIV x_23234 x_23233
    2522 | DA x_23235 -> h_DA x_23235
    2523 | JC x_23236 -> h_JC x_23236
    2524 | JNC x_23237 -> h_JNC x_23237
    2525 | JB (x_23239, x_23238) -> h_JB x_23239 x_23238
    2526 | JNB (x_23241, x_23240) -> h_JNB x_23241 x_23240
    2527 | JBC (x_23243, x_23242) -> h_JBC x_23243 x_23242
    2528 | JZ x_23244 -> h_JZ x_23244
    2529 | JNZ x_23245 -> h_JNZ x_23245
    2530 | CJNE (x_23247, x_23246) -> h_CJNE x_23247 x_23246
    2531 | DJNZ (x_23249, x_23248) -> h_DJNZ x_23249 x_23248
    2532 | ANL x_23250 -> h_ANL x_23250
    2533 | ORL x_23251 -> h_ORL x_23251
    2534 | XRL x_23252 -> h_XRL x_23252
    2535 | CLR x_23253 -> h_CLR x_23253
    2536 | CPL x_23254 -> h_CPL x_23254
    2537 | RL x_23255 -> h_RL x_23255
    2538 | RLC x_23256 -> h_RLC x_23256
    2539 | RR x_23257 -> h_RR x_23257
    2540 | RRC x_23258 -> h_RRC x_23258
    2541 | SWAP x_23259 -> h_SWAP x_23259
    2542 | MOV x_23260 -> h_MOV x_23260
    2543 | MOVX x_23261 -> h_MOVX x_23261
    2544 | SETB x_23262 -> h_SETB x_23262
    2545 | PUSH x_23263 -> h_PUSH x_23263
    2546 | POP x_23264 -> h_POP x_23264
    2547 | XCH (x_23266, x_23265) -> h_XCH x_23266 x_23265
    2548 | XCHD (x_23268, x_23267) -> h_XCHD x_23268 x_23267
     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_23269 -> h_JMP x_23269
     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_23310, x_23309) -> h_ADD x_23310 x_23309
    2591 | ADDC (x_23312, x_23311) -> h_ADDC x_23312 x_23311
    2592 | SUBB (x_23314, x_23313) -> h_SUBB x_23314 x_23313
    2593 | INC x_23315 -> h_INC x_23315
    2594 | DEC x_23316 -> h_DEC x_23316
    2595 | MUL (x_23318, x_23317) -> h_MUL x_23318 x_23317
    2596 | DIV (x_23320, x_23319) -> h_DIV x_23320 x_23319
    2597 | DA x_23321 -> h_DA x_23321
    2598 | JC x_23322 -> h_JC x_23322
    2599 | JNC x_23323 -> h_JNC x_23323
    2600 | JB (x_23325, x_23324) -> h_JB x_23325 x_23324
    2601 | JNB (x_23327, x_23326) -> h_JNB x_23327 x_23326
    2602 | JBC (x_23329, x_23328) -> h_JBC x_23329 x_23328
    2603 | JZ x_23330 -> h_JZ x_23330
    2604 | JNZ x_23331 -> h_JNZ x_23331
    2605 | CJNE (x_23333, x_23332) -> h_CJNE x_23333 x_23332
    2606 | DJNZ (x_23335, x_23334) -> h_DJNZ x_23335 x_23334
    2607 | ANL x_23336 -> h_ANL x_23336
    2608 | ORL x_23337 -> h_ORL x_23337
    2609 | XRL x_23338 -> h_XRL x_23338
    2610 | CLR x_23339 -> h_CLR x_23339
    2611 | CPL x_23340 -> h_CPL x_23340
    2612 | RL x_23341 -> h_RL x_23341
    2613 | RLC x_23342 -> h_RLC x_23342
    2614 | RR x_23343 -> h_RR x_23343
    2615 | RRC x_23344 -> h_RRC x_23344
    2616 | SWAP x_23345 -> h_SWAP x_23345
    2617 | MOV x_23346 -> h_MOV x_23346
    2618 | MOVX x_23347 -> h_MOVX x_23347
    2619 | SETB x_23348 -> h_SETB x_23348
    2620 | PUSH x_23349 -> h_PUSH x_23349
    2621 | POP x_23350 -> h_POP x_23350
    2622 | XCH (x_23352, x_23351) -> h_XCH x_23352 x_23351
    2623 | XCHD (x_23354, x_23353) -> h_XCHD x_23354 x_23353
     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_23355 -> h_JMP x_23355
     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_23396, x_23395) -> h_ADD x_23396 x_23395
    2666 | ADDC (x_23398, x_23397) -> h_ADDC x_23398 x_23397
    2667 | SUBB (x_23400, x_23399) -> h_SUBB x_23400 x_23399
    2668 | INC x_23401 -> h_INC x_23401
    2669 | DEC x_23402 -> h_DEC x_23402
    2670 | MUL (x_23404, x_23403) -> h_MUL x_23404 x_23403
    2671 | DIV (x_23406, x_23405) -> h_DIV x_23406 x_23405
    2672 | DA x_23407 -> h_DA x_23407
    2673 | JC x_23408 -> h_JC x_23408
    2674 | JNC x_23409 -> h_JNC x_23409
    2675 | JB (x_23411, x_23410) -> h_JB x_23411 x_23410
    2676 | JNB (x_23413, x_23412) -> h_JNB x_23413 x_23412
    2677 | JBC (x_23415, x_23414) -> h_JBC x_23415 x_23414
    2678 | JZ x_23416 -> h_JZ x_23416
    2679 | JNZ x_23417 -> h_JNZ x_23417
    2680 | CJNE (x_23419, x_23418) -> h_CJNE x_23419 x_23418
    2681 | DJNZ (x_23421, x_23420) -> h_DJNZ x_23421 x_23420
    2682 | ANL x_23422 -> h_ANL x_23422
    2683 | ORL x_23423 -> h_ORL x_23423
    2684 | XRL x_23424 -> h_XRL x_23424
    2685 | CLR x_23425 -> h_CLR x_23425
    2686 | CPL x_23426 -> h_CPL x_23426
    2687 | RL x_23427 -> h_RL x_23427
    2688 | RLC x_23428 -> h_RLC x_23428
    2689 | RR x_23429 -> h_RR x_23429
    2690 | RRC x_23430 -> h_RRC x_23430
    2691 | SWAP x_23431 -> h_SWAP x_23431
    2692 | MOV x_23432 -> h_MOV x_23432
    2693 | MOVX x_23433 -> h_MOVX x_23433
    2694 | SETB x_23434 -> h_SETB x_23434
    2695 | PUSH x_23435 -> h_PUSH x_23435
    2696 | POP x_23436 -> h_POP x_23436
    2697 | XCH (x_23438, x_23437) -> h_XCH x_23438 x_23437
    2698 | XCHD (x_23440, x_23439) -> h_XCHD x_23440 x_23439
     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_23441 -> h_JMP x_23441
     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_24013 -> h_ACALL x_24013
    5107 | LCALL x_24014 -> h_LCALL x_24014
    5108 | AJMP x_24015 -> h_AJMP x_24015
    5109 | LJMP x_24016 -> h_LJMP x_24016
    5110 | SJMP x_24017 -> h_SJMP x_24017
    5111 | MOVC (x_24019, x_24018) -> h_MOVC x_24019 x_24018
    5112 | RealInstruction x_24020 -> h_RealInstruction x_24020
     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_24029 -> h_ACALL x_24029
    5122 | LCALL x_24030 -> h_LCALL x_24030
    5123 | AJMP x_24031 -> h_AJMP x_24031
    5124 | LJMP x_24032 -> h_LJMP x_24032
    5125 | SJMP x_24033 -> h_SJMP x_24033
    5126 | MOVC (x_24035, x_24034) -> h_MOVC x_24035 x_24034
    5127 | RealInstruction x_24036 -> h_RealInstruction x_24036
     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_24045 -> h_ACALL x_24045
    5137 | LCALL x_24046 -> h_LCALL x_24046
    5138 | AJMP x_24047 -> h_AJMP x_24047
    5139 | LJMP x_24048 -> h_LJMP x_24048
    5140 | SJMP x_24049 -> h_SJMP x_24049
    5141 | MOVC (x_24051, x_24050) -> h_MOVC x_24051 x_24050
    5142 | RealInstruction x_24052 -> h_RealInstruction x_24052
     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_24061 -> h_ACALL x_24061
    5152 | LCALL x_24062 -> h_LCALL x_24062
    5153 | AJMP x_24063 -> h_AJMP x_24063
    5154 | LJMP x_24064 -> h_LJMP x_24064
    5155 | SJMP x_24065 -> h_SJMP x_24065
    5156 | MOVC (x_24067, x_24066) -> h_MOVC x_24067 x_24066
    5157 | RealInstruction x_24068 -> h_RealInstruction x_24068
     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_24077 -> h_ACALL x_24077
    5167 | LCALL x_24078 -> h_LCALL x_24078
    5168 | AJMP x_24079 -> h_AJMP x_24079
    5169 | LJMP x_24080 -> h_LJMP x_24080
    5170 | SJMP x_24081 -> h_SJMP x_24081
    5171 | MOVC (x_24083, x_24082) -> h_MOVC x_24083 x_24082
    5172 | RealInstruction x_24084 -> h_RealInstruction x_24084
     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_24093 -> h_ACALL x_24093
    5182 | LCALL x_24094 -> h_LCALL x_24094
    5183 | AJMP x_24095 -> h_AJMP x_24095
    5184 | LJMP x_24096 -> h_LJMP x_24096
    5185 | SJMP x_24097 -> h_SJMP x_24097
    5186 | MOVC (x_24099, x_24098) -> h_MOVC x_24099 x_24098
    5187 | RealInstruction x_24100 -> h_RealInstruction x_24100
     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_MovSuccessor h_Call h_Mov = function
    5478 | Instruction x_24266 -> h_Instruction x_24266
    5479 | Comment x_24267 -> h_Comment x_24267
    5480 | Cost x_24268 -> h_Cost x_24268
    5481 | Jmp x_24269 -> h_Jmp x_24269
    5482 | Jnz (x_24272, x_24271, x_24270) -> h_Jnz x_24272 x_24271 x_24270
    5483 | MovSuccessor (x_24275, x_24274, x_24273) ->
    5484   h_MovSuccessor x_24275 x_24274 x_24273
    5485 | Call x_24276 -> h_Call x_24276
    5486 | Mov (x_24278, x_24277) -> h_Mov x_24278 x_24277
     5478| Instruction x_2078 -> h_Instruction x_2078
     5479| Comment x_2079 -> h_Comment x_2079
     5480| Cost x_2080 -> h_Cost x_2080
     5481| Jmp x_2081 -> h_Jmp x_2081
     5482| Jnz (x_2084, x_2083, x_2082) -> h_Jnz x_2084 x_2083 x_2082
     5483| MovSuccessor (x_2087, x_2086, x_2085) ->
     5484  h_MovSuccessor x_2087 x_2086 x_2085
     5485| Call x_2088 -> h_Call x_2088
     5486| Mov (x_2090, x_2089) -> h_Mov x_2090 x_2089
    54875487
    54885488(** val pseudo_instruction_rect_Type5 :
     
    54945494    -> 'a1 **)
    54955495let rec pseudo_instruction_rect_Type5 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5496 | Instruction x_24288 -> h_Instruction x_24288
    5497 | Comment x_24289 -> h_Comment x_24289
    5498 | Cost x_24290 -> h_Cost x_24290
    5499 | Jmp x_24291 -> h_Jmp x_24291
    5500 | Jnz (x_24294, x_24293, x_24292) -> h_Jnz x_24294 x_24293 x_24292
    5501 | MovSuccessor (x_24297, x_24296, x_24295) ->
    5502   h_MovSuccessor x_24297 x_24296 x_24295
    5503 | Call x_24298 -> h_Call x_24298
    5504 | Mov (x_24300, x_24299) -> h_Mov x_24300 x_24299
     5496| Instruction x_2100 -> h_Instruction x_2100
     5497| Comment x_2101 -> h_Comment x_2101
     5498| Cost x_2102 -> h_Cost x_2102
     5499| Jmp x_2103 -> h_Jmp x_2103
     5500| Jnz (x_2106, x_2105, x_2104) -> h_Jnz x_2106 x_2105 x_2104
     5501| MovSuccessor (x_2109, x_2108, x_2107) ->
     5502  h_MovSuccessor x_2109 x_2108 x_2107
     5503| Call x_2110 -> h_Call x_2110
     5504| Mov (x_2112, x_2111) -> h_Mov x_2112 x_2111
    55055505
    55065506(** val pseudo_instruction_rect_Type3 :
     
    55125512    -> 'a1 **)
    55135513let rec pseudo_instruction_rect_Type3 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5514 | Instruction x_24310 -> h_Instruction x_24310
    5515 | Comment x_24311 -> h_Comment x_24311
    5516 | Cost x_24312 -> h_Cost x_24312
    5517 | Jmp x_24313 -> h_Jmp x_24313
    5518 | Jnz (x_24316, x_24315, x_24314) -> h_Jnz x_24316 x_24315 x_24314
    5519 | MovSuccessor (x_24319, x_24318, x_24317) ->
    5520   h_MovSuccessor x_24319 x_24318 x_24317
    5521 | Call x_24320 -> h_Call x_24320
    5522 | Mov (x_24322, x_24321) -> h_Mov x_24322 x_24321
     5514| Instruction x_2122 -> h_Instruction x_2122
     5515| Comment x_2123 -> h_Comment x_2123
     5516| Cost x_2124 -> h_Cost x_2124
     5517| Jmp x_2125 -> h_Jmp x_2125
     5518| Jnz (x_2128, x_2127, x_2126) -> h_Jnz x_2128 x_2127 x_2126
     5519| MovSuccessor (x_2131, x_2130, x_2129) ->
     5520  h_MovSuccessor x_2131 x_2130 x_2129
     5521| Call x_2132 -> h_Call x_2132
     5522| Mov (x_2134, x_2133) -> h_Mov x_2134 x_2133
    55235523
    55245524(** val pseudo_instruction_rect_Type2 :
     
    55305530    -> 'a1 **)
    55315531let rec pseudo_instruction_rect_Type2 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5532 | Instruction x_24332 -> h_Instruction x_24332
    5533 | Comment x_24333 -> h_Comment x_24333
    5534 | Cost x_24334 -> h_Cost x_24334
    5535 | Jmp x_24335 -> h_Jmp x_24335
    5536 | Jnz (x_24338, x_24337, x_24336) -> h_Jnz x_24338 x_24337 x_24336
    5537 | MovSuccessor (x_24341, x_24340, x_24339) ->
    5538   h_MovSuccessor x_24341 x_24340 x_24339
    5539 | Call x_24342 -> h_Call x_24342
    5540 | Mov (x_24344, x_24343) -> h_Mov x_24344 x_24343
     5532| Instruction x_2144 -> h_Instruction x_2144
     5533| Comment x_2145 -> h_Comment x_2145
     5534| Cost x_2146 -> h_Cost x_2146
     5535| Jmp x_2147 -> h_Jmp x_2147
     5536| Jnz (x_2150, x_2149, x_2148) -> h_Jnz x_2150 x_2149 x_2148
     5537| MovSuccessor (x_2153, x_2152, x_2151) ->
     5538  h_MovSuccessor x_2153 x_2152 x_2151
     5539| Call x_2154 -> h_Call x_2154
     5540| Mov (x_2156, x_2155) -> h_Mov x_2156 x_2155
    55415541
    55425542(** val pseudo_instruction_rect_Type1 :
     
    55485548    -> 'a1 **)
    55495549let rec pseudo_instruction_rect_Type1 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5550 | Instruction x_24354 -> h_Instruction x_24354
    5551 | Comment x_24355 -> h_Comment x_24355
    5552 | Cost x_24356 -> h_Cost x_24356
    5553 | Jmp x_24357 -> h_Jmp x_24357
    5554 | Jnz (x_24360, x_24359, x_24358) -> h_Jnz x_24360 x_24359 x_24358
    5555 | MovSuccessor (x_24363, x_24362, x_24361) ->
    5556   h_MovSuccessor x_24363 x_24362 x_24361
    5557 | Call x_24364 -> h_Call x_24364
    5558 | Mov (x_24366, x_24365) -> h_Mov x_24366 x_24365
     5550| Instruction x_2166 -> h_Instruction x_2166
     5551| Comment x_2167 -> h_Comment x_2167
     5552| Cost x_2168 -> h_Cost x_2168
     5553| Jmp x_2169 -> h_Jmp x_2169
     5554| Jnz (x_2172, x_2171, x_2170) -> h_Jnz x_2172 x_2171 x_2170
     5555| MovSuccessor (x_2175, x_2174, x_2173) ->
     5556  h_MovSuccessor x_2175 x_2174 x_2173
     5557| Call x_2176 -> h_Call x_2176
     5558| Mov (x_2178, x_2177) -> h_Mov x_2178 x_2177
    55595559
    55605560(** val pseudo_instruction_rect_Type0 :
     
    55665566    -> 'a1 **)
    55675567let rec pseudo_instruction_rect_Type0 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5568 | Instruction x_24376 -> h_Instruction x_24376
    5569 | Comment x_24377 -> h_Comment x_24377
    5570 | Cost x_24378 -> h_Cost x_24378
    5571 | Jmp x_24379 -> h_Jmp x_24379
    5572 | Jnz (x_24382, x_24381, x_24380) -> h_Jnz x_24382 x_24381 x_24380
    5573 | MovSuccessor (x_24385, x_24384, x_24383) ->
    5574   h_MovSuccessor x_24385 x_24384 x_24383
    5575 | Call x_24386 -> h_Call x_24386
    5576 | Mov (x_24388, x_24387) -> h_Mov x_24388 x_24387
     5568| Instruction x_2188 -> h_Instruction x_2188
     5569| Comment x_2189 -> h_Comment x_2189
     5570| Cost x_2190 -> h_Cost x_2190
     5571| Jmp x_2191 -> h_Jmp x_2191
     5572| Jnz (x_2194, x_2193, x_2192) -> h_Jnz x_2194 x_2193 x_2192
     5573| MovSuccessor (x_2197, x_2196, x_2195) ->
     5574  h_MovSuccessor x_2197 x_2196 x_2195
     5575| Call x_2198 -> h_Call x_2198
     5576| Mov (x_2200, x_2199) -> h_Mov x_2200 x_2199
    55775577
    55785578(** val pseudo_instruction_inv_rect_Type4 :
     
    57965796    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
    57975797    pseudo_assembly_program -> 'a1 **)
    5798 let rec pseudo_assembly_program_rect_Type4 h_mk_pseudo_assembly_program x_24531 =
     5798let rec pseudo_assembly_program_rect_Type4 h_mk_pseudo_assembly_program x_2343 =
    57995799  let { preamble = preamble0; code = code0; renamed_symbols =
    5800     renamed_symbols0; final_label = final_label0 } = x_24531
     5800    renamed_symbols0; final_label = final_label0 } = x_2343
    58015801  in
    58025802  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     
    58085808    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
    58095809    pseudo_assembly_program -> 'a1 **)
    5810 let rec pseudo_assembly_program_rect_Type5 h_mk_pseudo_assembly_program x_24533 =
     5810let rec pseudo_assembly_program_rect_Type5 h_mk_pseudo_assembly_program x_2345 =
    58115811  let { preamble = preamble0; code = code0; renamed_symbols =
    5812     renamed_symbols0; final_label = final_label0 } = x_24533
     5812    renamed_symbols0; final_label = final_label0 } = x_2345
    58135813  in
    58145814  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     
    58205820    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
    58215821    pseudo_assembly_program -> 'a1 **)
    5822 let rec pseudo_assembly_program_rect_Type3 h_mk_pseudo_assembly_program x_24535 =
     5822let rec pseudo_assembly_program_rect_Type3 h_mk_pseudo_assembly_program x_2347 =
    58235823  let { preamble = preamble0; code = code0; renamed_symbols =
    5824     renamed_symbols0; final_label = final_label0 } = x_24535
     5824    renamed_symbols0; final_label = final_label0 } = x_2347
    58255825  in
    58265826  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     
    58325832    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
    58335833    pseudo_assembly_program -> 'a1 **)
    5834 let rec pseudo_assembly_program_rect_Type2 h_mk_pseudo_assembly_program x_24537 =
     5834let rec pseudo_assembly_program_rect_Type2 h_mk_pseudo_assembly_program x_2349 =
    58355835  let { preamble = preamble0; code = code0; renamed_symbols =
    5836     renamed_symbols0; final_label = final_label0 } = x_24537
     5836    renamed_symbols0; final_label = final_label0 } = x_2349
    58375837  in
    58385838  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     
    58445844    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
    58455845    pseudo_assembly_program -> 'a1 **)
    5846 let rec pseudo_assembly_program_rect_Type1 h_mk_pseudo_assembly_program x_24539 =
     5846let rec pseudo_assembly_program_rect_Type1 h_mk_pseudo_assembly_program x_2351 =
    58475847  let { preamble = preamble0; code = code0; renamed_symbols =
    5848     renamed_symbols0; final_label = final_label0 } = x_24539
     5848    renamed_symbols0; final_label = final_label0 } = x_2351
    58495849  in
    58505850  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     
    58565856    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
    58575857    pseudo_assembly_program -> 'a1 **)
    5858 let rec pseudo_assembly_program_rect_Type0 h_mk_pseudo_assembly_program x_24541 =
     5858let rec pseudo_assembly_program_rect_Type0 h_mk_pseudo_assembly_program x_2353 =
    58595859  let { preamble = preamble0; code = code0; renamed_symbols =
    5860     renamed_symbols0; final_label = final_label0 } = x_24541
     5860    renamed_symbols0; final_label = final_label0 } = x_2353
    58615861  in
    58625862  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     
    59445944    (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
    59455945    -> 'a1) -> labelled_object_code -> 'a1 **)
    5946 let rec labelled_object_code_rect_Type4 h_mk_labelled_object_code x_24557 =
     5946let rec labelled_object_code_rect_Type4 h_mk_labelled_object_code x_2369 =
    59475947  let { oc = oc0; costlabels = costlabels0; symboltable = symboltable0;
    5948     final_pc = final_pc0 } = x_24557
     5948    final_pc = final_pc0 } = x_2369
    59495949  in
    59505950  h_mk_labelled_object_code oc0 costlabels0 symboltable0 final_pc0 __
     
    59535953    (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
    59545954    -> 'a1) -> labelled_object_code -> 'a1 **)
    5955 let rec labelled_object_code_rect_Type5 h_mk_labelled_object_code x_24559 =
     5955let rec labelled_object_code_rect_Type5 h_mk_labelled_object_code x_2371 =
    59565956  let { oc = oc0; costlabels = costlabels0; symboltable = symboltable0;
    5957     final_pc = final_pc0 } = x_24559
     5957    final_pc = final_pc0 } = x_2371
    59585958  in
    59595959  h_mk_labelled_object_code oc0 costlabels0 symboltable0 final_pc0 __
     
    59625962    (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
    59635963    -> 'a1) -> labelled_object_code -> 'a1 **)
    5964 let rec labelled_object_code_rect_Type3 h_mk_labelled_object_code x_24561 =
     5964let rec labelled_object_code_rect_Type3 h_mk_labelled_object_code x_2373 =
    59655965  let { oc = oc0; costlabels = costlabels0; symboltable = symboltable0;
    5966     final_pc = final_pc0 } = x_24561
     5966    final_pc = final_pc0 } = x_2373
    59675967  in
    59685968  h_mk_labelled_object_code oc0 costlabels0 symboltable0 final_pc0 __
     
    59715971    (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
    59725972    -> 'a1) -> labelled_object_code -> 'a1 **)
    5973 let rec labelled_object_code_rect_Type2 h_mk_labelled_object_code x_24563 =
     5973let rec labelled_object_code_rect_Type2 h_mk_labelled_object_code x_2375 =
    59745974  let { oc = oc0; costlabels = costlabels0; symboltable = symboltable0;
    5975     final_pc = final_pc0 } = x_24563
     5975    final_pc = final_pc0 } = x_2375
    59765976  in
    59775977  h_mk_labelled_object_code oc0 costlabels0 symboltable0 final_pc0 __
     
    59805980    (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
    59815981    -> 'a1) -> labelled_object_code -> 'a1 **)
    5982 let rec labelled_object_code_rect_Type1 h_mk_labelled_object_code x_24565 =
     5982let rec labelled_object_code_rect_Type1 h_mk_labelled_object_code x_2377 =
    59835983  let { oc = oc0; costlabels = costlabels0; symboltable = symboltable0;
    5984     final_pc = final_pc0 } = x_24565
     5984    final_pc = final_pc0 } = x_2377
    59855985  in
    59865986  h_mk_labelled_object_code oc0 costlabels0 symboltable0 final_pc0 __
     
    59895989    (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
    59905990    -> 'a1) -> labelled_object_code -> 'a1 **)
    5991 let rec labelled_object_code_rect_Type0 h_mk_labelled_object_code x_24567 =
     5991let rec labelled_object_code_rect_Type0 h_mk_labelled_object_code x_2379 =
    59925992  let { oc = oc0; costlabels = costlabels0; symboltable = symboltable0;
    5993     final_pc = final_pc0 } = x_24567
     5993    final_pc = final_pc0 } = x_2379
    59945994  in
    59955995  h_mk_labelled_object_code oc0 costlabels0 symboltable0 final_pc0 __
Note: See TracChangeset for help on using the changeset viewer.