(BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word
-> 'a1) -> addressing_mode -> 'a1 **)
let 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
-| DIRECT x_19160 -> h_DIRECT x_19160
-| INDIRECT x_19161 -> h_INDIRECT x_19161
-| EXT_INDIRECT x_19162 -> h_EXT_INDIRECT x_19162
-| REGISTER x_19163 -> h_REGISTER x_19163
+| DIRECT x_33 -> h_DIRECT x_33
+| INDIRECT x_34 -> h_INDIRECT x_34
+| EXT_INDIRECT x_35 -> h_EXT_INDIRECT x_35
+| REGISTER x_36 -> h_REGISTER x_36
| ACC_A -> h_ACC_A
| ACC_B -> h_ACC_B
| DPTR -> h_DPTR
-| DATA x_19164 -> h_DATA x_19164
-| DATA16 x_19165 -> h_DATA16 x_19165
+| DATA x_37 -> h_DATA x_37
+| DATA16 x_38 -> h_DATA16 x_38
| ACC_DPTR -> h_ACC_DPTR
| ACC_PC -> h_ACC_PC
| EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR
| INDIRECT_DPTR -> h_INDIRECT_DPTR
| CARRY -> h_CARRY
-| BIT_ADDR x_19166 -> h_BIT_ADDR x_19166
-| N_BIT_ADDR x_19167 -> h_N_BIT_ADDR x_19167
-| RELATIVE x_19168 -> h_RELATIVE x_19168
-| ADDR11 x_19169 -> h_ADDR11 x_19169
-| ADDR16 x_19170 -> h_ADDR16 x_19170
+| BIT_ADDR x_39 -> h_BIT_ADDR x_39
+| N_BIT_ADDR x_40 -> h_N_BIT_ADDR x_40
+| RELATIVE x_41 -> h_RELATIVE x_41
+| ADDR11 x_42 -> h_ADDR11 x_42
+| ADDR16 x_43 -> h_ADDR16 x_43
(** val addressing_mode_rect_Type5 :
(BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit ->
(BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word
-> 'a1) -> addressing_mode -> 'a1 **)
let 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
-| DIRECT x_19191 -> h_DIRECT x_19191
-| INDIRECT x_19192 -> h_INDIRECT x_19192
-| EXT_INDIRECT x_19193 -> h_EXT_INDIRECT x_19193
-| REGISTER x_19194 -> h_REGISTER x_19194
+| DIRECT x_64 -> h_DIRECT x_64
+| INDIRECT x_65 -> h_INDIRECT x_65
+| EXT_INDIRECT x_66 -> h_EXT_INDIRECT x_66
+| REGISTER x_67 -> h_REGISTER x_67
| ACC_A -> h_ACC_A
| ACC_B -> h_ACC_B
| DPTR -> h_DPTR
-| DATA x_19195 -> h_DATA x_19195
-| DATA16 x_19196 -> h_DATA16 x_19196
+| DATA x_68 -> h_DATA x_68
+| DATA16 x_69 -> h_DATA16 x_69
| ACC_DPTR -> h_ACC_DPTR
| ACC_PC -> h_ACC_PC
| EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR
| INDIRECT_DPTR -> h_INDIRECT_DPTR
| CARRY -> h_CARRY
-| BIT_ADDR x_19197 -> h_BIT_ADDR x_19197
-| N_BIT_ADDR x_19198 -> h_N_BIT_ADDR x_19198
-| RELATIVE x_19199 -> h_RELATIVE x_19199
-| ADDR11 x_19200 -> h_ADDR11 x_19200
-| ADDR16 x_19201 -> h_ADDR16 x_19201
+| BIT_ADDR x_70 -> h_BIT_ADDR x_70
+| N_BIT_ADDR x_71 -> h_N_BIT_ADDR x_71
+| RELATIVE x_72 -> h_RELATIVE x_72
+| ADDR11 x_73 -> h_ADDR11 x_73
+| ADDR16 x_74 -> h_ADDR16 x_74
(** val addressing_mode_rect_Type3 :
(BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit ->
(BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word
-> 'a1) -> addressing_mode -> 'a1 **)
let 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
-| DIRECT x_19222 -> h_DIRECT x_19222
-| INDIRECT x_19223 -> h_INDIRECT x_19223
-| EXT_INDIRECT x_19224 -> h_EXT_INDIRECT x_19224
-| REGISTER x_19225 -> h_REGISTER x_19225
+| DIRECT x_95 -> h_DIRECT x_95
+| INDIRECT x_96 -> h_INDIRECT x_96
+| EXT_INDIRECT x_97 -> h_EXT_INDIRECT x_97
+| REGISTER x_98 -> h_REGISTER x_98
| ACC_A -> h_ACC_A
| ACC_B -> h_ACC_B
| DPTR -> h_DPTR
-| DATA x_19226 -> h_DATA x_19226
-| DATA16 x_19227 -> h_DATA16 x_19227
+| DATA x_99 -> h_DATA x_99
+| DATA16 x_100 -> h_DATA16 x_100
| ACC_DPTR -> h_ACC_DPTR
| ACC_PC -> h_ACC_PC
| EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR
| INDIRECT_DPTR -> h_INDIRECT_DPTR
| CARRY -> h_CARRY
-| BIT_ADDR x_19228 -> h_BIT_ADDR x_19228
-| N_BIT_ADDR x_19229 -> h_N_BIT_ADDR x_19229
-| RELATIVE x_19230 -> h_RELATIVE x_19230
-| ADDR11 x_19231 -> h_ADDR11 x_19231
-| ADDR16 x_19232 -> h_ADDR16 x_19232
+| BIT_ADDR x_101 -> h_BIT_ADDR x_101
+| N_BIT_ADDR x_102 -> h_N_BIT_ADDR x_102
+| RELATIVE x_103 -> h_RELATIVE x_103
+| ADDR11 x_104 -> h_ADDR11 x_104
+| ADDR16 x_105 -> h_ADDR16 x_105
(** val addressing_mode_rect_Type2 :
(BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit ->
(BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word
-> 'a1) -> addressing_mode -> 'a1 **)
let 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
-| DIRECT x_19253 -> h_DIRECT x_19253
-| INDIRECT x_19254 -> h_INDIRECT x_19254
-| EXT_INDIRECT x_19255 -> h_EXT_INDIRECT x_19255
-| REGISTER x_19256 -> h_REGISTER x_19256
+| DIRECT x_126 -> h_DIRECT x_126
+| INDIRECT x_127 -> h_INDIRECT x_127
+| EXT_INDIRECT x_128 -> h_EXT_INDIRECT x_128
+| REGISTER x_129 -> h_REGISTER x_129
| ACC_A -> h_ACC_A
| ACC_B -> h_ACC_B
| DPTR -> h_DPTR
-| DATA x_19257 -> h_DATA x_19257
-| DATA16 x_19258 -> h_DATA16 x_19258
+| DATA x_130 -> h_DATA x_130
+| DATA16 x_131 -> h_DATA16 x_131
| ACC_DPTR -> h_ACC_DPTR
| ACC_PC -> h_ACC_PC
| EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR
| INDIRECT_DPTR -> h_INDIRECT_DPTR
| CARRY -> h_CARRY
-| BIT_ADDR x_19259 -> h_BIT_ADDR x_19259
-| N_BIT_ADDR x_19260 -> h_N_BIT_ADDR x_19260
-| RELATIVE x_19261 -> h_RELATIVE x_19261
-| ADDR11 x_19262 -> h_ADDR11 x_19262
-| ADDR16 x_19263 -> h_ADDR16 x_19263
+| BIT_ADDR x_132 -> h_BIT_ADDR x_132
+| N_BIT_ADDR x_133 -> h_N_BIT_ADDR x_133
+| RELATIVE x_134 -> h_RELATIVE x_134
+| ADDR11 x_135 -> h_ADDR11 x_135
+| ADDR16 x_136 -> h_ADDR16 x_136
(** val addressing_mode_rect_Type1 :
(BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit ->
(BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word
-> 'a1) -> addressing_mode -> 'a1 **)
let 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
-| DIRECT x_19284 -> h_DIRECT x_19284
-| INDIRECT x_19285 -> h_INDIRECT x_19285
-| EXT_INDIRECT x_19286 -> h_EXT_INDIRECT x_19286
-| REGISTER x_19287 -> h_REGISTER x_19287
+| DIRECT x_157 -> h_DIRECT x_157
+| INDIRECT x_158 -> h_INDIRECT x_158
+| EXT_INDIRECT x_159 -> h_EXT_INDIRECT x_159
+| REGISTER x_160 -> h_REGISTER x_160
| ACC_A -> h_ACC_A
| ACC_B -> h_ACC_B
| DPTR -> h_DPTR
-| DATA x_19288 -> h_DATA x_19288
-| DATA16 x_19289 -> h_DATA16 x_19289
+| DATA x_161 -> h_DATA x_161
+| DATA16 x_162 -> h_DATA16 x_162
| ACC_DPTR -> h_ACC_DPTR
| ACC_PC -> h_ACC_PC
| EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR
| INDIRECT_DPTR -> h_INDIRECT_DPTR
| CARRY -> h_CARRY
-| BIT_ADDR x_19290 -> h_BIT_ADDR x_19290
-| N_BIT_ADDR x_19291 -> h_N_BIT_ADDR x_19291
-| RELATIVE x_19292 -> h_RELATIVE x_19292
-| ADDR11 x_19293 -> h_ADDR11 x_19293
-| ADDR16 x_19294 -> h_ADDR16 x_19294
+| BIT_ADDR x_163 -> h_BIT_ADDR x_163
+| N_BIT_ADDR x_164 -> h_N_BIT_ADDR x_164
+| RELATIVE x_165 -> h_RELATIVE x_165
+| ADDR11 x_166 -> h_ADDR11 x_166
+| ADDR16 x_167 -> h_ADDR16 x_167
(** val addressing_mode_rect_Type0 :
(BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit ->
(BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word
-> 'a1) -> addressing_mode -> 'a1 **)
let 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
-| DIRECT x_19315 -> h_DIRECT x_19315
-| INDIRECT x_19316 -> h_INDIRECT x_19316
-| EXT_INDIRECT x_19317 -> h_EXT_INDIRECT x_19317
-| REGISTER x_19318 -> h_REGISTER x_19318
+| DIRECT x_188 -> h_DIRECT x_188
+| INDIRECT x_189 -> h_INDIRECT x_189
+| EXT_INDIRECT x_190 -> h_EXT_INDIRECT x_190
+| REGISTER x_191 -> h_REGISTER x_191
| ACC_A -> h_ACC_A
| ACC_B -> h_ACC_B
| DPTR -> h_DPTR
-| DATA x_19319 -> h_DATA x_19319
-| DATA16 x_19320 -> h_DATA16 x_19320
+| DATA x_192 -> h_DATA x_192
+| DATA16 x_193 -> h_DATA16 x_193
| ACC_DPTR -> h_ACC_DPTR
| ACC_PC -> h_ACC_PC
| EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR
| INDIRECT_DPTR -> h_INDIRECT_DPTR
| CARRY -> h_CARRY
-| BIT_ADDR x_19321 -> h_BIT_ADDR x_19321
-| N_BIT_ADDR x_19322 -> h_N_BIT_ADDR x_19322
-| RELATIVE x_19323 -> h_RELATIVE x_19323
-| ADDR11 x_19324 -> h_ADDR11 x_19324
-| ADDR16 x_19325 -> h_ADDR16 x_19325
+| BIT_ADDR x_194 -> h_BIT_ADDR x_194
+| N_BIT_ADDR x_195 -> h_N_BIT_ADDR x_195
+| RELATIVE x_196 -> h_RELATIVE x_196
+| ADDR11 x_197 -> h_ADDR11 x_197
+| ADDR16 x_198 -> h_ADDR16 x_198
(** val addressing_mode_inv_rect_Type4 :
addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __
(** val subaddressing_mode_rect_Type4 :
Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
'a1) -> subaddressing_mode -> 'a1 **)
-let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_19793 =
- let subaddressing_modeel = x_19793 in
+let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_666 =
+ let subaddressing_modeel = x_666 in
h_mk_subaddressing_mode subaddressing_modeel __
(** val subaddressing_mode_rect_Type5 :
Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
'a1) -> subaddressing_mode -> 'a1 **)
-let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_19795 =
- let subaddressing_modeel = x_19795 in
+let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_668 =
+ let subaddressing_modeel = x_668 in
h_mk_subaddressing_mode subaddressing_modeel __
(** val subaddressing_mode_rect_Type3 :
Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
'a1) -> subaddressing_mode -> 'a1 **)
-let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_19797 =
- let subaddressing_modeel = x_19797 in
+let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_670 =
+ let subaddressing_modeel = x_670 in
h_mk_subaddressing_mode subaddressing_modeel __
(** val subaddressing_mode_rect_Type2 :
Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
'a1) -> subaddressing_mode -> 'a1 **)
-let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_19799 =
- let subaddressing_modeel = x_19799 in
+let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_672 =
+ let subaddressing_modeel = x_672 in
h_mk_subaddressing_mode subaddressing_modeel __
(** val subaddressing_mode_rect_Type1 :
Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
'a1) -> subaddressing_mode -> 'a1 **)
-let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_19801 =
- let subaddressing_modeel = x_19801 in
+let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_674 =
+ let subaddressing_modeel = x_674 in
h_mk_subaddressing_mode subaddressing_modeel __
(** val subaddressing_mode_rect_Type0 :
Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
'a1) -> subaddressing_mode -> 'a1 **)
-let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_19803 =
- let subaddressing_modeel = x_19803 in
+let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_676 =
+ let subaddressing_modeel = x_676 in
h_mk_subaddressing_mode subaddressing_modeel __
(** val subaddressing_modeel :
-> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 ->
'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
let rec preinstruction_rect_Type4 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function
-| ADD (x_19905, x_19904) -> h_ADD x_19905 x_19904
-| ADDC (x_19907, x_19906) -> h_ADDC x_19907 x_19906
-| SUBB (x_19909, x_19908) -> h_SUBB x_19909 x_19908
-| INC x_19910 -> h_INC x_19910
-| DEC x_19911 -> h_DEC x_19911
-| MUL (x_19913, x_19912) -> h_MUL x_19913 x_19912
-| DIV (x_19915, x_19914) -> h_DIV x_19915 x_19914
-| DA x_19916 -> h_DA x_19916
-| JC x_19917 -> h_JC x_19917
-| JNC x_19918 -> h_JNC x_19918
-| JB (x_19920, x_19919) -> h_JB x_19920 x_19919
-| JNB (x_19922, x_19921) -> h_JNB x_19922 x_19921
-| JBC (x_19924, x_19923) -> h_JBC x_19924 x_19923
-| JZ x_19925 -> h_JZ x_19925
-| JNZ x_19926 -> h_JNZ x_19926
-| CJNE (x_19928, x_19927) -> h_CJNE x_19928 x_19927
-| DJNZ (x_19930, x_19929) -> h_DJNZ x_19930 x_19929
-| ANL x_19931 -> h_ANL x_19931
-| ORL x_19932 -> h_ORL x_19932
-| XRL x_19933 -> h_XRL x_19933
-| CLR x_19934 -> h_CLR x_19934
-| CPL x_19935 -> h_CPL x_19935
-| RL x_19936 -> h_RL x_19936
-| RLC x_19937 -> h_RLC x_19937
-| RR x_19938 -> h_RR x_19938
-| RRC x_19939 -> h_RRC x_19939
-| SWAP x_19940 -> h_SWAP x_19940
-| MOV x_19941 -> h_MOV x_19941
-| MOVX x_19942 -> h_MOVX x_19942
-| SETB x_19943 -> h_SETB x_19943
-| PUSH x_19944 -> h_PUSH x_19944
-| POP x_19945 -> h_POP x_19945
-| XCH (x_19947, x_19946) -> h_XCH x_19947 x_19946
-| XCHD (x_19949, x_19948) -> h_XCHD x_19949 x_19948
+| ADD (x_778, x_777) -> h_ADD x_778 x_777
+| ADDC (x_780, x_779) -> h_ADDC x_780 x_779
+| SUBB (x_782, x_781) -> h_SUBB x_782 x_781
+| INC x_783 -> h_INC x_783
+| DEC x_784 -> h_DEC x_784
+| MUL (x_786, x_785) -> h_MUL x_786 x_785
+| DIV (x_788, x_787) -> h_DIV x_788 x_787
+| DA x_789 -> h_DA x_789
+| JC x_790 -> h_JC x_790
+| JNC x_791 -> h_JNC x_791
+| JB (x_793, x_792) -> h_JB x_793 x_792
+| JNB (x_795, x_794) -> h_JNB x_795 x_794
+| JBC (x_797, x_796) -> h_JBC x_797 x_796
+| JZ x_798 -> h_JZ x_798
+| JNZ x_799 -> h_JNZ x_799
+| CJNE (x_801, x_800) -> h_CJNE x_801 x_800
+| DJNZ (x_803, x_802) -> h_DJNZ x_803 x_802
+| ANL x_804 -> h_ANL x_804
+| ORL x_805 -> h_ORL x_805
+| XRL x_806 -> h_XRL x_806
+| CLR x_807 -> h_CLR x_807
+| CPL x_808 -> h_CPL x_808
+| RL x_809 -> h_RL x_809
+| RLC x_810 -> h_RLC x_810
+| RR x_811 -> h_RR x_811
+| RRC x_812 -> h_RRC x_812
+| SWAP x_813 -> h_SWAP x_813
+| MOV x_814 -> h_MOV x_814
+| MOVX x_815 -> h_MOVX x_815
+| SETB x_816 -> h_SETB x_816
+| PUSH x_817 -> h_PUSH x_817
+| POP x_818 -> h_POP x_818
+| XCH (x_820, x_819) -> h_XCH x_820 x_819
+| XCHD (x_822, x_821) -> h_XCHD x_822 x_821
| RET -> h_RET
| RETI -> h_RETI
| NOP -> h_NOP
-| JMP x_19950 -> h_JMP x_19950
+| JMP x_823 -> h_JMP x_823
(** val preinstruction_rect_Type5 :
(subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode
-> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 ->
'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
let rec preinstruction_rect_Type5 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function
-| ADD (x_19991, x_19990) -> h_ADD x_19991 x_19990
-| ADDC (x_19993, x_19992) -> h_ADDC x_19993 x_19992
-| SUBB (x_19995, x_19994) -> h_SUBB x_19995 x_19994
-| INC x_19996 -> h_INC x_19996
-| DEC x_19997 -> h_DEC x_19997
-| MUL (x_19999, x_19998) -> h_MUL x_19999 x_19998
-| DIV (x_20001, x_20000) -> h_DIV x_20001 x_20000
-| DA x_20002 -> h_DA x_20002
-| JC x_20003 -> h_JC x_20003
-| JNC x_20004 -> h_JNC x_20004
-| JB (x_20006, x_20005) -> h_JB x_20006 x_20005
-| JNB (x_20008, x_20007) -> h_JNB x_20008 x_20007
-| JBC (x_20010, x_20009) -> h_JBC x_20010 x_20009
-| JZ x_20011 -> h_JZ x_20011
-| JNZ x_20012 -> h_JNZ x_20012
-| CJNE (x_20014, x_20013) -> h_CJNE x_20014 x_20013
-| DJNZ (x_20016, x_20015) -> h_DJNZ x_20016 x_20015
-| ANL x_20017 -> h_ANL x_20017
-| ORL x_20018 -> h_ORL x_20018
-| XRL x_20019 -> h_XRL x_20019
-| CLR x_20020 -> h_CLR x_20020
-| CPL x_20021 -> h_CPL x_20021
-| RL x_20022 -> h_RL x_20022
-| RLC x_20023 -> h_RLC x_20023
-| RR x_20024 -> h_RR x_20024
-| RRC x_20025 -> h_RRC x_20025
-| SWAP x_20026 -> h_SWAP x_20026
-| MOV x_20027 -> h_MOV x_20027
-| MOVX x_20028 -> h_MOVX x_20028
-| SETB x_20029 -> h_SETB x_20029
-| PUSH x_20030 -> h_PUSH x_20030
-| POP x_20031 -> h_POP x_20031
-| XCH (x_20033, x_20032) -> h_XCH x_20033 x_20032
-| XCHD (x_20035, x_20034) -> h_XCHD x_20035 x_20034
+| ADD (x_864, x_863) -> h_ADD x_864 x_863
+| ADDC (x_866, x_865) -> h_ADDC x_866 x_865
+| SUBB (x_868, x_867) -> h_SUBB x_868 x_867
+| INC x_869 -> h_INC x_869
+| DEC x_870 -> h_DEC x_870
+| MUL (x_872, x_871) -> h_MUL x_872 x_871
+| DIV (x_874, x_873) -> h_DIV x_874 x_873
+| DA x_875 -> h_DA x_875
+| JC x_876 -> h_JC x_876
+| JNC x_877 -> h_JNC x_877
+| JB (x_879, x_878) -> h_JB x_879 x_878
+| JNB (x_881, x_880) -> h_JNB x_881 x_880
+| JBC (x_883, x_882) -> h_JBC x_883 x_882
+| JZ x_884 -> h_JZ x_884
+| JNZ x_885 -> h_JNZ x_885
+| CJNE (x_887, x_886) -> h_CJNE x_887 x_886
+| DJNZ (x_889, x_888) -> h_DJNZ x_889 x_888
+| ANL x_890 -> h_ANL x_890
+| ORL x_891 -> h_ORL x_891
+| XRL x_892 -> h_XRL x_892
+| CLR x_893 -> h_CLR x_893
+| CPL x_894 -> h_CPL x_894
+| RL x_895 -> h_RL x_895
+| RLC x_896 -> h_RLC x_896
+| RR x_897 -> h_RR x_897
+| RRC x_898 -> h_RRC x_898
+| SWAP x_899 -> h_SWAP x_899
+| MOV x_900 -> h_MOV x_900
+| MOVX x_901 -> h_MOVX x_901
+| SETB x_902 -> h_SETB x_902
+| PUSH x_903 -> h_PUSH x_903
+| POP x_904 -> h_POP x_904
+| XCH (x_906, x_905) -> h_XCH x_906 x_905
+| XCHD (x_908, x_907) -> h_XCHD x_908 x_907
| RET -> h_RET
| RETI -> h_RETI
| NOP -> h_NOP
-| JMP x_20036 -> h_JMP x_20036
+| JMP x_909 -> h_JMP x_909
(** val preinstruction_rect_Type3 :
(subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode
-> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 ->
'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
let rec preinstruction_rect_Type3 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function
-| ADD (x_20077, x_20076) -> h_ADD x_20077 x_20076
-| ADDC (x_20079, x_20078) -> h_ADDC x_20079 x_20078
-| SUBB (x_20081, x_20080) -> h_SUBB x_20081 x_20080
-| INC x_20082 -> h_INC x_20082
-| DEC x_20083 -> h_DEC x_20083
-| MUL (x_20085, x_20084) -> h_MUL x_20085 x_20084
-| DIV (x_20087, x_20086) -> h_DIV x_20087 x_20086
-| DA x_20088 -> h_DA x_20088
-| JC x_20089 -> h_JC x_20089
-| JNC x_20090 -> h_JNC x_20090
-| JB (x_20092, x_20091) -> h_JB x_20092 x_20091
-| JNB (x_20094, x_20093) -> h_JNB x_20094 x_20093
-| JBC (x_20096, x_20095) -> h_JBC x_20096 x_20095
-| JZ x_20097 -> h_JZ x_20097
-| JNZ x_20098 -> h_JNZ x_20098
-| CJNE (x_20100, x_20099) -> h_CJNE x_20100 x_20099
-| DJNZ (x_20102, x_20101) -> h_DJNZ x_20102 x_20101
-| ANL x_20103 -> h_ANL x_20103
-| ORL x_20104 -> h_ORL x_20104
-| XRL x_20105 -> h_XRL x_20105
-| CLR x_20106 -> h_CLR x_20106
-| CPL x_20107 -> h_CPL x_20107
-| RL x_20108 -> h_RL x_20108
-| RLC x_20109 -> h_RLC x_20109
-| RR x_20110 -> h_RR x_20110
-| RRC x_20111 -> h_RRC x_20111
-| SWAP x_20112 -> h_SWAP x_20112
-| MOV x_20113 -> h_MOV x_20113
-| MOVX x_20114 -> h_MOVX x_20114
-| SETB x_20115 -> h_SETB x_20115
-| PUSH x_20116 -> h_PUSH x_20116
-| POP x_20117 -> h_POP x_20117
-| XCH (x_20119, x_20118) -> h_XCH x_20119 x_20118
-| XCHD (x_20121, x_20120) -> h_XCHD x_20121 x_20120
+| ADD (x_950, x_949) -> h_ADD x_950 x_949
+| ADDC (x_952, x_951) -> h_ADDC x_952 x_951
+| SUBB (x_954, x_953) -> h_SUBB x_954 x_953
+| INC x_955 -> h_INC x_955
+| DEC x_956 -> h_DEC x_956
+| MUL (x_958, x_957) -> h_MUL x_958 x_957
+| DIV (x_960, x_959) -> h_DIV x_960 x_959
+| DA x_961 -> h_DA x_961
+| JC x_962 -> h_JC x_962
+| JNC x_963 -> h_JNC x_963
+| JB (x_965, x_964) -> h_JB x_965 x_964
+| JNB (x_967, x_966) -> h_JNB x_967 x_966
+| JBC (x_969, x_968) -> h_JBC x_969 x_968
+| JZ x_970 -> h_JZ x_970
+| JNZ x_971 -> h_JNZ x_971
+| CJNE (x_973, x_972) -> h_CJNE x_973 x_972
+| DJNZ (x_975, x_974) -> h_DJNZ x_975 x_974
+| ANL x_976 -> h_ANL x_976
+| ORL x_977 -> h_ORL x_977
+| XRL x_978 -> h_XRL x_978
+| CLR x_979 -> h_CLR x_979
+| CPL x_980 -> h_CPL x_980
+| RL x_981 -> h_RL x_981
+| RLC x_982 -> h_RLC x_982
+| RR x_983 -> h_RR x_983
+| RRC x_984 -> h_RRC x_984
+| SWAP x_985 -> h_SWAP x_985
+| MOV x_986 -> h_MOV x_986
+| MOVX x_987 -> h_MOVX x_987
+| SETB x_988 -> h_SETB x_988
+| PUSH x_989 -> h_PUSH x_989
+| POP x_990 -> h_POP x_990
+| XCH (x_992, x_991) -> h_XCH x_992 x_991
+| XCHD (x_994, x_993) -> h_XCHD x_994 x_993
| RET -> h_RET
| RETI -> h_RETI
| NOP -> h_NOP
-| JMP x_20122 -> h_JMP x_20122
+| JMP x_995 -> h_JMP x_995
(** val preinstruction_rect_Type2 :
(subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode
-> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 ->
'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
let rec preinstruction_rect_Type2 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function
-| ADD (x_20163, x_20162) -> h_ADD x_20163 x_20162
-| ADDC (x_20165, x_20164) -> h_ADDC x_20165 x_20164
-| SUBB (x_20167, x_20166) -> h_SUBB x_20167 x_20166
-| INC x_20168 -> h_INC x_20168
-| DEC x_20169 -> h_DEC x_20169
-| MUL (x_20171, x_20170) -> h_MUL x_20171 x_20170
-| DIV (x_20173, x_20172) -> h_DIV x_20173 x_20172
-| DA x_20174 -> h_DA x_20174
-| JC x_20175 -> h_JC x_20175
-| JNC x_20176 -> h_JNC x_20176
-| JB (x_20178, x_20177) -> h_JB x_20178 x_20177
-| JNB (x_20180, x_20179) -> h_JNB x_20180 x_20179
-| JBC (x_20182, x_20181) -> h_JBC x_20182 x_20181
-| JZ x_20183 -> h_JZ x_20183
-| JNZ x_20184 -> h_JNZ x_20184
-| CJNE (x_20186, x_20185) -> h_CJNE x_20186 x_20185
-| DJNZ (x_20188, x_20187) -> h_DJNZ x_20188 x_20187
-| ANL x_20189 -> h_ANL x_20189
-| ORL x_20190 -> h_ORL x_20190
-| XRL x_20191 -> h_XRL x_20191
-| CLR x_20192 -> h_CLR x_20192
-| CPL x_20193 -> h_CPL x_20193
-| RL x_20194 -> h_RL x_20194
-| RLC x_20195 -> h_RLC x_20195
-| RR x_20196 -> h_RR x_20196
-| RRC x_20197 -> h_RRC x_20197
-| SWAP x_20198 -> h_SWAP x_20198
-| MOV x_20199 -> h_MOV x_20199
-| MOVX x_20200 -> h_MOVX x_20200
-| SETB x_20201 -> h_SETB x_20201
-| PUSH x_20202 -> h_PUSH x_20202
-| POP x_20203 -> h_POP x_20203
-| XCH (x_20205, x_20204) -> h_XCH x_20205 x_20204
-| XCHD (x_20207, x_20206) -> h_XCHD x_20207 x_20206
+| ADD (x_1036, x_1035) -> h_ADD x_1036 x_1035
+| ADDC (x_1038, x_1037) -> h_ADDC x_1038 x_1037
+| SUBB (x_1040, x_1039) -> h_SUBB x_1040 x_1039
+| INC x_1041 -> h_INC x_1041
+| DEC x_1042 -> h_DEC x_1042
+| MUL (x_1044, x_1043) -> h_MUL x_1044 x_1043
+| DIV (x_1046, x_1045) -> h_DIV x_1046 x_1045
+| DA x_1047 -> h_DA x_1047
+| JC x_1048 -> h_JC x_1048
+| JNC x_1049 -> h_JNC x_1049
+| JB (x_1051, x_1050) -> h_JB x_1051 x_1050
+| JNB (x_1053, x_1052) -> h_JNB x_1053 x_1052
+| JBC (x_1055, x_1054) -> h_JBC x_1055 x_1054
+| JZ x_1056 -> h_JZ x_1056
+| JNZ x_1057 -> h_JNZ x_1057
+| CJNE (x_1059, x_1058) -> h_CJNE x_1059 x_1058
+| DJNZ (x_1061, x_1060) -> h_DJNZ x_1061 x_1060
+| ANL x_1062 -> h_ANL x_1062
+| ORL x_1063 -> h_ORL x_1063
+| XRL x_1064 -> h_XRL x_1064
+| CLR x_1065 -> h_CLR x_1065
+| CPL x_1066 -> h_CPL x_1066
+| RL x_1067 -> h_RL x_1067
+| RLC x_1068 -> h_RLC x_1068
+| RR x_1069 -> h_RR x_1069
+| RRC x_1070 -> h_RRC x_1070
+| SWAP x_1071 -> h_SWAP x_1071
+| MOV x_1072 -> h_MOV x_1072
+| MOVX x_1073 -> h_MOVX x_1073
+| SETB x_1074 -> h_SETB x_1074
+| PUSH x_1075 -> h_PUSH x_1075
+| POP x_1076 -> h_POP x_1076
+| XCH (x_1078, x_1077) -> h_XCH x_1078 x_1077
+| XCHD (x_1080, x_1079) -> h_XCHD x_1080 x_1079
| RET -> h_RET
| RETI -> h_RETI
| NOP -> h_NOP
-| JMP x_20208 -> h_JMP x_20208
+| JMP x_1081 -> h_JMP x_1081
(** val preinstruction_rect_Type1 :
(subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode
-> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 ->
'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
let rec preinstruction_rect_Type1 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function
-| ADD (x_20249, x_20248) -> h_ADD x_20249 x_20248
-| ADDC (x_20251, x_20250) -> h_ADDC x_20251 x_20250
-| SUBB (x_20253, x_20252) -> h_SUBB x_20253 x_20252
-| INC x_20254 -> h_INC x_20254
-| DEC x_20255 -> h_DEC x_20255
-| MUL (x_20257, x_20256) -> h_MUL x_20257 x_20256
-| DIV (x_20259, x_20258) -> h_DIV x_20259 x_20258
-| DA x_20260 -> h_DA x_20260
-| JC x_20261 -> h_JC x_20261
-| JNC x_20262 -> h_JNC x_20262
-| JB (x_20264, x_20263) -> h_JB x_20264 x_20263
-| JNB (x_20266, x_20265) -> h_JNB x_20266 x_20265
-| JBC (x_20268, x_20267) -> h_JBC x_20268 x_20267
-| JZ x_20269 -> h_JZ x_20269
-| JNZ x_20270 -> h_JNZ x_20270
-| CJNE (x_20272, x_20271) -> h_CJNE x_20272 x_20271
-| DJNZ (x_20274, x_20273) -> h_DJNZ x_20274 x_20273
-| ANL x_20275 -> h_ANL x_20275
-| ORL x_20276 -> h_ORL x_20276
-| XRL x_20277 -> h_XRL x_20277
-| CLR x_20278 -> h_CLR x_20278
-| CPL x_20279 -> h_CPL x_20279
-| RL x_20280 -> h_RL x_20280
-| RLC x_20281 -> h_RLC x_20281
-| RR x_20282 -> h_RR x_20282
-| RRC x_20283 -> h_RRC x_20283
-| SWAP x_20284 -> h_SWAP x_20284
-| MOV x_20285 -> h_MOV x_20285
-| MOVX x_20286 -> h_MOVX x_20286
-| SETB x_20287 -> h_SETB x_20287
-| PUSH x_20288 -> h_PUSH x_20288
-| POP x_20289 -> h_POP x_20289
-| XCH (x_20291, x_20290) -> h_XCH x_20291 x_20290
-| XCHD (x_20293, x_20292) -> h_XCHD x_20293 x_20292
+| ADD (x_1122, x_1121) -> h_ADD x_1122 x_1121
+| ADDC (x_1124, x_1123) -> h_ADDC x_1124 x_1123
+| SUBB (x_1126, x_1125) -> h_SUBB x_1126 x_1125
+| INC x_1127 -> h_INC x_1127
+| DEC x_1128 -> h_DEC x_1128
+| MUL (x_1130, x_1129) -> h_MUL x_1130 x_1129
+| DIV (x_1132, x_1131) -> h_DIV x_1132 x_1131
+| DA x_1133 -> h_DA x_1133
+| JC x_1134 -> h_JC x_1134
+| JNC x_1135 -> h_JNC x_1135
+| JB (x_1137, x_1136) -> h_JB x_1137 x_1136
+| JNB (x_1139, x_1138) -> h_JNB x_1139 x_1138
+| JBC (x_1141, x_1140) -> h_JBC x_1141 x_1140
+| JZ x_1142 -> h_JZ x_1142
+| JNZ x_1143 -> h_JNZ x_1143
+| CJNE (x_1145, x_1144) -> h_CJNE x_1145 x_1144
+| DJNZ (x_1147, x_1146) -> h_DJNZ x_1147 x_1146
+| ANL x_1148 -> h_ANL x_1148
+| ORL x_1149 -> h_ORL x_1149
+| XRL x_1150 -> h_XRL x_1150
+| CLR x_1151 -> h_CLR x_1151
+| CPL x_1152 -> h_CPL x_1152
+| RL x_1153 -> h_RL x_1153
+| RLC x_1154 -> h_RLC x_1154
+| RR x_1155 -> h_RR x_1155
+| RRC x_1156 -> h_RRC x_1156
+| SWAP x_1157 -> h_SWAP x_1157
+| MOV x_1158 -> h_MOV x_1158
+| MOVX x_1159 -> h_MOVX x_1159
+| SETB x_1160 -> h_SETB x_1160
+| PUSH x_1161 -> h_PUSH x_1161
+| POP x_1162 -> h_POP x_1162
+| XCH (x_1164, x_1163) -> h_XCH x_1164 x_1163
+| XCHD (x_1166, x_1165) -> h_XCHD x_1166 x_1165
| RET -> h_RET
| RETI -> h_RETI
| NOP -> h_NOP
-| JMP x_20294 -> h_JMP x_20294
+| JMP x_1167 -> h_JMP x_1167
(** val preinstruction_rect_Type0 :
(subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode
-> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 ->
'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
let rec preinstruction_rect_Type0 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function
-| ADD (x_20335, x_20334) -> h_ADD x_20335 x_20334
-| ADDC (x_20337, x_20336) -> h_ADDC x_20337 x_20336
-| SUBB (x_20339, x_20338) -> h_SUBB x_20339 x_20338
-| INC x_20340 -> h_INC x_20340
-| DEC x_20341 -> h_DEC x_20341
-| MUL (x_20343, x_20342) -> h_MUL x_20343 x_20342
-| DIV (x_20345, x_20344) -> h_DIV x_20345 x_20344
-| DA x_20346 -> h_DA x_20346
-| JC x_20347 -> h_JC x_20347
-| JNC x_20348 -> h_JNC x_20348
-| JB (x_20350, x_20349) -> h_JB x_20350 x_20349
-| JNB (x_20352, x_20351) -> h_JNB x_20352 x_20351
-| JBC (x_20354, x_20353) -> h_JBC x_20354 x_20353
-| JZ x_20355 -> h_JZ x_20355
-| JNZ x_20356 -> h_JNZ x_20356
-| CJNE (x_20358, x_20357) -> h_CJNE x_20358 x_20357
-| DJNZ (x_20360, x_20359) -> h_DJNZ x_20360 x_20359
-| ANL x_20361 -> h_ANL x_20361
-| ORL x_20362 -> h_ORL x_20362
-| XRL x_20363 -> h_XRL x_20363
-| CLR x_20364 -> h_CLR x_20364
-| CPL x_20365 -> h_CPL x_20365
-| RL x_20366 -> h_RL x_20366
-| RLC x_20367 -> h_RLC x_20367
-| RR x_20368 -> h_RR x_20368
-| RRC x_20369 -> h_RRC x_20369
-| SWAP x_20370 -> h_SWAP x_20370
-| MOV x_20371 -> h_MOV x_20371
-| MOVX x_20372 -> h_MOVX x_20372
-| SETB x_20373 -> h_SETB x_20373
-| PUSH x_20374 -> h_PUSH x_20374
-| POP x_20375 -> h_POP x_20375
-| XCH (x_20377, x_20376) -> h_XCH x_20377 x_20376
-| XCHD (x_20379, x_20378) -> h_XCHD x_20379 x_20378
+| ADD (x_1208, x_1207) -> h_ADD x_1208 x_1207
+| ADDC (x_1210, x_1209) -> h_ADDC x_1210 x_1209
+| SUBB (x_1212, x_1211) -> h_SUBB x_1212 x_1211
+| INC x_1213 -> h_INC x_1213
+| DEC x_1214 -> h_DEC x_1214
+| MUL (x_1216, x_1215) -> h_MUL x_1216 x_1215
+| DIV (x_1218, x_1217) -> h_DIV x_1218 x_1217
+| DA x_1219 -> h_DA x_1219
+| JC x_1220 -> h_JC x_1220
+| JNC x_1221 -> h_JNC x_1221
+| JB (x_1223, x_1222) -> h_JB x_1223 x_1222
+| JNB (x_1225, x_1224) -> h_JNB x_1225 x_1224
+| JBC (x_1227, x_1226) -> h_JBC x_1227 x_1226
+| JZ x_1228 -> h_JZ x_1228
+| JNZ x_1229 -> h_JNZ x_1229
+| CJNE (x_1231, x_1230) -> h_CJNE x_1231 x_1230
+| DJNZ (x_1233, x_1232) -> h_DJNZ x_1233 x_1232
+| ANL x_1234 -> h_ANL x_1234
+| ORL x_1235 -> h_ORL x_1235
+| XRL x_1236 -> h_XRL x_1236
+| CLR x_1237 -> h_CLR x_1237
+| CPL x_1238 -> h_CPL x_1238
+| RL x_1239 -> h_RL x_1239
+| RLC x_1240 -> h_RLC x_1240
+| RR x_1241 -> h_RR x_1241
+| RRC x_1242 -> h_RRC x_1242
+| SWAP x_1243 -> h_SWAP x_1243
+| MOV x_1244 -> h_MOV x_1244
+| MOVX x_1245 -> h_MOVX x_1245
+| SETB x_1246 -> h_SETB x_1246
+| PUSH x_1247 -> h_PUSH x_1247
+| POP x_1248 -> h_POP x_1248
+| XCH (x_1250, x_1249) -> h_XCH x_1250 x_1249
+| XCHD (x_1252, x_1251) -> h_XCHD x_1252 x_1251
| RET -> h_RET
| RETI -> h_RETI
| NOP -> h_NOP
-| JMP x_20380 -> h_JMP x_20380
+| JMP x_1253 -> h_JMP x_1253
(** val preinstruction_inv_rect_Type4 :
'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
-> 'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction ->
'a1 **)
let rec instruction_rect_Type4 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
-| ACALL x_20952 -> h_ACALL x_20952
-| LCALL x_20953 -> h_LCALL x_20953
-| AJMP x_20954 -> h_AJMP x_20954
-| LJMP x_20955 -> h_LJMP x_20955
-| SJMP x_20956 -> h_SJMP x_20956
-| MOVC (x_20958, x_20957) -> h_MOVC x_20958 x_20957
-| RealInstruction x_20959 -> h_RealInstruction x_20959
+| ACALL x_1825 -> h_ACALL x_1825
+| LCALL x_1826 -> h_LCALL x_1826
+| AJMP x_1827 -> h_AJMP x_1827
+| LJMP x_1828 -> h_LJMP x_1828
+| SJMP x_1829 -> h_SJMP x_1829
+| MOVC (x_1831, x_1830) -> h_MOVC x_1831 x_1830
+| RealInstruction x_1832 -> h_RealInstruction x_1832
(** val instruction_rect_Type5 :
(subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
-> 'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction ->
'a1 **)
let rec instruction_rect_Type5 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
-| ACALL x_20968 -> h_ACALL x_20968
-| LCALL x_20969 -> h_LCALL x_20969
-| AJMP x_20970 -> h_AJMP x_20970
-| LJMP x_20971 -> h_LJMP x_20971
-| SJMP x_20972 -> h_SJMP x_20972
-| MOVC (x_20974, x_20973) -> h_MOVC x_20974 x_20973
-| RealInstruction x_20975 -> h_RealInstruction x_20975
+| ACALL x_1841 -> h_ACALL x_1841
+| LCALL x_1842 -> h_LCALL x_1842
+| AJMP x_1843 -> h_AJMP x_1843
+| LJMP x_1844 -> h_LJMP x_1844
+| SJMP x_1845 -> h_SJMP x_1845
+| MOVC (x_1847, x_1846) -> h_MOVC x_1847 x_1846
+| RealInstruction x_1848 -> h_RealInstruction x_1848
(** val instruction_rect_Type3 :
(subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
-> 'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction ->
'a1 **)
let rec instruction_rect_Type3 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
-| ACALL x_20984 -> h_ACALL x_20984
-| LCALL x_20985 -> h_LCALL x_20985
-| AJMP x_20986 -> h_AJMP x_20986
-| LJMP x_20987 -> h_LJMP x_20987
-| SJMP x_20988 -> h_SJMP x_20988
-| MOVC (x_20990, x_20989) -> h_MOVC x_20990 x_20989
-| RealInstruction x_20991 -> h_RealInstruction x_20991
+| ACALL x_1857 -> h_ACALL x_1857
+| LCALL x_1858 -> h_LCALL x_1858
+| AJMP x_1859 -> h_AJMP x_1859
+| LJMP x_1860 -> h_LJMP x_1860
+| SJMP x_1861 -> h_SJMP x_1861
+| MOVC (x_1863, x_1862) -> h_MOVC x_1863 x_1862
+| RealInstruction x_1864 -> h_RealInstruction x_1864
(** val instruction_rect_Type2 :
(subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
-> 'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction ->
'a1 **)
let rec instruction_rect_Type2 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
-| ACALL x_21000 -> h_ACALL x_21000
-| LCALL x_21001 -> h_LCALL x_21001
-| AJMP x_21002 -> h_AJMP x_21002
-| LJMP x_21003 -> h_LJMP x_21003
-| SJMP x_21004 -> h_SJMP x_21004
-| MOVC (x_21006, x_21005) -> h_MOVC x_21006 x_21005
-| RealInstruction x_21007 -> h_RealInstruction x_21007
+| ACALL x_1873 -> h_ACALL x_1873
+| LCALL x_1874 -> h_LCALL x_1874
+| AJMP x_1875 -> h_AJMP x_1875
+| LJMP x_1876 -> h_LJMP x_1876
+| SJMP x_1877 -> h_SJMP x_1877
+| MOVC (x_1879, x_1878) -> h_MOVC x_1879 x_1878
+| RealInstruction x_1880 -> h_RealInstruction x_1880
(** val instruction_rect_Type1 :
(subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
-> 'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction ->
'a1 **)
let rec instruction_rect_Type1 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
-| ACALL x_21016 -> h_ACALL x_21016
-| LCALL x_21017 -> h_LCALL x_21017
-| AJMP x_21018 -> h_AJMP x_21018
-| LJMP x_21019 -> h_LJMP x_21019
-| SJMP x_21020 -> h_SJMP x_21020
-| MOVC (x_21022, x_21021) -> h_MOVC x_21022 x_21021
-| RealInstruction x_21023 -> h_RealInstruction x_21023
+| ACALL x_1889 -> h_ACALL x_1889
+| LCALL x_1890 -> h_LCALL x_1890
+| AJMP x_1891 -> h_AJMP x_1891
+| LJMP x_1892 -> h_LJMP x_1892
+| SJMP x_1893 -> h_SJMP x_1893
+| MOVC (x_1895, x_1894) -> h_MOVC x_1895 x_1894
+| RealInstruction x_1896 -> h_RealInstruction x_1896
(** val instruction_rect_Type0 :
(subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
-> 'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction ->
'a1 **)
let rec instruction_rect_Type0 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
-| ACALL x_21032 -> h_ACALL x_21032
-| LCALL x_21033 -> h_LCALL x_21033
-| AJMP x_21034 -> h_AJMP x_21034
-| LJMP x_21035 -> h_LJMP x_21035
-| SJMP x_21036 -> h_SJMP x_21036
-| MOVC (x_21038, x_21037) -> h_MOVC x_21038 x_21037
-| RealInstruction x_21039 -> h_RealInstruction x_21039
+| ACALL x_1905 -> h_ACALL x_1905
+| LCALL x_1906 -> h_LCALL x_1906
+| AJMP x_1907 -> h_AJMP x_1907
+| LJMP x_1908 -> h_LJMP x_1908
+| SJMP x_1909 -> h_SJMP x_1909
+| MOVC (x_1911, x_1910) -> h_MOVC x_1911 x_1910
+| RealInstruction x_1912 -> h_RealInstruction x_1912
(** val instruction_inv_rect_Type4 :
instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode
Types.sum -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction
-> 'a1 **)
let rec pseudo_instruction_rect_Type4 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function
-| Instruction x_21202 -> h_Instruction x_21202
-| Comment x_21203 -> h_Comment x_21203
-| Cost x_21204 -> h_Cost x_21204
-| Jmp x_21205 -> h_Jmp x_21205
-| Jnz (x_21208, x_21207, x_21206) -> h_Jnz x_21208 x_21207 x_21206
-| Call x_21209 -> h_Call x_21209
-| Mov (x_21212, x_21211, x_21210) -> h_Mov x_21212 x_21211 x_21210
+| Instruction x_2075 -> h_Instruction x_2075
+| Comment x_2076 -> h_Comment x_2076
+| Cost x_2077 -> h_Cost x_2077
+| Jmp x_2078 -> h_Jmp x_2078
+| Jnz (x_2081, x_2080, x_2079) -> h_Jnz x_2081 x_2080 x_2079
+| Call x_2082 -> h_Call x_2082
+| Mov (x_2085, x_2084, x_2083) -> h_Mov x_2085 x_2084 x_2083
(** val pseudo_instruction_rect_Type5 :
(identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
Types.sum -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction
-> 'a1 **)
let rec pseudo_instruction_rect_Type5 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function
-| Instruction x_21221 -> h_Instruction x_21221
-| Comment x_21222 -> h_Comment x_21222
-| Cost x_21223 -> h_Cost x_21223
-| Jmp x_21224 -> h_Jmp x_21224
-| Jnz (x_21227, x_21226, x_21225) -> h_Jnz x_21227 x_21226 x_21225
-| Call x_21228 -> h_Call x_21228
-| Mov (x_21231, x_21230, x_21229) -> h_Mov x_21231 x_21230 x_21229
+| Instruction x_2094 -> h_Instruction x_2094
+| Comment x_2095 -> h_Comment x_2095
+| Cost x_2096 -> h_Cost x_2096
+| Jmp x_2097 -> h_Jmp x_2097
+| Jnz (x_2100, x_2099, x_2098) -> h_Jnz x_2100 x_2099 x_2098
+| Call x_2101 -> h_Call x_2101
+| Mov (x_2104, x_2103, x_2102) -> h_Mov x_2104 x_2103 x_2102
(** val pseudo_instruction_rect_Type3 :
(identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
Types.sum -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction
-> 'a1 **)
let rec pseudo_instruction_rect_Type3 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function
-| Instruction x_21240 -> h_Instruction x_21240
-| Comment x_21241 -> h_Comment x_21241
-| Cost x_21242 -> h_Cost x_21242
-| Jmp x_21243 -> h_Jmp x_21243
-| Jnz (x_21246, x_21245, x_21244) -> h_Jnz x_21246 x_21245 x_21244
-| Call x_21247 -> h_Call x_21247
-| Mov (x_21250, x_21249, x_21248) -> h_Mov x_21250 x_21249 x_21248
+| Instruction x_2113 -> h_Instruction x_2113
+| Comment x_2114 -> h_Comment x_2114
+| Cost x_2115 -> h_Cost x_2115
+| Jmp x_2116 -> h_Jmp x_2116
+| Jnz (x_2119, x_2118, x_2117) -> h_Jnz x_2119 x_2118 x_2117
+| Call x_2120 -> h_Call x_2120
+| Mov (x_2123, x_2122, x_2121) -> h_Mov x_2123 x_2122 x_2121
(** val pseudo_instruction_rect_Type2 :
(identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
Types.sum -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction
-> 'a1 **)
let rec pseudo_instruction_rect_Type2 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function
-| Instruction x_21259 -> h_Instruction x_21259
-| Comment x_21260 -> h_Comment x_21260
-| Cost x_21261 -> h_Cost x_21261
-| Jmp x_21262 -> h_Jmp x_21262
-| Jnz (x_21265, x_21264, x_21263) -> h_Jnz x_21265 x_21264 x_21263
-| Call x_21266 -> h_Call x_21266
-| Mov (x_21269, x_21268, x_21267) -> h_Mov x_21269 x_21268 x_21267
+| Instruction x_2132 -> h_Instruction x_2132
+| Comment x_2133 -> h_Comment x_2133
+| Cost x_2134 -> h_Cost x_2134
+| Jmp x_2135 -> h_Jmp x_2135
+| Jnz (x_2138, x_2137, x_2136) -> h_Jnz x_2138 x_2137 x_2136
+| Call x_2139 -> h_Call x_2139
+| Mov (x_2142, x_2141, x_2140) -> h_Mov x_2142 x_2141 x_2140
(** val pseudo_instruction_rect_Type1 :
(identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
Types.sum -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction
-> 'a1 **)
let rec pseudo_instruction_rect_Type1 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function
-| Instruction x_21278 -> h_Instruction x_21278
-| Comment x_21279 -> h_Comment x_21279
-| Cost x_21280 -> h_Cost x_21280
-| Jmp x_21281 -> h_Jmp x_21281
-| Jnz (x_21284, x_21283, x_21282) -> h_Jnz x_21284 x_21283 x_21282
-| Call x_21285 -> h_Call x_21285
-| Mov (x_21288, x_21287, x_21286) -> h_Mov x_21288 x_21287 x_21286
+| Instruction x_2151 -> h_Instruction x_2151
+| Comment x_2152 -> h_Comment x_2152
+| Cost x_2153 -> h_Cost x_2153
+| Jmp x_2154 -> h_Jmp x_2154
+| Jnz (x_2157, x_2156, x_2155) -> h_Jnz x_2157 x_2156 x_2155
+| Call x_2158 -> h_Call x_2158
+| Mov (x_2161, x_2160, x_2159) -> h_Mov x_2161 x_2160 x_2159
(** val pseudo_instruction_rect_Type0 :
(identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
Types.sum -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction
-> 'a1 **)
let rec pseudo_instruction_rect_Type0 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function
-| Instruction x_21297 -> h_Instruction x_21297
-| Comment x_21298 -> h_Comment x_21298
-| Cost x_21299 -> h_Cost x_21299
-| Jmp x_21300 -> h_Jmp x_21300
-| Jnz (x_21303, x_21302, x_21301) -> h_Jnz x_21303 x_21302 x_21301
-| Call x_21304 -> h_Call x_21304
-| Mov (x_21307, x_21306, x_21305) -> h_Mov x_21307 x_21306 x_21305
+| Instruction x_2170 -> h_Instruction x_2170
+| Comment x_2171 -> h_Comment x_2171
+| Cost x_2172 -> h_Cost x_2172
+| Jmp x_2173 -> h_Jmp x_2173
+| Jnz (x_2176, x_2175, x_2174) -> h_Jnz x_2176 x_2175 x_2174
+| Call x_2177 -> h_Call x_2177
+| Mov (x_2180, x_2179, x_2178) -> h_Mov x_2180 x_2179 x_2178
(** val pseudo_instruction_inv_rect_Type4 :
pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
labelled_instruction List.list -> __ -> (identifier, AST.ident)
Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
pseudo_assembly_program -> 'a1 **)
-let rec pseudo_assembly_program_rect_Type4 h_mk_pseudo_assembly_program x_21431 =
+let rec pseudo_assembly_program_rect_Type4 h_mk_pseudo_assembly_program x_2304 =
let { preamble = preamble0; code = code0; renamed_symbols =
- renamed_symbols0; final_label = final_label0 } = x_21431
+ renamed_symbols0; final_label = final_label0 } = x_2304
in
h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
final_label0 __ __
labelled_instruction List.list -> __ -> (identifier, AST.ident)
Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
pseudo_assembly_program -> 'a1 **)
-let rec pseudo_assembly_program_rect_Type5 h_mk_pseudo_assembly_program x_21433 =
+let rec pseudo_assembly_program_rect_Type5 h_mk_pseudo_assembly_program x_2306 =
let { preamble = preamble0; code = code0; renamed_symbols =
- renamed_symbols0; final_label = final_label0 } = x_21433
+ renamed_symbols0; final_label = final_label0 } = x_2306
in
h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
final_label0 __ __
labelled_instruction List.list -> __ -> (identifier, AST.ident)
Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
pseudo_assembly_program -> 'a1 **)
-let rec pseudo_assembly_program_rect_Type3 h_mk_pseudo_assembly_program x_21435 =
+let rec pseudo_assembly_program_rect_Type3 h_mk_pseudo_assembly_program x_2308 =
let { preamble = preamble0; code = code0; renamed_symbols =
- renamed_symbols0; final_label = final_label0 } = x_21435
+ renamed_symbols0; final_label = final_label0 } = x_2308
in
h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
final_label0 __ __
labelled_instruction List.list -> __ -> (identifier, AST.ident)
Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
pseudo_assembly_program -> 'a1 **)
-let rec pseudo_assembly_program_rect_Type2 h_mk_pseudo_assembly_program x_21437 =
+let rec pseudo_assembly_program_rect_Type2 h_mk_pseudo_assembly_program x_2310 =
let { preamble = preamble0; code = code0; renamed_symbols =
- renamed_symbols0; final_label = final_label0 } = x_21437
+ renamed_symbols0; final_label = final_label0 } = x_2310
in
h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
final_label0 __ __
labelled_instruction List.list -> __ -> (identifier, AST.ident)
Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
pseudo_assembly_program -> 'a1 **)
-let rec pseudo_assembly_program_rect_Type1 h_mk_pseudo_assembly_program x_21439 =
+let rec pseudo_assembly_program_rect_Type1 h_mk_pseudo_assembly_program x_2312 =
let { preamble = preamble0; code = code0; renamed_symbols =
- renamed_symbols0; final_label = final_label0 } = x_21439
+ renamed_symbols0; final_label = final_label0 } = x_2312
in
h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
final_label0 __ __
labelled_instruction List.list -> __ -> (identifier, AST.ident)
Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
pseudo_assembly_program -> 'a1 **)
-let rec pseudo_assembly_program_rect_Type0 h_mk_pseudo_assembly_program x_21441 =
+let rec pseudo_assembly_program_rect_Type0 h_mk_pseudo_assembly_program x_2314 =
let { preamble = preamble0; code = code0; renamed_symbols =
- renamed_symbols0; final_label = final_label0 } = x_21441
+ renamed_symbols0; final_label = final_label0 } = x_2314
in
h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
final_label0 __ __
let load_code_memory0 program =
(Types.pi1
(FoldStuff.foldl_strong program (fun prefix v tl _ i_mem ->
- (let { Types.fst = i; Types.snd = mem } = Types.pi1 i_mem in
- (fun _ -> { Types.fst = (Nat.S i); Types.snd =
+ (let { Types.fst = eta24568; Types.snd = mem } = Types.pi1 i_mem in
+ (fun _ ->
+ (let { Types.fst = i; Types.snd = bvi } = eta24568 in
+ (fun _ -> { Types.fst = { Types.fst = (Nat.S i); Types.snd =
+ (Arithmetic.increment (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ Nat.O)))))))))))))))) bvi) }; Types.snd =
(BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- Nat.O))))))))))))))))
- (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S Nat.O)))))))))))))))) i) v mem) })) __) { Types.fst =
- Nat.O; Types.snd = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S
+ Nat.O)))))))))))))))) bvi v mem) })) __)) __) { Types.fst =
+ { Types.fst = Nat.O; Types.snd =
+ (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ Nat.O))))))))))))))))) }; Types.snd = (BitVectorTrie.Stub (Nat.S
(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S Nat.O))))))))))))))))) })).Types.snd
+ (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))) })).Types.snd
(** val load_code_memory :
object_code -> BitVector.byte BitVectorTrie.bitVectorTrie **)
(object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
labelled_object_code -> 'a1 **)
-let rec labelled_object_code_rect_Type4 h_mk_labelled_object_code x_21457 =
+let rec labelled_object_code_rect_Type4 h_mk_labelled_object_code x_2330 =
let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
- symboltable0; final_pc = final_pc0 } = x_21457
+ symboltable0; final_pc = final_pc0 } = x_2330
in
h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __
(object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
labelled_object_code -> 'a1 **)
-let rec labelled_object_code_rect_Type5 h_mk_labelled_object_code x_21459 =
+let rec labelled_object_code_rect_Type5 h_mk_labelled_object_code x_2332 =
let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
- symboltable0; final_pc = final_pc0 } = x_21459
+ symboltable0; final_pc = final_pc0 } = x_2332
in
h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __
(object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
labelled_object_code -> 'a1 **)
-let rec labelled_object_code_rect_Type3 h_mk_labelled_object_code x_21461 =
+let rec labelled_object_code_rect_Type3 h_mk_labelled_object_code x_2334 =
let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
- symboltable0; final_pc = final_pc0 } = x_21461
+ symboltable0; final_pc = final_pc0 } = x_2334
in
h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __
(object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
labelled_object_code -> 'a1 **)
-let rec labelled_object_code_rect_Type2 h_mk_labelled_object_code x_21463 =
+let rec labelled_object_code_rect_Type2 h_mk_labelled_object_code x_2336 =
let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
- symboltable0; final_pc = final_pc0 } = x_21463
+ symboltable0; final_pc = final_pc0 } = x_2336
in
h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __
(object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
labelled_object_code -> 'a1 **)
-let rec labelled_object_code_rect_Type1 h_mk_labelled_object_code x_21465 =
+let rec labelled_object_code_rect_Type1 h_mk_labelled_object_code x_2338 =
let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
- symboltable0; final_pc = final_pc0 } = x_21465
+ symboltable0; final_pc = final_pc0 } = x_2338
in
h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __
(object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
labelled_object_code -> 'a1 **)
-let rec labelled_object_code_rect_Type0 h_mk_labelled_object_code x_21467 =
+let rec labelled_object_code_rect_Type0 h_mk_labelled_object_code x_2340 =
let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
- symboltable0; final_pc = final_pc0 } = x_21467
+ symboltable0; final_pc = final_pc0 } = x_2340
in
h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __
| Nat.O -> (fun _ -> Nat.O)
| Nat.S program_size' ->
(fun _ ->
- (let { Types.fst = eta31588; Types.snd = ticks } =
+ (let { Types.fst = eta302; Types.snd = ticks } =
Fetch.fetch prog.ASM.cm program_counter'
in
let { Types.fst = instruction; Types.snd = program_counter'' } =
- eta31588
+ eta302
in
(fun _ ->
let to_continue =
| ASM.MOVC (x, x0) -> StructuredTraces.Cl_other
| ASM.RealInstruction pre -> aSM_classify00 pre
-(** val current_instruction0 :
- BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
- ASM.instruction **)
-let current_instruction0 code_memory program_counter =
- (Fetch.fetch code_memory program_counter).Types.fst.Types.fst
-
(** val current_instruction :
BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
ASM.instruction **)
let current_instruction code_memory s =
- current_instruction0 code_memory s.Status.program_counter
+ (Fetch.fetch code_memory s.Status.program_counter).Types.fst.Types.fst
(** val current_instruction_label :
- BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
- BitVectorTrie.bitVectorTrie -> Status.status -> CostLabel.costlabel
- Types.option **)
+ BitVector.byte BitVectorTrie.bitVectorTrie -> ASM.costlabel_map ->
+ Status.status -> CostLabel.costlabel Types.option **)
let current_instruction_label code_memory cost_labels s =
let pc = s.Status.program_counter in
BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
val aSM_classify0 : ASM.instruction -> StructuredTraces.status_class
-val current_instruction0 :
- BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
- ASM.instruction
-
val current_instruction :
BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
ASM.instruction
val current_instruction_label :
- BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
- BitVectorTrie.bitVectorTrie -> Status.status -> CostLabel.costlabel
- Types.option
+ BitVector.byte BitVectorTrie.bitVectorTrie -> ASM.costlabel_map ->
+ Status.status -> CostLabel.costlabel Types.option
val word_deqset : Deqsets.deqSet
observe_pass -> ASM.pseudo_assembly_program -> ASM.labelled_object_code
Errors.res **)
let assembler observe p =
+prerr_endline "Y1";
Obj.magic
(Monad.m_bind0 (Monad.max_def Errors.res0)
(Obj.magic
(Errors.opt_to_res (Errors.msg ErrorMessages.Jump_expansion_failed)
(Policy.jump_expansion' p))) (fun sigma_pol ->
+prerr_endline "Y2";
let sigma = fun ppc -> (Types.pi1 sigma_pol).Types.fst ppc in
let pol = fun ppc -> (Types.pi1 sigma_pol).Types.snd ppc in
let i =
Obj.magic observe Assembly_pass { Types.fst = { Types.fst = p;
Types.snd = sigma }; Types.snd = pol }
in
+prerr_endline "Y3";
let p0 = Assembly.assembly p sigma pol in
+prerr_endline "Y4";
let i0 = Obj.magic observe Object_code_pass (Types.pi1 p0) in
+prerr_endline "Y5";
Obj.magic (Errors.OK (Types.pi1 p0))))
open StructuredTraces
(((ASM.pseudo_assembly_program, CostLabel.costlabel) Types.prod,
Joint.stack_cost_model) Types.prod, Nat.nat) Types.prod Errors.res
-open Assembly
-
open Status
open Fetch
+open Assembly
+
open PolicyFront
open PolicyStep
open Preamble
+open Types
+
+open Hints_declaration
+
+open Core_notation
+
+open Pts
+
+open Logic
+
+open Jmeq
+
+open Russell
+
open Exp
open Setoids
open Div_and_mod
-open Jmeq
-
-open Russell
-
-open Types
-
open List
open Util
open Bool
-open Hints_declaration
-
-open Core_notation
-
-open Pts
-
-open Logic
-
open Relations
open Nat
open ASM
-(** val inefficient_address_of_word_labels_code_mem :
- ASM.labelled_instruction List.list -> ASM.identifier ->
- BitVector.bitVector **)
-let inefficient_address_of_word_labels_code_mem code_mem id =
- Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- Nat.O))))))))))))))))
- (LabelledObjects.index_of
- (LabelledObjects.instruction_matches_identifier PreIdentifiers.ASMTag
- id) code_mem)
+(** val inefficient_address_of_label :
+ ASM.labelled_instruction List.list -> ASM.identifier -> Nat.nat **)
+let inefficient_address_of_label instr_list id =
+ LabelledObjects.index_of
+ (LabelledObjects.instruction_matches_identifier PreIdentifiers.ASMTag id)
+ instr_list
type label_map = Nat.nat Identifiers.identifier_map
(** val create_label_cost_map0 :
- ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
- BitVectorTrie.bitVectorTrie) Types.prod Types.sig0 **)
+ ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map)
+ Types.prod Types.sig0 **)
let create_label_cost_map0 program =
(Types.pi1
(FoldStuff.foldl_strong program (fun prefix x tl _ labels_costs_ppc ->
- (let { Types.fst = eta28695; Types.snd = ppc } =
+ (let { Types.fst = eta19; Types.snd = ppc } =
Types.pi1 labels_costs_ppc
in
(fun _ ->
- (let { Types.fst = labels; Types.snd = costs } = eta28695 in
+ (let { Types.fst = labels; Types.snd = costs } = eta19 in
(fun _ ->
(let { Types.fst = label; Types.snd = instr } = x in
(fun _ ->
Nat.O))))))))))))))))) }; Types.snd = Nat.O })).Types.fst
(** val create_label_cost_map :
- ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
- BitVectorTrie.bitVectorTrie) Types.prod **)
+ ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map)
+ Types.prod **)
let create_label_cost_map program =
Types.pi1 (create_label_cost_map0 program)
(** val address_of_word_labels :
ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.word **)
-let address_of_word_labels code_mem id =
- let labels = (create_label_cost_map code_mem).Types.fst in
+let address_of_word_labels program id =
+ let labels = (create_label_cost_map program).Types.fst in
+ let address_of_label = fun l ->
+ Identifiers.lookup_def PreIdentifiers.ASMTag labels l Nat.O
+ in
Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- Nat.O))))))))))))))))
- (Identifiers.lookup_def PreIdentifiers.ASMTag labels id Nat.O)
-
-(** val bitvector_max_nat : Nat.nat -> Nat.nat **)
-let bitvector_max_nat length =
- Exp.exp (Nat.S (Nat.S Nat.O)) length
-
-(** val code_memory_size : Nat.nat **)
-let code_memory_size =
- bitvector_max_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- Nat.O))))))))))))))))
+ Nat.O)))))))))))))))) (address_of_label id)
(** val prod_inv_rect_Type0 :
('a1, 'a2) Types.prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
open Preamble
+open Types
+
+open Hints_declaration
+
+open Core_notation
+
+open Pts
+
+open Logic
+
+open Jmeq
+
+open Russell
+
open Exp
open Setoids
open Div_and_mod
-open Jmeq
-
-open Russell
-
-open Types
-
open List
open Util
open Bool
-open Hints_declaration
-
-open Core_notation
-
-open Pts
-
-open Logic
-
open Relations
open Nat
open ASM
-val inefficient_address_of_word_labels_code_mem :
- ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.bitVector
+val inefficient_address_of_label :
+ ASM.labelled_instruction List.list -> ASM.identifier -> Nat.nat
type label_map = Nat.nat Identifiers.identifier_map
val create_label_cost_map0 :
- ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
- BitVectorTrie.bitVectorTrie) Types.prod Types.sig0
+ ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map)
+ Types.prod Types.sig0
val create_label_cost_map :
- ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
- BitVectorTrie.bitVectorTrie) Types.prod
+ ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map)
+ Types.prod
val address_of_word_labels :
ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.word
-val bitvector_max_nat : Nat.nat -> Nat.nat
-
-val code_memory_size : Nat.nat
-
val prod_inv_rect_Type0 :
('a1, 'a2) Types.prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
genv_t, GenMem.mem) Types.prod **)
let add_globals extract_init init_env vars =
Util.foldl (fun g_st id_init ->
- let { Types.fst = eta1345; Types.snd = init_info } = id_init in
- let { Types.fst = id; Types.snd = r } = eta1345 in
+ let { Types.fst = eta1367; Types.snd = init_info } = id_init in
+ let { Types.fst = id; Types.snd = r } = eta1367 in
let init = extract_init init_info in
let { Types.fst = g; Types.snd = st } = g_st in
let { Types.fst = st'; Types.snd = b } =
GenMem.mem Errors.res **)
let init_globals extract_init g m vars =
Util.foldl (fun st id_init ->
- let { Types.fst = eta1346; Types.snd = init_info } = id_init in
- let { Types.fst = id; Types.snd = r } = eta1346 in
+ let { Types.fst = eta1368; Types.snd = init_info } = id_init in
+ let { Types.fst = id; Types.snd = r } = eta1368 in
let init = extract_init init_info in
Obj.magic
(Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic st) (fun st0 ->
(execute_1_pseudo_instruction' c addr_of_label addr_of_symbol sigma
policy (Obj.magic st))) (Obj.magic (Status.initialise_status c))
+(** val aSM_status :
+ ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
+ (BitVector.word -> Bool.bool) -> StructuredTraces.abstract_status **)
+let aSM_status c sigma policy =
+ let label_map = (Fetch.create_label_cost_map c.ASM.code).Types.fst in
+ let symbol_map = Status.construct_datalabels c.ASM.preamble in
+ let addr_of_label = fun x ->
+ Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ Nat.O))))))))))))))))
+ (Identifiers.lookup_def PreIdentifiers.ASMTag label_map x Nat.O)
+ in
+ let addr_of_symbol = fun x ->
+ Identifiers.lookup_def PreIdentifiers.ASMTag symbol_map x
+ (addr_of_label x)
+ in
+ aSM_abstract_status c addr_of_label addr_of_symbol sigma policy
+
ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
(BitVector.word -> Bool.bool) -> Measurable.preclassified_system
+val aSM_status :
+ ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
+ (BitVector.word -> Bool.bool) -> StructuredTraces.abstract_status
+
(BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
printing_pass_independent_params -> 'a2 **)
-let rec printing_pass_independent_params_rect_Type4 h_mk_printing_pass_independent_params x_263 =
+let rec printing_pass_independent_params_rect_Type4 h_mk_printing_pass_independent_params x_25506 =
let { print_String = print_String0; print_keyword = print_keyword0;
print_concat = print_concat0; print_empty = print_empty0; print_ident =
print_ident0; print_costlabel = print_costlabel0; print_label =
print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
- print_bitvector0 } = x_263
+ print_bitvector0 } = x_25506
in
h_mk_printing_pass_independent_params print_String0 print_keyword0
print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
(BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
printing_pass_independent_params -> 'a2 **)
-let rec printing_pass_independent_params_rect_Type5 h_mk_printing_pass_independent_params x_265 =
+let rec printing_pass_independent_params_rect_Type5 h_mk_printing_pass_independent_params x_25508 =
let { print_String = print_String0; print_keyword = print_keyword0;
print_concat = print_concat0; print_empty = print_empty0; print_ident =
print_ident0; print_costlabel = print_costlabel0; print_label =
print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
- print_bitvector0 } = x_265
+ print_bitvector0 } = x_25508
in
h_mk_printing_pass_independent_params print_String0 print_keyword0
print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
(BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
printing_pass_independent_params -> 'a2 **)
-let rec printing_pass_independent_params_rect_Type3 h_mk_printing_pass_independent_params x_267 =
+let rec printing_pass_independent_params_rect_Type3 h_mk_printing_pass_independent_params x_25510 =
let { print_String = print_String0; print_keyword = print_keyword0;
print_concat = print_concat0; print_empty = print_empty0; print_ident =
print_ident0; print_costlabel = print_costlabel0; print_label =
print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
- print_bitvector0 } = x_267
+ print_bitvector0 } = x_25510
in
h_mk_printing_pass_independent_params print_String0 print_keyword0
print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
(BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
printing_pass_independent_params -> 'a2 **)
-let rec printing_pass_independent_params_rect_Type2 h_mk_printing_pass_independent_params x_269 =
+let rec printing_pass_independent_params_rect_Type2 h_mk_printing_pass_independent_params x_25512 =
let { print_String = print_String0; print_keyword = print_keyword0;
print_concat = print_concat0; print_empty = print_empty0; print_ident =
print_ident0; print_costlabel = print_costlabel0; print_label =
print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
- print_bitvector0 } = x_269
+ print_bitvector0 } = x_25512
in
h_mk_printing_pass_independent_params print_String0 print_keyword0
print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
(BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
printing_pass_independent_params -> 'a2 **)
-let rec printing_pass_independent_params_rect_Type1 h_mk_printing_pass_independent_params x_271 =
+let rec printing_pass_independent_params_rect_Type1 h_mk_printing_pass_independent_params x_25514 =
let { print_String = print_String0; print_keyword = print_keyword0;
print_concat = print_concat0; print_empty = print_empty0; print_ident =
print_ident0; print_costlabel = print_costlabel0; print_label =
print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
- print_bitvector0 } = x_271
+ print_bitvector0 } = x_25514
in
h_mk_printing_pass_independent_params print_String0 print_keyword0
print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
(BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
printing_pass_independent_params -> 'a2 **)
-let rec printing_pass_independent_params_rect_Type0 h_mk_printing_pass_independent_params x_273 =
+let rec printing_pass_independent_params_rect_Type0 h_mk_printing_pass_independent_params x_25516 =
let { print_String = print_String0; print_keyword = print_keyword0;
print_concat = print_concat0; print_empty = print_empty0; print_ident =
print_ident0; print_costlabel = print_costlabel0; print_label =
print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
- print_bitvector0 } = x_273
+ print_bitvector0 } = x_25516
in
h_mk_printing_pass_independent_params print_String0 print_keyword0
print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0
(__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
-> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
printing_params -> 'a2 **)
-let rec printing_params_rect_Type4 p h_mk_printing_params x_301 =
+let rec printing_params_rect_Type4 p h_mk_printing_params x_25544 =
let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
print_pair_move = print_pair_move0; print_call_args = print_call_args0;
print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
- x_301
+ x_25544
in
h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
(__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
-> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
printing_params -> 'a2 **)
-let rec printing_params_rect_Type5 p h_mk_printing_params x_303 =
+let rec printing_params_rect_Type5 p h_mk_printing_params x_25546 =
let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
print_pair_move = print_pair_move0; print_call_args = print_call_args0;
print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
- x_303
+ x_25546
in
h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
(__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
-> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
printing_params -> 'a2 **)
-let rec printing_params_rect_Type3 p h_mk_printing_params x_305 =
+let rec printing_params_rect_Type3 p h_mk_printing_params x_25548 =
let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
print_pair_move = print_pair_move0; print_call_args = print_call_args0;
print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
- x_305
+ x_25548
in
h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
(__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
-> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
printing_params -> 'a2 **)
-let rec printing_params_rect_Type2 p h_mk_printing_params x_307 =
+let rec printing_params_rect_Type2 p h_mk_printing_params x_25550 =
let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
print_pair_move = print_pair_move0; print_call_args = print_call_args0;
print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
- x_307
+ x_25550
in
h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
(__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
-> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
printing_params -> 'a2 **)
-let rec printing_params_rect_Type1 p h_mk_printing_params x_309 =
+let rec printing_params_rect_Type1 p h_mk_printing_params x_25552 =
let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
print_pair_move = print_pair_move0; print_call_args = print_call_args0;
print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
- x_309
+ x_25552
in
h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
(__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
-> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
printing_params -> 'a2 **)
-let rec printing_params_rect_Type0 p h_mk_printing_params x_311 =
+let rec printing_params_rect_Type0 p h_mk_printing_params x_25554 =
let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0;
print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0;
print_pair_move = print_pair_move0; print_call_args = print_call_args0;
print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
- x_311
+ x_25554
in
h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0
(** val print_serialization_params_rect_Type4 :
Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
print_serialization_params -> 'a2 **)
-let rec print_serialization_params_rect_Type4 p h_mk_print_serialization_params x_340 =
+let rec print_serialization_params_rect_Type4 p h_mk_print_serialization_params x_25583 =
let { print_succ = print_succ0; print_code_point = print_code_point0 } =
- x_340
+ x_25583
in
h_mk_print_serialization_params print_succ0 print_code_point0
(** val print_serialization_params_rect_Type5 :
Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
print_serialization_params -> 'a2 **)
-let rec print_serialization_params_rect_Type5 p h_mk_print_serialization_params x_342 =
+let rec print_serialization_params_rect_Type5 p h_mk_print_serialization_params x_25585 =
let { print_succ = print_succ0; print_code_point = print_code_point0 } =
- x_342
+ x_25585
in
h_mk_print_serialization_params print_succ0 print_code_point0
(** val print_serialization_params_rect_Type3 :
Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
print_serialization_params -> 'a2 **)
-let rec print_serialization_params_rect_Type3 p h_mk_print_serialization_params x_344 =
+let rec print_serialization_params_rect_Type3 p h_mk_print_serialization_params x_25587 =
let { print_succ = print_succ0; print_code_point = print_code_point0 } =
- x_344
+ x_25587
in
h_mk_print_serialization_params print_succ0 print_code_point0
(** val print_serialization_params_rect_Type2 :
Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
print_serialization_params -> 'a2 **)
-let rec print_serialization_params_rect_Type2 p h_mk_print_serialization_params x_346 =
+let rec print_serialization_params_rect_Type2 p h_mk_print_serialization_params x_25589 =
let { print_succ = print_succ0; print_code_point = print_code_point0 } =
- x_346
+ x_25589
in
h_mk_print_serialization_params print_succ0 print_code_point0
(** val print_serialization_params_rect_Type1 :
Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
print_serialization_params -> 'a2 **)
-let rec print_serialization_params_rect_Type1 p h_mk_print_serialization_params x_348 =
+let rec print_serialization_params_rect_Type1 p h_mk_print_serialization_params x_25591 =
let { print_succ = print_succ0; print_code_point = print_code_point0 } =
- x_348
+ x_25591
in
h_mk_print_serialization_params print_succ0 print_code_point0
(** val print_serialization_params_rect_Type0 :
Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
print_serialization_params -> 'a2 **)
-let rec print_serialization_params_rect_Type0 p h_mk_print_serialization_params x_350 =
+let rec print_serialization_params_rect_Type0 p h_mk_print_serialization_params x_25593 =
let { print_succ = print_succ0; print_code_point = print_code_point0 } =
- x_350
+ x_25593
in
h_mk_print_serialization_params print_succ0 print_code_point0
Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
(__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
-> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
-let rec code_iteration_params_rect_Type4 p globals h_mk_code_iteration_params x_368 =
+let rec code_iteration_params_rect_Type4 p globals h_mk_code_iteration_params x_25611 =
let { cip_print_serialization_params = cip_print_serialization_params0;
- fold_code = fold_code0; print_statementT = print_statementT0 } = x_368
+ fold_code = fold_code0; print_statementT = print_statementT0 } = x_25611
in
h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
print_statementT0
Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
(__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
-> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
-let rec code_iteration_params_rect_Type5 p globals h_mk_code_iteration_params x_370 =
+let rec code_iteration_params_rect_Type5 p globals h_mk_code_iteration_params x_25613 =
let { cip_print_serialization_params = cip_print_serialization_params0;
- fold_code = fold_code0; print_statementT = print_statementT0 } = x_370
+ fold_code = fold_code0; print_statementT = print_statementT0 } = x_25613
in
h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
print_statementT0
Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
(__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
-> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
-let rec code_iteration_params_rect_Type3 p globals h_mk_code_iteration_params x_372 =
+let rec code_iteration_params_rect_Type3 p globals h_mk_code_iteration_params x_25615 =
let { cip_print_serialization_params = cip_print_serialization_params0;
- fold_code = fold_code0; print_statementT = print_statementT0 } = x_372
+ fold_code = fold_code0; print_statementT = print_statementT0 } = x_25615
in
h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
print_statementT0
Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
(__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
-> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
-let rec code_iteration_params_rect_Type2 p globals h_mk_code_iteration_params x_374 =
+let rec code_iteration_params_rect_Type2 p globals h_mk_code_iteration_params x_25617 =
let { cip_print_serialization_params = cip_print_serialization_params0;
- fold_code = fold_code0; print_statementT = print_statementT0 } = x_374
+ fold_code = fold_code0; print_statementT = print_statementT0 } = x_25617
in
h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
print_statementT0
Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
(__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
-> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
-let rec code_iteration_params_rect_Type1 p globals h_mk_code_iteration_params x_376 =
+let rec code_iteration_params_rect_Type1 p globals h_mk_code_iteration_params x_25619 =
let { cip_print_serialization_params = cip_print_serialization_params0;
- fold_code = fold_code0; print_statementT = print_statementT0 } = x_376
+ fold_code = fold_code0; print_statementT = print_statementT0 } = x_25619
in
h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
print_statementT0
Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
(__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
-> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
-let rec code_iteration_params_rect_Type0 p globals h_mk_code_iteration_params x_378 =
+let rec code_iteration_params_rect_Type0 p globals h_mk_code_iteration_params x_25621 =
let { cip_print_serialization_params = cip_print_serialization_params0;
- fold_code = fold_code0; print_statementT = print_statementT0 } = x_378
+ fold_code = fold_code0; print_statementT = print_statementT0 } = x_25621
in
h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
print_statementT0
(** val fold_code0 :
Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
-> (__ -> 'a2 -> 'a3 -> 'a3) -> __ -> __ -> 'a3 -> 'a3 **)
-let rec fold_code0 p globals xxx x_393 x_394 x_395 x_396 =
+let rec fold_code0 p globals xxx x_25636 x_25637 x_25638 x_25639 =
(let { cip_print_serialization_params = x; fold_code = yyy;
print_statementT = x0 } = xxx
in
- Obj.magic yyy) __ x_393 x_394 x_395 x_396
+ Obj.magic yyy) __ x_25636 x_25637 x_25638 x_25639
(** val print_statementT :
Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
(match pm_choose_with_pref m n with
| Types.None -> b
| Types.Some res ->
- let { Types.fst = eta2; Types.snd = m' } = res in
- let { Types.fst = pos; Types.snd = a } = eta2 in
+ let { Types.fst = eta32074; Types.snd = m' } = res in
+ let { Types.fst = pos; Types.snd = a } = eta32074 in
visit_graph next f (f pos a b) (next a) m' y)
(** val print_list :
(Identifiers.universe -> AST.ident -> ASM.identifier
Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
-let rec aSM_universe_rect_Type4 h_mk_ASM_universe x_21483 =
+let rec aSM_universe_rect_Type4 h_mk_ASM_universe x_588 =
let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
ident_map0; label_map = label_map0; fresh_cost_label =
- fresh_cost_label0 } = x_21483
+ fresh_cost_label0 } = x_588
in
h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
fresh_cost_label0
(Identifiers.universe -> AST.ident -> ASM.identifier
Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
-let rec aSM_universe_rect_Type5 h_mk_ASM_universe x_21485 =
+let rec aSM_universe_rect_Type5 h_mk_ASM_universe x_590 =
let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
ident_map0; label_map = label_map0; fresh_cost_label =
- fresh_cost_label0 } = x_21485
+ fresh_cost_label0 } = x_590
in
h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
fresh_cost_label0
(Identifiers.universe -> AST.ident -> ASM.identifier
Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
-let rec aSM_universe_rect_Type3 h_mk_ASM_universe x_21487 =
+let rec aSM_universe_rect_Type3 h_mk_ASM_universe x_592 =
let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
ident_map0; label_map = label_map0; fresh_cost_label =
- fresh_cost_label0 } = x_21487
+ fresh_cost_label0 } = x_592
in
h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
fresh_cost_label0
(Identifiers.universe -> AST.ident -> ASM.identifier
Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
-let rec aSM_universe_rect_Type2 h_mk_ASM_universe x_21489 =
+let rec aSM_universe_rect_Type2 h_mk_ASM_universe x_594 =
let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
ident_map0; label_map = label_map0; fresh_cost_label =
- fresh_cost_label0 } = x_21489
+ fresh_cost_label0 } = x_594
in
h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
fresh_cost_label0
(Identifiers.universe -> AST.ident -> ASM.identifier
Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
-let rec aSM_universe_rect_Type1 h_mk_ASM_universe x_21491 =
+let rec aSM_universe_rect_Type1 h_mk_ASM_universe x_596 =
let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
ident_map0; label_map = label_map0; fresh_cost_label =
- fresh_cost_label0 } = x_21491
+ fresh_cost_label0 } = x_596
in
h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
fresh_cost_label0
(Identifiers.universe -> AST.ident -> ASM.identifier
Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
-let rec aSM_universe_rect_Type0 h_mk_ASM_universe x_21493 =
+let rec aSM_universe_rect_Type0 h_mk_ASM_universe x_598 =
let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
ident_map0; label_map = label_map0; fresh_cost_label =
- fresh_cost_label0 } = x_21493
+ fresh_cost_label0 } = x_598
in
h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
fresh_cost_label0
Identifiers.lookup_def PreIdentifiers.SymbolTag u.label_map current
(Identifiers.empty_map PreIdentifiers.LabelTag)
in
- let { Types.fst = eta28616; Types.snd = lmap0 } =
+ let { Types.fst = eta2825; Types.snd = lmap0 } =
match Identifiers.lookup PreIdentifiers.LabelTag lmap l with
| Types.None ->
let { Types.fst = id; Types.snd = univ } =
{ Types.fst = { Types.fst = id; Types.snd = u.id_univ }; Types.snd =
lmap }
in
- let { Types.fst = id; Types.snd = univ } = eta28616 in
+ let { Types.fst = id; Types.snd = univ } = eta2825 in
{ Types.fst = { id_univ = univ; current_funct = current; ident_map =
u.ident_map; label_map =
(Identifiers.add PreIdentifiers.SymbolTag u.label_map current lmap0);
((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
ASM.labelled_instruction List.list List.list -> (ASM.identifier,
BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
-let rec init_mutable_rect_Type4 h_mk_init_mutable x_21509 =
+let rec init_mutable_rect_Type4 h_mk_init_mutable x_614 =
let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
- built_code = built_code0; built_preamble = built_preamble0 } = x_21509
+ built_code = built_code0; built_preamble = built_preamble0 } = x_614
in
h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
ASM.labelled_instruction List.list List.list -> (ASM.identifier,
BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
-let rec init_mutable_rect_Type5 h_mk_init_mutable x_21511 =
+let rec init_mutable_rect_Type5 h_mk_init_mutable x_616 =
let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
- built_code = built_code0; built_preamble = built_preamble0 } = x_21511
+ built_code = built_code0; built_preamble = built_preamble0 } = x_616
in
h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
ASM.labelled_instruction List.list List.list -> (ASM.identifier,
BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
-let rec init_mutable_rect_Type3 h_mk_init_mutable x_21513 =
+let rec init_mutable_rect_Type3 h_mk_init_mutable x_618 =
let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
- built_code = built_code0; built_preamble = built_preamble0 } = x_21513
+ built_code = built_code0; built_preamble = built_preamble0 } = x_618
in
h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
ASM.labelled_instruction List.list List.list -> (ASM.identifier,
BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
-let rec init_mutable_rect_Type2 h_mk_init_mutable x_21515 =
+let rec init_mutable_rect_Type2 h_mk_init_mutable x_620 =
let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
- built_code = built_code0; built_preamble = built_preamble0 } = x_21515
+ built_code = built_code0; built_preamble = built_preamble0 } = x_620
in
h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
ASM.labelled_instruction List.list List.list -> (ASM.identifier,
BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
-let rec init_mutable_rect_Type1 h_mk_init_mutable x_21517 =
+let rec init_mutable_rect_Type1 h_mk_init_mutable x_622 =
let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
- built_code = built_code0; built_preamble = built_preamble0 } = x_21517
+ built_code = built_code0; built_preamble = built_preamble0 } = x_622
in
h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
ASM.labelled_instruction List.list List.list -> (ASM.identifier,
BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
-let rec init_mutable_rect_Type0 h_mk_init_mutable x_21519 =
+let rec init_mutable_rect_Type0 h_mk_init_mutable x_624 =
let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
- built_code = built_code0; built_preamble = built_preamble0 } = x_21519
+ built_code = built_code0; built_preamble = built_preamble0 } = x_624
in
h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
Monad.smax_def__o__monad **)
let do_store_global m_mut id_reg_data =
Monad.m_bind0 (Monad.smax_def State.state_monad) m_mut (fun mut ->
- let { Types.fst = eta28633; Types.snd = data } = id_reg_data in
- let { Types.fst = id; Types.snd = reg } = eta28633 in
+ let { Types.fst = eta2842; Types.snd = data } = id_reg_data in
+ let { Types.fst = id; Types.snd = reg } = eta2842 in
Monad.m_bind0 (Monad.smax_def State.state_monad) (identifier_of_ident id)
(fun id0 ->
let mut0 = { virtual_dptr = { Types.fst = id0; Types.snd = Z.OZ };
let rec jump_expansion_internal program n =
let labels = PolicyFront.create_label_map (Types.pi1 program) in
let rec aux res =
-prerr_endline "JEI_start";
+prerr_endline "JEI";
let { Types.fst = no_ch; Types.snd = z } = res in
match z with
| Types.None ->
(PolicyStep.jump_expansion_step program (Types.pi1 labels)
op))
in
+prerr_endline "JES";
+let init =(PolicyFront.jump_expansion_start program (Types.pi1 labels)) in
aux
{ Types.fst = Bool.False; Types.snd =
- (Types.pi1
- (PolicyFront.jump_expansion_start program (Types.pi1 labels))) }
+ (Types.pi1 init) }
(*
(match n with
| Nat.O ->
(Nat.S Nat.O)))))))))))))))) ppc x.Types.snd { Types.fst = Nat.O;
Types.snd = Assembly.Short_jump }).Types.fst
in
+(*prerr_endline "Z3";*)
Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
(Nat.S Nat.O)))))))))))))))) pc); Types.snd = (fun ppc ->
open Preamble
-open Assembly
-
open Status
-open Fetch
-
open BitVectorTrie
open String
-open Exp
-
-open Arithmetic
-
-open Vector
-
-open FoldStuff
-
-open BitVector
-
-open Extranat
-
open Integers
open AST
open Errors
-open Extralib
+open Lists
+
+open Positive
+
+open Identifiers
+
+open CostLabel
+
+open ASM
+
+open Exp
open Setoids
open Option
+open Extranat
+
+open Vector
+
+open FoldStuff
+
+open BitVector
+
+open Arithmetic
+
+open Fetch
+
+open Assembly
+
open Div_and_mod
open Jmeq
open Util
-open List
-
-open Lists
-
open Bool
open Relations
open Nat
-open Positive
+open List
open Hints_declaration
open Types
-open Identifiers
-
-open CostLabel
-
-open ASM
+open Extralib
open PolicyFront
open Preamble
-open BitVectorTrie
+open Div_and_mod
-open String
+open Jmeq
-open Exp
+open Russell
-open Arithmetic
+open Util
-open Vector
+open Bool
-open FoldStuff
+open Relations
-open BitVector
+open Nat
-open Extranat
+open List
-open Integers
+open Hints_declaration
-open AST
+open Core_notation
-open LabelledObjects
+open Pts
-open Proper
+open Logic
-open PositiveMap
+open Types
-open Deqsets
+open Extralib
-open ErrorMessages
+open Status
-open PreIdentifiers
+open BitVectorTrie
-open Errors
+open String
-open Extralib
+open Integers
-open Setoids
+open AST
-open Monad
+open LabelledObjects
-open Option
+open Proper
-open Div_and_mod
+open PositiveMap
-open Jmeq
+open Deqsets
-open Russell
+open ErrorMessages
-open Util
+open PreIdentifiers
-open List
+open Errors
open Lists
-open Bool
+open Positive
-open Relations
+open Identifiers
-open Nat
+open CostLabel
-open Positive
+open ASM
-open Hints_declaration
+open Exp
-open Core_notation
+open Setoids
-open Pts
+open Monad
-open Logic
+open Option
-open Types
+open Extranat
-open Identifiers
+open Vector
-open CostLabel
+open FoldStuff
-open ASM
+open BitVector
-open Fetch
+open Arithmetic
-open Status
+open Fetch
open Assembly
ASM.labelled_instruction List.list Types.sig0 -> Fetch.label_map ->
ppc_pc_map Types.option Types.sig0 **)
let jump_expansion_start program labels =
- let final_policy =
- FoldStuff.foldl_strong (Types.pi1 program) (fun prefix x tl _ p ->
- let { Types.fst = pc; Types.snd = sigma } = Types.pi1 p in
- let { Types.fst = label; Types.snd = instr } = x in
- let isize = instruction_size_jmplen Assembly.Short_jump instr in
- { Types.fst = (Nat.plus pc isize); Types.snd =
- (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- Nat.O))))))))))))))))
- (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S (List.length prefix)))
- { Types.fst = (Nat.plus pc isize); Types.snd = Assembly.Short_jump }
- sigma) }) { Types.fst = Nat.O; Types.snd =
- (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- Nat.O))))))))))))))))
- (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S Nat.O)))))))))))))))) Nat.O) { Types.fst = Nat.O;
- Types.snd = Assembly.Short_jump } (BitVectorTrie.Stub (Nat.S (Nat.S
- (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))) }
- in
- (match Util.gtb (Types.pi1 final_policy).Types.fst
+ (let { Types.fst = ignore; Types.snd = final_policy } =
+ Types.pi1
+ (FoldStuff.foldl_strong (Types.pi1 program)
+ (fun prefix x tl _ acc_pol ->
+ (let { Types.fst = acc; Types.snd = p } = Types.pi1 acc_pol in
+ (fun _ ->
+ let { Types.fst = pc; Types.snd = sigma } = p in
+ let { Types.fst = label; Types.snd = instr } = x in
+ let isize = instruction_size_jmplen Assembly.Short_jump instr in
+ let sacc =
+ Arithmetic.increment (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ (Nat.S Nat.O)))))))))))))))) acc
+ in
+ { Types.fst = sacc; Types.snd = { Types.fst = (Nat.plus pc isize);
+ Types.snd =
+ (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ (Nat.S Nat.O)))))))))))))))) sacc { Types.fst =
+ (Nat.plus pc isize); Types.snd = Assembly.Short_jump } sigma) } }))
+ __) { Types.fst =
+ (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ Nat.O))))))))))))))))); Types.snd = { Types.fst = Nat.O;
+ Types.snd =
+ (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ (Nat.S Nat.O))))))))))))))))
+ (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ (Nat.S (Nat.S Nat.O)))))))))))))))) Nat.O) { Types.fst = Nat.O;
+ Types.snd = Assembly.Short_jump } (BitVectorTrie.Stub (Nat.S
+ (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))) } })
+ in
+ (fun _ ->
+ (match Util.gtb final_policy.Types.fst
(Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
(Nat.S (Nat.S Nat.O))))))))))))))))) with
| Bool.True -> (fun _ -> Types.None)
- | Bool.False -> (fun _ -> Types.Some (Types.pi1 final_policy))) __
+ | Bool.False -> (fun _ -> Types.Some final_policy)) __)) __
open Preamble
-open BitVectorTrie
+open Div_and_mod
-open String
+open Jmeq
-open Exp
+open Russell
-open Arithmetic
+open Util
-open Vector
+open Bool
-open FoldStuff
+open Relations
-open BitVector
+open Nat
-open Extranat
+open List
-open Integers
+open Hints_declaration
-open AST
+open Core_notation
-open LabelledObjects
+open Pts
-open Proper
+open Logic
-open PositiveMap
+open Types
-open Deqsets
+open Extralib
-open ErrorMessages
+open Status
-open PreIdentifiers
+open BitVectorTrie
-open Errors
+open String
-open Extralib
+open Integers
-open Setoids
+open AST
-open Monad
+open LabelledObjects
-open Option
+open Proper
-open Div_and_mod
+open PositiveMap
-open Jmeq
+open Deqsets
-open Russell
+open ErrorMessages
-open Util
+open PreIdentifiers
-open List
+open Errors
open Lists
-open Bool
+open Positive
-open Relations
+open Identifiers
-open Nat
+open CostLabel
-open Positive
+open ASM
-open Hints_declaration
+open Exp
-open Core_notation
+open Setoids
-open Pts
+open Monad
-open Logic
+open Option
-open Types
+open Extranat
-open Identifiers
+open Vector
-open CostLabel
+open FoldStuff
-open ASM
+open BitVector
-open Fetch
+open Arithmetic
-open Status
+open Fetch
open Assembly
open Preamble
-open Assembly
-
open Status
-open Fetch
-
open BitVectorTrie
open String
-open Exp
-
-open Arithmetic
-
-open Vector
-
-open FoldStuff
-
-open BitVector
-
-open Extranat
-
open Integers
open AST
open Errors
-open Extralib
+open Lists
+
+open Positive
+
+open Identifiers
+
+open CostLabel
+
+open ASM
+
+open Exp
open Setoids
open Option
+open Extranat
+
+open Vector
+
+open FoldStuff
+
+open BitVector
+
+open Arithmetic
+
+open Fetch
+
+open Assembly
+
open Div_and_mod
open Jmeq
open Util
-open List
-
-open Lists
-
open Bool
open Relations
open Nat
-open Positive
+open List
open Hints_declaration
open Types
-open Identifiers
-
-open CostLabel
-
-open ASM
+open Extralib
open PolicyFront
Types.sig0 -> PolicyFront.ppc_pc_map Types.sig0 -> (Bool.bool,
PolicyFront.ppc_pc_map Types.option) Types.prod Types.sig0 **)
let jump_expansion_step program labels old_sigma =
- (let { Types.fst = final_added; Types.snd = final_policy } =
+ (let { Types.fst = ignore; Types.snd = res } =
Types.pi1
- (FoldStuff.foldl_strong (Types.pi1 program) (fun prefix x tl _ acc ->
- (let { Types.fst = inc_added; Types.snd = inc_pc_sigma } =
- Types.pi1 acc
+ (FoldStuff.foldl_strong (Types.pi1 program)
+ (fun prefix x tl _ prefixlens_acc ->
+ (let { Types.fst = prefixlens; Types.snd = acc } =
+ Types.pi1 prefixlens_acc
+ in
+ (fun _ ->
+ (let { Types.fst = prefixlen; Types.snd = bvprefixlen } = prefixlens
in
(fun _ ->
+ let bvSprefixlen =
+ Arithmetic.increment (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ (Nat.S Nat.O)))))))))))))))) bvprefixlen
+ in
+ (let { Types.fst = inc_added; Types.snd = inc_pc_sigma } = acc in
+ (fun _ ->
(let { Types.fst = label; Types.snd = instr } = x in
(fun _ ->
let add_instr =
match instr with
| ASM.Instruction i ->
PolicyFront.jump_expansion_step_instruction (Types.pi1 labels)
- (Types.pi1 old_sigma) inc_pc_sigma (List.length prefix) i
+ (Types.pi1 old_sigma) inc_pc_sigma prefixlen i
| ASM.Comment x0 -> Types.None
| ASM.Cost x0 -> Types.None
| ASM.Jmp j ->
Types.Some
(PolicyFront.select_jump_length (Types.pi1 labels)
- (Types.pi1 old_sigma) inc_pc_sigma (List.length prefix) j)
+ (Types.pi1 old_sigma) inc_pc_sigma prefixlen j)
| ASM.Jnz (x0, x1, x2) -> Types.None
| ASM.Call c ->
Types.Some
(PolicyFront.select_call_length (Types.pi1 labels)
- (Types.pi1 old_sigma) inc_pc_sigma (List.length prefix) c)
+ (Types.pi1 old_sigma) inc_pc_sigma prefixlen c)
| ASM.Mov (x0, x1, x2) -> Types.None
in
let { Types.fst = inc_pc; Types.snd = inc_sigma } = inc_pc_sigma in
let old_length =
(BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S Nat.O))))))))))))))))
- (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S Nat.O)))))))))))))))) (List.length prefix))
+ (Nat.S Nat.O)))))))))))))))) bvprefixlen
(Types.pi1 old_sigma).Types.snd { Types.fst = Nat.O; Types.snd =
Assembly.Short_jump }).Types.snd
in
let old_Slength =
(BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S Nat.O))))))))))))))))
- (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S
- (List.length prefix))) (Types.pi1 old_sigma).Types.snd
- { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.snd
+ (Nat.S Nat.O)))))))))))))))) bvSprefixlen
+ (Types.pi1 old_sigma).Types.snd { Types.fst = Nat.O; Types.snd =
+ Assembly.Short_jump }).Types.snd
in
let updated_sigma =
BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S Nat.O))))))))))))))))
- (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S
- (List.length prefix))) { Types.fst = (Nat.plus inc_pc isize);
- Types.snd = old_Slength }
+ (Nat.S Nat.O)))))))))))))))) bvSprefixlen { Types.fst =
+ (Nat.plus inc_pc isize); Types.snd = old_Slength }
(BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S Nat.O))))))))))))))))
- (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))
- (List.length prefix)) { Types.fst = inc_pc; Types.snd =
- new_length } inc_sigma)
+ (Nat.S Nat.O)))))))))))))))) bvprefixlen { Types.fst = inc_pc;
+ Types.snd = new_length } inc_sigma)
in
+ { Types.fst = { Types.fst = (Nat.S prefixlen); Types.snd =
+ (Arithmetic.increment (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ (Nat.S Nat.O)))))))))))))))) bvprefixlen) }; Types.snd =
{ Types.fst = new_added; Types.snd = { Types.fst =
- (Nat.plus inc_pc isize); Types.snd = updated_sigma } })) __)) __)
- { Types.fst = Nat.O; Types.snd = { Types.fst = Nat.O; Types.snd =
+ (Nat.plus inc_pc isize); Types.snd = updated_sigma } } })) __)) __))
+ __)) __) { Types.fst = { Types.fst = Nat.O; Types.snd =
+ (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ Nat.O))))))))))))))))) }; Types.snd = { Types.fst = Nat.O;
+ Types.snd = { Types.fst = Nat.O; Types.snd =
(BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
(Nat.S Nat.O))))))))))))))))
(Types.pi1 old_sigma).Types.snd { Types.fst = Nat.O; Types.snd =
Assembly.Short_jump }).Types.snd } (BitVectorTrie.Stub (Nat.S
(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))) } })
+ (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))) } } })
in
(fun _ ->
+ (let { Types.fst = final_added; Types.snd = final_policy } = res in
+ (fun _ ->
(match Util.gtb final_policy.Types.fst
(Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
Types.None })
| Bool.False ->
(fun _ -> { Types.fst = (Nat.eqb final_added Nat.O); Types.snd =
- (Types.Some final_policy) })) __)) __
+ (Types.Some final_policy) })) __)) __)) __
open Preamble
-open Assembly
-
open Status
-open Fetch
-
open BitVectorTrie
open String
-open Exp
-
-open Arithmetic
-
-open Vector
-
-open FoldStuff
-
-open BitVector
-
-open Extranat
-
open Integers
open AST
open Errors
-open Extralib
+open Lists
+
+open Positive
+
+open Identifiers
+
+open CostLabel
+
+open ASM
+
+open Exp
open Setoids
open Option
+open Extranat
+
+open Vector
+
+open FoldStuff
+
+open BitVector
+
+open Arithmetic
+
+open Fetch
+
+open Assembly
+
open Div_and_mod
open Jmeq
open Util
-open List
-
-open Lists
-
open Bool
open Relations
open Nat
-open Positive
+open List
open Hints_declaration
open Types
-open Identifiers
-
-open CostLabel
-
-open ASM
+open Extralib
open PolicyFront
open ASMCosts
-open Assembly
-
open Status
open Fetch
+open Assembly
+
open PolicyFront
open PolicyStep
(** val preclassified_system_pass_rect_Type4 :
Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
preclassified_system_pass -> 'a1 **)
-let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_25220 =
- let pcs_pcs = x_25220 in h_mk_preclassified_system_pass pcs_pcs __
+let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_3 =
+ let pcs_pcs = x_3 in h_mk_preclassified_system_pass pcs_pcs __
(** val preclassified_system_pass_rect_Type5 :
Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
preclassified_system_pass -> 'a1 **)
-let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_25222 =
- let pcs_pcs = x_25222 in h_mk_preclassified_system_pass pcs_pcs __
+let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_5 =
+ let pcs_pcs = x_5 in h_mk_preclassified_system_pass pcs_pcs __
(** val preclassified_system_pass_rect_Type3 :
Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
preclassified_system_pass -> 'a1 **)
-let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_25224 =
- let pcs_pcs = x_25224 in h_mk_preclassified_system_pass pcs_pcs __
+let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_7 =
+ let pcs_pcs = x_7 in h_mk_preclassified_system_pass pcs_pcs __
(** val preclassified_system_pass_rect_Type2 :
Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
preclassified_system_pass -> 'a1 **)
-let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_25226 =
- let pcs_pcs = x_25226 in h_mk_preclassified_system_pass pcs_pcs __
+let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_9 =
+ let pcs_pcs = x_9 in h_mk_preclassified_system_pass pcs_pcs __
(** val preclassified_system_pass_rect_Type1 :
Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
preclassified_system_pass -> 'a1 **)
-let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_25228 =
- let pcs_pcs = x_25228 in h_mk_preclassified_system_pass pcs_pcs __
+let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_11 =
+ let pcs_pcs = x_11 in h_mk_preclassified_system_pass pcs_pcs __
(** val preclassified_system_pass_rect_Type0 :
Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
preclassified_system_pass -> 'a1 **)
-let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_25230 =
- let pcs_pcs = x_25230 in h_mk_preclassified_system_pass pcs_pcs __
+let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_13 =
+ let pcs_pcs = x_13 in h_mk_preclassified_system_pass pcs_pcs __
(** val pcs_pcs :
Compiler.pass -> preclassified_system_pass ->
Joint_fullexec.joint_preclassified_system LIN_semantics.lIN_semantics)
| Compiler.Assembly_pass ->
(fun prog ->
- let { Types.fst = eta32049; Types.snd = policy } = Obj.magic prog in
- let { Types.fst = code; Types.snd = sigma } = eta32049 in
+ let { Types.fst = eta4; Types.snd = policy } = Obj.magic prog in
+ let { Types.fst = code; Types.snd = sigma } = eta4 in
Interpret2.aSM_preclassified_system code sigma policy)
| Compiler.Object_code_pass ->
(fun prog -> Interpret2.oC_preclassified_system (Obj.magic prog))
open ASMCosts
-open Assembly
-
open Status
open Fetch
+open Assembly
+
open PolicyFront
open PolicyStep
(match TypeComparison.assert_type_eq (Csyntax.typeof lhs)
(Csyntax.typeof rhs) with
| Errors.OK _ ->
- (let eta2011 = simplify_expr lhs target_sz target_sg in
+ (let eta2033 = simplify_expr lhs target_sz target_sg in
(fun _ ->
(let { Types.fst = desired_type_lhs; Types.snd = lhs1 } =
- eta2011
+ eta2033
in
(fun _ ->
- (let eta2010 = simplify_expr rhs target_sz target_sg in
+ (let eta2032 = simplify_expr rhs target_sz target_sg in
(fun _ ->
(let { Types.fst = desired_type_rhs; Types.snd =
- rhs1 } = eta2010
+ rhs1 } = eta2032
in
(fun _ ->
(match Bool.andb desired_type_lhs desired_type_rhs with
(match necessary_conditions cast_sz cast_sg target_sz target_sg with
| Bool.True ->
(fun _ ->
- (let eta2013 = simplify_expr castee target_sz target_sg in
+ (let eta2035 = simplify_expr castee target_sz target_sg in
(fun _ ->
(let { Types.fst = desired_type; Types.snd = castee1 } =
- eta2013
+ eta2035
in
(fun _ ->
(match desired_type with
castee1 })
| Bool.False ->
(fun _ ->
- (let eta2012 = simplify_expr castee cast_sz cast_sg
+ (let eta2034 = simplify_expr castee cast_sz cast_sg
in
(fun _ ->
(let { Types.fst = desired_type2; Types.snd =
- castee2 } = eta2012
+ castee2 } = eta2034
in
(fun _ ->
(match desired_type2 with
__)) __)) __)
| Bool.False ->
(fun _ ->
- (let eta2014 = simplify_expr castee cast_sz cast_sg in
+ (let eta2036 = simplify_expr castee cast_sz cast_sg in
(fun _ ->
(let { Types.fst = desired_type2; Types.snd =
- castee2 } = eta2014
+ castee2 } = eta2036
in
(fun _ ->
(match desired_type2 with
(match TypeComparison.assert_type_eq (Csyntax.typeof iftrue)
(Csyntax.typeof iffalse) with
| Errors.OK _ ->
- (let eta2016 = simplify_expr iftrue target_sz target_sg in
+ (let eta2038 = simplify_expr iftrue target_sz target_sg in
(fun _ ->
(let { Types.fst = desired_true; Types.snd = iftrue1 } =
- eta2016
+ eta2038
in
(fun _ ->
- (let eta2015 = simplify_expr iffalse target_sz target_sg in
+ (let eta2037 = simplify_expr iffalse target_sz target_sg in
(fun _ ->
(let { Types.fst = desired_false; Types.snd = iffalse1 } =
- eta2015
+ eta2037
in
(fun _ ->
(match Bool.andb desired_true desired_false with
(fun _ ->
match TypeComparison.type_eq_dec ty (Csyntax.typeof e1) with
| Types.Inl _ ->
- (let eta2017 = simplify_expr e1 target_sz target_sg in
+ (let eta2039 = simplify_expr e1 target_sz target_sg in
(fun _ ->
- (let { Types.fst = desired_type; Types.snd = e2 } = eta2017 in
+ (let { Types.fst = desired_type; Types.snd = e2 } = eta2039 in
(fun _ -> { Types.fst = desired_type; Types.snd = (Csyntax.Expr
((Csyntax.Ecost (l, e2)), (Csyntax.typeof e2))) })) __)) __
| Types.Inr _ ->
| Csyntax.Tvoid -> (fun _ -> e)
| Csyntax.Tint (cast_sz, cast_sg) ->
(fun _ ->
- (let eta2018 = simplify_expr castee cast_sz cast_sg in
+ (let eta2040 = simplify_expr castee cast_sz cast_sg in
(fun _ ->
- (let { Types.fst = success; Types.snd = castee1 } = eta2018
+ (let { Types.fst = success; Types.snd = castee1 } = eta2040
in
(fun _ ->
(match success with
(BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
serialBufferType -> 'a1 **)
let rec serialBufferType_rect_Type4 h_Eight h_Nine = function
-| Eight x_21722 -> h_Eight x_21722
-| Nine (x_21724, x_21723) -> h_Nine x_21724 x_21723
+| Eight x_8 -> h_Eight x_8
+| Nine (x_10, x_9) -> h_Nine x_10 x_9
(** val serialBufferType_rect_Type5 :
(BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
serialBufferType -> 'a1 **)
let rec serialBufferType_rect_Type5 h_Eight h_Nine = function
-| Eight x_21728 -> h_Eight x_21728
-| Nine (x_21730, x_21729) -> h_Nine x_21730 x_21729
+| Eight x_14 -> h_Eight x_14
+| Nine (x_16, x_15) -> h_Nine x_16 x_15
(** val serialBufferType_rect_Type3 :
(BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
serialBufferType -> 'a1 **)
let rec serialBufferType_rect_Type3 h_Eight h_Nine = function
-| Eight x_21734 -> h_Eight x_21734
-| Nine (x_21736, x_21735) -> h_Nine x_21736 x_21735
+| Eight x_20 -> h_Eight x_20
+| Nine (x_22, x_21) -> h_Nine x_22 x_21
(** val serialBufferType_rect_Type2 :
(BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
serialBufferType -> 'a1 **)
let rec serialBufferType_rect_Type2 h_Eight h_Nine = function
-| Eight x_21740 -> h_Eight x_21740
-| Nine (x_21742, x_21741) -> h_Nine x_21742 x_21741
+| Eight x_26 -> h_Eight x_26
+| Nine (x_28, x_27) -> h_Nine x_28 x_27
(** val serialBufferType_rect_Type1 :
(BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
serialBufferType -> 'a1 **)
let rec serialBufferType_rect_Type1 h_Eight h_Nine = function
-| Eight x_21746 -> h_Eight x_21746
-| Nine (x_21748, x_21747) -> h_Nine x_21748 x_21747
+| Eight x_32 -> h_Eight x_32
+| Nine (x_34, x_33) -> h_Nine x_34 x_33
(** val serialBufferType_rect_Type0 :
(BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
serialBufferType -> 'a1 **)
let rec serialBufferType_rect_Type0 h_Eight h_Nine = function
-| Eight x_21752 -> h_Eight x_21752
-| Nine (x_21754, x_21753) -> h_Nine x_21754 x_21753
+| Eight x_38 -> h_Eight x_38
+| Nine (x_40, x_39) -> h_Nine x_40 x_39
(** val serialBufferType_inv_rect_Type4 :
serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
(BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
-> 'a1) -> lineType -> 'a1 **)
let rec lineType_rect_Type4 h_P1 h_P3 h_SerialBuffer = function
-| P1 x_21801 -> h_P1 x_21801
-| P3 x_21802 -> h_P3 x_21802
-| SerialBuffer x_21803 -> h_SerialBuffer x_21803
+| P1 x_87 -> h_P1 x_87
+| P3 x_88 -> h_P3 x_88
+| SerialBuffer x_89 -> h_SerialBuffer x_89
(** val lineType_rect_Type5 :
(BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
-> 'a1) -> lineType -> 'a1 **)
let rec lineType_rect_Type5 h_P1 h_P3 h_SerialBuffer = function
-| P1 x_21808 -> h_P1 x_21808
-| P3 x_21809 -> h_P3 x_21809
-| SerialBuffer x_21810 -> h_SerialBuffer x_21810
+| P1 x_94 -> h_P1 x_94
+| P3 x_95 -> h_P3 x_95
+| SerialBuffer x_96 -> h_SerialBuffer x_96
(** val lineType_rect_Type3 :
(BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
-> 'a1) -> lineType -> 'a1 **)
let rec lineType_rect_Type3 h_P1 h_P3 h_SerialBuffer = function
-| P1 x_21815 -> h_P1 x_21815
-| P3 x_21816 -> h_P3 x_21816
-| SerialBuffer x_21817 -> h_SerialBuffer x_21817
+| P1 x_101 -> h_P1 x_101
+| P3 x_102 -> h_P3 x_102
+| SerialBuffer x_103 -> h_SerialBuffer x_103
(** val lineType_rect_Type2 :
(BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
-> 'a1) -> lineType -> 'a1 **)
let rec lineType_rect_Type2 h_P1 h_P3 h_SerialBuffer = function
-| P1 x_21822 -> h_P1 x_21822
-| P3 x_21823 -> h_P3 x_21823
-| SerialBuffer x_21824 -> h_SerialBuffer x_21824
+| P1 x_108 -> h_P1 x_108
+| P3 x_109 -> h_P3 x_109
+| SerialBuffer x_110 -> h_SerialBuffer x_110
(** val lineType_rect_Type1 :
(BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
-> 'a1) -> lineType -> 'a1 **)
let rec lineType_rect_Type1 h_P1 h_P3 h_SerialBuffer = function
-| P1 x_21829 -> h_P1 x_21829
-| P3 x_21830 -> h_P3 x_21830
-| SerialBuffer x_21831 -> h_SerialBuffer x_21831
+| P1 x_115 -> h_P1 x_115
+| P3 x_116 -> h_P3 x_116
+| SerialBuffer x_117 -> h_SerialBuffer x_117
(** val lineType_rect_Type0 :
(BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
-> 'a1) -> lineType -> 'a1 **)
let rec lineType_rect_Type0 h_P1 h_P3 h_SerialBuffer = function
-| P1 x_21836 -> h_P1 x_21836
-| P3 x_21837 -> h_P3 x_21837
-| SerialBuffer x_21838 -> h_SerialBuffer x_21838
+| P1 x_122 -> h_P1 x_122
+| P3 x_123 -> h_P3 x_123
+| SerialBuffer x_124 -> h_SerialBuffer x_124
(** val lineType_inv_rect_Type4 :
lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
-> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
preStatus -> 'a2 **)
-let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_22224 =
+let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_510 =
let { low_internal_ram = low_internal_ram0; high_internal_ram =
high_internal_ram0; external_ram = external_ram0; program_counter =
program_counter0; special_function_registers_8051 =
special_function_registers_8053; special_function_registers_8052 =
special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
- p3_latch0; clock = clock0 } = x_22224
+ p3_latch0; clock = clock0 } = x_510
in
h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
program_counter0 special_function_registers_8053
-> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
preStatus -> 'a2 **)
-let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_22226 =
+let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_512 =
let { low_internal_ram = low_internal_ram0; high_internal_ram =
high_internal_ram0; external_ram = external_ram0; program_counter =
program_counter0; special_function_registers_8051 =
special_function_registers_8053; special_function_registers_8052 =
special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
- p3_latch0; clock = clock0 } = x_22226
+ p3_latch0; clock = clock0 } = x_512
in
h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
program_counter0 special_function_registers_8053
-> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
preStatus -> 'a2 **)
-let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_22228 =
+let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_514 =
let { low_internal_ram = low_internal_ram0; high_internal_ram =
high_internal_ram0; external_ram = external_ram0; program_counter =
program_counter0; special_function_registers_8051 =
special_function_registers_8053; special_function_registers_8052 =
special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
- p3_latch0; clock = clock0 } = x_22228
+ p3_latch0; clock = clock0 } = x_514
in
h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
program_counter0 special_function_registers_8053
-> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
preStatus -> 'a2 **)
-let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_22230 =
+let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_516 =
let { low_internal_ram = low_internal_ram0; high_internal_ram =
high_internal_ram0; external_ram = external_ram0; program_counter =
program_counter0; special_function_registers_8051 =
special_function_registers_8053; special_function_registers_8052 =
special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
- p3_latch0; clock = clock0 } = x_22230
+ p3_latch0; clock = clock0 } = x_516
in
h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
program_counter0 special_function_registers_8053
-> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
preStatus -> 'a2 **)
-let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_22232 =
+let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_518 =
let { low_internal_ram = low_internal_ram0; high_internal_ram =
high_internal_ram0; external_ram = external_ram0; program_counter =
program_counter0; special_function_registers_8051 =
special_function_registers_8053; special_function_registers_8052 =
special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
- p3_latch0; clock = clock0 } = x_22232
+ p3_latch0; clock = clock0 } = x_518
in
h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
program_counter0 special_function_registers_8053
-> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
preStatus -> 'a2 **)
-let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_22234 =
+let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_520 =
let { low_internal_ram = low_internal_ram0; high_internal_ram =
high_internal_ram0; external_ram = external_ram0; program_counter =
program_counter0; special_function_registers_8051 =
special_function_registers_8053; special_function_registers_8052 =
special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
- p3_latch0; clock = clock0 } = x_22234
+ p3_latch0; clock = clock0 } = x_520
in
h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
program_counter0 special_function_registers_8053
{ Types.fst = { Types.fst = (Csyntax.Slabel (lab, st')); Types.snd =
lab }; Types.snd = u1 }
| Csyntax.LScase (sz, tag, st, other_cases) ->
- let { Types.fst = eta2108; Types.snd = u1 } =
+ let { Types.fst = eta2130; Types.snd = u1 } =
produce_cond e other_cases u exit
in
- let { Types.fst = sub_statements; Types.snd = sub_label } = eta2108 in
+ let { Types.fst = sub_statements; Types.snd = sub_label } = eta2130 in
let st' = convert_break_to_goto st exit in
let { Types.fst = lab; Types.snd = u2 } =
Identifiers.fresh PreIdentifiers.SymbolTag u1
let { Types.fst = exit_label; Types.snd = uv1 } =
Identifiers.fresh PreIdentifiers.SymbolTag uv
in
- let { Types.fst = eta2109; Types.snd = uv2 } =
+ let { Types.fst = eta2131; Types.snd = uv2 } =
produce_cond e switch_cases uv1 exit_label
in
- let { Types.fst = result; Types.snd = useless_label } = eta2109 in
+ let { Types.fst = result; Types.snd = useless_label } = eta2131 in
{ Types.fst = (Csyntax.Ssequence (result, (Csyntax.Slabel (exit_label,
Csyntax.Sskip)))); Types.snd = uv2 }
| Csyntax.Scall (x, x0, x1) ->
{ Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
| Csyntax.Ssequence (s1, s2) ->
- let { Types.fst = eta2123; Types.snd = u' } = switch_removal s1 u in
- let { Types.fst = s1'; Types.snd = acc1 } = eta2123 in
- let { Types.fst = eta2122; Types.snd = u'' } = switch_removal s2 u' in
- let { Types.fst = s2'; Types.snd = acc2 } = eta2122 in
+ let { Types.fst = eta2145; Types.snd = u' } = switch_removal s1 u in
+ let { Types.fst = s1'; Types.snd = acc1 } = eta2145 in
+ let { Types.fst = eta2144; Types.snd = u'' } = switch_removal s2 u' in
+ let { Types.fst = s2'; Types.snd = acc2 } = eta2144 in
{ Types.fst = { Types.fst = (Csyntax.Ssequence (s1', s2')); Types.snd =
(List.append acc1 acc2) }; Types.snd = u'' }
| Csyntax.Sifthenelse (e, s1, s2) ->
- let { Types.fst = eta2125; Types.snd = u' } = switch_removal s1 u in
- let { Types.fst = s1'; Types.snd = acc1 } = eta2125 in
- let { Types.fst = eta2124; Types.snd = u'' } = switch_removal s2 u' in
- let { Types.fst = s2'; Types.snd = acc2 } = eta2124 in
+ let { Types.fst = eta2147; Types.snd = u' } = switch_removal s1 u in
+ let { Types.fst = s1'; Types.snd = acc1 } = eta2147 in
+ let { Types.fst = eta2146; Types.snd = u'' } = switch_removal s2 u' in
+ let { Types.fst = s2'; Types.snd = acc2 } = eta2146 in
{ Types.fst = { Types.fst = (Csyntax.Sifthenelse (e, s1', s2'));
Types.snd = (List.append acc1 acc2) }; Types.snd = u'' }
| Csyntax.Swhile (e, body) ->
- let { Types.fst = eta2126; Types.snd = u' } = switch_removal body u in
- let { Types.fst = body'; Types.snd = acc } = eta2126 in
+ let { Types.fst = eta2148; Types.snd = u' } = switch_removal body u in
+ let { Types.fst = body'; Types.snd = acc } = eta2148 in
{ Types.fst = { Types.fst = (Csyntax.Swhile (e, body')); Types.snd =
acc }; Types.snd = u' }
| Csyntax.Sdowhile (e, body) ->
- let { Types.fst = eta2127; Types.snd = u' } = switch_removal body u in
- let { Types.fst = body'; Types.snd = acc } = eta2127 in
+ let { Types.fst = eta2149; Types.snd = u' } = switch_removal body u in
+ let { Types.fst = body'; Types.snd = acc } = eta2149 in
{ Types.fst = { Types.fst = (Csyntax.Sdowhile (e, body')); Types.snd =
acc }; Types.snd = u' }
| Csyntax.Sfor (s1, e, s2, s3) ->
- let { Types.fst = eta2130; Types.snd = u' } = switch_removal s1 u in
- let { Types.fst = s1'; Types.snd = acc1 } = eta2130 in
- let { Types.fst = eta2129; Types.snd = u'' } = switch_removal s2 u' in
- let { Types.fst = s2'; Types.snd = acc2 } = eta2129 in
- let { Types.fst = eta2128; Types.snd = u''' } = switch_removal s3 u'' in
- let { Types.fst = s3'; Types.snd = acc3 } = eta2128 in
+ let { Types.fst = eta2152; Types.snd = u' } = switch_removal s1 u in
+ let { Types.fst = s1'; Types.snd = acc1 } = eta2152 in
+ let { Types.fst = eta2151; Types.snd = u'' } = switch_removal s2 u' in
+ let { Types.fst = s2'; Types.snd = acc2 } = eta2151 in
+ let { Types.fst = eta2150; Types.snd = u''' } = switch_removal s3 u'' in
+ let { Types.fst = s3'; Types.snd = acc3 } = eta2150 in
{ Types.fst = { Types.fst = (Csyntax.Sfor (s1', e, s2', s3'));
Types.snd = (List.append acc1 (List.append acc2 acc3)) }; Types.snd =
u''' }
| Csyntax.Sreturn x ->
{ Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
| Csyntax.Sswitch (e, branches) ->
- let { Types.fst = eta2131; Types.snd = u' } =
+ let { Types.fst = eta2153; Types.snd = u' } =
switch_removal_branches branches u
in
- let { Types.fst = sf_branches; Types.snd = acc } = eta2131 in
+ let { Types.fst = sf_branches; Types.snd = acc } = eta2153 in
let { Types.fst = switch_tmp; Types.snd = u'' } =
Identifiers.fresh PreIdentifiers.SymbolTag u'
in
Types.snd = (List.Cons ({ Types.fst = switch_tmp; Types.snd =
(Csyntax.typeof e) }, acc)) }; Types.snd = u''' }
| Csyntax.Slabel (label, body) ->
- let { Types.fst = eta2132; Types.snd = u' } = switch_removal body u in
- let { Types.fst = body'; Types.snd = acc } = eta2132 in
+ let { Types.fst = eta2154; Types.snd = u' } = switch_removal body u in
+ let { Types.fst = body'; Types.snd = acc } = eta2154 in
{ Types.fst = { Types.fst = (Csyntax.Slabel (label, body')); Types.snd =
acc }; Types.snd = u' }
| Csyntax.Sgoto x ->
{ Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
| Csyntax.Scost (cost, body) ->
- let { Types.fst = eta2133; Types.snd = u' } = switch_removal body u in
- let { Types.fst = body'; Types.snd = acc } = eta2133 in
+ let { Types.fst = eta2155; Types.snd = u' } = switch_removal body u in
+ let { Types.fst = body'; Types.snd = acc } = eta2155 in
{ Types.fst = { Types.fst = (Csyntax.Scost (cost, body')); Types.snd =
acc }; Types.snd = u' }
(** val switch_removal_branches :
and switch_removal_branches l u =
match l with
| Csyntax.LSdefault st ->
- let { Types.fst = eta2134; Types.snd = u' } = switch_removal st u in
- let { Types.fst = st'; Types.snd = acc1 } = eta2134 in
+ let { Types.fst = eta2156; Types.snd = u' } = switch_removal st u in
+ let { Types.fst = st'; Types.snd = acc1 } = eta2156 in
{ Types.fst = { Types.fst = (Csyntax.LSdefault st'); Types.snd = acc1 };
Types.snd = u' }
| Csyntax.LScase (sz, int, st, tl) ->
- let { Types.fst = eta2136; Types.snd = u' } =
+ let { Types.fst = eta2158; Types.snd = u' } =
switch_removal_branches tl u
in
- let { Types.fst = tl_result; Types.snd = acc1 } = eta2136 in
- let { Types.fst = eta2135; Types.snd = u'' } = switch_removal st u' in
- let { Types.fst = st'; Types.snd = acc2 } = eta2135 in
+ let { Types.fst = tl_result; Types.snd = acc1 } = eta2158 in
+ let { Types.fst = eta2157; Types.snd = u'' } = switch_removal st u' in
+ let { Types.fst = st'; Types.snd = acc2 } = eta2157 in
{ Types.fst = { Types.fst = (Csyntax.LScase (sz, int, st', tl_result));
Types.snd = (List.append acc1 acc2) }; Types.snd = u'' }
(('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
Identifiers.universe) Types.prod -> 'a1 **)
let ret_st x =
- let { Types.fst = eta2137; Types.snd = u } = x in eta2137.Types.fst
+ let { Types.fst = eta2159; Types.snd = u } = x in eta2159.Types.fst
(** val ret_vars :
(('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
Identifiers.universe) Types.prod -> (AST.ident, Csyntax.type0) Types.prod
List.list **)
let ret_vars x =
- let { Types.fst = eta2138; Types.snd = u } = x in eta2138.Types.snd
+ let { Types.fst = eta2160; Types.snd = u } = x in eta2160.Types.snd
(** val ret_u :
(('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
Identifiers.universe) Types.prod -> Identifiers.universe **)
let ret_u x =
- let { Types.fst = eta2139; Types.snd = u } = x in
- let { Types.fst = s; Types.snd = vars } = eta2139 in u
+ let { Types.fst = eta2161; Types.snd = u } = x in
+ let { Types.fst = s; Types.snd = vars } = eta2161 in u
(** val least_identifier : PreIdentifiers.identifier **)
let least_identifier =
Types.prod List.list) Types.prod **)
let function_switch_removal f =
let u = Fresh.universe_of_max (max_id_of_function f) in
- let { Types.fst = eta2140; Types.snd = u' } =
+ let { Types.fst = eta2162; Types.snd = u' } =
switch_removal f.Csyntax.fn_body u
in
- let { Types.fst = st; Types.snd = vars } = eta2140 in
+ let { Types.fst = st; Types.snd = vars } = eta2162 in
let result = { Csyntax.fn_return = f.Csyntax.fn_return; Csyntax.fn_params =
f.Csyntax.fn_params; Csyntax.fn_vars =
(List.append vars f.Csyntax.fn_vars); Csyntax.fn_body = st }
let { Types.fst = id; Types.snd = ty } = it in
Obj.magic
(Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su)
- (fun eta2356 ->
- let result = eta2356 in
+ (fun eta2378 ->
+ let result = eta2378 in
(let { Types.fst = fgens1; Types.snd = s0 } = result in
(fun _ ->
Obj.magic
let populate_env en gen =
List.foldr (fun idt rsengen ->
let { Types.fst = id; Types.snd = ty } = idt in
- let { Types.fst = eta2859; Types.snd = gen0 } = rsengen in
- let { Types.fst = rs; Types.snd = en0 } = eta2859 in
+ let { Types.fst = eta2881; Types.snd = gen0 } = rsengen in
+ let { Types.fst = rs; Types.snd = en0 } = eta2881 in
let { Types.fst = r; Types.snd = gen' } =
Identifiers.fresh PreIdentifiers.RegisterTag gen0
in
let labgen0 = Identifiers.new_universe PreIdentifiers.LabelTag in
let reggen0 = Identifiers.new_universe PreIdentifiers.RegisterTag in
let cminor_labels = Cminor_syntax.labels_of f.Cminor_syntax.f_body in
- (let { Types.fst = eta3086; Types.snd = reggen1 } =
+ (let { Types.fst = eta3108; Types.snd = reggen1 } =
populate_env (Identifiers.empty_map PreIdentifiers.SymbolTag) reggen0
f.Cminor_syntax.f_params
in
- let { Types.fst = params; Types.snd = env1 } = eta3086 in
+ let { Types.fst = params; Types.snd = env1 } = eta3108 in
(fun _ ->
- (let { Types.fst = eta3085; Types.snd = reggen2 } =
+ (let { Types.fst = eta3107; Types.snd = reggen2 } =
populate_env env1 reggen1 f.Cminor_syntax.f_vars
in
- let { Types.fst = locals0; Types.snd = env0 } = eta3085 in
+ let { Types.fst = locals0; Types.snd = env0 } = eta3107 in
(fun _ ->
(let { Types.dpi1 = locals_reggen; Types.dpi2 = result } =
match f.Cminor_syntax.f_return with
projects / pkg-cerco / acc-trusted.git / commitdiff