63 open Hints_declaration
81 type cpointer = Pointers.pointer Types.sig0
83 type xpointer = Pointers.pointer Types.sig0
85 type program_counter = { pc_block : Pointers.block Types.sig0;
86 pc_offset : Positive.pos }
88 (** val program_counter_rect_Type4 :
89 (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
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
95 (** val program_counter_rect_Type5 :
96 (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
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
102 (** val program_counter_rect_Type3 :
103 (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
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
109 (** val program_counter_rect_Type2 :
110 (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
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
116 (** val program_counter_rect_Type1 :
117 (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
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
123 (** val program_counter_rect_Type0 :
124 (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
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
130 (** val pc_block : program_counter -> Pointers.block Types.sig0 **)
131 let rec pc_block xxx =
134 (** val pc_offset : program_counter -> Positive.pos **)
135 let rec pc_offset xxx =
138 (** val program_counter_inv_rect_Type4 :
139 program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
141 let program_counter_inv_rect_Type4 hterm h1 =
142 let hcut = program_counter_rect_Type4 h1 hterm in hcut __
144 (** val program_counter_inv_rect_Type3 :
145 program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
147 let program_counter_inv_rect_Type3 hterm h1 =
148 let hcut = program_counter_rect_Type3 h1 hterm in hcut __
150 (** val program_counter_inv_rect_Type2 :
151 program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
153 let program_counter_inv_rect_Type2 hterm h1 =
154 let hcut = program_counter_rect_Type2 h1 hterm in hcut __
156 (** val program_counter_inv_rect_Type1 :
157 program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
159 let program_counter_inv_rect_Type1 hterm h1 =
160 let hcut = program_counter_rect_Type1 h1 hterm in hcut __
162 (** val program_counter_inv_rect_Type0 :
163 program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
165 let program_counter_inv_rect_Type0 hterm h1 =
166 let hcut = program_counter_rect_Type0 h1 hterm in hcut __
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
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
181 (** val eq_program_counter :
182 program_counter -> program_counter -> Bool.bool **)
183 let eq_program_counter pc1 pc2 =
185 (Pointers.eq_block (Types.pi1 pc1.pc_block) (Types.pi1 pc2.pc_block))
186 (Positive.eqb pc1.pc_offset pc2.pc_offset)
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))
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 *))) __
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
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)
214 (* singleton inductive, whose constructor was mk_part *)
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 __
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 __
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 __
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 __
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 __
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 __
240 (** val part_no : part -> Nat.nat **)
241 let rec part_no xxx =
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 __
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 __
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 __
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 __
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 __
264 (** val part_discr : part -> part -> __ **)
266 Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y
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
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
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)
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)
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))
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)
294 (** val part_no__o__inject : part -> Nat.nat Types.sig0 **)
295 let part_no__o__inject x1 =
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
302 (** val eject__o__part_no : part Types.sig0 -> Nat.nat **)
303 let eject__o__part_no x1 =
304 part_no (Types.pi1 x1)
306 (** val part_from_sig : Nat.nat Types.sig0 -> part **)
307 let part_from_sig n_sig =
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)
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))
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))
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))
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)
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))
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))
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))
350 (** val inject__o__sig_to_part__o__inject : Nat.nat -> part Types.sig0 **)
351 let inject__o__sig_to_part__o__inject x0 =
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)
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)
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)
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)
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))
377 (** val part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat :
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))
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))
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
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)
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)
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)
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)
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))
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))
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))
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)
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)
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)
439 (** val sig_to_part__o__inject : Nat.nat Types.sig0 -> part Types.sig0 **)
440 let sig_to_part__o__inject x1 =
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)
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)
453 (** val inject__o__sig_to_part : Nat.nat -> part **)
454 let inject__o__sig_to_part x0 =
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)
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
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)
473 | BVXor of Pointers.pointer Types.option * Pointers.pointer Types.option
475 | BVByte of BitVector.byte
477 | BVptr of Pointers.pointer * part
478 | BVpc of program_counter * part
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)
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
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)
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
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)
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
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)
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
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)
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
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)
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
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 __
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 __
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 __
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 __
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 __
604 (** val beval_discr : beval -> beval -> __ **)
605 let beval_discr x y =
606 Logic.eq_rect_Type2 x
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
616 (** val beval_jmdiscr : beval -> beval -> __ **)
617 let beval_jmdiscr x y =
618 Logic.eq_rect_Type2 x
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
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
635 (** val pointer_of_bevals :
636 beval List.list -> Pointers.pointer Errors.res **)
637 let pointer_of_bevals = function
639 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
641 | List.Cons (bv1, tl) ->
644 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
646 | List.Cons (bv2, tl') ->
651 Errors.Error (List.Cons ((Errors.MSG
652 ErrorMessages.CorruptedPointer), List.Nil))
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))
660 Errors.Error (List.Cons ((Errors.MSG
661 ErrorMessages.CorruptedPointer), List.Nil))
663 Errors.Error (List.Cons ((Errors.MSG
664 ErrorMessages.CorruptedPointer), List.Nil))
665 | BVptr (ptr1, p1) ->
668 Errors.Error (List.Cons ((Errors.MSG
669 ErrorMessages.CorruptedPointer), List.Nil))
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))
677 Errors.Error (List.Cons ((Errors.MSG
678 ErrorMessages.CorruptedPointer), List.Nil))
680 Errors.Error (List.Cons ((Errors.MSG
681 ErrorMessages.CorruptedPointer), List.Nil))
682 | BVptr (ptr2, p2) ->
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
697 Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) ptr2)
699 Errors.Error (List.Cons ((Errors.MSG
700 ErrorMessages.CorruptedPointer), List.Nil)))
702 Errors.Error (List.Cons ((Errors.MSG
703 ErrorMessages.CorruptedPointer), List.Nil)))
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),
711 (** val pc_of_bevals : beval List.list -> program_counter Errors.res **)
712 let pc_of_bevals = function
714 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
716 | List.Cons (bv1, tl) ->
719 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
721 | List.Cons (bv2, tl') ->
726 Errors.Error (List.Cons ((Errors.MSG
727 ErrorMessages.CorruptedPointer), List.Nil))
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))
735 Errors.Error (List.Cons ((Errors.MSG
736 ErrorMessages.CorruptedPointer), List.Nil))
738 Errors.Error (List.Cons ((Errors.MSG
739 ErrorMessages.CorruptedPointer), List.Nil))
741 Errors.Error (List.Cons ((Errors.MSG
742 ErrorMessages.CorruptedPointer), List.Nil))
746 Errors.Error (List.Cons ((Errors.MSG
747 ErrorMessages.CorruptedPointer), List.Nil))
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))
755 Errors.Error (List.Cons ((Errors.MSG
756 ErrorMessages.CorruptedPointer), List.Nil))
758 Errors.Error (List.Cons ((Errors.MSG
759 ErrorMessages.CorruptedPointer), List.Nil))
761 Errors.Error (List.Cons ((Errors.MSG
762 ErrorMessages.CorruptedPointer), List.Nil))
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
769 Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) ptr2)
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),
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)
782 (** val bevals_of_pc : program_counter -> beval List.list **)
784 List.map (fun n_sig -> BVpc (p, (part_from_sig n_sig)))
785 (Lists.range_strong AST.size_pointer)
787 (** val list_to_pair : 'a1 List.list -> ('a1, 'a1) Types.prod **)
791 (fun _ -> Obj.magic Nat.nat_discr Nat.O (Nat.S (Nat.S Nat.O)) __)
792 | List.Cons (a, tl) ->
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') ->
800 | List.Nil -> (fun _ -> { Types.fst = a; Types.snd = b })
801 | List.Cons (c, tl'') ->
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 __))))))
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)
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)
819 (** val bool_of_beval : beval -> Bool.bool Errors.res **)
820 let bool_of_beval = function
822 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.ValueNotABoolean),
824 | BVnonzero -> Errors.OK Bool.True
825 | BVXor (x, x0, x1) ->
826 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.ValueNotABoolean),
831 (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
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
838 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.ValueNotABoolean),
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))
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 ->
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 }))
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)
869 Monad.m_bind2 (Monad.max_def Errors.res0) (first_byte l2)
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
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))))))))
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
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
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
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
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
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
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 __
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 __
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 __
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 __
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 __
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
956 | Do_add -> Obj.magic (fun _ dH -> dH)
957 | Do_sub -> Obj.magic (fun _ dH -> dH)) y
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
963 | Do_add -> Obj.magic (fun _ dH -> dH)
964 | Do_sub -> Obj.magic (fun _ dH -> dH)) y
966 (** val eq_add_or_sub : add_or_sub -> add_or_sub -> Bool.bool **)
967 let eq_add_or_sub x y =
971 | Do_add -> Bool.True
972 | Do_sub -> Bool.False)
975 | Do_add -> Bool.False
976 | Do_sub -> Bool.True)
981 | BBptrcarry of add_or_sub * Pointers.pointer * part * BitVector.bitVector
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
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
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
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
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
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
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 __
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 __
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 __
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 __
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 __
1067 (** val bebit_discr : bebit -> bebit -> __ **)
1068 let bebit_discr x y =
1069 Logic.eq_rect_Type2 x
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 __ __ __ __))
1076 (** val bebit_jmdiscr : bebit -> bebit -> __ **)
1077 let bebit_jmdiscr x y =
1078 Logic.eq_rect_Type2 x
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 __ __ __ __))
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))