Changeset 2773 for extracted/aSM.ml


Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/aSM.ml

    r2743 r2773  
    11open Preamble
    22
     3open Proper
     4
     5open PositiveMap
     6
     7open Deqsets
     8
     9open ErrorMessages
     10
     11open PreIdentifiers
     12
     13open Errors
     14
     15open Extralib
     16
     17open Setoids
     18
     19open Monad
     20
     21open Option
     22
     23open Div_and_mod
     24
     25open Jmeq
     26
     27open Russell
     28
     29open Util
     30
     31open List
     32
     33open Lists
     34
     35open Bool
     36
     37open Relations
     38
     39open Nat
     40
     41open Positive
     42
     43open Hints_declaration
     44
     45open Core_notation
     46
     47open Pts
     48
     49open Logic
     50
     51open Types
     52
     53open Identifiers
     54
     55open CostLabel
     56
     57open LabelledObjects
     58
     59open Exp
     60
     61open Arithmetic
     62
     63open Vector
     64
     65open FoldStuff
     66
     67open BitVector
     68
    369open Extranat
    470
    5 open Vector
    6 
    7 open Div_and_mod
    8 
    9 open Jmeq
    10 
    11 open Russell
    12 
    13 open Types
    14 
    15 open List
    16 
    17 open Util
    18 
    19 open FoldStuff
    20 
    21 open Bool
    22 
    23 open Hints_declaration
    24 
    25 open Core_notation
    26 
    27 open Pts
    28 
    29 open Logic
    30 
    31 open Relations
    32 
    33 open Nat
    34 
    35 open BitVector
    36 
    37 open Proper
    38 
    39 open PositiveMap
    40 
    41 open Deqsets
    42 
    43 open ErrorMessages
    44 
    45 open PreIdentifiers
    46 
    47 open Errors
    48 
    49 open Extralib
    50 
    51 open Setoids
    52 
    53 open Monad
    54 
    55 open Option
    56 
    57 open Lists
    58 
    59 open Positive
    60 
    61 open Identifiers
     71open Integers
     72
     73open AST
     74
     75open String
    6276
    6377open BitVectorTrie
    6478
    65 open Exp
    66 
    67 open Arithmetic
    68 
    69 open Integers
    70 
    71 open AST
    72 
    73 open CostLabel
    74 
    75 open LabelledObjects
    76 
    77 open String
    78 
    79 type identifier0 = PreIdentifiers.identifier
     79type identifier = PreIdentifiers.identifier
    8080
    8181(** val toASM_ident :
    82     PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> identifier0 **)
     82    PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> identifier **)
    8383let toASM_ident t i =
    8484  let id = i in id
     
    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_21796 -> h_DIRECT x_21796
    116 | INDIRECT x_21797 -> h_INDIRECT x_21797
    117 | EXT_INDIRECT x_21798 -> h_EXT_INDIRECT x_21798
    118 | REGISTER x_21799 -> h_REGISTER x_21799
     115| DIRECT x_17106 -> h_DIRECT x_17106
     116| INDIRECT x_17107 -> h_INDIRECT x_17107
     117| EXT_INDIRECT x_17108 -> h_EXT_INDIRECT x_17108
     118| REGISTER x_17109 -> h_REGISTER x_17109
    119119| ACC_A -> h_ACC_A
    120120| ACC_B -> h_ACC_B
    121121| DPTR -> h_DPTR
    122 | DATA x_21800 -> h_DATA x_21800
    123 | DATA16 x_21801 -> h_DATA16 x_21801
     122| DATA x_17110 -> h_DATA x_17110
     123| DATA16 x_17111 -> h_DATA16 x_17111
    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_21802 -> h_BIT_ADDR x_21802
    130 | N_BIT_ADDR x_21803 -> h_N_BIT_ADDR x_21803
    131 | RELATIVE x_21804 -> h_RELATIVE x_21804
    132 | ADDR11 x_21805 -> h_ADDR11 x_21805
    133 | ADDR16 x_21806 -> h_ADDR16 x_21806
     129| BIT_ADDR x_17112 -> h_BIT_ADDR x_17112
     130| N_BIT_ADDR x_17113 -> h_N_BIT_ADDR x_17113
     131| RELATIVE x_17114 -> h_RELATIVE x_17114
     132| ADDR11 x_17115 -> h_ADDR11 x_17115
     133| ADDR16 x_17116 -> h_ADDR16 x_17116
    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_21827 -> h_DIRECT x_21827
    144 | INDIRECT x_21828 -> h_INDIRECT x_21828
    145 | EXT_INDIRECT x_21829 -> h_EXT_INDIRECT x_21829
    146 | REGISTER x_21830 -> h_REGISTER x_21830
     143| DIRECT x_17137 -> h_DIRECT x_17137
     144| INDIRECT x_17138 -> h_INDIRECT x_17138
     145| EXT_INDIRECT x_17139 -> h_EXT_INDIRECT x_17139
     146| REGISTER x_17140 -> h_REGISTER x_17140
    147147| ACC_A -> h_ACC_A
    148148| ACC_B -> h_ACC_B
    149149| DPTR -> h_DPTR
    150 | DATA x_21831 -> h_DATA x_21831
    151 | DATA16 x_21832 -> h_DATA16 x_21832
     150| DATA x_17141 -> h_DATA x_17141
     151| DATA16 x_17142 -> h_DATA16 x_17142
    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_21833 -> h_BIT_ADDR x_21833
    158 | N_BIT_ADDR x_21834 -> h_N_BIT_ADDR x_21834
    159 | RELATIVE x_21835 -> h_RELATIVE x_21835
    160 | ADDR11 x_21836 -> h_ADDR11 x_21836
    161 | ADDR16 x_21837 -> h_ADDR16 x_21837
     157| BIT_ADDR x_17143 -> h_BIT_ADDR x_17143
     158| N_BIT_ADDR x_17144 -> h_N_BIT_ADDR x_17144
     159| RELATIVE x_17145 -> h_RELATIVE x_17145
     160| ADDR11 x_17146 -> h_ADDR11 x_17146
     161| ADDR16 x_17147 -> h_ADDR16 x_17147
    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_21858 -> h_DIRECT x_21858
    172 | INDIRECT x_21859 -> h_INDIRECT x_21859
    173 | EXT_INDIRECT x_21860 -> h_EXT_INDIRECT x_21860
    174 | REGISTER x_21861 -> h_REGISTER x_21861
     171| DIRECT x_17168 -> h_DIRECT x_17168
     172| INDIRECT x_17169 -> h_INDIRECT x_17169
     173| EXT_INDIRECT x_17170 -> h_EXT_INDIRECT x_17170
     174| REGISTER x_17171 -> h_REGISTER x_17171
    175175| ACC_A -> h_ACC_A
    176176| ACC_B -> h_ACC_B
    177177| DPTR -> h_DPTR
    178 | DATA x_21862 -> h_DATA x_21862
    179 | DATA16 x_21863 -> h_DATA16 x_21863
     178| DATA x_17172 -> h_DATA x_17172
     179| DATA16 x_17173 -> h_DATA16 x_17173
    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_21864 -> h_BIT_ADDR x_21864
    186 | N_BIT_ADDR x_21865 -> h_N_BIT_ADDR x_21865
    187 | RELATIVE x_21866 -> h_RELATIVE x_21866
    188 | ADDR11 x_21867 -> h_ADDR11 x_21867
    189 | ADDR16 x_21868 -> h_ADDR16 x_21868
     185| BIT_ADDR x_17174 -> h_BIT_ADDR x_17174
     186| N_BIT_ADDR x_17175 -> h_N_BIT_ADDR x_17175
     187| RELATIVE x_17176 -> h_RELATIVE x_17176
     188| ADDR11 x_17177 -> h_ADDR11 x_17177
     189| ADDR16 x_17178 -> h_ADDR16 x_17178
    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_21889 -> h_DIRECT x_21889
    200 | INDIRECT x_21890 -> h_INDIRECT x_21890
    201 | EXT_INDIRECT x_21891 -> h_EXT_INDIRECT x_21891
    202 | REGISTER x_21892 -> h_REGISTER x_21892
     199| DIRECT x_17199 -> h_DIRECT x_17199
     200| INDIRECT x_17200 -> h_INDIRECT x_17200
     201| EXT_INDIRECT x_17201 -> h_EXT_INDIRECT x_17201
     202| REGISTER x_17202 -> h_REGISTER x_17202
    203203| ACC_A -> h_ACC_A
    204204| ACC_B -> h_ACC_B
    205205| DPTR -> h_DPTR
    206 | DATA x_21893 -> h_DATA x_21893
    207 | DATA16 x_21894 -> h_DATA16 x_21894
     206| DATA x_17203 -> h_DATA x_17203
     207| DATA16 x_17204 -> h_DATA16 x_17204
    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_21895 -> h_BIT_ADDR x_21895
    214 | N_BIT_ADDR x_21896 -> h_N_BIT_ADDR x_21896
    215 | RELATIVE x_21897 -> h_RELATIVE x_21897
    216 | ADDR11 x_21898 -> h_ADDR11 x_21898
    217 | ADDR16 x_21899 -> h_ADDR16 x_21899
     213| BIT_ADDR x_17205 -> h_BIT_ADDR x_17205
     214| N_BIT_ADDR x_17206 -> h_N_BIT_ADDR x_17206
     215| RELATIVE x_17207 -> h_RELATIVE x_17207
     216| ADDR11 x_17208 -> h_ADDR11 x_17208
     217| ADDR16 x_17209 -> h_ADDR16 x_17209
    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_21920 -> h_DIRECT x_21920
    228 | INDIRECT x_21921 -> h_INDIRECT x_21921
    229 | EXT_INDIRECT x_21922 -> h_EXT_INDIRECT x_21922
    230 | REGISTER x_21923 -> h_REGISTER x_21923
     227| DIRECT x_17230 -> h_DIRECT x_17230
     228| INDIRECT x_17231 -> h_INDIRECT x_17231
     229| EXT_INDIRECT x_17232 -> h_EXT_INDIRECT x_17232
     230| REGISTER x_17233 -> h_REGISTER x_17233
    231231| ACC_A -> h_ACC_A
    232232| ACC_B -> h_ACC_B
    233233| DPTR -> h_DPTR
    234 | DATA x_21924 -> h_DATA x_21924
    235 | DATA16 x_21925 -> h_DATA16 x_21925
     234| DATA x_17234 -> h_DATA x_17234
     235| DATA16 x_17235 -> h_DATA16 x_17235
    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_21926 -> h_BIT_ADDR x_21926
    242 | N_BIT_ADDR x_21927 -> h_N_BIT_ADDR x_21927
    243 | RELATIVE x_21928 -> h_RELATIVE x_21928
    244 | ADDR11 x_21929 -> h_ADDR11 x_21929
    245 | ADDR16 x_21930 -> h_ADDR16 x_21930
     241| BIT_ADDR x_17236 -> h_BIT_ADDR x_17236
     242| N_BIT_ADDR x_17237 -> h_N_BIT_ADDR x_17237
     243| RELATIVE x_17238 -> h_RELATIVE x_17238
     244| ADDR11 x_17239 -> h_ADDR11 x_17239
     245| ADDR16 x_17240 -> h_ADDR16 x_17240
    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_21951 -> h_DIRECT x_21951
    256 | INDIRECT x_21952 -> h_INDIRECT x_21952
    257 | EXT_INDIRECT x_21953 -> h_EXT_INDIRECT x_21953
    258 | REGISTER x_21954 -> h_REGISTER x_21954
     255| DIRECT x_17261 -> h_DIRECT x_17261
     256| INDIRECT x_17262 -> h_INDIRECT x_17262
     257| EXT_INDIRECT x_17263 -> h_EXT_INDIRECT x_17263
     258| REGISTER x_17264 -> h_REGISTER x_17264
    259259| ACC_A -> h_ACC_A
    260260| ACC_B -> h_ACC_B
    261261| DPTR -> h_DPTR
    262 | DATA x_21955 -> h_DATA x_21955
    263 | DATA16 x_21956 -> h_DATA16 x_21956
     262| DATA x_17265 -> h_DATA x_17265
     263| DATA16 x_17266 -> h_DATA16 x_17266
    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_21957 -> h_BIT_ADDR x_21957
    270 | N_BIT_ADDR x_21958 -> h_N_BIT_ADDR x_21958
    271 | RELATIVE x_21959 -> h_RELATIVE x_21959
    272 | ADDR11 x_21960 -> h_ADDR11 x_21960
    273 | ADDR16 x_21961 -> h_ADDR16 x_21961
     269| BIT_ADDR x_17267 -> h_BIT_ADDR x_17267
     270| N_BIT_ADDR x_17268 -> h_N_BIT_ADDR x_17268
     271| RELATIVE x_17269 -> h_RELATIVE x_17269
     272| ADDR11 x_17270 -> h_ADDR11 x_17270
     273| ADDR16 x_17271 -> h_ADDR16 x_17271
    274274
    275275(** val addressing_mode_inv_rect_Type4 :
     
    403403  | DIRECT d ->
    404404    (match b with
    405      | DIRECT e0 ->
     405     | DIRECT e ->
    406406       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    407          (Nat.S Nat.O)))))))) d e0
     407         (Nat.S Nat.O)))))))) d e
    408408     | INDIRECT x -> Bool.False
    409409     | EXT_INDIRECT x -> Bool.False
     
    427427    (match b with
    428428     | DIRECT x -> Bool.False
    429      | INDIRECT e0 -> BitVector.eq_b b' e0
     429     | INDIRECT e -> BitVector.eq_b b' e
    430430     | EXT_INDIRECT x -> Bool.False
    431431     | REGISTER x -> Bool.False
     
    449449     | DIRECT x -> Bool.False
    450450     | INDIRECT x -> Bool.False
    451      | EXT_INDIRECT e0 -> BitVector.eq_b b' e0
     451     | EXT_INDIRECT e -> BitVector.eq_b b' e
    452452     | REGISTER x -> Bool.False
    453453     | ACC_A -> Bool.False
     
    559559     | ACC_B -> Bool.False
    560560     | DPTR -> Bool.False
    561      | DATA e0 ->
     561     | DATA e ->
    562562       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    563          (Nat.S Nat.O)))))))) b' e0
     563         (Nat.S Nat.O)))))))) b' e
    564564     | DATA16 x -> Bool.False
    565565     | ACC_DPTR -> Bool.False
     
    583583     | DPTR -> Bool.False
    584584     | DATA x -> Bool.False
    585      | DATA16 e0 ->
     585     | DATA16 e ->
    586586       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    587587         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    588          Nat.O)))))))))))))))) w e0
     588         Nat.O)))))))))))))))) w e
    589589     | ACC_DPTR -> Bool.False
    590590     | ACC_PC -> Bool.False
     
    718718     | INDIRECT_DPTR -> Bool.False
    719719     | CARRY -> Bool.False
    720      | BIT_ADDR e0 ->
     720     | BIT_ADDR e ->
    721721       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    722          (Nat.S Nat.O)))))))) b' e0
     722         (Nat.S Nat.O)))))))) b' e
    723723     | N_BIT_ADDR x -> Bool.False
    724724     | RELATIVE x -> Bool.False
     
    742742     | CARRY -> Bool.False
    743743     | BIT_ADDR x -> Bool.False
    744      | N_BIT_ADDR e0 ->
     744     | N_BIT_ADDR e ->
    745745       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    746          (Nat.S Nat.O)))))))) b' e0
     746         (Nat.S Nat.O)))))))) b' e
    747747     | RELATIVE x -> Bool.False
    748748     | ADDR11 x -> Bool.False
     
    766766     | BIT_ADDR x -> Bool.False
    767767     | N_BIT_ADDR x -> Bool.False
    768      | RELATIVE e0 ->
     768     | RELATIVE e ->
    769769       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    770          (Nat.S Nat.O)))))))) n e0
     770         (Nat.S Nat.O)))))))) n e
    771771     | ADDR11 x -> Bool.False
    772772     | ADDR16 x -> Bool.False)
     
    790790     | N_BIT_ADDR x -> Bool.False
    791791     | RELATIVE x -> Bool.False
    792      | ADDR11 e0 ->
     792     | ADDR11 e ->
    793793       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    794          (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))) w e0
     794         (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))) w e
    795795     | ADDR16 x -> Bool.False)
    796796  | ADDR16 w ->
     
    814814     | RELATIVE x -> Bool.False
    815815     | ADDR11 x -> Bool.False
    816      | ADDR16 e0 ->
     816     | ADDR16 e ->
    817817       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    818818         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    819          Nat.O)))))))))))))))) w e0)
     819         Nat.O)))))))))))))))) w e)
    820820
    821821type addressing_mode_tag =
     
    15081508     | Addr16 -> Bool.True)
    15091509
    1510 type member_addressing_mode_tag = __
    1511 
    15121510(** val is_a : addressing_mode_tag -> addressing_mode -> Bool.bool **)
    15131511let rec is_a d a =
     
    19281926    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19291927    'a1) -> subaddressing_mode -> 'a1 **)
    1930 let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_22429 =
    1931   let subaddressing_modeel = x_22429 in
     1928let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_17739 =
     1929  let subaddressing_modeel = x_17739 in
    19321930  h_mk_subaddressing_mode subaddressing_modeel __
    19331931
     
    19351933    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19361934    'a1) -> subaddressing_mode -> 'a1 **)
    1937 let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_22431 =
    1938   let subaddressing_modeel = x_22431 in
     1935let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_17741 =
     1936  let subaddressing_modeel = x_17741 in
    19391937  h_mk_subaddressing_mode subaddressing_modeel __
    19401938
     
    19421940    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19431941    'a1) -> subaddressing_mode -> 'a1 **)
    1944 let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_22433 =
    1945   let subaddressing_modeel = x_22433 in
     1942let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_17743 =
     1943  let subaddressing_modeel = x_17743 in
    19461944  h_mk_subaddressing_mode subaddressing_modeel __
    19471945
     
    19491947    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19501948    'a1) -> subaddressing_mode -> 'a1 **)
    1951 let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_22435 =
    1952   let subaddressing_modeel = x_22435 in
     1949let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_17745 =
     1950  let subaddressing_modeel = x_17745 in
    19531951  h_mk_subaddressing_mode subaddressing_modeel __
    19541952
     
    19561954    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19571955    'a1) -> subaddressing_mode -> 'a1 **)
    1958 let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_22437 =
    1959   let subaddressing_modeel = x_22437 in
     1956let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_17747 =
     1957  let subaddressing_modeel = x_17747 in
    19601958  h_mk_subaddressing_mode subaddressing_modeel __
    19611959
     
    19631961    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19641962    'a1) -> subaddressing_mode -> 'a1 **)
    1965 let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_22439 =
    1966   let subaddressing_modeel = x_22439 in
     1963let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_17749 =
     1964  let subaddressing_modeel = x_17749 in
    19671965  h_mk_subaddressing_mode subaddressing_modeel __
    19681966
     
    22002198let eject__o__mk_subaddressing_mode x1 x2 x3 =
    22012199  Types.pi1 x2
    2202 
    2203 type subaddressing_mode_elim_type = __
    22042200
    22052201type 'a preinstruction =
     
    22922288    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    22932289let 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
    2294 | ADD (x_22541, x_22540) -> h_ADD x_22541 x_22540
    2295 | ADDC (x_22543, x_22542) -> h_ADDC x_22543 x_22542
    2296 | SUBB (x_22545, x_22544) -> h_SUBB x_22545 x_22544
    2297 | INC x_22546 -> h_INC x_22546
    2298 | DEC x_22547 -> h_DEC x_22547
    2299 | MUL (x_22549, x_22548) -> h_MUL x_22549 x_22548
    2300 | DIV (x_22551, x_22550) -> h_DIV x_22551 x_22550
    2301 | DA x_22552 -> h_DA x_22552
    2302 | JC x_22553 -> h_JC x_22553
    2303 | JNC x_22554 -> h_JNC x_22554
    2304 | JB (x_22556, x_22555) -> h_JB x_22556 x_22555
    2305 | JNB (x_22558, x_22557) -> h_JNB x_22558 x_22557
    2306 | JBC (x_22560, x_22559) -> h_JBC x_22560 x_22559
    2307 | JZ x_22561 -> h_JZ x_22561
    2308 | JNZ x_22562 -> h_JNZ x_22562
    2309 | CJNE (x_22564, x_22563) -> h_CJNE x_22564 x_22563
    2310 | DJNZ (x_22566, x_22565) -> h_DJNZ x_22566 x_22565
    2311 | ANL x_22567 -> h_ANL x_22567
    2312 | ORL x_22568 -> h_ORL x_22568
    2313 | XRL x_22569 -> h_XRL x_22569
    2314 | CLR x_22570 -> h_CLR x_22570
    2315 | CPL x_22571 -> h_CPL x_22571
    2316 | RL x_22572 -> h_RL x_22572
    2317 | RLC x_22573 -> h_RLC x_22573
    2318 | RR x_22574 -> h_RR x_22574
    2319 | RRC x_22575 -> h_RRC x_22575
    2320 | SWAP x_22576 -> h_SWAP x_22576
    2321 | MOV x_22577 -> h_MOV x_22577
    2322 | MOVX x_22578 -> h_MOVX x_22578
    2323 | SETB x_22579 -> h_SETB x_22579
    2324 | PUSH x_22580 -> h_PUSH x_22580
    2325 | POP x_22581 -> h_POP x_22581
    2326 | XCH (x_22583, x_22582) -> h_XCH x_22583 x_22582
    2327 | XCHD (x_22585, x_22584) -> h_XCHD x_22585 x_22584
     2290| ADD (x_17851, x_17850) -> h_ADD x_17851 x_17850
     2291| ADDC (x_17853, x_17852) -> h_ADDC x_17853 x_17852
     2292| SUBB (x_17855, x_17854) -> h_SUBB x_17855 x_17854
     2293| INC x_17856 -> h_INC x_17856
     2294| DEC x_17857 -> h_DEC x_17857
     2295| MUL (x_17859, x_17858) -> h_MUL x_17859 x_17858
     2296| DIV (x_17861, x_17860) -> h_DIV x_17861 x_17860
     2297| DA x_17862 -> h_DA x_17862
     2298| JC x_17863 -> h_JC x_17863
     2299| JNC x_17864 -> h_JNC x_17864
     2300| JB (x_17866, x_17865) -> h_JB x_17866 x_17865
     2301| JNB (x_17868, x_17867) -> h_JNB x_17868 x_17867
     2302| JBC (x_17870, x_17869) -> h_JBC x_17870 x_17869
     2303| JZ x_17871 -> h_JZ x_17871
     2304| JNZ x_17872 -> h_JNZ x_17872
     2305| CJNE (x_17874, x_17873) -> h_CJNE x_17874 x_17873
     2306| DJNZ (x_17876, x_17875) -> h_DJNZ x_17876 x_17875
     2307| ANL x_17877 -> h_ANL x_17877
     2308| ORL x_17878 -> h_ORL x_17878
     2309| XRL x_17879 -> h_XRL x_17879
     2310| CLR x_17880 -> h_CLR x_17880
     2311| CPL x_17881 -> h_CPL x_17881
     2312| RL x_17882 -> h_RL x_17882
     2313| RLC x_17883 -> h_RLC x_17883
     2314| RR x_17884 -> h_RR x_17884
     2315| RRC x_17885 -> h_RRC x_17885
     2316| SWAP x_17886 -> h_SWAP x_17886
     2317| MOV x_17887 -> h_MOV x_17887
     2318| MOVX x_17888 -> h_MOVX x_17888
     2319| SETB x_17889 -> h_SETB x_17889
     2320| PUSH x_17890 -> h_PUSH x_17890
     2321| POP x_17891 -> h_POP x_17891
     2322| XCH (x_17893, x_17892) -> h_XCH x_17893 x_17892
     2323| XCHD (x_17895, x_17894) -> h_XCHD x_17895 x_17894
    23282324| RET -> h_RET
    23292325| RETI -> h_RETI
    23302326| NOP -> h_NOP
    2331 | JMP x_22586 -> h_JMP x_22586
     2327| JMP x_17896 -> h_JMP x_17896
    23322328
    23332329(** val preinstruction_rect_Type5 :
     
    23672363    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    23682364let 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
    2369 | ADD (x_22627, x_22626) -> h_ADD x_22627 x_22626
    2370 | ADDC (x_22629, x_22628) -> h_ADDC x_22629 x_22628
    2371 | SUBB (x_22631, x_22630) -> h_SUBB x_22631 x_22630
    2372 | INC x_22632 -> h_INC x_22632
    2373 | DEC x_22633 -> h_DEC x_22633
    2374 | MUL (x_22635, x_22634) -> h_MUL x_22635 x_22634
    2375 | DIV (x_22637, x_22636) -> h_DIV x_22637 x_22636
    2376 | DA x_22638 -> h_DA x_22638
    2377 | JC x_22639 -> h_JC x_22639
    2378 | JNC x_22640 -> h_JNC x_22640
    2379 | JB (x_22642, x_22641) -> h_JB x_22642 x_22641
    2380 | JNB (x_22644, x_22643) -> h_JNB x_22644 x_22643
    2381 | JBC (x_22646, x_22645) -> h_JBC x_22646 x_22645
    2382 | JZ x_22647 -> h_JZ x_22647
    2383 | JNZ x_22648 -> h_JNZ x_22648
    2384 | CJNE (x_22650, x_22649) -> h_CJNE x_22650 x_22649
    2385 | DJNZ (x_22652, x_22651) -> h_DJNZ x_22652 x_22651
    2386 | ANL x_22653 -> h_ANL x_22653
    2387 | ORL x_22654 -> h_ORL x_22654
    2388 | XRL x_22655 -> h_XRL x_22655
    2389 | CLR x_22656 -> h_CLR x_22656
    2390 | CPL x_22657 -> h_CPL x_22657
    2391 | RL x_22658 -> h_RL x_22658
    2392 | RLC x_22659 -> h_RLC x_22659
    2393 | RR x_22660 -> h_RR x_22660
    2394 | RRC x_22661 -> h_RRC x_22661
    2395 | SWAP x_22662 -> h_SWAP x_22662
    2396 | MOV x_22663 -> h_MOV x_22663
    2397 | MOVX x_22664 -> h_MOVX x_22664
    2398 | SETB x_22665 -> h_SETB x_22665
    2399 | PUSH x_22666 -> h_PUSH x_22666
    2400 | POP x_22667 -> h_POP x_22667
    2401 | XCH (x_22669, x_22668) -> h_XCH x_22669 x_22668
    2402 | XCHD (x_22671, x_22670) -> h_XCHD x_22671 x_22670
     2365| ADD (x_17937, x_17936) -> h_ADD x_17937 x_17936
     2366| ADDC (x_17939, x_17938) -> h_ADDC x_17939 x_17938
     2367| SUBB (x_17941, x_17940) -> h_SUBB x_17941 x_17940
     2368| INC x_17942 -> h_INC x_17942
     2369| DEC x_17943 -> h_DEC x_17943
     2370| MUL (x_17945, x_17944) -> h_MUL x_17945 x_17944
     2371| DIV (x_17947, x_17946) -> h_DIV x_17947 x_17946
     2372| DA x_17948 -> h_DA x_17948
     2373| JC x_17949 -> h_JC x_17949
     2374| JNC x_17950 -> h_JNC x_17950
     2375| JB (x_17952, x_17951) -> h_JB x_17952 x_17951
     2376| JNB (x_17954, x_17953) -> h_JNB x_17954 x_17953
     2377| JBC (x_17956, x_17955) -> h_JBC x_17956 x_17955
     2378| JZ x_17957 -> h_JZ x_17957
     2379| JNZ x_17958 -> h_JNZ x_17958
     2380| CJNE (x_17960, x_17959) -> h_CJNE x_17960 x_17959
     2381| DJNZ (x_17962, x_17961) -> h_DJNZ x_17962 x_17961
     2382| ANL x_17963 -> h_ANL x_17963
     2383| ORL x_17964 -> h_ORL x_17964
     2384| XRL x_17965 -> h_XRL x_17965
     2385| CLR x_17966 -> h_CLR x_17966
     2386| CPL x_17967 -> h_CPL x_17967
     2387| RL x_17968 -> h_RL x_17968
     2388| RLC x_17969 -> h_RLC x_17969
     2389| RR x_17970 -> h_RR x_17970
     2390| RRC x_17971 -> h_RRC x_17971
     2391| SWAP x_17972 -> h_SWAP x_17972
     2392| MOV x_17973 -> h_MOV x_17973
     2393| MOVX x_17974 -> h_MOVX x_17974
     2394| SETB x_17975 -> h_SETB x_17975
     2395| PUSH x_17976 -> h_PUSH x_17976
     2396| POP x_17977 -> h_POP x_17977
     2397| XCH (x_17979, x_17978) -> h_XCH x_17979 x_17978
     2398| XCHD (x_17981, x_17980) -> h_XCHD x_17981 x_17980
    24032399| RET -> h_RET
    24042400| RETI -> h_RETI
    24052401| NOP -> h_NOP
    2406 | JMP x_22672 -> h_JMP x_22672
     2402| JMP x_17982 -> h_JMP x_17982
    24072403
    24082404(** val preinstruction_rect_Type3 :
     
    24422438    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    24432439let 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
    2444 | ADD (x_22713, x_22712) -> h_ADD x_22713 x_22712
    2445 | ADDC (x_22715, x_22714) -> h_ADDC x_22715 x_22714
    2446 | SUBB (x_22717, x_22716) -> h_SUBB x_22717 x_22716
    2447 | INC x_22718 -> h_INC x_22718
    2448 | DEC x_22719 -> h_DEC x_22719
    2449 | MUL (x_22721, x_22720) -> h_MUL x_22721 x_22720
    2450 | DIV (x_22723, x_22722) -> h_DIV x_22723 x_22722
    2451 | DA x_22724 -> h_DA x_22724
    2452 | JC x_22725 -> h_JC x_22725
    2453 | JNC x_22726 -> h_JNC x_22726
    2454 | JB (x_22728, x_22727) -> h_JB x_22728 x_22727
    2455 | JNB (x_22730, x_22729) -> h_JNB x_22730 x_22729
    2456 | JBC (x_22732, x_22731) -> h_JBC x_22732 x_22731
    2457 | JZ x_22733 -> h_JZ x_22733
    2458 | JNZ x_22734 -> h_JNZ x_22734
    2459 | CJNE (x_22736, x_22735) -> h_CJNE x_22736 x_22735
    2460 | DJNZ (x_22738, x_22737) -> h_DJNZ x_22738 x_22737
    2461 | ANL x_22739 -> h_ANL x_22739
    2462 | ORL x_22740 -> h_ORL x_22740
    2463 | XRL x_22741 -> h_XRL x_22741
    2464 | CLR x_22742 -> h_CLR x_22742
    2465 | CPL x_22743 -> h_CPL x_22743
    2466 | RL x_22744 -> h_RL x_22744
    2467 | RLC x_22745 -> h_RLC x_22745
    2468 | RR x_22746 -> h_RR x_22746
    2469 | RRC x_22747 -> h_RRC x_22747
    2470 | SWAP x_22748 -> h_SWAP x_22748
    2471 | MOV x_22749 -> h_MOV x_22749
    2472 | MOVX x_22750 -> h_MOVX x_22750
    2473 | SETB x_22751 -> h_SETB x_22751
    2474 | PUSH x_22752 -> h_PUSH x_22752
    2475 | POP x_22753 -> h_POP x_22753
    2476 | XCH (x_22755, x_22754) -> h_XCH x_22755 x_22754
    2477 | XCHD (x_22757, x_22756) -> h_XCHD x_22757 x_22756
     2440| ADD (x_18023, x_18022) -> h_ADD x_18023 x_18022
     2441| ADDC (x_18025, x_18024) -> h_ADDC x_18025 x_18024
     2442| SUBB (x_18027, x_18026) -> h_SUBB x_18027 x_18026
     2443| INC x_18028 -> h_INC x_18028
     2444| DEC x_18029 -> h_DEC x_18029
     2445| MUL (x_18031, x_18030) -> h_MUL x_18031 x_18030
     2446| DIV (x_18033, x_18032) -> h_DIV x_18033 x_18032
     2447| DA x_18034 -> h_DA x_18034
     2448| JC x_18035 -> h_JC x_18035
     2449| JNC x_18036 -> h_JNC x_18036
     2450| JB (x_18038, x_18037) -> h_JB x_18038 x_18037
     2451| JNB (x_18040, x_18039) -> h_JNB x_18040 x_18039
     2452| JBC (x_18042, x_18041) -> h_JBC x_18042 x_18041
     2453| JZ x_18043 -> h_JZ x_18043
     2454| JNZ x_18044 -> h_JNZ x_18044
     2455| CJNE (x_18046, x_18045) -> h_CJNE x_18046 x_18045
     2456| DJNZ (x_18048, x_18047) -> h_DJNZ x_18048 x_18047
     2457| ANL x_18049 -> h_ANL x_18049
     2458| ORL x_18050 -> h_ORL x_18050
     2459| XRL x_18051 -> h_XRL x_18051
     2460| CLR x_18052 -> h_CLR x_18052
     2461| CPL x_18053 -> h_CPL x_18053
     2462| RL x_18054 -> h_RL x_18054
     2463| RLC x_18055 -> h_RLC x_18055
     2464| RR x_18056 -> h_RR x_18056
     2465| RRC x_18057 -> h_RRC x_18057
     2466| SWAP x_18058 -> h_SWAP x_18058
     2467| MOV x_18059 -> h_MOV x_18059
     2468| MOVX x_18060 -> h_MOVX x_18060
     2469| SETB x_18061 -> h_SETB x_18061
     2470| PUSH x_18062 -> h_PUSH x_18062
     2471| POP x_18063 -> h_POP x_18063
     2472| XCH (x_18065, x_18064) -> h_XCH x_18065 x_18064
     2473| XCHD (x_18067, x_18066) -> h_XCHD x_18067 x_18066
    24782474| RET -> h_RET
    24792475| RETI -> h_RETI
    24802476| NOP -> h_NOP
    2481 | JMP x_22758 -> h_JMP x_22758
     2477| JMP x_18068 -> h_JMP x_18068
    24822478
    24832479(** val preinstruction_rect_Type2 :
     
    25172513    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    25182514let 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
    2519 | ADD (x_22799, x_22798) -> h_ADD x_22799 x_22798
    2520 | ADDC (x_22801, x_22800) -> h_ADDC x_22801 x_22800
    2521 | SUBB (x_22803, x_22802) -> h_SUBB x_22803 x_22802
    2522 | INC x_22804 -> h_INC x_22804
    2523 | DEC x_22805 -> h_DEC x_22805
    2524 | MUL (x_22807, x_22806) -> h_MUL x_22807 x_22806
    2525 | DIV (x_22809, x_22808) -> h_DIV x_22809 x_22808
    2526 | DA x_22810 -> h_DA x_22810
    2527 | JC x_22811 -> h_JC x_22811
    2528 | JNC x_22812 -> h_JNC x_22812
    2529 | JB (x_22814, x_22813) -> h_JB x_22814 x_22813
    2530 | JNB (x_22816, x_22815) -> h_JNB x_22816 x_22815
    2531 | JBC (x_22818, x_22817) -> h_JBC x_22818 x_22817
    2532 | JZ x_22819 -> h_JZ x_22819
    2533 | JNZ x_22820 -> h_JNZ x_22820
    2534 | CJNE (x_22822, x_22821) -> h_CJNE x_22822 x_22821
    2535 | DJNZ (x_22824, x_22823) -> h_DJNZ x_22824 x_22823
    2536 | ANL x_22825 -> h_ANL x_22825
    2537 | ORL x_22826 -> h_ORL x_22826
    2538 | XRL x_22827 -> h_XRL x_22827
    2539 | CLR x_22828 -> h_CLR x_22828
    2540 | CPL x_22829 -> h_CPL x_22829
    2541 | RL x_22830 -> h_RL x_22830
    2542 | RLC x_22831 -> h_RLC x_22831
    2543 | RR x_22832 -> h_RR x_22832
    2544 | RRC x_22833 -> h_RRC x_22833
    2545 | SWAP x_22834 -> h_SWAP x_22834
    2546 | MOV x_22835 -> h_MOV x_22835
    2547 | MOVX x_22836 -> h_MOVX x_22836
    2548 | SETB x_22837 -> h_SETB x_22837
    2549 | PUSH x_22838 -> h_PUSH x_22838
    2550 | POP x_22839 -> h_POP x_22839
    2551 | XCH (x_22841, x_22840) -> h_XCH x_22841 x_22840
    2552 | XCHD (x_22843, x_22842) -> h_XCHD x_22843 x_22842
     2515| ADD (x_18109, x_18108) -> h_ADD x_18109 x_18108
     2516| ADDC (x_18111, x_18110) -> h_ADDC x_18111 x_18110
     2517| SUBB (x_18113, x_18112) -> h_SUBB x_18113 x_18112
     2518| INC x_18114 -> h_INC x_18114
     2519| DEC x_18115 -> h_DEC x_18115
     2520| MUL (x_18117, x_18116) -> h_MUL x_18117 x_18116
     2521| DIV (x_18119, x_18118) -> h_DIV x_18119 x_18118
     2522| DA x_18120 -> h_DA x_18120
     2523| JC x_18121 -> h_JC x_18121
     2524| JNC x_18122 -> h_JNC x_18122
     2525| JB (x_18124, x_18123) -> h_JB x_18124 x_18123
     2526| JNB (x_18126, x_18125) -> h_JNB x_18126 x_18125
     2527| JBC (x_18128, x_18127) -> h_JBC x_18128 x_18127
     2528| JZ x_18129 -> h_JZ x_18129
     2529| JNZ x_18130 -> h_JNZ x_18130
     2530| CJNE (x_18132, x_18131) -> h_CJNE x_18132 x_18131
     2531| DJNZ (x_18134, x_18133) -> h_DJNZ x_18134 x_18133
     2532| ANL x_18135 -> h_ANL x_18135
     2533| ORL x_18136 -> h_ORL x_18136
     2534| XRL x_18137 -> h_XRL x_18137
     2535| CLR x_18138 -> h_CLR x_18138
     2536| CPL x_18139 -> h_CPL x_18139
     2537| RL x_18140 -> h_RL x_18140
     2538| RLC x_18141 -> h_RLC x_18141
     2539| RR x_18142 -> h_RR x_18142
     2540| RRC x_18143 -> h_RRC x_18143
     2541| SWAP x_18144 -> h_SWAP x_18144
     2542| MOV x_18145 -> h_MOV x_18145
     2543| MOVX x_18146 -> h_MOVX x_18146
     2544| SETB x_18147 -> h_SETB x_18147
     2545| PUSH x_18148 -> h_PUSH x_18148
     2546| POP x_18149 -> h_POP x_18149
     2547| XCH (x_18151, x_18150) -> h_XCH x_18151 x_18150
     2548| XCHD (x_18153, x_18152) -> h_XCHD x_18153 x_18152
    25532549| RET -> h_RET
    25542550| RETI -> h_RETI
    25552551| NOP -> h_NOP
    2556 | JMP x_22844 -> h_JMP x_22844
     2552| JMP x_18154 -> h_JMP x_18154
    25572553
    25582554(** val preinstruction_rect_Type1 :
     
    25922588    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    25932589let 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
    2594 | ADD (x_22885, x_22884) -> h_ADD x_22885 x_22884
    2595 | ADDC (x_22887, x_22886) -> h_ADDC x_22887 x_22886
    2596 | SUBB (x_22889, x_22888) -> h_SUBB x_22889 x_22888
    2597 | INC x_22890 -> h_INC x_22890
    2598 | DEC x_22891 -> h_DEC x_22891
    2599 | MUL (x_22893, x_22892) -> h_MUL x_22893 x_22892
    2600 | DIV (x_22895, x_22894) -> h_DIV x_22895 x_22894
    2601 | DA x_22896 -> h_DA x_22896
    2602 | JC x_22897 -> h_JC x_22897
    2603 | JNC x_22898 -> h_JNC x_22898
    2604 | JB (x_22900, x_22899) -> h_JB x_22900 x_22899
    2605 | JNB (x_22902, x_22901) -> h_JNB x_22902 x_22901
    2606 | JBC (x_22904, x_22903) -> h_JBC x_22904 x_22903
    2607 | JZ x_22905 -> h_JZ x_22905
    2608 | JNZ x_22906 -> h_JNZ x_22906
    2609 | CJNE (x_22908, x_22907) -> h_CJNE x_22908 x_22907
    2610 | DJNZ (x_22910, x_22909) -> h_DJNZ x_22910 x_22909
    2611 | ANL x_22911 -> h_ANL x_22911
    2612 | ORL x_22912 -> h_ORL x_22912
    2613 | XRL x_22913 -> h_XRL x_22913
    2614 | CLR x_22914 -> h_CLR x_22914
    2615 | CPL x_22915 -> h_CPL x_22915
    2616 | RL x_22916 -> h_RL x_22916
    2617 | RLC x_22917 -> h_RLC x_22917
    2618 | RR x_22918 -> h_RR x_22918
    2619 | RRC x_22919 -> h_RRC x_22919
    2620 | SWAP x_22920 -> h_SWAP x_22920
    2621 | MOV x_22921 -> h_MOV x_22921
    2622 | MOVX x_22922 -> h_MOVX x_22922
    2623 | SETB x_22923 -> h_SETB x_22923
    2624 | PUSH x_22924 -> h_PUSH x_22924
    2625 | POP x_22925 -> h_POP x_22925
    2626 | XCH (x_22927, x_22926) -> h_XCH x_22927 x_22926
    2627 | XCHD (x_22929, x_22928) -> h_XCHD x_22929 x_22928
     2590| ADD (x_18195, x_18194) -> h_ADD x_18195 x_18194
     2591| ADDC (x_18197, x_18196) -> h_ADDC x_18197 x_18196
     2592| SUBB (x_18199, x_18198) -> h_SUBB x_18199 x_18198
     2593| INC x_18200 -> h_INC x_18200
     2594| DEC x_18201 -> h_DEC x_18201
     2595| MUL (x_18203, x_18202) -> h_MUL x_18203 x_18202
     2596| DIV (x_18205, x_18204) -> h_DIV x_18205 x_18204
     2597| DA x_18206 -> h_DA x_18206
     2598| JC x_18207 -> h_JC x_18207
     2599| JNC x_18208 -> h_JNC x_18208
     2600| JB (x_18210, x_18209) -> h_JB x_18210 x_18209
     2601| JNB (x_18212, x_18211) -> h_JNB x_18212 x_18211
     2602| JBC (x_18214, x_18213) -> h_JBC x_18214 x_18213
     2603| JZ x_18215 -> h_JZ x_18215
     2604| JNZ x_18216 -> h_JNZ x_18216
     2605| CJNE (x_18218, x_18217) -> h_CJNE x_18218 x_18217
     2606| DJNZ (x_18220, x_18219) -> h_DJNZ x_18220 x_18219
     2607| ANL x_18221 -> h_ANL x_18221
     2608| ORL x_18222 -> h_ORL x_18222
     2609| XRL x_18223 -> h_XRL x_18223
     2610| CLR x_18224 -> h_CLR x_18224
     2611| CPL x_18225 -> h_CPL x_18225
     2612| RL x_18226 -> h_RL x_18226
     2613| RLC x_18227 -> h_RLC x_18227
     2614| RR x_18228 -> h_RR x_18228
     2615| RRC x_18229 -> h_RRC x_18229
     2616| SWAP x_18230 -> h_SWAP x_18230
     2617| MOV x_18231 -> h_MOV x_18231
     2618| MOVX x_18232 -> h_MOVX x_18232
     2619| SETB x_18233 -> h_SETB x_18233
     2620| PUSH x_18234 -> h_PUSH x_18234
     2621| POP x_18235 -> h_POP x_18235
     2622| XCH (x_18237, x_18236) -> h_XCH x_18237 x_18236
     2623| XCHD (x_18239, x_18238) -> h_XCHD x_18239 x_18238
    26282624| RET -> h_RET
    26292625| RETI -> h_RETI
    26302626| NOP -> h_NOP
    2631 | JMP x_22930 -> h_JMP x_22930
     2627| JMP x_18240 -> h_JMP x_18240
    26322628
    26332629(** val preinstruction_rect_Type0 :
     
    26672663    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    26682664let 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
    2669 | ADD (x_22971, x_22970) -> h_ADD x_22971 x_22970
    2670 | ADDC (x_22973, x_22972) -> h_ADDC x_22973 x_22972
    2671 | SUBB (x_22975, x_22974) -> h_SUBB x_22975 x_22974
    2672 | INC x_22976 -> h_INC x_22976
    2673 | DEC x_22977 -> h_DEC x_22977
    2674 | MUL (x_22979, x_22978) -> h_MUL x_22979 x_22978
    2675 | DIV (x_22981, x_22980) -> h_DIV x_22981 x_22980
    2676 | DA x_22982 -> h_DA x_22982
    2677 | JC x_22983 -> h_JC x_22983
    2678 | JNC x_22984 -> h_JNC x_22984
    2679 | JB (x_22986, x_22985) -> h_JB x_22986 x_22985
    2680 | JNB (x_22988, x_22987) -> h_JNB x_22988 x_22987
    2681 | JBC (x_22990, x_22989) -> h_JBC x_22990 x_22989
    2682 | JZ x_22991 -> h_JZ x_22991
    2683 | JNZ x_22992 -> h_JNZ x_22992
    2684 | CJNE (x_22994, x_22993) -> h_CJNE x_22994 x_22993
    2685 | DJNZ (x_22996, x_22995) -> h_DJNZ x_22996 x_22995
    2686 | ANL x_22997 -> h_ANL x_22997
    2687 | ORL x_22998 -> h_ORL x_22998
    2688 | XRL x_22999 -> h_XRL x_22999
    2689 | CLR x_23000 -> h_CLR x_23000
    2690 | CPL x_23001 -> h_CPL x_23001
    2691 | RL x_23002 -> h_RL x_23002
    2692 | RLC x_23003 -> h_RLC x_23003
    2693 | RR x_23004 -> h_RR x_23004
    2694 | RRC x_23005 -> h_RRC x_23005
    2695 | SWAP x_23006 -> h_SWAP x_23006
    2696 | MOV x_23007 -> h_MOV x_23007
    2697 | MOVX x_23008 -> h_MOVX x_23008
    2698 | SETB x_23009 -> h_SETB x_23009
    2699 | PUSH x_23010 -> h_PUSH x_23010
    2700 | POP x_23011 -> h_POP x_23011
    2701 | XCH (x_23013, x_23012) -> h_XCH x_23013 x_23012
    2702 | XCHD (x_23015, x_23014) -> h_XCHD x_23015 x_23014
     2665| ADD (x_18281, x_18280) -> h_ADD x_18281 x_18280
     2666| ADDC (x_18283, x_18282) -> h_ADDC x_18283 x_18282
     2667| SUBB (x_18285, x_18284) -> h_SUBB x_18285 x_18284
     2668| INC x_18286 -> h_INC x_18286
     2669| DEC x_18287 -> h_DEC x_18287
     2670| MUL (x_18289, x_18288) -> h_MUL x_18289 x_18288
     2671| DIV (x_18291, x_18290) -> h_DIV x_18291 x_18290
     2672| DA x_18292 -> h_DA x_18292
     2673| JC x_18293 -> h_JC x_18293
     2674| JNC x_18294 -> h_JNC x_18294
     2675| JB (x_18296, x_18295) -> h_JB x_18296 x_18295
     2676| JNB (x_18298, x_18297) -> h_JNB x_18298 x_18297
     2677| JBC (x_18300, x_18299) -> h_JBC x_18300 x_18299
     2678| JZ x_18301 -> h_JZ x_18301
     2679| JNZ x_18302 -> h_JNZ x_18302
     2680| CJNE (x_18304, x_18303) -> h_CJNE x_18304 x_18303
     2681| DJNZ (x_18306, x_18305) -> h_DJNZ x_18306 x_18305
     2682| ANL x_18307 -> h_ANL x_18307
     2683| ORL x_18308 -> h_ORL x_18308
     2684| XRL x_18309 -> h_XRL x_18309
     2685| CLR x_18310 -> h_CLR x_18310
     2686| CPL x_18311 -> h_CPL x_18311
     2687| RL x_18312 -> h_RL x_18312
     2688| RLC x_18313 -> h_RLC x_18313
     2689| RR x_18314 -> h_RR x_18314
     2690| RRC x_18315 -> h_RRC x_18315
     2691| SWAP x_18316 -> h_SWAP x_18316
     2692| MOV x_18317 -> h_MOV x_18317
     2693| MOVX x_18318 -> h_MOVX x_18318
     2694| SETB x_18319 -> h_SETB x_18319
     2695| PUSH x_18320 -> h_PUSH x_18320
     2696| POP x_18321 -> h_POP x_18321
     2697| XCH (x_18323, x_18322) -> h_XCH x_18323 x_18322
     2698| XCHD (x_18325, x_18324) -> h_XCHD x_18325 x_18324
    27032699| RET -> h_RET
    27042700| RETI -> h_RETI
    27052701| NOP -> h_NOP
    2706 | JMP x_23016 -> h_JMP x_23016
     2702| JMP x_18326 -> h_JMP x_18326
    27072703
    27082704(** val preinstruction_inv_rect_Type4 :
     
    51085104    'a1 **)
    51095105let rec instruction_rect_Type4 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    5110 | ACALL x_23588 -> h_ACALL x_23588
    5111 | LCALL x_23589 -> h_LCALL x_23589
    5112 | AJMP x_23590 -> h_AJMP x_23590
    5113 | LJMP x_23591 -> h_LJMP x_23591
    5114 | SJMP x_23592 -> h_SJMP x_23592
    5115 | MOVC (x_23594, x_23593) -> h_MOVC x_23594 x_23593
    5116 | RealInstruction x_23595 -> h_RealInstruction x_23595
     5106| ACALL x_18898 -> h_ACALL x_18898
     5107| LCALL x_18899 -> h_LCALL x_18899
     5108| AJMP x_18900 -> h_AJMP x_18900
     5109| LJMP x_18901 -> h_LJMP x_18901
     5110| SJMP x_18902 -> h_SJMP x_18902
     5111| MOVC (x_18904, x_18903) -> h_MOVC x_18904 x_18903
     5112| RealInstruction x_18905 -> h_RealInstruction x_18905
    51175113
    51185114(** val instruction_rect_Type5 :
     
    51235119    'a1 **)
    51245120let rec instruction_rect_Type5 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    5125 | ACALL x_23604 -> h_ACALL x_23604
    5126 | LCALL x_23605 -> h_LCALL x_23605
    5127 | AJMP x_23606 -> h_AJMP x_23606
    5128 | LJMP x_23607 -> h_LJMP x_23607
    5129 | SJMP x_23608 -> h_SJMP x_23608
    5130 | MOVC (x_23610, x_23609) -> h_MOVC x_23610 x_23609
    5131 | RealInstruction x_23611 -> h_RealInstruction x_23611
     5121| ACALL x_18914 -> h_ACALL x_18914
     5122| LCALL x_18915 -> h_LCALL x_18915
     5123| AJMP x_18916 -> h_AJMP x_18916
     5124| LJMP x_18917 -> h_LJMP x_18917
     5125| SJMP x_18918 -> h_SJMP x_18918
     5126| MOVC (x_18920, x_18919) -> h_MOVC x_18920 x_18919
     5127| RealInstruction x_18921 -> h_RealInstruction x_18921
    51325128
    51335129(** val instruction_rect_Type3 :
     
    51385134    'a1 **)
    51395135let rec instruction_rect_Type3 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    5140 | ACALL x_23620 -> h_ACALL x_23620
    5141 | LCALL x_23621 -> h_LCALL x_23621
    5142 | AJMP x_23622 -> h_AJMP x_23622
    5143 | LJMP x_23623 -> h_LJMP x_23623
    5144 | SJMP x_23624 -> h_SJMP x_23624
    5145 | MOVC (x_23626, x_23625) -> h_MOVC x_23626 x_23625
    5146 | RealInstruction x_23627 -> h_RealInstruction x_23627
     5136| ACALL x_18930 -> h_ACALL x_18930
     5137| LCALL x_18931 -> h_LCALL x_18931
     5138| AJMP x_18932 -> h_AJMP x_18932
     5139| LJMP x_18933 -> h_LJMP x_18933
     5140| SJMP x_18934 -> h_SJMP x_18934
     5141| MOVC (x_18936, x_18935) -> h_MOVC x_18936 x_18935
     5142| RealInstruction x_18937 -> h_RealInstruction x_18937
    51475143
    51485144(** val instruction_rect_Type2 :
     
    51535149    'a1 **)
    51545150let rec instruction_rect_Type2 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    5155 | ACALL x_23636 -> h_ACALL x_23636
    5156 | LCALL x_23637 -> h_LCALL x_23637
    5157 | AJMP x_23638 -> h_AJMP x_23638
    5158 | LJMP x_23639 -> h_LJMP x_23639
    5159 | SJMP x_23640 -> h_SJMP x_23640
    5160 | MOVC (x_23642, x_23641) -> h_MOVC x_23642 x_23641
    5161 | RealInstruction x_23643 -> h_RealInstruction x_23643
     5151| ACALL x_18946 -> h_ACALL x_18946
     5152| LCALL x_18947 -> h_LCALL x_18947
     5153| AJMP x_18948 -> h_AJMP x_18948
     5154| LJMP x_18949 -> h_LJMP x_18949
     5155| SJMP x_18950 -> h_SJMP x_18950
     5156| MOVC (x_18952, x_18951) -> h_MOVC x_18952 x_18951
     5157| RealInstruction x_18953 -> h_RealInstruction x_18953
    51625158
    51635159(** val instruction_rect_Type1 :
     
    51685164    'a1 **)
    51695165let rec instruction_rect_Type1 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    5170 | ACALL x_23652 -> h_ACALL x_23652
    5171 | LCALL x_23653 -> h_LCALL x_23653
    5172 | AJMP x_23654 -> h_AJMP x_23654
    5173 | LJMP x_23655 -> h_LJMP x_23655
    5174 | SJMP x_23656 -> h_SJMP x_23656
    5175 | MOVC (x_23658, x_23657) -> h_MOVC x_23658 x_23657
    5176 | RealInstruction x_23659 -> h_RealInstruction x_23659
     5166| ACALL x_18962 -> h_ACALL x_18962
     5167| LCALL x_18963 -> h_LCALL x_18963
     5168| AJMP x_18964 -> h_AJMP x_18964
     5169| LJMP x_18965 -> h_LJMP x_18965
     5170| SJMP x_18966 -> h_SJMP x_18966
     5171| MOVC (x_18968, x_18967) -> h_MOVC x_18968 x_18967
     5172| RealInstruction x_18969 -> h_RealInstruction x_18969
    51775173
    51785174(** val instruction_rect_Type0 :
     
    51835179    'a1 **)
    51845180let rec instruction_rect_Type0 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    5185 | ACALL x_23668 -> h_ACALL x_23668
    5186 | LCALL x_23669 -> h_LCALL x_23669
    5187 | AJMP x_23670 -> h_AJMP x_23670
    5188 | LJMP x_23671 -> h_LJMP x_23671
    5189 | SJMP x_23672 -> h_SJMP x_23672
    5190 | MOVC (x_23674, x_23673) -> h_MOVC x_23674 x_23673
    5191 | RealInstruction x_23675 -> h_RealInstruction x_23675
     5181| ACALL x_18978 -> h_ACALL x_18978
     5182| LCALL x_18979 -> h_LCALL x_18979
     5183| AJMP x_18980 -> h_AJMP x_18980
     5184| LJMP x_18981 -> h_LJMP x_18981
     5185| SJMP x_18982 -> h_SJMP x_18982
     5186| MOVC (x_18984, x_18983) -> h_MOVC x_18984 x_18983
     5187| RealInstruction x_18985 -> h_RealInstruction x_18985
    51925188
    51935189(** val instruction_inv_rect_Type4 :
     
    54635459
    54645460type pseudo_instruction =
    5465 | Instruction of identifier0 preinstruction
     5461| Instruction of identifier preinstruction
    54665462| Comment of String.string
    54675463| Cost of CostLabel.costlabel
    5468 | Jmp of identifier0
    5469 | Jnz of subaddressing_mode * identifier0 * identifier0
    5470 | MovSuccessor of subaddressing_mode * word_side * identifier0
    5471 | Call of identifier0
    5472 | Mov of subaddressing_mode * identifier0
     5464| Jmp of identifier
     5465| Jnz of subaddressing_mode * identifier * identifier
     5466| MovSuccessor of subaddressing_mode * word_side * identifier
     5467| Call of identifier
     5468| Mov of subaddressing_mode * identifier
    54735469
    54745470(** val pseudo_instruction_rect_Type4 :
    5475     (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    5476     (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) ->
    5477     (subaddressing_mode -> identifier0 -> identifier0 -> 'a1) ->
    5478     (subaddressing_mode -> word_side -> identifier0 -> 'a1) -> (identifier0
    5479     -> 'a1) -> (subaddressing_mode -> identifier0 -> 'a1) ->
    5480     pseudo_instruction -> 'a1 **)
     5471    (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
     5472    (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) ->
     5473    (subaddressing_mode -> identifier -> identifier -> 'a1) ->
     5474    (subaddressing_mode -> word_side -> identifier -> 'a1) -> (identifier ->
     5475    'a1) -> (subaddressing_mode -> identifier -> 'a1) -> pseudo_instruction
     5476    -> 'a1 **)
    54815477let rec pseudo_instruction_rect_Type4 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5482 | Instruction x_23841 -> h_Instruction x_23841
    5483 | Comment x_23842 -> h_Comment x_23842
    5484 | Cost x_23843 -> h_Cost x_23843
    5485 | Jmp x_23844 -> h_Jmp x_23844
    5486 | Jnz (x_23847, x_23846, x_23845) -> h_Jnz x_23847 x_23846 x_23845
    5487 | MovSuccessor (x_23850, x_23849, x_23848) ->
    5488   h_MovSuccessor x_23850 x_23849 x_23848
    5489 | Call x_23851 -> h_Call x_23851
    5490 | Mov (x_23853, x_23852) -> h_Mov x_23853 x_23852
     5478| Instruction x_19151 -> h_Instruction x_19151
     5479| Comment x_19152 -> h_Comment x_19152
     5480| Cost x_19153 -> h_Cost x_19153
     5481| Jmp x_19154 -> h_Jmp x_19154
     5482| Jnz (x_19157, x_19156, x_19155) -> h_Jnz x_19157 x_19156 x_19155
     5483| MovSuccessor (x_19160, x_19159, x_19158) ->
     5484  h_MovSuccessor x_19160 x_19159 x_19158
     5485| Call x_19161 -> h_Call x_19161
     5486| Mov (x_19163, x_19162) -> h_Mov x_19163 x_19162
    54915487
    54925488(** val pseudo_instruction_rect_Type5 :
    5493     (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    5494     (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) ->
    5495     (subaddressing_mode -> identifier0 -> identifier0 -> 'a1) ->
    5496     (subaddressing_mode -> word_side -> identifier0 -> 'a1) -> (identifier0
    5497     -> 'a1) -> (subaddressing_mode -> identifier0 -> 'a1) ->
    5498     pseudo_instruction -> 'a1 **)
     5489    (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
     5490    (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) ->
     5491    (subaddressing_mode -> identifier -> identifier -> 'a1) ->
     5492    (subaddressing_mode -> word_side -> identifier -> 'a1) -> (identifier ->
     5493    'a1) -> (subaddressing_mode -> identifier -> 'a1) -> pseudo_instruction
     5494    -> 'a1 **)
    54995495let rec pseudo_instruction_rect_Type5 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5500 | Instruction x_23863 -> h_Instruction x_23863
    5501 | Comment x_23864 -> h_Comment x_23864
    5502 | Cost x_23865 -> h_Cost x_23865
    5503 | Jmp x_23866 -> h_Jmp x_23866
    5504 | Jnz (x_23869, x_23868, x_23867) -> h_Jnz x_23869 x_23868 x_23867
    5505 | MovSuccessor (x_23872, x_23871, x_23870) ->
    5506   h_MovSuccessor x_23872 x_23871 x_23870
    5507 | Call x_23873 -> h_Call x_23873
    5508 | Mov (x_23875, x_23874) -> h_Mov x_23875 x_23874
     5496| Instruction x_19173 -> h_Instruction x_19173
     5497| Comment x_19174 -> h_Comment x_19174
     5498| Cost x_19175 -> h_Cost x_19175
     5499| Jmp x_19176 -> h_Jmp x_19176
     5500| Jnz (x_19179, x_19178, x_19177) -> h_Jnz x_19179 x_19178 x_19177
     5501| MovSuccessor (x_19182, x_19181, x_19180) ->
     5502  h_MovSuccessor x_19182 x_19181 x_19180
     5503| Call x_19183 -> h_Call x_19183
     5504| Mov (x_19185, x_19184) -> h_Mov x_19185 x_19184
    55095505
    55105506(** val pseudo_instruction_rect_Type3 :
    5511     (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    5512     (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) ->
    5513     (subaddressing_mode -> identifier0 -> identifier0 -> 'a1) ->
    5514     (subaddressing_mode -> word_side -> identifier0 -> 'a1) -> (identifier0
    5515     -> 'a1) -> (subaddressing_mode -> identifier0 -> 'a1) ->
    5516     pseudo_instruction -> 'a1 **)
     5507    (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
     5508    (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) ->
     5509    (subaddressing_mode -> identifier -> identifier -> 'a1) ->
     5510    (subaddressing_mode -> word_side -> identifier -> 'a1) -> (identifier ->
     5511    'a1) -> (subaddressing_mode -> identifier -> 'a1) -> pseudo_instruction
     5512    -> 'a1 **)
    55175513let rec pseudo_instruction_rect_Type3 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5518 | Instruction x_23885 -> h_Instruction x_23885
    5519 | Comment x_23886 -> h_Comment x_23886
    5520 | Cost x_23887 -> h_Cost x_23887
    5521 | Jmp x_23888 -> h_Jmp x_23888
    5522 | Jnz (x_23891, x_23890, x_23889) -> h_Jnz x_23891 x_23890 x_23889
    5523 | MovSuccessor (x_23894, x_23893, x_23892) ->
    5524   h_MovSuccessor x_23894 x_23893 x_23892
    5525 | Call x_23895 -> h_Call x_23895
    5526 | Mov (x_23897, x_23896) -> h_Mov x_23897 x_23896
     5514| Instruction x_19195 -> h_Instruction x_19195
     5515| Comment x_19196 -> h_Comment x_19196
     5516| Cost x_19197 -> h_Cost x_19197
     5517| Jmp x_19198 -> h_Jmp x_19198
     5518| Jnz (x_19201, x_19200, x_19199) -> h_Jnz x_19201 x_19200 x_19199
     5519| MovSuccessor (x_19204, x_19203, x_19202) ->
     5520  h_MovSuccessor x_19204 x_19203 x_19202
     5521| Call x_19205 -> h_Call x_19205
     5522| Mov (x_19207, x_19206) -> h_Mov x_19207 x_19206
    55275523
    55285524(** val pseudo_instruction_rect_Type2 :
    5529     (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    5530     (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) ->
    5531     (subaddressing_mode -> identifier0 -> identifier0 -> 'a1) ->
    5532     (subaddressing_mode -> word_side -> identifier0 -> 'a1) -> (identifier0
    5533     -> 'a1) -> (subaddressing_mode -> identifier0 -> 'a1) ->
    5534     pseudo_instruction -> 'a1 **)
     5525    (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
     5526    (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) ->
     5527    (subaddressing_mode -> identifier -> identifier -> 'a1) ->
     5528    (subaddressing_mode -> word_side -> identifier -> 'a1) -> (identifier ->
     5529    'a1) -> (subaddressing_mode -> identifier -> 'a1) -> pseudo_instruction
     5530    -> 'a1 **)
    55355531let rec pseudo_instruction_rect_Type2 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5536 | Instruction x_23907 -> h_Instruction x_23907
    5537 | Comment x_23908 -> h_Comment x_23908
    5538 | Cost x_23909 -> h_Cost x_23909
    5539 | Jmp x_23910 -> h_Jmp x_23910
    5540 | Jnz (x_23913, x_23912, x_23911) -> h_Jnz x_23913 x_23912 x_23911
    5541 | MovSuccessor (x_23916, x_23915, x_23914) ->
    5542   h_MovSuccessor x_23916 x_23915 x_23914
    5543 | Call x_23917 -> h_Call x_23917
    5544 | Mov (x_23919, x_23918) -> h_Mov x_23919 x_23918
     5532| Instruction x_19217 -> h_Instruction x_19217
     5533| Comment x_19218 -> h_Comment x_19218
     5534| Cost x_19219 -> h_Cost x_19219
     5535| Jmp x_19220 -> h_Jmp x_19220
     5536| Jnz (x_19223, x_19222, x_19221) -> h_Jnz x_19223 x_19222 x_19221
     5537| MovSuccessor (x_19226, x_19225, x_19224) ->
     5538  h_MovSuccessor x_19226 x_19225 x_19224
     5539| Call x_19227 -> h_Call x_19227
     5540| Mov (x_19229, x_19228) -> h_Mov x_19229 x_19228
    55455541
    55465542(** val pseudo_instruction_rect_Type1 :
    5547     (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    5548     (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) ->
    5549     (subaddressing_mode -> identifier0 -> identifier0 -> 'a1) ->
    5550     (subaddressing_mode -> word_side -> identifier0 -> 'a1) -> (identifier0
    5551     -> 'a1) -> (subaddressing_mode -> identifier0 -> 'a1) ->
    5552     pseudo_instruction -> 'a1 **)
     5543    (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
     5544    (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) ->
     5545    (subaddressing_mode -> identifier -> identifier -> 'a1) ->
     5546    (subaddressing_mode -> word_side -> identifier -> 'a1) -> (identifier ->
     5547    'a1) -> (subaddressing_mode -> identifier -> 'a1) -> pseudo_instruction
     5548    -> 'a1 **)
    55535549let rec pseudo_instruction_rect_Type1 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5554 | Instruction x_23929 -> h_Instruction x_23929
    5555 | Comment x_23930 -> h_Comment x_23930
    5556 | Cost x_23931 -> h_Cost x_23931
    5557 | Jmp x_23932 -> h_Jmp x_23932
    5558 | Jnz (x_23935, x_23934, x_23933) -> h_Jnz x_23935 x_23934 x_23933
    5559 | MovSuccessor (x_23938, x_23937, x_23936) ->
    5560   h_MovSuccessor x_23938 x_23937 x_23936
    5561 | Call x_23939 -> h_Call x_23939
    5562 | Mov (x_23941, x_23940) -> h_Mov x_23941 x_23940
     5550| Instruction x_19239 -> h_Instruction x_19239
     5551| Comment x_19240 -> h_Comment x_19240
     5552| Cost x_19241 -> h_Cost x_19241
     5553| Jmp x_19242 -> h_Jmp x_19242
     5554| Jnz (x_19245, x_19244, x_19243) -> h_Jnz x_19245 x_19244 x_19243
     5555| MovSuccessor (x_19248, x_19247, x_19246) ->
     5556  h_MovSuccessor x_19248 x_19247 x_19246
     5557| Call x_19249 -> h_Call x_19249
     5558| Mov (x_19251, x_19250) -> h_Mov x_19251 x_19250
    55635559
    55645560(** val pseudo_instruction_rect_Type0 :
    5565     (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    5566     (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) ->
    5567     (subaddressing_mode -> identifier0 -> identifier0 -> 'a1) ->
    5568     (subaddressing_mode -> word_side -> identifier0 -> 'a1) -> (identifier0
    5569     -> 'a1) -> (subaddressing_mode -> identifier0 -> 'a1) ->
    5570     pseudo_instruction -> 'a1 **)
     5561    (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
     5562    (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) ->
     5563    (subaddressing_mode -> identifier -> identifier -> 'a1) ->
     5564    (subaddressing_mode -> word_side -> identifier -> 'a1) -> (identifier ->
     5565    'a1) -> (subaddressing_mode -> identifier -> 'a1) -> pseudo_instruction
     5566    -> 'a1 **)
    55715567let rec pseudo_instruction_rect_Type0 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5572 | Instruction x_23951 -> h_Instruction x_23951
    5573 | Comment x_23952 -> h_Comment x_23952
    5574 | Cost x_23953 -> h_Cost x_23953
    5575 | Jmp x_23954 -> h_Jmp x_23954
    5576 | Jnz (x_23957, x_23956, x_23955) -> h_Jnz x_23957 x_23956 x_23955
    5577 | MovSuccessor (x_23960, x_23959, x_23958) ->
    5578   h_MovSuccessor x_23960 x_23959 x_23958
    5579 | Call x_23961 -> h_Call x_23961
    5580 | Mov (x_23963, x_23962) -> h_Mov x_23963 x_23962
     5568| Instruction x_19261 -> h_Instruction x_19261
     5569| Comment x_19262 -> h_Comment x_19262
     5570| Cost x_19263 -> h_Cost x_19263
     5571| Jmp x_19264 -> h_Jmp x_19264
     5572| Jnz (x_19267, x_19266, x_19265) -> h_Jnz x_19267 x_19266 x_19265
     5573| MovSuccessor (x_19270, x_19269, x_19268) ->
     5574  h_MovSuccessor x_19270 x_19269 x_19268
     5575| Call x_19271 -> h_Call x_19271
     5576| Mov (x_19273, x_19272) -> h_Mov x_19273 x_19272
    55815577
    55825578(** val pseudo_instruction_inv_rect_Type4 :
    5583     pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
     5579    pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
    55845580    (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
    5585     (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
    5586     identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
    5587     identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
    5588     (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1 **)
     5581    (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
     5582    identifier -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
     5583    identifier -> __ -> 'a1) -> (identifier -> __ -> 'a1) ->
     5584    (subaddressing_mode -> identifier -> __ -> 'a1) -> 'a1 **)
    55895585let pseudo_instruction_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
    55905586  let hcut = pseudo_instruction_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 hterm in
     
    55925588
    55935589(** val pseudo_instruction_inv_rect_Type3 :
    5594     pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
     5590    pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
    55955591    (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
    5596     (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
    5597     identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
    5598     identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
    5599     (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1 **)
     5592    (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
     5593    identifier -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
     5594    identifier -> __ -> 'a1) -> (identifier -> __ -> 'a1) ->
     5595    (subaddressing_mode -> identifier -> __ -> 'a1) -> 'a1 **)
    56005596let pseudo_instruction_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
    56015597  let hcut = pseudo_instruction_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 hterm in
     
    56035599
    56045600(** val pseudo_instruction_inv_rect_Type2 :
    5605     pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
     5601    pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
    56065602    (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
    5607     (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
    5608     identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
    5609     identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
    5610     (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1 **)
     5603    (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
     5604    identifier -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
     5605    identifier -> __ -> 'a1) -> (identifier -> __ -> 'a1) ->
     5606    (subaddressing_mode -> identifier -> __ -> 'a1) -> 'a1 **)
    56115607let pseudo_instruction_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
    56125608  let hcut = pseudo_instruction_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 hterm in
     
    56145610
    56155611(** val pseudo_instruction_inv_rect_Type1 :
    5616     pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
     5612    pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
    56175613    (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
    5618     (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
    5619     identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
    5620     identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
    5621     (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1 **)
     5614    (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
     5615    identifier -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
     5616    identifier -> __ -> 'a1) -> (identifier -> __ -> 'a1) ->
     5617    (subaddressing_mode -> identifier -> __ -> 'a1) -> 'a1 **)
    56225618let pseudo_instruction_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
    56235619  let hcut = pseudo_instruction_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 hterm in
     
    56255621
    56265622(** val pseudo_instruction_inv_rect_Type0 :
    5627     pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
     5623    pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
    56285624    (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
    5629     (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
    5630     identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
    5631     identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
    5632     (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1 **)
     5625    (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
     5626    identifier -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
     5627    identifier -> __ -> 'a1) -> (identifier -> __ -> 'a1) ->
     5628    (subaddressing_mode -> identifier -> __ -> 'a1) -> 'a1 **)
    56335629let pseudo_instruction_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
    56345630  let hcut = pseudo_instruction_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 hterm in
     
    56655661type labelled_instruction = pseudo_instruction LabelledObjects.labelled_obj
    56665662
    5667 type preamble = (identifier0, BitVector.word) Types.prod List.list
    5668 
    56695663type assembly_program = instruction List.list
    56705664
    5671 type pseudo_assembly_program =
    5672   (preamble, labelled_instruction List.list) Types.prod
    5673 
    5674 (** val is_jump' : identifier0 preinstruction -> Bool.bool **)
     5665(** val fetch_pseudo_instruction :
     5666    labelled_instruction List.list -> BitVector.word -> (pseudo_instruction,
     5667    BitVector.word) Types.prod **)
     5668let fetch_pseudo_instruction code_mem pc =
     5669  let { Types.fst = lbl; Types.snd = instr } =
     5670    Util.nth_safe
     5671      (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5672        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5673        Nat.O)))))))))))))))) pc) code_mem
     5674  in
     5675  let new_pc =
     5676    Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5677      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5678      Nat.O)))))))))))))))) pc
     5679      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5680        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5681        Nat.O)))))))))))))))) (Nat.S Nat.O))
     5682  in
     5683  { Types.fst = instr; Types.snd = new_pc }
     5684
     5685(** val is_jump' : identifier preinstruction -> Bool.bool **)
    56755686let is_jump' = function
    56765687| ADD (x0, x1) -> Bool.False
     
    57465757| Mov (x, x0) -> Bool.False
    57475758
     5759(** val asm_cost_label :
     5760    labelled_instruction List.list -> BitVector.word Types.sig0 ->
     5761    CostLabel.costlabel Types.option **)
     5762let asm_cost_label mem w_prf =
     5763  match (fetch_pseudo_instruction mem (Types.pi1 w_prf)).Types.fst with
     5764  | Instruction x -> Types.None
     5765  | Comment x -> Types.None
     5766  | Cost c -> Types.Some c
     5767  | Jmp x -> Types.None
     5768  | Jnz (x, x0, x1) -> Types.None
     5769  | MovSuccessor (x, x0, x1) -> Types.None
     5770  | Call x -> Types.None
     5771  | Mov (x, x0) -> Types.None
     5772
     5773(** val aDDRESS_WIDTH : Nat.nat **)
     5774let aDDRESS_WIDTH =
     5775  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5776    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))
     5777
     5778(** val mAX_CODE_SIZE : Nat.nat **)
     5779let mAX_CODE_SIZE =
     5780  Exp.exp (Nat.S (Nat.S Nat.O)) aDDRESS_WIDTH
     5781
     5782(** val code_size_opt : labelled_instruction List.list -> __ Types.option **)
     5783let code_size_opt code =
     5784  Extranat.nat_bound_opt mAX_CODE_SIZE (Nat.S (List.length code))
     5785
     5786type pseudo_assembly_program = { preamble : (identifier, BitVector.word)
     5787                                            Types.prod List.list;
     5788                                 code : labelled_instruction List.list;
     5789                                 renamed_symbols : (identifier, AST.ident)
     5790                                                   Types.prod List.list;
     5791                                 final_label : identifier }
     5792
     5793(** val pseudo_assembly_program_rect_Type4 :
     5794    ((identifier, BitVector.word) Types.prod List.list ->
     5795    labelled_instruction List.list -> __ -> (identifier, AST.ident)
     5796    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
     5797    pseudo_assembly_program -> 'a1 **)
     5798let rec pseudo_assembly_program_rect_Type4 h_mk_pseudo_assembly_program x_19416 =
     5799  let { preamble = preamble0; code = code0; renamed_symbols =
     5800    renamed_symbols0; final_label = final_label0 } = x_19416
     5801  in
     5802  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     5803    final_label0 __ __
     5804
     5805(** val pseudo_assembly_program_rect_Type5 :
     5806    ((identifier, BitVector.word) Types.prod List.list ->
     5807    labelled_instruction List.list -> __ -> (identifier, AST.ident)
     5808    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
     5809    pseudo_assembly_program -> 'a1 **)
     5810let rec pseudo_assembly_program_rect_Type5 h_mk_pseudo_assembly_program x_19418 =
     5811  let { preamble = preamble0; code = code0; renamed_symbols =
     5812    renamed_symbols0; final_label = final_label0 } = x_19418
     5813  in
     5814  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     5815    final_label0 __ __
     5816
     5817(** val pseudo_assembly_program_rect_Type3 :
     5818    ((identifier, BitVector.word) Types.prod List.list ->
     5819    labelled_instruction List.list -> __ -> (identifier, AST.ident)
     5820    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
     5821    pseudo_assembly_program -> 'a1 **)
     5822let rec pseudo_assembly_program_rect_Type3 h_mk_pseudo_assembly_program x_19420 =
     5823  let { preamble = preamble0; code = code0; renamed_symbols =
     5824    renamed_symbols0; final_label = final_label0 } = x_19420
     5825  in
     5826  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     5827    final_label0 __ __
     5828
     5829(** val pseudo_assembly_program_rect_Type2 :
     5830    ((identifier, BitVector.word) Types.prod List.list ->
     5831    labelled_instruction List.list -> __ -> (identifier, AST.ident)
     5832    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
     5833    pseudo_assembly_program -> 'a1 **)
     5834let rec pseudo_assembly_program_rect_Type2 h_mk_pseudo_assembly_program x_19422 =
     5835  let { preamble = preamble0; code = code0; renamed_symbols =
     5836    renamed_symbols0; final_label = final_label0 } = x_19422
     5837  in
     5838  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     5839    final_label0 __ __
     5840
     5841(** val pseudo_assembly_program_rect_Type1 :
     5842    ((identifier, BitVector.word) Types.prod List.list ->
     5843    labelled_instruction List.list -> __ -> (identifier, AST.ident)
     5844    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
     5845    pseudo_assembly_program -> 'a1 **)
     5846let rec pseudo_assembly_program_rect_Type1 h_mk_pseudo_assembly_program x_19424 =
     5847  let { preamble = preamble0; code = code0; renamed_symbols =
     5848    renamed_symbols0; final_label = final_label0 } = x_19424
     5849  in
     5850  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     5851    final_label0 __ __
     5852
     5853(** val pseudo_assembly_program_rect_Type0 :
     5854    ((identifier, BitVector.word) Types.prod List.list ->
     5855    labelled_instruction List.list -> __ -> (identifier, AST.ident)
     5856    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
     5857    pseudo_assembly_program -> 'a1 **)
     5858let rec pseudo_assembly_program_rect_Type0 h_mk_pseudo_assembly_program x_19426 =
     5859  let { preamble = preamble0; code = code0; renamed_symbols =
     5860    renamed_symbols0; final_label = final_label0 } = x_19426
     5861  in
     5862  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     5863    final_label0 __ __
     5864
     5865(** val preamble :
     5866    pseudo_assembly_program -> (identifier, BitVector.word) Types.prod
     5867    List.list **)
     5868let rec preamble xxx =
     5869  xxx.preamble
     5870
     5871(** val code : pseudo_assembly_program -> labelled_instruction List.list **)
     5872let rec code xxx =
     5873  xxx.code
     5874
     5875(** val renamed_symbols :
     5876    pseudo_assembly_program -> (identifier, AST.ident) Types.prod List.list **)
     5877let rec renamed_symbols xxx =
     5878  xxx.renamed_symbols
     5879
     5880(** val final_label : pseudo_assembly_program -> identifier **)
     5881let rec final_label xxx =
     5882  xxx.final_label
     5883
     5884(** val pseudo_assembly_program_inv_rect_Type4 :
     5885    pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
     5886    List.list -> labelled_instruction List.list -> __ -> (identifier,
     5887    AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1)
     5888    -> 'a1 **)
     5889let pseudo_assembly_program_inv_rect_Type4 hterm h1 =
     5890  let hcut = pseudo_assembly_program_rect_Type4 h1 hterm in hcut __
     5891
     5892(** val pseudo_assembly_program_inv_rect_Type3 :
     5893    pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
     5894    List.list -> labelled_instruction List.list -> __ -> (identifier,
     5895    AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1)
     5896    -> 'a1 **)
     5897let pseudo_assembly_program_inv_rect_Type3 hterm h1 =
     5898  let hcut = pseudo_assembly_program_rect_Type3 h1 hterm in hcut __
     5899
     5900(** val pseudo_assembly_program_inv_rect_Type2 :
     5901    pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
     5902    List.list -> labelled_instruction List.list -> __ -> (identifier,
     5903    AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1)
     5904    -> 'a1 **)
     5905let pseudo_assembly_program_inv_rect_Type2 hterm h1 =
     5906  let hcut = pseudo_assembly_program_rect_Type2 h1 hterm in hcut __
     5907
     5908(** val pseudo_assembly_program_inv_rect_Type1 :
     5909    pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
     5910    List.list -> labelled_instruction List.list -> __ -> (identifier,
     5911    AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1)
     5912    -> 'a1 **)
     5913let pseudo_assembly_program_inv_rect_Type1 hterm h1 =
     5914  let hcut = pseudo_assembly_program_rect_Type1 h1 hterm in hcut __
     5915
     5916(** val pseudo_assembly_program_inv_rect_Type0 :
     5917    pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
     5918    List.list -> labelled_instruction List.list -> __ -> (identifier,
     5919    AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1)
     5920    -> 'a1 **)
     5921let pseudo_assembly_program_inv_rect_Type0 hterm h1 =
     5922  let hcut = pseudo_assembly_program_rect_Type0 h1 hterm in hcut __
     5923
     5924(** val pseudo_assembly_program_jmdiscr :
     5925    pseudo_assembly_program -> pseudo_assembly_program -> __ **)
     5926let pseudo_assembly_program_jmdiscr x y =
     5927  Logic.eq_rect_Type2 x
     5928    (let { preamble = a0; code = a1; renamed_symbols = a3; final_label =
     5929       a4 } = x
     5930     in
     5931    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
     5932
     5933type object_code = BitVector.byte List.list
     5934
     5935type costlabel_map = CostLabel.costlabel BitVectorTrie.bitVectorTrie
     5936
     5937type symboltable_type = AST.ident BitVectorTrie.bitVectorTrie
     5938
     5939type labelled_object_code = { oc : object_code; costlabels : costlabel_map;
     5940                              symboltable : symboltable_type;
     5941                              final_pc : BitVector.word }
     5942
     5943(** val labelled_object_code_rect_Type4 :
     5944    (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
     5945    -> 'a1) -> labelled_object_code -> 'a1 **)
     5946let rec labelled_object_code_rect_Type4 h_mk_labelled_object_code x_19442 =
     5947  let { oc = oc0; costlabels = costlabels0; symboltable = symboltable0;
     5948    final_pc = final_pc0 } = x_19442
     5949  in
     5950  h_mk_labelled_object_code oc0 costlabels0 symboltable0 final_pc0 __
     5951
     5952(** val labelled_object_code_rect_Type5 :
     5953    (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
     5954    -> 'a1) -> labelled_object_code -> 'a1 **)
     5955let rec labelled_object_code_rect_Type5 h_mk_labelled_object_code x_19444 =
     5956  let { oc = oc0; costlabels = costlabels0; symboltable = symboltable0;
     5957    final_pc = final_pc0 } = x_19444
     5958  in
     5959  h_mk_labelled_object_code oc0 costlabels0 symboltable0 final_pc0 __
     5960
     5961(** val labelled_object_code_rect_Type3 :
     5962    (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
     5963    -> 'a1) -> labelled_object_code -> 'a1 **)
     5964let rec labelled_object_code_rect_Type3 h_mk_labelled_object_code x_19446 =
     5965  let { oc = oc0; costlabels = costlabels0; symboltable = symboltable0;
     5966    final_pc = final_pc0 } = x_19446
     5967  in
     5968  h_mk_labelled_object_code oc0 costlabels0 symboltable0 final_pc0 __
     5969
     5970(** val labelled_object_code_rect_Type2 :
     5971    (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
     5972    -> 'a1) -> labelled_object_code -> 'a1 **)
     5973let rec labelled_object_code_rect_Type2 h_mk_labelled_object_code x_19448 =
     5974  let { oc = oc0; costlabels = costlabels0; symboltable = symboltable0;
     5975    final_pc = final_pc0 } = x_19448
     5976  in
     5977  h_mk_labelled_object_code oc0 costlabels0 symboltable0 final_pc0 __
     5978
     5979(** val labelled_object_code_rect_Type1 :
     5980    (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
     5981    -> 'a1) -> labelled_object_code -> 'a1 **)
     5982let rec labelled_object_code_rect_Type1 h_mk_labelled_object_code x_19450 =
     5983  let { oc = oc0; costlabels = costlabels0; symboltable = symboltable0;
     5984    final_pc = final_pc0 } = x_19450
     5985  in
     5986  h_mk_labelled_object_code oc0 costlabels0 symboltable0 final_pc0 __
     5987
     5988(** val labelled_object_code_rect_Type0 :
     5989    (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
     5990    -> 'a1) -> labelled_object_code -> 'a1 **)
     5991let rec labelled_object_code_rect_Type0 h_mk_labelled_object_code x_19452 =
     5992  let { oc = oc0; costlabels = costlabels0; symboltable = symboltable0;
     5993    final_pc = final_pc0 } = x_19452
     5994  in
     5995  h_mk_labelled_object_code oc0 costlabels0 symboltable0 final_pc0 __
     5996
     5997(** val oc : labelled_object_code -> object_code **)
     5998let rec oc xxx =
     5999  xxx.oc
     6000
     6001(** val costlabels : labelled_object_code -> costlabel_map **)
     6002let rec costlabels xxx =
     6003  xxx.costlabels
     6004
     6005(** val symboltable : labelled_object_code -> symboltable_type **)
     6006let rec symboltable xxx =
     6007  xxx.symboltable
     6008
     6009(** val final_pc : labelled_object_code -> BitVector.word **)
     6010let rec final_pc xxx =
     6011  xxx.final_pc
     6012
     6013(** val labelled_object_code_inv_rect_Type4 :
     6014    labelled_object_code -> (object_code -> costlabel_map -> symboltable_type
     6015    -> BitVector.word -> __ -> __ -> 'a1) -> 'a1 **)
     6016let labelled_object_code_inv_rect_Type4 hterm h1 =
     6017  let hcut = labelled_object_code_rect_Type4 h1 hterm in hcut __
     6018
     6019(** val labelled_object_code_inv_rect_Type3 :
     6020    labelled_object_code -> (object_code -> costlabel_map -> symboltable_type
     6021    -> BitVector.word -> __ -> __ -> 'a1) -> 'a1 **)
     6022let labelled_object_code_inv_rect_Type3 hterm h1 =
     6023  let hcut = labelled_object_code_rect_Type3 h1 hterm in hcut __
     6024
     6025(** val labelled_object_code_inv_rect_Type2 :
     6026    labelled_object_code -> (object_code -> costlabel_map -> symboltable_type
     6027    -> BitVector.word -> __ -> __ -> 'a1) -> 'a1 **)
     6028let labelled_object_code_inv_rect_Type2 hterm h1 =
     6029  let hcut = labelled_object_code_rect_Type2 h1 hterm in hcut __
     6030
     6031(** val labelled_object_code_inv_rect_Type1 :
     6032    labelled_object_code -> (object_code -> costlabel_map -> symboltable_type
     6033    -> BitVector.word -> __ -> __ -> 'a1) -> 'a1 **)
     6034let labelled_object_code_inv_rect_Type1 hterm h1 =
     6035  let hcut = labelled_object_code_rect_Type1 h1 hterm in hcut __
     6036
     6037(** val labelled_object_code_inv_rect_Type0 :
     6038    labelled_object_code -> (object_code -> costlabel_map -> symboltable_type
     6039    -> BitVector.word -> __ -> __ -> 'a1) -> 'a1 **)
     6040let labelled_object_code_inv_rect_Type0 hterm h1 =
     6041  let hcut = labelled_object_code_rect_Type0 h1 hterm in hcut __
     6042
     6043(** val labelled_object_code_discr :
     6044    labelled_object_code -> labelled_object_code -> __ **)
     6045let labelled_object_code_discr x y =
     6046  Logic.eq_rect_Type2 x
     6047    (let { oc = a0; costlabels = a1; symboltable = a2; final_pc = a3 } = x in
     6048    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
     6049
     6050(** val labelled_object_code_jmdiscr :
     6051    labelled_object_code -> labelled_object_code -> __ **)
     6052let labelled_object_code_jmdiscr x y =
     6053  Logic.eq_rect_Type2 x
     6054    (let { oc = a0; costlabels = a1; symboltable = a2; final_pc = a3 } = x in
     6055    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
     6056
Note: See TracChangeset for help on using the changeset viewer.