extracted/byteValues.ml

   1 open Preamble
   2
   3 open Proper
   4
   5 open PositiveMap
   6
   7 open Deqsets
   8
   9 open ErrorMessages
  10
  11 open PreIdentifiers
  12
  13 open Errors
  14
  15 open Extralib
  16
  17 open Lists
  18
  19 open Identifiers
  20
  21 open Integers
  22
  23 open AST
  24
  25 open Division
  26
  27 open Exp
  28
  29 open Arithmetic
  30
  31 open Setoids
  32
  33 open Monad
  34
  35 open Option
  36
  37 open Extranat
  38
  39 open Vector
  40
  41 open Div_and_mod
  42
  43 open Jmeq
  44
  45 open Russell
  46
  47 open List
  48
  49 open Util
  50
  51 open FoldStuff
  52
  53 open BitVector
  54
  55 open Types
  56
  57 open Bool
  58
  59 open Relations
  60
  61 open Nat
  62
  63 open Hints_declaration
  64
  65 open Core_notation
  66
  67 open Pts
  68
  69 open Logic
  70
  71 open Positive
  72
  73 open Z
  74
  75 open BitVectorZ
  76
  77 open Pointers
  78
  79 open Hide
  80
  81 type cpointer = Pointers.pointer Types.sig0
  82
  83 type xpointer = Pointers.pointer Types.sig0
  84
  85 type program_counter = { pc_block : Pointers.block Types.sig0;
  86                          pc_offset : Positive.pos }
  87
  88 (** val program_counter_rect_Type4 :
  89     (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
  90     'a1 **)
  91 let rec program_counter_rect_Type4 h_mk_program_counter x_6152 =
  92   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6152 in
  93   h_mk_program_counter pc_block0 pc_offset0
  94
  95 (** val program_counter_rect_Type5 :
  96     (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
  97     'a1 **)
  98 let rec program_counter_rect_Type5 h_mk_program_counter x_6154 =
  99   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6154 in
 100   h_mk_program_counter pc_block0 pc_offset0
 101
 102 (** val program_counter_rect_Type3 :
 103     (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
 104     'a1 **)
 105 let rec program_counter_rect_Type3 h_mk_program_counter x_6156 =
 106   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6156 in
 107   h_mk_program_counter pc_block0 pc_offset0
 108
 109 (** val program_counter_rect_Type2 :
 110     (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
 111     'a1 **)
 112 let rec program_counter_rect_Type2 h_mk_program_counter x_6158 =
 113   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6158 in
 114   h_mk_program_counter pc_block0 pc_offset0
 115
 116 (** val program_counter_rect_Type1 :
 117     (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
 118     'a1 **)
 119 let rec program_counter_rect_Type1 h_mk_program_counter x_6160 =
 120   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6160 in
 121   h_mk_program_counter pc_block0 pc_offset0
 122
 123 (** val program_counter_rect_Type0 :
 124     (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
 125     'a1 **)
 126 let rec program_counter_rect_Type0 h_mk_program_counter x_6162 =
 127   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6162 in
 128   h_mk_program_counter pc_block0 pc_offset0
 129
 130 (** val pc_block : program_counter -> Pointers.block Types.sig0 **)
 131 let rec pc_block xxx =
 132   xxx.pc_block
 133
 134 (** val pc_offset : program_counter -> Positive.pos **)
 135 let rec pc_offset xxx =
 136   xxx.pc_offset
 137
 138 (** val program_counter_inv_rect_Type4 :
 139     program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
 140     'a1) -> 'a1 **)
 141 let program_counter_inv_rect_Type4 hterm h1 =
 142   let hcut = program_counter_rect_Type4 h1 hterm in hcut __
 143
 144 (** val program_counter_inv_rect_Type3 :
 145     program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
 146     'a1) -> 'a1 **)
 147 let program_counter_inv_rect_Type3 hterm h1 =
 148   let hcut = program_counter_rect_Type3 h1 hterm in hcut __
 149
 150 (** val program_counter_inv_rect_Type2 :
 151     program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
 152     'a1) -> 'a1 **)
 153 let program_counter_inv_rect_Type2 hterm h1 =
 154   let hcut = program_counter_rect_Type2 h1 hterm in hcut __
 155
 156 (** val program_counter_inv_rect_Type1 :
 157     program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
 158     'a1) -> 'a1 **)
 159 let program_counter_inv_rect_Type1 hterm h1 =
 160   let hcut = program_counter_rect_Type1 h1 hterm in hcut __
 161
 162 (** val program_counter_inv_rect_Type0 :
 163     program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
 164     'a1) -> 'a1 **)
 165 let program_counter_inv_rect_Type0 hterm h1 =
 166   let hcut = program_counter_rect_Type0 h1 hterm in hcut __
 167
 168 (** val program_counter_discr : program_counter -> program_counter -> __ **)
 169 let program_counter_discr x y =
 170   Logic.eq_rect_Type2 x
 171     (let { pc_block = a0; pc_offset = a1 } = x in
 172     Obj.magic (fun _ dH -> dH __ __)) y
 173
 174 (** val program_counter_jmdiscr :
 175     program_counter -> program_counter -> __ **)
 176 let program_counter_jmdiscr x y =
 177   Logic.eq_rect_Type2 x
 178     (let { pc_block = a0; pc_offset = a1 } = x in
 179     Obj.magic (fun _ dH -> dH __ __)) y
 180
 181 (** val eq_program_counter :
 182     program_counter -> program_counter -> Bool.bool **)
 183 let eq_program_counter pc1 pc2 =
 184   Bool.andb
 185     (Pointers.eq_block (Types.pi1 pc1.pc_block) (Types.pi1 pc2.pc_block))
 186     (Positive.eqb pc1.pc_offset pc2.pc_offset)
 187
 188 (** val bitvector_from_pos :
 189     Nat.nat -> Positive.pos -> BitVector.bitVector **)
 190 let bitvector_from_pos n p =
 191   BitVectorZ.bitvector_of_Z n (Z.zpred (Z.Pos p))
 192
 193 (** val pos_from_bitvector :
 194     Nat.nat -> BitVector.bitVector -> Positive.pos **)
 195 let pos_from_bitvector n v =
 196   (match Z.zsucc (BitVectorZ.z_of_unsigned_bitvector n v) with
 197    | Z.OZ -> (fun _ -> assert false (* absurd case *))
 198    | Z.Pos x -> (fun _ -> x)
 199    | Z.Neg x -> (fun _ -> assert false (* absurd case *))) __
 200
 201 (** val cpointer_of_pc : program_counter -> cpointer Types.option **)
 202 let cpointer_of_pc pc =
 203   let pc_off = pc.pc_offset in
 204   (match Positive.leb pc_off (Positive.two_power_nat Pointers.offset_size) with
 205    | Bool.True ->
 206      Obj.magic
 207        (Monad.m_return0 (Monad.max_def Option.option) { Pointers.pblock =
 208          (Types.pi1 pc.pc_block); Pointers.poff =
 209          (bitvector_from_pos Pointers.offset_size pc_off) })
 210    | Bool.False -> Types.None)
 211
 212 type part =
 213   Nat.nat
 214   (* singleton inductive, whose constructor was mk_part *)
 215
 216 (** val part_rect_Type4 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
 217 let rec part_rect_Type4 h_mk_part x_6178 =
 218   let part_no = x_6178 in h_mk_part part_no __
 219
 220 (** val part_rect_Type5 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
 221 let rec part_rect_Type5 h_mk_part x_6180 =
 222   let part_no = x_6180 in h_mk_part part_no __
 223
 224 (** val part_rect_Type3 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
 225 let rec part_rect_Type3 h_mk_part x_6182 =
 226   let part_no = x_6182 in h_mk_part part_no __
 227
 228 (** val part_rect_Type2 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
 229 let rec part_rect_Type2 h_mk_part x_6184 =
 230   let part_no = x_6184 in h_mk_part part_no __
 231
 232 (** val part_rect_Type1 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
 233 let rec part_rect_Type1 h_mk_part x_6186 =
 234   let part_no = x_6186 in h_mk_part part_no __
 235
 236 (** val part_rect_Type0 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
 237 let rec part_rect_Type0 h_mk_part x_6188 =
 238   let part_no = x_6188 in h_mk_part part_no __
 239
 240 (** val part_no : part -> Nat.nat **)
 241 let rec part_no xxx =
 242   let yyy = xxx in yyy
 243
 244 (** val part_inv_rect_Type4 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
 245 let part_inv_rect_Type4 hterm h1 =
 246   let hcut = part_rect_Type4 h1 hterm in hcut __
 247
 248 (** val part_inv_rect_Type3 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
 249 let part_inv_rect_Type3 hterm h1 =
 250   let hcut = part_rect_Type3 h1 hterm in hcut __
 251
 252 (** val part_inv_rect_Type2 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
 253 let part_inv_rect_Type2 hterm h1 =
 254   let hcut = part_rect_Type2 h1 hterm in hcut __
 255
 256 (** val part_inv_rect_Type1 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
 257 let part_inv_rect_Type1 hterm h1 =
 258   let hcut = part_rect_Type1 h1 hterm in hcut __
 259
 260 (** val part_inv_rect_Type0 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
 261 let part_inv_rect_Type0 hterm h1 =
 262   let hcut = part_rect_Type0 h1 hterm in hcut __
 263
 264 (** val part_discr : part -> part -> __ **)
 265 let part_discr x y =
 266   Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y
 267
 268 (** val part_jmdiscr : part -> part -> __ **)
 269 let part_jmdiscr x y =
 270   Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y
 271
 272 (** val dpi1__o__part_no__o__inject :
 273     (part, 'a1) Types.dPair -> Nat.nat Types.sig0 **)
 274 let dpi1__o__part_no__o__inject x2 =
 275   part_no x2.Types.dpi1
 276
 277 (** val dpi1__o__part_no__o__Z_of_nat : (part, 'a1) Types.dPair -> Z.z **)
 278 let dpi1__o__part_no__o__Z_of_nat x1 =
 279   Z.z_of_nat (part_no x1.Types.dpi1)
 280
 281 (** val eject__o__part_no__o__inject :
 282     part Types.sig0 -> Nat.nat Types.sig0 **)
 283 let eject__o__part_no__o__inject x2 =
 284   part_no (Types.pi1 x2)
 285
 286 (** val eject__o__part_no__o__Z_of_nat : part Types.sig0 -> Z.z **)
 287 let eject__o__part_no__o__Z_of_nat x1 =
 288   Z.z_of_nat (part_no (Types.pi1 x1))
 289
 290 (** val part_no__o__Z_of_nat : part -> Z.z **)
 291 let part_no__o__Z_of_nat x0 =
 292   Z.z_of_nat (part_no x0)
 293
 294 (** val part_no__o__inject : part -> Nat.nat Types.sig0 **)
 295 let part_no__o__inject x1 =
 296   part_no x1
 297
 298 (** val dpi1__o__part_no : (part, 'a1) Types.dPair -> Nat.nat **)
 299 let dpi1__o__part_no x1 =
 300   part_no x1.Types.dpi1
 301
 302 (** val eject__o__part_no : part Types.sig0 -> Nat.nat **)
 303 let eject__o__part_no x1 =
 304   part_no (Types.pi1 x1)
 305
 306 (** val part_from_sig : Nat.nat Types.sig0 -> part **)
 307 let part_from_sig n_sig =
 308   Types.pi1 n_sig
 309
 310 (** val dpi1__o__part_no__o__inject__o__sig_to_part__o__inject :
 311     (part, 'a1) Types.dPair -> part Types.sig0 **)
 312 let dpi1__o__part_no__o__inject__o__sig_to_part__o__inject x2 =
 313   part_from_sig (dpi1__o__part_no__o__inject x2)
 314
 315 (** val dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no__o__inject :
 316     (part, 'a1) Types.dPair -> Nat.nat Types.sig0 **)
 317 let dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no__o__inject x2 =
 318   part_no__o__inject (part_from_sig (dpi1__o__part_no__o__inject x2))
 319
 320 (** val dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat :
 321     (part, 'a1) Types.dPair -> Z.z **)
 322 let dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat x1 =
 323   part_no__o__Z_of_nat (part_from_sig (dpi1__o__part_no__o__inject x1))
 324
 325 (** val dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no :
 326     (part, 'a1) Types.dPair -> Nat.nat **)
 327 let dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no x1 =
 328   part_no (part_from_sig (dpi1__o__part_no__o__inject x1))
 329
 330 (** val eject__o__part_no__o__inject__o__sig_to_part__o__inject :
 331     part Types.sig0 -> part Types.sig0 **)
 332 let eject__o__part_no__o__inject__o__sig_to_part__o__inject x2 =
 333   part_from_sig (eject__o__part_no__o__inject x2)
 334
 335 (** val eject__o__part_no__o__inject__o__sig_to_part__o__part_no__o__inject :
 336     part Types.sig0 -> Nat.nat Types.sig0 **)
 337 let eject__o__part_no__o__inject__o__sig_to_part__o__part_no__o__inject x2 =
 338   part_no__o__inject (part_from_sig (eject__o__part_no__o__inject x2))
 339
 340 (** val eject__o__part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat :
 341     part Types.sig0 -> Z.z **)
 342 let eject__o__part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat x1 =
 343   part_no__o__Z_of_nat (part_from_sig (eject__o__part_no__o__inject x1))
 344
 345 (** val eject__o__part_no__o__inject__o__sig_to_part__o__part_no :
 346     part Types.sig0 -> Nat.nat **)
 347 let eject__o__part_no__o__inject__o__sig_to_part__o__part_no x1 =
 348   part_no (part_from_sig (eject__o__part_no__o__inject x1))
 349
 350 (** val inject__o__sig_to_part__o__inject : Nat.nat -> part Types.sig0 **)
 351 let inject__o__sig_to_part__o__inject x0 =
 352   part_from_sig x0
 353
 354 (** val inject__o__sig_to_part__o__part_no__o__inject :
 355     Nat.nat -> Nat.nat Types.sig0 **)
 356 let inject__o__sig_to_part__o__part_no__o__inject x0 =
 357   part_no__o__inject (part_from_sig x0)
 358
 359 (** val inject__o__sig_to_part__o__part_no__o__Z_of_nat : Nat.nat -> Z.z **)
 360 let inject__o__sig_to_part__o__part_no__o__Z_of_nat x0 =
 361   part_no__o__Z_of_nat (part_from_sig x0)
 362
 363 (** val inject__o__sig_to_part__o__part_no : Nat.nat -> Nat.nat **)
 364 let inject__o__sig_to_part__o__part_no x0 =
 365   part_no (part_from_sig x0)
 366
 367 (** val part_no__o__inject__o__sig_to_part__o__inject :
 368     part -> part Types.sig0 **)
 369 let part_no__o__inject__o__sig_to_part__o__inject x0 =
 370   part_from_sig (part_no__o__inject x0)
 371
 372 (** val part_no__o__inject__o__sig_to_part__o__part_no__o__inject :
 373     part -> Nat.nat Types.sig0 **)
 374 let part_no__o__inject__o__sig_to_part__o__part_no__o__inject x0 =
 375   part_no__o__inject (part_from_sig (part_no__o__inject x0))
 376
 377 (** val part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat :
 378     part -> Z.z **)
 379 let part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat x0 =
 380   part_no__o__Z_of_nat (part_from_sig (part_no__o__inject x0))
 381
 382 (** val part_no__o__inject__o__sig_to_part__o__part_no : part -> Nat.nat **)
 383 let part_no__o__inject__o__sig_to_part__o__part_no x0 =
 384   part_no (part_from_sig (part_no__o__inject x0))
 385
 386 (** val dpi1__o__sig_to_part__o__inject :
 387     (Nat.nat Types.sig0, 'a1) Types.dPair -> part Types.sig0 **)
 388 let dpi1__o__sig_to_part__o__inject x2 =
 389   part_from_sig x2.Types.dpi1
 390
 391 (** val dpi1__o__sig_to_part__o__part_no__o__inject :
 392     (Nat.nat Types.sig0, 'a1) Types.dPair -> Nat.nat Types.sig0 **)
 393 let dpi1__o__sig_to_part__o__part_no__o__inject x2 =
 394   part_no__o__inject (part_from_sig x2.Types.dpi1)
 395
 396 (** val dpi1__o__sig_to_part__o__part_no__o__Z_of_nat :
 397     (Nat.nat Types.sig0, 'a1) Types.dPair -> Z.z **)
 398 let dpi1__o__sig_to_part__o__part_no__o__Z_of_nat x1 =
 399   part_no__o__Z_of_nat (part_from_sig x1.Types.dpi1)
 400
 401 (** val dpi1__o__sig_to_part__o__part_no :
 402     (Nat.nat Types.sig0, 'a1) Types.dPair -> Nat.nat **)
 403 let dpi1__o__sig_to_part__o__part_no x1 =
 404   part_no (part_from_sig x1.Types.dpi1)
 405
 406 (** val eject__o__sig_to_part__o__inject :
 407     Nat.nat Types.sig0 Types.sig0 -> part Types.sig0 **)
 408 let eject__o__sig_to_part__o__inject x2 =
 409   part_from_sig (Types.pi1 x2)
 410
 411 (** val eject__o__sig_to_part__o__part_no__o__inject :
 412     Nat.nat Types.sig0 Types.sig0 -> Nat.nat Types.sig0 **)
 413 let eject__o__sig_to_part__o__part_no__o__inject x2 =
 414   part_no__o__inject (part_from_sig (Types.pi1 x2))
 415
 416 (** val eject__o__sig_to_part__o__part_no__o__Z_of_nat :
 417     Nat.nat Types.sig0 Types.sig0 -> Z.z **)
 418 let eject__o__sig_to_part__o__part_no__o__Z_of_nat x1 =
 419   part_no__o__Z_of_nat (part_from_sig (Types.pi1 x1))
 420
 421 (** val eject__o__sig_to_part__o__part_no :
 422     Nat.nat Types.sig0 Types.sig0 -> Nat.nat **)
 423 let eject__o__sig_to_part__o__part_no x1 =
 424   part_no (part_from_sig (Types.pi1 x1))
 425
 426 (** val sig_to_part__o__part_no : Nat.nat Types.sig0 -> Nat.nat **)
 427 let sig_to_part__o__part_no x0 =
 428   part_no (part_from_sig x0)
 429
 430 (** val sig_to_part__o__part_no__o__Z_of_nat : Nat.nat Types.sig0 -> Z.z **)
 431 let sig_to_part__o__part_no__o__Z_of_nat x0 =
 432   part_no__o__Z_of_nat (part_from_sig x0)
 433
 434 (** val sig_to_part__o__part_no__o__inject :
 435     Nat.nat Types.sig0 -> Nat.nat Types.sig0 **)
 436 let sig_to_part__o__part_no__o__inject x1 =
 437   part_no__o__inject (part_from_sig x1)
 438
 439 (** val sig_to_part__o__inject : Nat.nat Types.sig0 -> part Types.sig0 **)
 440 let sig_to_part__o__inject x1 =
 441   part_from_sig x1
 442
 443 (** val dpi1__o__part_no__o__inject__o__sig_to_part :
 444     (part, 'a1) Types.dPair -> part **)
 445 let dpi1__o__part_no__o__inject__o__sig_to_part x1 =
 446   part_from_sig (dpi1__o__part_no__o__inject x1)
 447
 448 (** val eject__o__part_no__o__inject__o__sig_to_part :
 449     part Types.sig0 -> part **)
 450 let eject__o__part_no__o__inject__o__sig_to_part x1 =
 451   part_from_sig (eject__o__part_no__o__inject x1)
 452
 453 (** val inject__o__sig_to_part : Nat.nat -> part **)
 454 let inject__o__sig_to_part x0 =
 455   part_from_sig x0
 456
 457 (** val part_no__o__inject__o__sig_to_part : part -> part **)
 458 let part_no__o__inject__o__sig_to_part x0 =
 459   part_from_sig (part_no__o__inject x0)
 460
 461 (** val dpi1__o__sig_to_part :
 462     (Nat.nat Types.sig0, 'a1) Types.dPair -> part **)
 463 let dpi1__o__sig_to_part x1 =
 464   part_from_sig x1.Types.dpi1
 465
 466 (** val eject__o__sig_to_part : Nat.nat Types.sig0 Types.sig0 -> part **)
 467 let eject__o__sig_to_part x1 =
 468   part_from_sig (Types.pi1 x1)
 469
 470 type beval =
 471 | BVundef
 472 | BVnonzero
 473 | BVXor of Pointers.pointer Types.option * Pointers.pointer Types.option
 474    * part
 475 | BVByte of BitVector.byte
 476 | BVnull of part
 477 | BVptr of Pointers.pointer * part
 478 | BVpc of program_counter * part
 479
 480 (** val beval_rect_Type4 :
 481     'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
 482     Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
 483     -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
 484     -> beval -> 'a1 **)
 485 let rec beval_rect_Type4 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
 486 | BVundef -> h_BVundef
 487 | BVnonzero -> h_BVnonzero
 488 | BVXor (x_6222, x_6221, x_6220) -> h_BVXor x_6222 x_6221 x_6220
 489 | BVByte x_6223 -> h_BVByte x_6223
 490 | BVnull x_6224 -> h_BVnull x_6224
 491 | BVptr (x_6226, x_6225) -> h_BVptr x_6226 x_6225
 492 | BVpc (x_6228, x_6227) -> h_BVpc x_6228 x_6227
 493
 494 (** val beval_rect_Type5 :
 495     'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
 496     Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
 497     -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
 498     -> beval -> 'a1 **)
 499 let rec beval_rect_Type5 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
 500 | BVundef -> h_BVundef
 501 | BVnonzero -> h_BVnonzero
 502 | BVXor (x_6239, x_6238, x_6237) -> h_BVXor x_6239 x_6238 x_6237
 503 | BVByte x_6240 -> h_BVByte x_6240
 504 | BVnull x_6241 -> h_BVnull x_6241
 505 | BVptr (x_6243, x_6242) -> h_BVptr x_6243 x_6242
 506 | BVpc (x_6245, x_6244) -> h_BVpc x_6245 x_6244
 507
 508 (** val beval_rect_Type3 :
 509     'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
 510     Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
 511     -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
 512     -> beval -> 'a1 **)
 513 let rec beval_rect_Type3 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
 514 | BVundef -> h_BVundef
 515 | BVnonzero -> h_BVnonzero
 516 | BVXor (x_6256, x_6255, x_6254) -> h_BVXor x_6256 x_6255 x_6254
 517 | BVByte x_6257 -> h_BVByte x_6257
 518 | BVnull x_6258 -> h_BVnull x_6258
 519 | BVptr (x_6260, x_6259) -> h_BVptr x_6260 x_6259
 520 | BVpc (x_6262, x_6261) -> h_BVpc x_6262 x_6261
 521
 522 (** val beval_rect_Type2 :
 523     'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
 524     Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
 525     -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
 526     -> beval -> 'a1 **)
 527 let rec beval_rect_Type2 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
 528 | BVundef -> h_BVundef
 529 | BVnonzero -> h_BVnonzero
 530 | BVXor (x_6273, x_6272, x_6271) -> h_BVXor x_6273 x_6272 x_6271
 531 | BVByte x_6274 -> h_BVByte x_6274
 532 | BVnull x_6275 -> h_BVnull x_6275
 533 | BVptr (x_6277, x_6276) -> h_BVptr x_6277 x_6276
 534 | BVpc (x_6279, x_6278) -> h_BVpc x_6279 x_6278
 535
 536 (** val beval_rect_Type1 :
 537     'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
 538     Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
 539     -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
 540     -> beval -> 'a1 **)
 541 let rec beval_rect_Type1 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
 542 | BVundef -> h_BVundef
 543 | BVnonzero -> h_BVnonzero
 544 | BVXor (x_6290, x_6289, x_6288) -> h_BVXor x_6290 x_6289 x_6288
 545 | BVByte x_6291 -> h_BVByte x_6291
 546 | BVnull x_6292 -> h_BVnull x_6292
 547 | BVptr (x_6294, x_6293) -> h_BVptr x_6294 x_6293
 548 | BVpc (x_6296, x_6295) -> h_BVpc x_6296 x_6295
 549
 550 (** val beval_rect_Type0 :
 551     'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
 552     Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
 553     -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
 554     -> beval -> 'a1 **)
 555 let rec beval_rect_Type0 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
 556 | BVundef -> h_BVundef
 557 | BVnonzero -> h_BVnonzero
 558 | BVXor (x_6307, x_6306, x_6305) -> h_BVXor x_6307 x_6306 x_6305
 559 | BVByte x_6308 -> h_BVByte x_6308
 560 | BVnull x_6309 -> h_BVnull x_6309
 561 | BVptr (x_6311, x_6310) -> h_BVptr x_6311 x_6310
 562 | BVpc (x_6313, x_6312) -> h_BVpc x_6313 x_6312
 563
 564 (** val beval_inv_rect_Type4 :
 565     beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
 566     Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
 567     __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
 568     'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1 **)
 569 let beval_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 =
 570   let hcut = beval_rect_Type4 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __
 571
 572 (** val beval_inv_rect_Type3 :
 573     beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
 574     Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
 575     __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
 576     'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1 **)
 577 let beval_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 =
 578   let hcut = beval_rect_Type3 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __
 579
 580 (** val beval_inv_rect_Type2 :
 581     beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
 582     Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
 583     __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
 584     'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1 **)
 585 let beval_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 =
 586   let hcut = beval_rect_Type2 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __
 587
 588 (** val beval_inv_rect_Type1 :
 589     beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
 590     Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
 591     __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
 592     'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1 **)
 593 let beval_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 =
 594   let hcut = beval_rect_Type1 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __
 595
 596 (** val beval_inv_rect_Type0 :
 597     beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
 598     Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
 599     __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
 600     'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1 **)
 601 let beval_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 =
 602   let hcut = beval_rect_Type0 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __
 603
 604 (** val beval_discr : beval -> beval -> __ **)
 605 let beval_discr x y =
 606   Logic.eq_rect_Type2 x
 607     (match x with
 608      | BVundef -> Obj.magic (fun _ dH -> dH)
 609      | BVnonzero -> Obj.magic (fun _ dH -> dH)
 610      | BVXor (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
 611      | BVByte a0 -> Obj.magic (fun _ dH -> dH __)
 612      | BVnull a0 -> Obj.magic (fun _ dH -> dH __)
 613      | BVptr (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 614      | BVpc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
 615
 616 (** val beval_jmdiscr : beval -> beval -> __ **)
 617 let beval_jmdiscr x y =
 618   Logic.eq_rect_Type2 x
 619     (match x with
 620      | BVundef -> Obj.magic (fun _ dH -> dH)
 621      | BVnonzero -> Obj.magic (fun _ dH -> dH)
 622      | BVXor (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
 623      | BVByte a0 -> Obj.magic (fun _ dH -> dH __)
 624      | BVnull a0 -> Obj.magic (fun _ dH -> dH __)
 625      | BVptr (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 626      | BVpc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
 627
 628 (** val eq_bv_suffix :
 629     Nat.nat -> Nat.nat -> Nat.nat -> BitVector.bitVector ->
 630     BitVector.bitVector -> Bool.bool **)
 631 let eq_bv_suffix n m p v1 v2 =
 632   let b1 = (Vector.vsplit n p v1).Types.snd in
 633   let b2 = (Vector.vsplit m p v2).Types.snd in BitVector.eq_bv p b1 b2
 634
 635 (** val pointer_of_bevals :
 636     beval List.list -> Pointers.pointer Errors.res **)
 637 let pointer_of_bevals = function
 638 | List.Nil ->
 639   Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
 640     List.Nil))
 641 | List.Cons (bv1, tl) ->
 642   (match tl with
 643    | List.Nil ->
 644      Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
 645        List.Nil))
 646    | List.Cons (bv2, tl') ->
 647      (match tl' with
 648       | List.Nil ->
 649         (match bv1 with
 650          | BVundef ->
 651            Errors.Error (List.Cons ((Errors.MSG
 652              ErrorMessages.CorruptedPointer), List.Nil))
 653          | BVnonzero ->
 654            Errors.Error (List.Cons ((Errors.MSG
 655              ErrorMessages.CorruptedPointer), List.Nil))
 656          | BVXor (x, x0, x1) ->
 657            Errors.Error (List.Cons ((Errors.MSG
 658              ErrorMessages.CorruptedPointer), List.Nil))
 659          | BVByte x ->
 660            Errors.Error (List.Cons ((Errors.MSG
 661              ErrorMessages.CorruptedPointer), List.Nil))
 662          | BVnull x ->
 663            Errors.Error (List.Cons ((Errors.MSG
 664              ErrorMessages.CorruptedPointer), List.Nil))
 665          | BVptr (ptr1, p1) ->
 666            (match bv2 with
 667             | BVundef ->
 668               Errors.Error (List.Cons ((Errors.MSG
 669                 ErrorMessages.CorruptedPointer), List.Nil))
 670             | BVnonzero ->
 671               Errors.Error (List.Cons ((Errors.MSG
 672                 ErrorMessages.CorruptedPointer), List.Nil))
 673             | BVXor (x, x0, x1) ->
 674               Errors.Error (List.Cons ((Errors.MSG
 675                 ErrorMessages.CorruptedPointer), List.Nil))
 676             | BVByte x ->
 677               Errors.Error (List.Cons ((Errors.MSG
 678                 ErrorMessages.CorruptedPointer), List.Nil))
 679             | BVnull x ->
 680               Errors.Error (List.Cons ((Errors.MSG
 681                 ErrorMessages.CorruptedPointer), List.Nil))
 682             | BVptr (ptr2, p2) ->
 683               (match Bool.andb
 684                        (Bool.andb
 685                          (Bool.andb (Nat.eqb (part_no p1) Nat.O)
 686                            (Nat.eqb (part_no p2) (Nat.S Nat.O)))
 687                          (Pointers.eq_block ptr1.Pointers.pblock
 688                            ptr2.Pointers.pblock))
 689                        (eq_bv_suffix (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 690                          (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S
 691                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 692                          Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 693                          (Nat.S (Nat.S (Nat.S Nat.O))))))))
 694                          (Pointers.offv ptr1.Pointers.poff)
 695                          (Pointers.offv ptr2.Pointers.poff)) with
 696                | Bool.True ->
 697                  Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) ptr2)
 698                | Bool.False ->
 699                  Errors.Error (List.Cons ((Errors.MSG
 700                    ErrorMessages.CorruptedPointer), List.Nil)))
 701             | BVpc (x, x0) ->
 702               Errors.Error (List.Cons ((Errors.MSG
 703                 ErrorMessages.CorruptedPointer), List.Nil)))
 704          | BVpc (x, x0) ->
 705            Errors.Error (List.Cons ((Errors.MSG
 706              ErrorMessages.CorruptedPointer), List.Nil)))
 707       | List.Cons (x, x0) ->
 708         Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
 709           List.Nil))))
 710
 711 (** val pc_of_bevals : beval List.list -> program_counter Errors.res **)
 712 let pc_of_bevals = function
 713 | List.Nil ->
 714   Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
 715     List.Nil))
 716 | List.Cons (bv1, tl) ->
 717   (match tl with
 718    | List.Nil ->
 719      Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
 720        List.Nil))
 721    | List.Cons (bv2, tl') ->
 722      (match tl' with
 723       | List.Nil ->
 724         (match bv1 with
 725          | BVundef ->
 726            Errors.Error (List.Cons ((Errors.MSG
 727              ErrorMessages.CorruptedPointer), List.Nil))
 728          | BVnonzero ->
 729            Errors.Error (List.Cons ((Errors.MSG
 730              ErrorMessages.CorruptedPointer), List.Nil))
 731          | BVXor (x, x0, x1) ->
 732            Errors.Error (List.Cons ((Errors.MSG
 733              ErrorMessages.CorruptedPointer), List.Nil))
 734          | BVByte x ->
 735            Errors.Error (List.Cons ((Errors.MSG
 736              ErrorMessages.CorruptedPointer), List.Nil))
 737          | BVnull x ->
 738            Errors.Error (List.Cons ((Errors.MSG
 739              ErrorMessages.CorruptedPointer), List.Nil))
 740          | BVptr (x, x0) ->
 741            Errors.Error (List.Cons ((Errors.MSG
 742              ErrorMessages.CorruptedPointer), List.Nil))
 743          | BVpc (ptr1, p1) ->
 744            (match bv2 with
 745             | BVundef ->
 746               Errors.Error (List.Cons ((Errors.MSG
 747                 ErrorMessages.CorruptedPointer), List.Nil))
 748             | BVnonzero ->
 749               Errors.Error (List.Cons ((Errors.MSG
 750                 ErrorMessages.CorruptedPointer), List.Nil))
 751             | BVXor (x, x0, x1) ->
 752               Errors.Error (List.Cons ((Errors.MSG
 753                 ErrorMessages.CorruptedPointer), List.Nil))
 754             | BVByte x ->
 755               Errors.Error (List.Cons ((Errors.MSG
 756                 ErrorMessages.CorruptedPointer), List.Nil))
 757             | BVnull x ->
 758               Errors.Error (List.Cons ((Errors.MSG
 759                 ErrorMessages.CorruptedPointer), List.Nil))
 760             | BVptr (x, x0) ->
 761               Errors.Error (List.Cons ((Errors.MSG
 762                 ErrorMessages.CorruptedPointer), List.Nil))
 763             | BVpc (ptr2, p2) ->
 764               (match Bool.andb
 765                        (Bool.andb (Nat.eqb (part_no p1) Nat.O)
 766                          (Nat.eqb (part_no p2) (Nat.S Nat.O)))
 767                        (eq_program_counter ptr1 ptr2) with
 768                | Bool.True ->
 769                  Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) ptr2)
 770                | Bool.False ->
 771                  Errors.Error (List.Cons ((Errors.MSG
 772                    ErrorMessages.CorruptedPointer), List.Nil)))))
 773       | List.Cons (x, x0) ->
 774         Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
 775           List.Nil))))
 776
 777 (** val bevals_of_pointer : Pointers.pointer -> beval List.list **)
 778 let bevals_of_pointer p =
 779   List.map (fun n_sig -> BVptr (p, (part_from_sig n_sig)))
 780     (Lists.range_strong AST.size_pointer)
 781
 782 (** val bevals_of_pc : program_counter -> beval List.list **)
 783 let bevals_of_pc p =
 784   List.map (fun n_sig -> BVpc (p, (part_from_sig n_sig)))
 785     (Lists.range_strong AST.size_pointer)
 786
 787 (** val list_to_pair : 'a1 List.list -> ('a1, 'a1) Types.prod **)
 788 let list_to_pair l =
 789   (match l with
 790    | List.Nil ->
 791      (fun _ -> Obj.magic Nat.nat_discr Nat.O (Nat.S (Nat.S Nat.O)) __)
 792    | List.Cons (a, tl) ->
 793      (match tl with
 794       | List.Nil ->
 795         (fun _ ->
 796           Obj.magic Nat.nat_discr (Nat.S Nat.O) (Nat.S (Nat.S Nat.O)) __
 797             (fun _ -> Obj.magic Nat.nat_discr Nat.O (Nat.S Nat.O) __))
 798       | List.Cons (b, tl') ->
 799         (match tl' with
 800          | List.Nil -> (fun _ -> { Types.fst = a; Types.snd = b })
 801          | List.Cons (c, tl'') ->
 802            (fun _ ->
 803              Obj.magic Nat.nat_discr (Nat.S (Nat.S (Nat.S
 804                (List.length tl'')))) (Nat.S (Nat.S Nat.O)) __ (fun _ ->
 805                Obj.magic Nat.nat_discr (Nat.S (Nat.S (List.length tl'')))
 806                  (Nat.S Nat.O) __ (fun _ ->
 807                  Obj.magic Nat.nat_discr (Nat.S (List.length tl'')) Nat.O __))))))
 808     __
 809
 810 (** val beval_pair_of_pointer :
 811     Pointers.pointer -> (beval, beval) Types.prod **)
 812 let beval_pair_of_pointer p =
 813   list_to_pair (bevals_of_pointer p)
 814
 815 (** val beval_pair_of_pc : program_counter -> (beval, beval) Types.prod **)
 816 let beval_pair_of_pc p =
 817   list_to_pair (bevals_of_pc p)
 818
 819 (** val bool_of_beval : beval -> Bool.bool Errors.res **)
 820 let bool_of_beval = function
 821 | BVundef ->
 822   Errors.Error (List.Cons ((Errors.MSG ErrorMessages.ValueNotABoolean),
 823     List.Nil))
 824 | BVnonzero -> Errors.OK Bool.True
 825 | BVXor (x, x0, x1) ->
 826   Errors.Error (List.Cons ((Errors.MSG ErrorMessages.ValueNotABoolean),
 827     List.Nil))
 828 | BVByte b ->
 829   Errors.OK
 830     (Bool.notb
 831       (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 832         (Nat.S Nat.O))))))))
 833         (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 834           (Nat.S Nat.O))))))))) b))
 835 | BVnull x -> Errors.OK Bool.False
 836 | BVptr (x, x0) -> Errors.OK Bool.True
 837 | BVpc (x, x0) ->
 838   Errors.Error (List.Cons ((Errors.MSG ErrorMessages.ValueNotABoolean),
 839     List.Nil))
 840
 841 (** val byte_of_val :
 842     ErrorMessages.errorMessage -> beval -> BitVector.byte Errors.res **)
 843 let byte_of_val err = function
 844 | BVundef -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
 845 | BVnonzero -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
 846 | BVXor (x, x0, x1) -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
 847 | BVByte b0 -> Errors.OK b0
 848 | BVnull x -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
 849 | BVptr (x, x0) -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
 850 | BVpc (x, x0) -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
 851
 852 (** val word_of_list_beval : beval List.list -> Integers.int Errors.res **)
 853 let word_of_list_beval l =
 854   let first_byte = fun l0 ->
 855     match l0 with
 856     | List.Nil ->
 857       Obj.magic (Errors.Error (List.Cons ((Errors.MSG
 858         ErrorMessages.NotAnInt32Val), List.Nil)))
 859     | List.Cons (hd, tl) ->
 860       Monad.m_bind0 (Monad.max_def Errors.res0)
 861         (Obj.magic (byte_of_val ErrorMessages.NotAnInt32Val hd)) (fun b ->
 862         Obj.magic (Errors.OK { Types.fst = b; Types.snd = tl }))
 863   in
 864   Obj.magic
 865     (Monad.m_bind2 (Monad.max_def Errors.res0) (first_byte l) (fun b1 l0 ->
 866       Monad.m_bind2 (Monad.max_def Errors.res0) (first_byte l0) (fun b2 l1 ->
 867         Monad.m_bind2 (Monad.max_def Errors.res0) (first_byte l1)
 868           (fun b3 l2 ->
 869           Monad.m_bind2 (Monad.max_def Errors.res0) (first_byte l2)
 870             (fun b4 l3 ->
 871             match l3 with
 872             | List.Nil ->
 873               Obj.magic (Errors.OK
 874                 (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 875                   (Nat.S (Nat.S Nat.O))))))))
 876                   (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 877                     (Nat.S Nat.O))))))))
 878                     (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 879                       (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
 880                       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) b4
 881                   (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 882                     (Nat.S (Nat.S Nat.O))))))))
 883                     (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 884                       (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
 885                       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) b3
 886                     (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 887                       (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
 888                       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) b2 b1))))
 889             | List.Cons (x, x0) ->
 890               Obj.magic (Errors.Error (List.Cons ((Errors.MSG
 891                 ErrorMessages.NotAnInt32Val), List.Nil))))))))
 892
 893 type add_or_sub =
 894 | Do_add
 895 | Do_sub
 896
 897 (** val add_or_sub_rect_Type4 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
 898 let rec add_or_sub_rect_Type4 h_do_add h_do_sub = function
 899 | Do_add -> h_do_add
 900 | Do_sub -> h_do_sub
 901
 902 (** val add_or_sub_rect_Type5 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
 903 let rec add_or_sub_rect_Type5 h_do_add h_do_sub = function
 904 | Do_add -> h_do_add
 905 | Do_sub -> h_do_sub
 906
 907 (** val add_or_sub_rect_Type3 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
 908 let rec add_or_sub_rect_Type3 h_do_add h_do_sub = function
 909 | Do_add -> h_do_add
 910 | Do_sub -> h_do_sub
 911
 912 (** val add_or_sub_rect_Type2 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
 913 let rec add_or_sub_rect_Type2 h_do_add h_do_sub = function
 914 | Do_add -> h_do_add
 915 | Do_sub -> h_do_sub
 916
 917 (** val add_or_sub_rect_Type1 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
 918 let rec add_or_sub_rect_Type1 h_do_add h_do_sub = function
 919 | Do_add -> h_do_add
 920 | Do_sub -> h_do_sub
 921
 922 (** val add_or_sub_rect_Type0 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
 923 let rec add_or_sub_rect_Type0 h_do_add h_do_sub = function
 924 | Do_add -> h_do_add
 925 | Do_sub -> h_do_sub
 926
 927 (** val add_or_sub_inv_rect_Type4 :
 928     add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 929 let add_or_sub_inv_rect_Type4 hterm h1 h2 =
 930   let hcut = add_or_sub_rect_Type4 h1 h2 hterm in hcut __
 931
 932 (** val add_or_sub_inv_rect_Type3 :
 933     add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 934 let add_or_sub_inv_rect_Type3 hterm h1 h2 =
 935   let hcut = add_or_sub_rect_Type3 h1 h2 hterm in hcut __
 936
 937 (** val add_or_sub_inv_rect_Type2 :
 938     add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 939 let add_or_sub_inv_rect_Type2 hterm h1 h2 =
 940   let hcut = add_or_sub_rect_Type2 h1 h2 hterm in hcut __
 941
 942 (** val add_or_sub_inv_rect_Type1 :
 943     add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 944 let add_or_sub_inv_rect_Type1 hterm h1 h2 =
 945   let hcut = add_or_sub_rect_Type1 h1 h2 hterm in hcut __
 946
 947 (** val add_or_sub_inv_rect_Type0 :
 948     add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 949 let add_or_sub_inv_rect_Type0 hterm h1 h2 =
 950   let hcut = add_or_sub_rect_Type0 h1 h2 hterm in hcut __
 951
 952 (** val add_or_sub_discr : add_or_sub -> add_or_sub -> __ **)
 953 let add_or_sub_discr x y =
 954   Logic.eq_rect_Type2 x
 955     (match x with
 956      | Do_add -> Obj.magic (fun _ dH -> dH)
 957      | Do_sub -> Obj.magic (fun _ dH -> dH)) y
 958
 959 (** val add_or_sub_jmdiscr : add_or_sub -> add_or_sub -> __ **)
 960 let add_or_sub_jmdiscr x y =
 961   Logic.eq_rect_Type2 x
 962     (match x with
 963      | Do_add -> Obj.magic (fun _ dH -> dH)
 964      | Do_sub -> Obj.magic (fun _ dH -> dH)) y
 965
 966 (** val eq_add_or_sub : add_or_sub -> add_or_sub -> Bool.bool **)
 967 let eq_add_or_sub x y =
 968   match x with
 969   | Do_add ->
 970     (match y with
 971      | Do_add -> Bool.True
 972      | Do_sub -> Bool.False)
 973   | Do_sub ->
 974     (match y with
 975      | Do_add -> Bool.False
 976      | Do_sub -> Bool.True)
 977
 978 type bebit =
 979 | BBbit of Bool.bool
 980 | BBundef
 981 | BBptrcarry of add_or_sub * Pointers.pointer * part * BitVector.bitVector
 982
 983 (** val bebit_rect_Type4 :
 984     (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
 985     BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
 986 let rec bebit_rect_Type4 h_BBbit h_BBundef h_BBptrcarry = function
 987 | BBbit x_6471 -> h_BBbit x_6471
 988 | BBundef -> h_BBundef
 989 | BBptrcarry (x_6474, x_6473, p, x_6472) ->
 990   h_BBptrcarry x_6474 x_6473 p x_6472
 991
 992 (** val bebit_rect_Type5 :
 993     (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
 994     BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
 995 let rec bebit_rect_Type5 h_BBbit h_BBundef h_BBptrcarry = function
 996 | BBbit x_6479 -> h_BBbit x_6479
 997 | BBundef -> h_BBundef
 998 | BBptrcarry (x_6482, x_6481, p, x_6480) ->
 999   h_BBptrcarry x_6482 x_6481 p x_6480
1000
1001 (** val bebit_rect_Type3 :
1002     (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
1003     BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
1004 let rec bebit_rect_Type3 h_BBbit h_BBundef h_BBptrcarry = function
1005 | BBbit x_6487 -> h_BBbit x_6487
1006 | BBundef -> h_BBundef
1007 | BBptrcarry (x_6490, x_6489, p, x_6488) ->
1008   h_BBptrcarry x_6490 x_6489 p x_6488
1009
1010 (** val bebit_rect_Type2 :
1011     (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
1012     BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
1013 let rec bebit_rect_Type2 h_BBbit h_BBundef h_BBptrcarry = function
1014 | BBbit x_6495 -> h_BBbit x_6495
1015 | BBundef -> h_BBundef
1016 | BBptrcarry (x_6498, x_6497, p, x_6496) ->
1017   h_BBptrcarry x_6498 x_6497 p x_6496
1018
1019 (** val bebit_rect_Type1 :
1020     (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
1021     BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
1022 let rec bebit_rect_Type1 h_BBbit h_BBundef h_BBptrcarry = function
1023 | BBbit x_6503 -> h_BBbit x_6503
1024 | BBundef -> h_BBundef
1025 | BBptrcarry (x_6506, x_6505, p, x_6504) ->
1026   h_BBptrcarry x_6506 x_6505 p x_6504
1027
1028 (** val bebit_rect_Type0 :
1029     (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
1030     BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
1031 let rec bebit_rect_Type0 h_BBbit h_BBundef h_BBptrcarry = function
1032 | BBbit x_6511 -> h_BBbit x_6511
1033 | BBundef -> h_BBundef
1034 | BBptrcarry (x_6514, x_6513, p, x_6512) ->
1035   h_BBptrcarry x_6514 x_6513 p x_6512
1036
1037 (** val bebit_inv_rect_Type4 :
1038     bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
1039     Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
1040 let bebit_inv_rect_Type4 hterm h1 h2 h3 =
1041   let hcut = bebit_rect_Type4 h1 h2 h3 hterm in hcut __
1042
1043 (** val bebit_inv_rect_Type3 :
1044     bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
1045     Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
1046 let bebit_inv_rect_Type3 hterm h1 h2 h3 =
1047   let hcut = bebit_rect_Type3 h1 h2 h3 hterm in hcut __
1048
1049 (** val bebit_inv_rect_Type2 :
1050     bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
1051     Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
1052 let bebit_inv_rect_Type2 hterm h1 h2 h3 =
1053   let hcut = bebit_rect_Type2 h1 h2 h3 hterm in hcut __
1054
1055 (** val bebit_inv_rect_Type1 :
1056     bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
1057     Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
1058 let bebit_inv_rect_Type1 hterm h1 h2 h3 =
1059   let hcut = bebit_rect_Type1 h1 h2 h3 hterm in hcut __
1060
1061 (** val bebit_inv_rect_Type0 :
1062     bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
1063     Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
1064 let bebit_inv_rect_Type0 hterm h1 h2 h3 =
1065   let hcut = bebit_rect_Type0 h1 h2 h3 hterm in hcut __
1066
1067 (** val bebit_discr : bebit -> bebit -> __ **)
1068 let bebit_discr x y =
1069   Logic.eq_rect_Type2 x
1070     (match x with
1071      | BBbit a0 -> Obj.magic (fun _ dH -> dH __)
1072      | BBundef -> Obj.magic (fun _ dH -> dH)
1073      | BBptrcarry (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __))
1074     y
1075
1076 (** val bebit_jmdiscr : bebit -> bebit -> __ **)
1077 let bebit_jmdiscr x y =
1078   Logic.eq_rect_Type2 x
1079     (match x with
1080      | BBbit a0 -> Obj.magic (fun _ dH -> dH __)
1081      | BBundef -> Obj.magic (fun _ dH -> dH)
1082      | BBptrcarry (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __))
1083     y
1084
1085 (** val bit_of_val :
1086     ErrorMessages.errorMessage -> bebit -> BitVector.bit Errors.res **)
1087 let bit_of_val err = function
1088 | BBbit b0 -> Errors.OK b0
1089 | BBundef -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
1090 | BBptrcarry (x, x0, x1, x2) ->
1091   Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
1092