Imported Upstream version 0.2

diff --git a/.build.swp b/.build.swp
new file mode 100644 (file)
index 0000000..2f910a1
Binary files /dev/null and b/.build.swp differ

diff --git a/extracted/aSM.ml b/extracted/aSM.ml
index e7665c57dc8840db85455a16b775f2ad5a4832c3..79ec03a881628a1ca8ce77405af5ebc0f08b1455 100644 (file)
--- a/extracted/aSM.ml
+++ b/extracted/aSM.ml
@@ -112,25 +112,25 @@ type addressing_mode =
     (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
     (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
 | 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
 | 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 ->
 
 (** val addressing_mode_rect_Type5 :
     (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit ->


@@ -140,25 +140,25 @@ let rec addressing_mode_rect_Type4 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER
     (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
     (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
 | 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
 | 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 ->
 
 (** val addressing_mode_rect_Type3 :
     (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit ->


@@ -168,25 +168,25 @@ let rec addressing_mode_rect_Type5 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER
     (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
     (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
 | 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
 | 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 ->
 
 (** val addressing_mode_rect_Type2 :
     (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit ->


@@ -196,25 +196,25 @@ let rec addressing_mode_rect_Type3 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER
     (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
     (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
 | 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
 | 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 ->
 
 (** val addressing_mode_rect_Type1 :
     (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit ->


@@ -224,25 +224,25 @@ let rec addressing_mode_rect_Type2 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER
     (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
     (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
 | 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
 | 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 ->
 
 (** val addressing_mode_rect_Type0 :
     (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit ->


@@ -252,25 +252,25 @@ let rec addressing_mode_rect_Type1 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER
     (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
     (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
 | 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
 | 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 addressing_mode_inv_rect_Type4 :
     addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __


@@ -1925,43 +1925,43 @@ type subaddressing_mode =
 (** val subaddressing_mode_rect_Type4 :
     Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
     'a1) -> subaddressing_mode -> 'a1 **)
 (** 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 **)
   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 **)
   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 **)
   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 **)
   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 **)
   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 :
   h_mk_subaddressing_mode subaddressing_modeel __
 
 (** val subaddressing_modeel :


@@ -2287,44 +2287,44 @@ type 'a preinstruction =
     -> '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
     -> '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
 | 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
 
 (** val preinstruction_rect_Type5 :
     (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode


@@ -2362,44 +2362,44 @@ let rec preinstruction_rect_Type4 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_
     -> '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
     -> '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
 | 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
 
 (** val preinstruction_rect_Type3 :
     (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode


@@ -2437,44 +2437,44 @@ let rec preinstruction_rect_Type5 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_
     -> '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
     -> '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
 | 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
 
 (** val preinstruction_rect_Type2 :
     (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode


@@ -2512,44 +2512,44 @@ let rec preinstruction_rect_Type3 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_
     -> '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
     -> '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
 | 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
 
 (** val preinstruction_rect_Type1 :
     (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode


@@ -2587,44 +2587,44 @@ let rec preinstruction_rect_Type2 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_
     -> '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
     -> '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
 | 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
 
 (** val preinstruction_rect_Type0 :
     (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode


@@ -2662,44 +2662,44 @@ let rec preinstruction_rect_Type1 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_
     -> '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
     -> '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
 | 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 -> __ ->
 
 (** val preinstruction_inv_rect_Type4 :
     'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->


@@ -5103,13 +5103,13 @@ type instruction =
     -> '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
     -> '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) ->
 
 (** val instruction_rect_Type5 :
     (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->


@@ -5118,13 +5118,13 @@ let rec instruction_rect_Type4 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_Rea
     -> '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
     -> '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) ->
 
 (** val instruction_rect_Type3 :
     (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->


@@ -5133,13 +5133,13 @@ let rec instruction_rect_Type5 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_Rea
     -> '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
     -> '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) ->
 
 (** val instruction_rect_Type2 :
     (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->


@@ -5148,13 +5148,13 @@ let rec instruction_rect_Type3 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_Rea
     -> '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
     -> '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) ->
 
 (** val instruction_rect_Type1 :
     (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->


@@ -5163,13 +5163,13 @@ let rec instruction_rect_Type2 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_Rea
     -> '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
     -> '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) ->
 
 (** val instruction_rect_Type0 :
     (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->


@@ -5178,13 +5178,13 @@ let rec instruction_rect_Type1 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_Rea
     -> '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
     -> '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
 
 (** val instruction_inv_rect_Type4 :
     instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode


@@ -5475,13 +5475,13 @@ type pseudo_instruction =
     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
     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) ->
 
 (** val pseudo_instruction_rect_Type5 :
     (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->


@@ -5491,13 +5491,13 @@ let rec pseudo_instruction_rect_Type4 h_Instruction h_Comment h_Cost h_Jmp h_Jnz
     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
     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) ->
 
 (** val pseudo_instruction_rect_Type3 :
     (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->


@@ -5507,13 +5507,13 @@ let rec pseudo_instruction_rect_Type5 h_Instruction h_Comment h_Cost h_Jmp h_Jnz
     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
     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) ->
 
 (** val pseudo_instruction_rect_Type2 :
     (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->


@@ -5523,13 +5523,13 @@ let rec pseudo_instruction_rect_Type3 h_Instruction h_Comment h_Cost h_Jmp h_Jnz
     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
     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) ->
 
 (** val pseudo_instruction_rect_Type1 :
     (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->


@@ -5539,13 +5539,13 @@ let rec pseudo_instruction_rect_Type2 h_Instruction h_Comment h_Cost h_Jmp h_Jnz
     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
     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) ->
 
 (** val pseudo_instruction_rect_Type0 :
     (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->


@@ -5555,13 +5555,13 @@ let rec pseudo_instruction_rect_Type1 h_Instruction h_Comment h_Cost h_Jmp h_Jnz
     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
     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) ->
 
 (** val pseudo_instruction_inv_rect_Type4 :
     pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->


@@ -5777,9 +5777,9 @@ type pseudo_assembly_program = { preamble : (identifier, BitVector.word)
     labelled_instruction List.list -> __ -> (identifier, AST.ident)
     Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
     pseudo_assembly_program -> '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 =
   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 __ __
   in
   h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     final_label0 __ __


@@ -5789,9 +5789,9 @@ let rec pseudo_assembly_program_rect_Type4 h_mk_pseudo_assembly_program x_21431
     labelled_instruction List.list -> __ -> (identifier, AST.ident)
     Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
     pseudo_assembly_program -> 'a1 **)
     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 =
   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 __ __
   in
   h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     final_label0 __ __


@@ -5801,9 +5801,9 @@ let rec pseudo_assembly_program_rect_Type5 h_mk_pseudo_assembly_program x_21433
     labelled_instruction List.list -> __ -> (identifier, AST.ident)
     Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
     pseudo_assembly_program -> 'a1 **)
     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 =
   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 __ __
   in
   h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     final_label0 __ __


@@ -5813,9 +5813,9 @@ let rec pseudo_assembly_program_rect_Type3 h_mk_pseudo_assembly_program x_21435
     labelled_instruction List.list -> __ -> (identifier, AST.ident)
     Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
     pseudo_assembly_program -> 'a1 **)
     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 =
   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 __ __
   in
   h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     final_label0 __ __


@@ -5825,9 +5825,9 @@ let rec pseudo_assembly_program_rect_Type2 h_mk_pseudo_assembly_program x_21437
     labelled_instruction List.list -> __ -> (identifier, AST.ident)
     Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
     pseudo_assembly_program -> 'a1 **)
     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 =
   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 __ __
   in
   h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     final_label0 __ __


@@ -5837,9 +5837,9 @@ let rec pseudo_assembly_program_rect_Type1 h_mk_pseudo_assembly_program x_21439
     labelled_instruction List.list -> __ -> (identifier, AST.ident)
     Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
     pseudo_assembly_program -> 'a1 **)
     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 =
   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 __ __
   in
   h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     final_label0 __ __


@@ -5936,17 +5936,22 @@ let next pmem pc =
 let load_code_memory0 program =
   (Types.pi1
     (FoldStuff.foldl_strong program (fun prefix v tl _ i_mem ->
 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
       (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.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 **)
 
 (** val load_code_memory :
     object_code -> BitVector.byte BitVectorTrie.bitVectorTrie **)


@@ -5967,9 +5972,9 @@ type labelled_object_code = { oc : object_code;
     (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
     costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
     labelled_object_code -> 'a1 **)
     (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 =
   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 __
 
   in
   h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __
 


@@ -5977,9 +5982,9 @@ let rec labelled_object_code_rect_Type4 h_mk_labelled_object_code x_21457 =
     (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
     costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
     labelled_object_code -> 'a1 **)
     (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 =
   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 __
 
   in
   h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __
 


@@ -5987,9 +5992,9 @@ let rec labelled_object_code_rect_Type5 h_mk_labelled_object_code x_21459 =
     (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
     costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
     labelled_object_code -> 'a1 **)
     (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 =
   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 __
 
   in
   h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __
 


@@ -5997,9 +6002,9 @@ let rec labelled_object_code_rect_Type3 h_mk_labelled_object_code x_21461 =
     (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
     costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
     labelled_object_code -> 'a1 **)
     (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 =
   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 __
 
   in
   h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __
 


@@ -6007,9 +6012,9 @@ let rec labelled_object_code_rect_Type2 h_mk_labelled_object_code x_21463 =
     (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
     costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
     labelled_object_code -> 'a1 **)
     (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 =
   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 __
 
   in
   h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __
 


@@ -6017,9 +6022,9 @@ let rec labelled_object_code_rect_Type1 h_mk_labelled_object_code x_21465 =
     (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
     costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
     labelled_object_code -> 'a1 **)
     (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 =
   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 __
 
   in
   h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __
 

diff --git a/extracted/aSMCosts.ml b/extracted/aSMCosts.ml
index 41ba9f9e4b5b842679676f5f004bd5f7b0dc6e7e..52d1276e8af6fb7d7349d13bac5ce29323945e3d 100644 (file)
--- a/extracted/aSMCosts.ml
+++ b/extracted/aSMCosts.ml
@@ -501,11 +501,11 @@ let rec block_cost' prog program_counter' program_size first_time_around =
    | Nat.O -> (fun _ -> Nat.O)
    | Nat.S program_size' ->
      (fun _ ->
    | 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'' } =
           Fetch.fetch prog.ASM.cm program_counter'
         in
        let { Types.fst = instruction; Types.snd = program_counter'' } =

-         eta31588
+         eta302

        in
        (fun _ ->
        let to_continue =
        in
        (fun _ ->
        let to_continue =

diff --git a/extracted/abstractStatus.ml b/extracted/abstractStatus.ml
index 61faf8d75c99295b93ba4ed379a96bf4b382d402..bc6bf1c0970960c06cf9556e38c063c922bd4764 100644 (file)
--- a/extracted/abstractStatus.ml
+++ b/extracted/abstractStatus.ml
@@ -160,22 +160,15 @@ let aSM_classify0 = function
 | ASM.MOVC (x, x0) -> StructuredTraces.Cl_other
 | ASM.RealInstruction pre -> aSM_classify00 pre
 
 | 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 =
 (** 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 :
 
 (** 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
 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

diff --git a/extracted/abstractStatus.mli b/extracted/abstractStatus.mli
index fe82c6af2d78a4d471d8d1c71e7c3a85698c5a01..118b5cb0accae30623be64f5a53286268d17e66f 100644 (file)
--- a/extracted/abstractStatus.mli
+++ b/extracted/abstractStatus.mli
@@ -112,18 +112,13 @@ val aSM_classify00 : 'a1 ASM.preinstruction -> StructuredTraces.status_class
 
 val aSM_classify0 : ASM.instruction -> StructuredTraces.status_class
 
 
 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 :
 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
 
 
 val word_deqset : Deqsets.deqSet
 

diff --git a/extracted/compiler.ml b/extracted/compiler.ml
index f2c456d3a4698b65525caa06b0a9f36d38a77cc2..eaae3c4b4315c406131ef82b46d77598ed0bfd7b 100644 (file)
--- a/extracted/compiler.ml
+++ b/extracted/compiler.ml
@@ -530,19 +530,24 @@ open Policy
     observe_pass -> ASM.pseudo_assembly_program -> ASM.labelled_object_code
     Errors.res **)
 let assembler observe p =
     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 ->
   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
       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
       let p0 = Assembly.assembly p sigma pol in

+prerr_endline "Y4";

       let i0 = Obj.magic observe Object_code_pass (Types.pi1 p0) in
       let i0 = Obj.magic observe Object_code_pass (Types.pi1 p0) in

+prerr_endline "Y5";

       Obj.magic (Errors.OK (Types.pi1 p0))))
 
 open StructuredTraces
       Obj.magic (Errors.OK (Types.pi1 p0))))
 
 open StructuredTraces

diff --git a/extracted/compiler.mli b/extracted/compiler.mli
index 26bd5740b353f110fd64192a468ba7c7fb252dbf..a2d8be900236789dbbe6ff615a245ac0ae45f045 100644 (file)
--- a/extracted/compiler.mli
+++ b/extracted/compiler.mli
@@ -322,12 +322,12 @@ val back_end :
   (((ASM.pseudo_assembly_program, CostLabel.costlabel) Types.prod,
   Joint.stack_cost_model) Types.prod, Nat.nat) Types.prod Errors.res
 
   (((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 Status
 
 open Fetch
 

+open Assembly
+

 open PolicyFront
 
 open PolicyStep
 open PolicyFront
 
 open PolicyStep

diff --git a/extracted/fetch.ml b/extracted/fetch.ml
index 4ad7b4f6387719f40bf33896e8d6dbb96a6bb894..0932432faba353fe8bf9751015c32cca36d2eaa6 100644 (file)
--- a/extracted/fetch.ml
+++ b/extracted/fetch.ml
@@ -1,5 +1,19 @@
 open Preamble
 
 open Preamble
 

+open Types
+
+open Hints_declaration
+
+open Core_notation
+
+open Pts
+
+open Logic
+
+open Jmeq
+
+open Russell
+

 open Exp
 
 open Setoids
 open Exp
 
 open Setoids


@@ -14,12 +28,6 @@ open Vector
 
 open Div_and_mod
 
 
 open Div_and_mod
 

-open Jmeq
-
-open Russell
-
-open Types
-

 open List
 
 open Util
 open List
 
 open Util


@@ -28,14 +36,6 @@ open FoldStuff
 
 open Bool
 
 
 open Bool
 

-open Hints_declaration
-
-open Core_notation
-
-open Pts
-
-open Logic
-

 open Relations
 
 open Nat
 open Relations
 
 open Nat


@@ -78,30 +78,26 @@ open CostLabel
 
 open ASM
 
 
 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 :
 
 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 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 _ ->
          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 _ ->
       (fun _ ->
       (let { Types.fst = label; Types.snd = instr } = x in
       (fun _ ->


@@ -134,29 +130,21 @@ let create_label_cost_map0 program =
       Nat.O))))))))))))))))) }; Types.snd = Nat.O })).Types.fst
 
 (** val create_label_cost_map :
       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 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
   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 **)
 
 (** val prod_inv_rect_Type0 :
     ('a1, 'a2) Types.prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)

diff --git a/extracted/fetch.mli b/extracted/fetch.mli
index bad649da146ff50f8d38c6cb60b031386004362b..283dc7f8501ed5ecb6f43fd0af6a154bea0d169a 100644 (file)
--- a/extracted/fetch.mli
+++ b/extracted/fetch.mli
@@ -1,5 +1,19 @@
 open Preamble
 
 open Preamble
 

+open Types
+
+open Hints_declaration
+
+open Core_notation
+
+open Pts
+
+open Logic
+
+open Jmeq
+
+open Russell
+

 open Exp
 
 open Setoids
 open Exp
 
 open Setoids


@@ -14,12 +28,6 @@ open Vector
 
 open Div_and_mod
 
 
 open Div_and_mod
 

-open Jmeq
-
-open Russell
-
-open Types
-

 open List
 
 open Util
 open List
 
 open Util


@@ -28,14 +36,6 @@ open FoldStuff
 
 open Bool
 
 
 open Bool
 

-open Hints_declaration
-
-open Core_notation
-
-open Pts
-
-open Logic
-

 open Relations
 
 open Nat
 open Relations
 
 open Nat


@@ -78,26 +78,22 @@ open CostLabel
 
 open ASM
 
 
 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 :
 
 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 :
 
 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 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
 
 val prod_inv_rect_Type0 :
   ('a1, 'a2) Types.prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
 

diff --git a/extracted/globalenvs.ml b/extracted/globalenvs.ml
index 1ae2aa34e01ffcf9d2d3782bfd976fb6299f310a..3e52b9c169832287b833151cdb6d082d36265bbb 100644 (file)
--- a/extracted/globalenvs.ml
+++ b/extracted/globalenvs.ml
@@ -313,8 +313,8 @@ let size_init_data_list i_data =
     genv_t, GenMem.mem) Types.prod **)
 let add_globals extract_init init_env vars =
   Util.foldl (fun g_st id_init ->
     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 } =
     let init = extract_init init_info in
     let { Types.fst = g; Types.snd = st } = g_st in
     let { Types.fst = st'; Types.snd = b } =


@@ -329,8 +329,8 @@ let add_globals extract_init init_env vars =
     GenMem.mem Errors.res **)
 let init_globals extract_init g m vars =
   Util.foldl (fun st id_init ->
     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 ->
     let init = extract_init init_info in
     Obj.magic
       (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic st) (fun st0 ->

diff --git a/extracted/interpret2.ml b/extracted/interpret2.ml
index 530ad615e803415f623a53c6cdd0778b076bca00..e4b89e432be127a70d5d982aacaa2f0d39ddf84f 100644 (file)
--- a/extracted/interpret2.ml
+++ b/extracted/interpret2.ml
@@ -467,3 +467,21 @@ let aSM_preclassified_system c sigma policy =
       (execute_1_pseudo_instruction' c addr_of_label addr_of_symbol sigma
         policy (Obj.magic st))) (Obj.magic (Status.initialise_status c))
 
       (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
+

diff --git a/extracted/interpret2.mli b/extracted/interpret2.mli
index 28582873c4f6ed2f7fd7a04874d68dc33870dff3..04900341765e1a5ab0377a117377f45aa557298b 100644 (file)
--- a/extracted/interpret2.mli
+++ b/extracted/interpret2.mli
@@ -178,3 +178,7 @@ val aSM_preclassified_system :
   ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
   (BitVector.word -> Bool.bool) -> Measurable.preclassified_system
 
   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
+

diff --git a/extracted/joint_printer.ml b/extracted/joint_printer.ml
index f463f2cc87f4a87e15bdb94964138964f1f8b887..ce4472bffe7af225bfc846f04dc19b96aa35983d 100644 (file)
--- a/extracted/joint_printer.ml
+++ b/extracted/joint_printer.ml
@@ -432,13 +432,13 @@ type 'string printing_pass_independent_params = { print_String : (String.string
     (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
     BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
     printing_pass_independent_params -> 'a2 **)
     (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 =
   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
   in
   h_mk_printing_pass_independent_params print_String0 print_keyword0
     print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0


@@ -451,13 +451,13 @@ let rec printing_pass_independent_params_rect_Type4 h_mk_printing_pass_independe
     (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
     BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
     printing_pass_independent_params -> 'a2 **)
     (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 =
   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
   in
   h_mk_printing_pass_independent_params print_String0 print_keyword0
     print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0


@@ -470,13 +470,13 @@ let rec printing_pass_independent_params_rect_Type5 h_mk_printing_pass_independe
     (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
     BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
     printing_pass_independent_params -> 'a2 **)
     (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 =
   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
   in
   h_mk_printing_pass_independent_params print_String0 print_keyword0
     print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0


@@ -489,13 +489,13 @@ let rec printing_pass_independent_params_rect_Type3 h_mk_printing_pass_independe
     (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
     BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
     printing_pass_independent_params -> 'a2 **)
     (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 =
   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
   in
   h_mk_printing_pass_independent_params print_String0 print_keyword0
     print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0


@@ -508,13 +508,13 @@ let rec printing_pass_independent_params_rect_Type2 h_mk_printing_pass_independe
     (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
     BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
     printing_pass_independent_params -> 'a2 **)
     (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 =
   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
   in
   h_mk_printing_pass_independent_params print_String0 print_keyword0
     print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0


@@ -527,13 +527,13 @@ let rec printing_pass_independent_params_rect_Type1 h_mk_printing_pass_independe
     (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat ->
     BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
     printing_pass_independent_params -> 'a2 **)
     (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 =
   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
   in
   h_mk_printing_pass_independent_params print_String0 print_keyword0
     print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0


@@ -683,7 +683,7 @@ type 'string printing_params = { print_pass_ind : 'string
     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
     printing_params -> 'a2 **)
     (__ -> '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;
   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;


@@ -691,7 +691,7 @@ let rec printing_params_rect_Type4 p h_mk_printing_params x_301 =
     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 } =
     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
   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


@@ -704,7 +704,7 @@ let rec printing_params_rect_Type4 p h_mk_printing_params x_301 =
     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
     printing_params -> 'a2 **)
     (__ -> '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;
   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;


@@ -712,7 +712,7 @@ let rec printing_params_rect_Type5 p h_mk_printing_params x_303 =
     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 } =
     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
   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


@@ -725,7 +725,7 @@ let rec printing_params_rect_Type5 p h_mk_printing_params x_303 =
     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
     printing_params -> 'a2 **)
     (__ -> '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;
   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;


@@ -733,7 +733,7 @@ let rec printing_params_rect_Type3 p h_mk_printing_params x_305 =
     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 } =
     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
   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


@@ -746,7 +746,7 @@ let rec printing_params_rect_Type3 p h_mk_printing_params x_305 =
     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
     printing_params -> 'a2 **)
     (__ -> '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;
   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;


@@ -754,7 +754,7 @@ let rec printing_params_rect_Type2 p h_mk_printing_params x_307 =
     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 } =
     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
   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


@@ -767,7 +767,7 @@ let rec printing_params_rect_Type2 p h_mk_printing_params x_307 =
     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
     printing_params -> 'a2 **)
     (__ -> '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;
   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;


@@ -775,7 +775,7 @@ let rec printing_params_rect_Type1 p h_mk_printing_params x_309 =
     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 } =
     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
   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


@@ -788,7 +788,7 @@ let rec printing_params_rect_Type1 p h_mk_printing_params x_309 =
     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
     printing_params -> 'a2 **)
     (__ -> '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;
   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;


@@ -796,7 +796,7 @@ let rec printing_params_rect_Type0 p h_mk_printing_params x_311 =
     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 } =
     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
   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


@@ -969,54 +969,54 @@ type 'string print_serialization_params = { print_succ : (__ -> 'string);
 (** val print_serialization_params_rect_Type4 :
     Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
     print_serialization_params -> 'a2 **)
 (** 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 } =
   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 **)
   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 } =
   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 **)
   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 } =
   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 **)
   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 } =
   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 **)
   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 } =
   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 **)
   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 } =
   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
 
   in
   h_mk_print_serialization_params print_succ0 print_code_point0
 


@@ -1094,9 +1094,9 @@ type ('string, 'statementT) code_iteration_params = { cip_print_serialization_pa
     Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
     (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
     -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
     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;
   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
   in
   h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
     print_statementT0


@@ -1105,9 +1105,9 @@ let rec code_iteration_params_rect_Type4 p globals h_mk_code_iteration_params x_
     Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
     (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
     -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
     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;
   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
   in
   h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
     print_statementT0


@@ -1116,9 +1116,9 @@ let rec code_iteration_params_rect_Type5 p globals h_mk_code_iteration_params x_
     Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
     (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
     -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
     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;
   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
   in
   h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
     print_statementT0


@@ -1127,9 +1127,9 @@ let rec code_iteration_params_rect_Type3 p globals h_mk_code_iteration_params x_
     Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
     (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
     -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
     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;
   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
   in
   h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
     print_statementT0


@@ -1138,9 +1138,9 @@ let rec code_iteration_params_rect_Type2 p globals h_mk_code_iteration_params x_
     Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
     (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
     -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
     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;
   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
   in
   h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
     print_statementT0


@@ -1149,9 +1149,9 @@ let rec code_iteration_params_rect_Type1 p globals h_mk_code_iteration_params x_
     Joint.params -> AST.ident List.list -> ('a1 print_serialization_params ->
     (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
     -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
     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;
   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
   in
   h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
     print_statementT0


@@ -1165,11 +1165,11 @@ let rec cip_print_serialization_params p globals xxx =
 (** val fold_code0 :
     Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
     -> (__ -> 'a2 -> 'a3 -> 'a3) -> __ -> __ -> 'a3 -> 'a3 **)
 (** 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
   (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
 
 (** val print_statementT :
     Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params


@@ -1246,8 +1246,8 @@ let rec visit_graph next f b n m = function
   (match pm_choose_with_pref m n with
    | Types.None -> b
    | Types.Some res ->
   (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 :
      visit_graph next f (f pos a b) (next a) m' y)
 
 (** val print_list :

diff --git a/extracted/lINToASM.ml b/extracted/lINToASM.ml
index 770789a79c89e6d9096d69d288633a4e86487cce..dc2b40bfdd8b90038ee17d8118cf854b179ece23 100644 (file)
--- a/extracted/lINToASM.ml
+++ b/extracted/lINToASM.ml
@@ -139,10 +139,10 @@ type aSM_universe = { id_univ : Identifiers.universe;
     (Identifiers.universe -> AST.ident -> ASM.identifier
     Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
     Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
     (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 =
   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
   in
   h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     fresh_cost_label0


@@ -151,10 +151,10 @@ let rec aSM_universe_rect_Type4 h_mk_ASM_universe x_21483 =
     (Identifiers.universe -> AST.ident -> ASM.identifier
     Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
     Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
     (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 =
   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
   in
   h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     fresh_cost_label0


@@ -163,10 +163,10 @@ let rec aSM_universe_rect_Type5 h_mk_ASM_universe x_21485 =
     (Identifiers.universe -> AST.ident -> ASM.identifier
     Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
     Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
     (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 =
   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
   in
   h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     fresh_cost_label0


@@ -175,10 +175,10 @@ let rec aSM_universe_rect_Type3 h_mk_ASM_universe x_21487 =
     (Identifiers.universe -> AST.ident -> ASM.identifier
     Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
     Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
     (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 =
   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
   in
   h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     fresh_cost_label0


@@ -187,10 +187,10 @@ let rec aSM_universe_rect_Type2 h_mk_ASM_universe x_21489 =
     (Identifiers.universe -> AST.ident -> ASM.identifier
     Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
     Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
     (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 =
   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
   in
   h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     fresh_cost_label0


@@ -199,10 +199,10 @@ let rec aSM_universe_rect_Type1 h_mk_ASM_universe x_21491 =
     (Identifiers.universe -> AST.ident -> ASM.identifier
     Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
     Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
     (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 =
   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
   in
   h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     fresh_cost_label0


@@ -302,7 +302,7 @@ let identifier_of_label l =
       Identifiers.lookup_def PreIdentifiers.SymbolTag u.label_map current
         (Identifiers.empty_map PreIdentifiers.LabelTag)
     in
       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 } =
       match Identifiers.lookup PreIdentifiers.LabelTag lmap l with
       | Types.None ->
         let { Types.fst = id; Types.snd = univ } =


@@ -314,7 +314,7 @@ let identifier_of_label l =
         { Types.fst = { Types.fst = id; Types.snd = u.id_univ }; Types.snd =
           lmap }
     in
         { 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);
     { Types.fst = { id_univ = univ; current_funct = current; ident_map =
     u.ident_map; label_map =
     (Identifiers.add PreIdentifiers.SymbolTag u.label_map current lmap0);


@@ -1050,9 +1050,9 @@ type init_mutable = { virtual_dptr : (ASM.identifier, Z.z) Types.prod;
     ((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 **)
     ((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;
   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
 
   in
   h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
 


@@ -1060,9 +1060,9 @@ let rec init_mutable_rect_Type4 h_mk_init_mutable x_21509 =
     ((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 **)
     ((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;
   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
 
   in
   h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
 


@@ -1070,9 +1070,9 @@ let rec init_mutable_rect_Type5 h_mk_init_mutable x_21511 =
     ((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 **)
     ((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;
   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
 
   in
   h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
 


@@ -1080,9 +1080,9 @@ let rec init_mutable_rect_Type3 h_mk_init_mutable x_21513 =
     ((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 **)
     ((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;
   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
 
   in
   h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
 


@@ -1090,9 +1090,9 @@ let rec init_mutable_rect_Type2 h_mk_init_mutable x_21515 =
     ((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 **)
     ((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;
   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
 
   in
   h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
 


@@ -1100,9 +1100,9 @@ let rec init_mutable_rect_Type1 h_mk_init_mutable x_21517 =
     ((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 **)
     ((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;
   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
 
   in
   h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
 


@@ -1303,8 +1303,8 @@ let do_store_init_data m_mut data =
     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 ->
     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 };
     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 };

diff --git a/extracted/policy.ml b/extracted/policy.ml
index 194fc73ffd6b740df40272e74998a7a340c79b47..e13f645185838e571aae30106e4425e0b59cbc32 100644 (file)
--- a/extracted/policy.ml
+++ b/extracted/policy.ml
@@ -94,7 +94,7 @@ open PolicyStep
 let rec jump_expansion_internal program n =
   let labels = PolicyFront.create_label_map (Types.pi1 program) in
   let rec aux res =
 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 ->
    let { Types.fst = no_ch; Types.snd = z } = res in
     match z with
      | Types.None ->


@@ -108,10 +108,11 @@ prerr_endline "JEI_start";
              (PolicyStep.jump_expansion_step program (Types.pi1 labels)
                op))
   in
              (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 =
    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 ->
 (*
   (match n with
    | Nat.O ->


@@ -180,6 +181,7 @@ let jump_expansion' program =
            (Nat.S Nat.O)))))))))))))))) ppc x.Types.snd { Types.fst = Nat.O;
            Types.snd = Assembly.Short_jump }).Types.fst
        in
            (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 ->
        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 ->

diff --git a/extracted/policy.mli b/extracted/policy.mli
index 3d8eb7f4722bd50b29710c46df79acd52c1f31d9..6794a520140b96a3c4964f701ac2d87375afd00b 100644 (file)
--- a/extracted/policy.mli
+++ b/extracted/policy.mli
@@ -1,27 +1,11 @@
 open Preamble
 
 open Preamble
 

-open Assembly
-

 open Status
 
 open Status
 

-open Fetch
-

 open BitVectorTrie
 
 open String
 
 open BitVectorTrie
 
 open String
 

-open Exp
-
-open Arithmetic
-
-open Vector
-
-open FoldStuff
-
-open BitVector
-
-open Extranat
-

 open Integers
 
 open AST
 open Integers
 
 open AST


@@ -40,7 +24,17 @@ open PreIdentifiers
 
 open Errors
 
 
 open Errors
 

-open Extralib
+open Lists
+
+open Positive
+
+open Identifiers
+
+open CostLabel
+
+open ASM
+
+open Exp

 
 open Setoids
 
 
 open Setoids
 


@@ -48,6 +42,20 @@ open Monad
 
 open Option
 
 
 open Option
 

+open Extranat
+
+open Vector
+
+open FoldStuff
+
+open BitVector
+
+open Arithmetic
+
+open Fetch
+
+open Assembly
+

 open Div_and_mod
 
 open Jmeq
 open Div_and_mod
 
 open Jmeq


@@ -56,17 +64,13 @@ open Russell
 
 open Util
 
 
 open Util
 

-open List
-
-open Lists
-

 open Bool
 
 open Relations
 
 open Nat
 
 open Bool
 
 open Relations
 
 open Nat
 

-open Positive
+open List

 
 open Hints_declaration
 
 
 open Hints_declaration
 


@@ -78,11 +82,7 @@ open Logic
 
 open Types
 
 
 open Types
 

-open Identifiers
-
-open CostLabel
-
-open ASM
+open Extralib

 
 open PolicyFront
 
 
 open PolicyFront
 

diff --git a/extracted/policyFront.ml b/extracted/policyFront.ml
index 1b8ccc5fe5613cdcc70c7ef37441965710097541..66d8985dadf91fd8c3afb6d8b17563dea5f5bd2f 100644 (file)
--- a/extracted/policyFront.ml
+++ b/extracted/policyFront.ml
@@ -1,86 +1,86 @@
 open Preamble
 
 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 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 Assembly
 


@@ -656,34 +656,46 @@ let jump_expansion_step_instruction labels old_sigma inc_sigma ppc i =
     ASM.labelled_instruction List.list Types.sig0 -> Fetch.label_map ->
     ppc_pc_map Types.option Types.sig0 **)
 let jump_expansion_start program labels =
     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)
            (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)) __)) __

 
 

diff --git a/extracted/policyFront.mli b/extracted/policyFront.mli
index d2a2c58f0d64f9ab7e8489cb034967e838690f42..814f98593c49b9ac753317533ff71d54abe99ec3 100644 (file)
--- a/extracted/policyFront.mli
+++ b/extracted/policyFront.mli
@@ -1,86 +1,86 @@
 open Preamble
 
 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 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 Assembly
 

diff --git a/extracted/policyStep.ml b/extracted/policyStep.ml
index ddc45e972de4e13ec6323beab9ecbb3733a61e8d..3d66283a6482f75c66be73a08526561a2426feb1 100644 (file)
--- a/extracted/policyStep.ml
+++ b/extracted/policyStep.ml
@@ -1,27 +1,11 @@
 open Preamble
 
 open Preamble
 

-open Assembly
-

 open Status
 
 open Status
 

-open Fetch
-

 open BitVectorTrie
 
 open String
 
 open BitVectorTrie
 
 open String
 

-open Exp
-
-open Arithmetic
-
-open Vector
-
-open FoldStuff
-
-open BitVector
-
-open Extranat
-

 open Integers
 
 open AST
 open Integers
 
 open AST


@@ -40,7 +24,17 @@ open PreIdentifiers
 
 open Errors
 
 
 open Errors
 

-open Extralib
+open Lists
+
+open Positive
+
+open Identifiers
+
+open CostLabel
+
+open ASM
+
+open Exp

 
 open Setoids
 
 
 open Setoids
 


@@ -48,6 +42,20 @@ open Monad
 
 open Option
 
 
 open Option
 

+open Extranat
+
+open Vector
+
+open FoldStuff
+
+open BitVector
+
+open Arithmetic
+
+open Fetch
+
+open Assembly
+

 open Div_and_mod
 
 open Jmeq
 open Div_and_mod
 
 open Jmeq


@@ -56,17 +64,13 @@ open Russell
 
 open Util
 
 
 open Util
 

-open List
-
-open Lists
-

 open Bool
 
 open Relations
 
 open Nat
 
 open Bool
 
 open Relations
 
 open Nat
 

-open Positive
+open List

 
 open Hints_declaration
 
 
 open Hints_declaration
 


@@ -78,11 +82,7 @@ open Logic
 
 open Types
 
 
 open Types
 

-open Identifiers
-
-open CostLabel
-
-open ASM
+open Extralib

 
 open PolicyFront
 
 
 open PolicyFront
 


@@ -91,41 +91,49 @@ 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 =
     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
      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 _ ->
           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)
          (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)
            | 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)
            | 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
            | 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
              (Types.pi1 old_sigma).Types.snd { Types.fst = Nat.O; Types.snd =
              Assembly.Short_jump }).Types.snd
          in


@@ -151,34 +159,31 @@ let jump_expansion_step program labels old_sigma =
          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
          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
          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
              (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
          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 =
          { 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))))))))))))))))
          (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))))))))))))))))


@@ -195,9 +200,11 @@ let jump_expansion_step program labels old_sigma =
              (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
              (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 _ ->
    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
   (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


@@ -207,5 +214,5 @@ let jump_expansion_step program labels old_sigma =
        Types.None })
    | Bool.False ->
      (fun _ -> { Types.fst = (Nat.eqb final_added Nat.O); Types.snd =
        Types.None })
    | Bool.False ->
      (fun _ -> { Types.fst = (Nat.eqb final_added Nat.O); Types.snd =

-       (Types.Some final_policy) })) __)) __
+       (Types.Some final_policy) })) __)) __)) __

 
 

diff --git a/extracted/policyStep.mli b/extracted/policyStep.mli
index 1e23babdbe7f8eb027b6e4213c8a3ff082dd2e8c..6f3ef4919838078800e71bfe1b8a27072660b70a 100644 (file)
--- a/extracted/policyStep.mli
+++ b/extracted/policyStep.mli
@@ -1,27 +1,11 @@
 open Preamble
 
 open Preamble
 

-open Assembly
-

 open Status
 
 open Status
 

-open Fetch
-

 open BitVectorTrie
 
 open String
 
 open BitVectorTrie
 
 open String
 

-open Exp
-
-open Arithmetic
-
-open Vector
-
-open FoldStuff
-
-open BitVector
-
-open Extranat
-

 open Integers
 
 open AST
 open Integers
 
 open AST


@@ -40,7 +24,17 @@ open PreIdentifiers
 
 open Errors
 
 
 open Errors
 

-open Extralib
+open Lists
+
+open Positive
+
+open Identifiers
+
+open CostLabel
+
+open ASM
+
+open Exp

 
 open Setoids
 
 
 open Setoids
 


@@ -48,6 +42,20 @@ open Monad
 
 open Option
 
 
 open Option
 

+open Extranat
+
+open Vector
+
+open FoldStuff
+
+open BitVector
+
+open Arithmetic
+
+open Fetch
+
+open Assembly
+

 open Div_and_mod
 
 open Jmeq
 open Div_and_mod
 
 open Jmeq


@@ -56,17 +64,13 @@ open Russell
 
 open Util
 
 
 open Util
 

-open List
-
-open Lists
-

 open Bool
 
 open Relations
 
 open Nat
 
 open Bool
 
 open Relations
 
 open Nat
 

-open Positive
+open List

 
 open Hints_declaration
 
 
 open Hints_declaration
 


@@ -78,11 +82,7 @@ open Logic
 
 open Types
 
 
 open Types
 

-open Identifiers
-
-open CostLabel
-
-open ASM
+open Extralib

 
 open PolicyFront
 
 
 open PolicyFront
 

diff --git a/extracted/semantics.ml b/extracted/semantics.ml
index 221a22e2f8959b9cff698d4dbdf85ac301487220..c49e25f6045d968ca2ff091454a95d33f5fc00ab 100644 (file)
--- a/extracted/semantics.ml
+++ b/extracted/semantics.ml
@@ -14,12 +14,12 @@ open Interpret
 
 open ASMCosts
 
 
 open ASMCosts
 

-open Assembly
-

 open Status
 
 open Fetch
 
 open Status
 
 open Fetch
 

+open Assembly
+

 open PolicyFront
 
 open PolicyStep
 open PolicyFront
 
 open PolicyStep


@@ -315,38 +315,38 @@ type preclassified_system_pass =
 (** val preclassified_system_pass_rect_Type4 :
     Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
     preclassified_system_pass -> 'a1 **)
 (** 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 **)
 
 (** 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 **)
 
 (** 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 **)
 
 (** 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 **)
 
 (** 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 **)
 
 (** 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 ->
 
 (** val pcs_pcs :
     Compiler.pass -> preclassified_system_pass ->


@@ -433,8 +433,8 @@ let preclassified_system_of_pass = function
     Joint_fullexec.joint_preclassified_system LIN_semantics.lIN_semantics)
 | Compiler.Assembly_pass ->
   (fun prog ->
     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))
     Interpret2.aSM_preclassified_system code sigma policy)
 | Compiler.Object_code_pass ->
   (fun prog -> Interpret2.oC_preclassified_system (Obj.magic prog))

diff --git a/extracted/semantics.mli b/extracted/semantics.mli
index 68973c5166a746cf6bfdd4b638391f89c5035888..5957a12f74c84cf74c8698396d6d0d77d78a4ce3 100644 (file)
--- a/extracted/semantics.mli
+++ b/extracted/semantics.mli
@@ -14,12 +14,12 @@ open Interpret
 
 open ASMCosts
 
 
 open ASMCosts
 

-open Assembly
-

 open Status
 
 open Fetch
 
 open Status
 
 open Fetch
 

+open Assembly
+

 open PolicyFront
 
 open PolicyStep
 open PolicyFront
 
 open PolicyStep

diff --git a/extracted/simplifyCasts.ml b/extracted/simplifyCasts.ml
index dd7afae5efbe110219ee4d44ff09d5631bb5538d..dc6f2bc86c37d60c6139cdae432ca499032a9bd7 100644 (file)
--- a/extracted/simplifyCasts.ml
+++ b/extracted/simplifyCasts.ml
@@ -356,16 +356,16 @@ let rec simplify_expr e target_sz target_sg =
               (match TypeComparison.assert_type_eq (Csyntax.typeof lhs)
                        (Csyntax.typeof rhs) with
                | Errors.OK _ ->
               (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 } =
                    (fun _ ->
                    (let { Types.fst = desired_type_lhs; Types.snd = lhs1 } =

-                      eta2011
+                      eta2033

                     in
                    (fun _ ->
                     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 =
                      (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
                       in
                      (fun _ ->
                      (match Bool.andb desired_type_lhs desired_type_rhs with


@@ -418,10 +418,10 @@ let rec simplify_expr e target_sz target_sg =
               (match necessary_conditions cast_sz cast_sg target_sz target_sg with
                | Bool.True ->
                  (fun _ ->
               (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 } =
                      (fun _ ->
                      (let { Types.fst = desired_type; Types.snd = castee1 } =

-                        eta2013
+                        eta2035

                       in
                      (fun _ ->
                      (match desired_type with
                       in
                      (fun _ ->
                      (match desired_type with


@@ -430,11 +430,11 @@ let rec simplify_expr e target_sz target_sg =
                           castee1 })
                       | Bool.False ->
                         (fun _ ->
                           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 =
                            in
                             (fun _ ->
                             (let { Types.fst = desired_type2; Types.snd =

-                               castee2 } = eta2012
+                               castee2 } = eta2034

                              in
                             (fun _ ->
                             (match desired_type2 with
                              in
                             (fun _ ->
                             (match desired_type2 with


@@ -448,10 +448,10 @@ let rec simplify_expr e target_sz target_sg =
                        __)) __)) __)
                | Bool.False ->
                  (fun _ ->
                        __)) __)) __)
                | 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 =
                      (fun _ ->
                      (let { Types.fst = desired_type2; Types.snd =

-                        castee2 } = eta2014
+                        castee2 } = eta2036

                       in
                      (fun _ ->
                      (match desired_type2 with
                       in
                      (fun _ ->
                      (match desired_type2 with


@@ -505,16 +505,16 @@ let rec simplify_expr e target_sz target_sg =
            (match TypeComparison.assert_type_eq (Csyntax.typeof iftrue)
                     (Csyntax.typeof iffalse) with
             | Errors.OK _ ->
            (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 } =
                 (fun _ ->
                 (let { Types.fst = desired_true; Types.snd = iftrue1 } =

-                   eta2016
+                   eta2038

                  in
                 (fun _ ->
                  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 } =
                   (fun _ ->
                   (let { Types.fst = desired_false; Types.snd = iffalse1 } =

-                     eta2015
+                     eta2037

                    in
                   (fun _ ->
                   (match Bool.andb desired_true desired_false with
                    in
                   (fun _ ->
                   (match Bool.andb desired_true desired_false with


@@ -572,9 +572,9 @@ let rec simplify_expr e target_sz target_sg =
      (fun _ ->
        match TypeComparison.type_eq_dec ty (Csyntax.typeof e1) with
        | Types.Inl _ ->
      (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 _ ->
            (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 _ ->
            (fun _ -> { Types.fst = desired_type; Types.snd = (Csyntax.Expr
            ((Csyntax.Ecost (l, e2)), (Csyntax.typeof e2))) })) __)) __
        | Types.Inr _ ->


@@ -615,9 +615,9 @@ and simplify_inside e =
           | Csyntax.Tvoid -> (fun _ -> e)
           | Csyntax.Tint (cast_sz, cast_sg) ->
             (fun _ ->
           | 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 _ ->
                 (fun _ ->

-                (let { Types.fst = success; Types.snd = castee1 } = eta2018
+                (let { Types.fst = success; Types.snd = castee1 } = eta2040

                  in
                 (fun _ ->
                 (match success with
                  in
                 (fun _ ->
                 (match success with

diff --git a/extracted/status.ml b/extracted/status.ml
index 7a08f700e269d4d3d107d26b91c98a3fe44febcb..2abe567963465f02ac48df2f6c24a92c223a0ac1 100644 (file)
--- a/extracted/status.ml
+++ b/extracted/status.ml
@@ -88,43 +88,43 @@ type serialBufferType =
     (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
     serialBufferType -> 'a1 **)
 let rec serialBufferType_rect_Type4 h_Eight h_Nine = function
     (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
 
 (** 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
 
 (** 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
 
 (** 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
 
 (** 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
 
 (** 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 ->
 
 (** val serialBufferType_inv_rect_Type4 :
     serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->


@@ -181,49 +181,49 @@ type lineType =
     (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
     -> 'a1) -> lineType -> 'a1 **)
 let rec lineType_rect_Type4 h_P1 h_P3 h_SerialBuffer = function
     (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
 
 (** 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
 
 (** 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
 
 (** 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
 
 (** 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
 
 (** 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 -> __ ->
 
 (** val lineType_inv_rect_Type4 :
     lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->


@@ -730,13 +730,13 @@ type 'm preStatus = { low_internal_ram : BitVector.byte
     -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
     Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
     preStatus -> 'a2 **)
     -> 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 =
   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
   in
   h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     program_counter0 special_function_registers_8053


@@ -748,13 +748,13 @@ let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_22224 =
     -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
     Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
     preStatus -> 'a2 **)
     -> 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 =
   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
   in
   h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     program_counter0 special_function_registers_8053


@@ -766,13 +766,13 @@ let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_22226 =
     -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
     Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
     preStatus -> 'a2 **)
     -> 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 =
   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
   in
   h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     program_counter0 special_function_registers_8053


@@ -784,13 +784,13 @@ let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_22228 =
     -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
     Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
     preStatus -> 'a2 **)
     -> 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 =
   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
   in
   h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     program_counter0 special_function_registers_8053


@@ -802,13 +802,13 @@ let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_22230 =
     -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
     Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
     preStatus -> 'a2 **)
     -> 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 =
   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
   in
   h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     program_counter0 special_function_registers_8053


@@ -820,13 +820,13 @@ let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_22232 =
     -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
     Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
     preStatus -> 'a2 **)
     -> 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 =
   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
   in
   h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     program_counter0 special_function_registers_8053

diff --git a/extracted/switchRemoval.ml b/extracted/switchRemoval.ml
index 3a873f716e9589180701189cb81ae442b8cf3166..c018da29d5b627768edebfc747e66d33f3d154e8 100644 (file)
--- a/extracted/switchRemoval.ml
+++ b/extracted/switchRemoval.ml
@@ -173,10 +173,10 @@ let rec produce_cond e switch_cases u exit =
     { Types.fst = { Types.fst = (Csyntax.Slabel (lab, st')); Types.snd =
     lab }; Types.snd = u1 }
   | Csyntax.LScase (sz, tag, st, other_cases) ->
     { 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
       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 st' = convert_break_to_goto st exit in
     let { Types.fst = lab; Types.snd = u2 } =
       Identifiers.fresh PreIdentifiers.SymbolTag u1


@@ -198,10 +198,10 @@ let simplify_switch e switch_cases uv =
   let { Types.fst = exit_label; Types.snd = uv1 } =
     Identifiers.fresh PreIdentifiers.SymbolTag uv
   in
   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
     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 }
 
   { Types.fst = (Csyntax.Ssequence (result, (Csyntax.Slabel (exit_label,
   Csyntax.Sskip)))); Types.snd = uv2 }
 


@@ -218,36 +218,36 @@ let rec switch_removal st u =
   | Csyntax.Scall (x, x0, x1) ->
     { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
   | Csyntax.Ssequence (s1, s2) ->
   | 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) ->
     { 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) ->
     { 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) ->
     { 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) ->
     { 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''' }
     { Types.fst = { Types.fst = (Csyntax.Sfor (s1', e, s2', s3'));
     Types.snd = (List.append acc1 (List.append acc2 acc3)) }; Types.snd =
     u''' }


@@ -258,10 +258,10 @@ let rec switch_removal st u =
   | Csyntax.Sreturn x ->
     { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
   | Csyntax.Sswitch (e, branches) ->
   | 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
       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
     let { Types.fst = switch_tmp; Types.snd = u'' } =
       Identifiers.fresh PreIdentifiers.SymbolTag u'
     in


@@ -275,15 +275,15 @@ let rec switch_removal st u =
     Types.snd = (List.Cons ({ Types.fst = switch_tmp; Types.snd =
     (Csyntax.typeof e) }, acc)) }; Types.snd = u''' }
   | Csyntax.Slabel (label, body) ->
     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) ->
     { 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 :
     { Types.fst = { Types.fst = (Csyntax.Scost (cost, body')); Types.snd =
     acc }; Types.snd = u' }
 (** val switch_removal_branches :


@@ -293,17 +293,17 @@ let rec switch_removal st u =
 and switch_removal_branches l u =
   match l with
   | Csyntax.LSdefault st ->
 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) ->
     { 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
       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'' }
 
     { Types.fst = { Types.fst = (Csyntax.LScase (sz, int, st', tl_result));
     Types.snd = (List.append acc1 acc2) }; Types.snd = u'' }
 


@@ -311,21 +311,21 @@ and switch_removal_branches l u =
     (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
     Identifiers.universe) Types.prod -> 'a1 **)
 let ret_st x =
     (('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 =
 
 (** 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 =
 
 (** 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 =
 
 (** val least_identifier : PreIdentifiers.identifier **)
 let least_identifier =


@@ -405,10 +405,10 @@ let max_id_of_function f =
     Types.prod List.list) Types.prod **)
 let function_switch_removal f =
   let u = Fresh.universe_of_max (max_id_of_function f) in
     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
     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 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 }

diff --git a/extracted/toCminor.ml b/extracted/toCminor.ml
index 4131f6c3fdb24e6d71eaf9bd743a0de41687f5b8..8e12b742db8bd1934770528537837d561e2bfcb5 100644 (file)
--- a/extracted/toCminor.ml
+++ b/extracted/toCminor.ml
@@ -2062,8 +2062,8 @@ let alloc_params_main vars lbls statement uv ul rettyp params s =
     let { Types.fst = id; Types.snd = ty } = it in
     Obj.magic
       (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su)
     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 { Types.fst = fgens1; Types.snd = s0 } = result in
         (fun _ ->
         Obj.magic

diff --git a/extracted/toRTLabs.ml b/extracted/toRTLabs.ml
index c33d803a8fc73037177a28851e5b1222f9d6e162..b5ca97295be613b741a10253976ae5f822696731 100644 (file)
--- a/extracted/toRTLabs.ml
+++ b/extracted/toRTLabs.ml
@@ -120,8 +120,8 @@ type env =
 let populate_env en gen =
   List.foldr (fun idt rsengen ->
     let { Types.fst = id; Types.snd = ty } = idt in
 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 { Types.fst = r; Types.snd = gen' } =
       Identifiers.fresh PreIdentifiers.RegisterTag gen0
     in


@@ -1344,16 +1344,16 @@ let c2ra_function f =
   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 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
      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 _ ->
   (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
      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
   (fun _ ->
   (let { Types.dpi1 = locals_reggen; Types.dpi2 = result } =
      match f.Cminor_syntax.f_return with