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 ->
92 val program_counter_rect_Type5 :
93 (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
96 val program_counter_rect_Type3 :
97 (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
100 val program_counter_rect_Type2 :
101 (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
104 val program_counter_rect_Type1 :
105 (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
108 val program_counter_rect_Type0 :
109 (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
112 val pc_block : program_counter -> Pointers.block Types.sig0
114 val pc_offset : program_counter -> Positive.pos
116 val program_counter_inv_rect_Type4 :
117 program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ -> 'a1)
120 val program_counter_inv_rect_Type3 :
121 program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ -> 'a1)
124 val program_counter_inv_rect_Type2 :
125 program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ -> 'a1)
128 val program_counter_inv_rect_Type1 :
129 program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ -> 'a1)
132 val program_counter_inv_rect_Type0 :
133 program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ -> 'a1)
136 val program_counter_discr : program_counter -> program_counter -> __
138 val program_counter_jmdiscr : program_counter -> program_counter -> __
140 val eq_program_counter : program_counter -> program_counter -> Bool.bool
142 val bitvector_from_pos : Nat.nat -> Positive.pos -> BitVector.bitVector
144 val pos_from_bitvector : Nat.nat -> BitVector.bitVector -> Positive.pos
146 val cpointer_of_pc : program_counter -> cpointer Types.option
150 (* singleton inductive, whose constructor was mk_part *)
152 val part_rect_Type4 : (Nat.nat -> __ -> 'a1) -> part -> 'a1
154 val part_rect_Type5 : (Nat.nat -> __ -> 'a1) -> part -> 'a1
156 val part_rect_Type3 : (Nat.nat -> __ -> 'a1) -> part -> 'a1
158 val part_rect_Type2 : (Nat.nat -> __ -> 'a1) -> part -> 'a1
160 val part_rect_Type1 : (Nat.nat -> __ -> 'a1) -> part -> 'a1
162 val part_rect_Type0 : (Nat.nat -> __ -> 'a1) -> part -> 'a1
164 val part_no : part -> Nat.nat
166 val part_inv_rect_Type4 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1
168 val part_inv_rect_Type3 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1
170 val part_inv_rect_Type2 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1
172 val part_inv_rect_Type1 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1
174 val part_inv_rect_Type0 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1
176 val part_discr : part -> part -> __
178 val part_jmdiscr : part -> part -> __
180 val dpi1__o__part_no__o__inject :
181 (part, 'a1) Types.dPair -> Nat.nat Types.sig0
183 val dpi1__o__part_no__o__Z_of_nat : (part, 'a1) Types.dPair -> Z.z
185 val eject__o__part_no__o__inject : part Types.sig0 -> Nat.nat Types.sig0
187 val eject__o__part_no__o__Z_of_nat : part Types.sig0 -> Z.z
189 val part_no__o__Z_of_nat : part -> Z.z
191 val part_no__o__inject : part -> Nat.nat Types.sig0
193 val dpi1__o__part_no : (part, 'a1) Types.dPair -> Nat.nat
195 val eject__o__part_no : part Types.sig0 -> Nat.nat
197 val part_from_sig : Nat.nat Types.sig0 -> part
199 val dpi1__o__part_no__o__inject__o__sig_to_part__o__inject :
200 (part, 'a1) Types.dPair -> part Types.sig0
202 val dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no__o__inject :
203 (part, 'a1) Types.dPair -> Nat.nat Types.sig0
205 val dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat :
206 (part, 'a1) Types.dPair -> Z.z
208 val dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no :
209 (part, 'a1) Types.dPair -> Nat.nat
211 val eject__o__part_no__o__inject__o__sig_to_part__o__inject :
212 part Types.sig0 -> part Types.sig0
214 val eject__o__part_no__o__inject__o__sig_to_part__o__part_no__o__inject :
215 part Types.sig0 -> Nat.nat Types.sig0
217 val eject__o__part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat :
218 part Types.sig0 -> Z.z
220 val eject__o__part_no__o__inject__o__sig_to_part__o__part_no :
221 part Types.sig0 -> Nat.nat
223 val inject__o__sig_to_part__o__inject : Nat.nat -> part Types.sig0
225 val inject__o__sig_to_part__o__part_no__o__inject :
226 Nat.nat -> Nat.nat Types.sig0
228 val inject__o__sig_to_part__o__part_no__o__Z_of_nat : Nat.nat -> Z.z
230 val inject__o__sig_to_part__o__part_no : Nat.nat -> Nat.nat
232 val part_no__o__inject__o__sig_to_part__o__inject : part -> part Types.sig0
234 val part_no__o__inject__o__sig_to_part__o__part_no__o__inject :
235 part -> Nat.nat Types.sig0
237 val part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat : part -> Z.z
239 val part_no__o__inject__o__sig_to_part__o__part_no : part -> Nat.nat
241 val dpi1__o__sig_to_part__o__inject :
242 (Nat.nat Types.sig0, 'a1) Types.dPair -> part Types.sig0
244 val dpi1__o__sig_to_part__o__part_no__o__inject :
245 (Nat.nat Types.sig0, 'a1) Types.dPair -> Nat.nat Types.sig0
247 val dpi1__o__sig_to_part__o__part_no__o__Z_of_nat :
248 (Nat.nat Types.sig0, 'a1) Types.dPair -> Z.z
250 val dpi1__o__sig_to_part__o__part_no :
251 (Nat.nat Types.sig0, 'a1) Types.dPair -> Nat.nat
253 val eject__o__sig_to_part__o__inject :
254 Nat.nat Types.sig0 Types.sig0 -> part Types.sig0
256 val eject__o__sig_to_part__o__part_no__o__inject :
257 Nat.nat Types.sig0 Types.sig0 -> Nat.nat Types.sig0
259 val eject__o__sig_to_part__o__part_no__o__Z_of_nat :
260 Nat.nat Types.sig0 Types.sig0 -> Z.z
262 val eject__o__sig_to_part__o__part_no :
263 Nat.nat Types.sig0 Types.sig0 -> Nat.nat
265 val sig_to_part__o__part_no : Nat.nat Types.sig0 -> Nat.nat
267 val sig_to_part__o__part_no__o__Z_of_nat : Nat.nat Types.sig0 -> Z.z
269 val sig_to_part__o__part_no__o__inject :
270 Nat.nat Types.sig0 -> Nat.nat Types.sig0
272 val sig_to_part__o__inject : Nat.nat Types.sig0 -> part Types.sig0
274 val dpi1__o__part_no__o__inject__o__sig_to_part :
275 (part, 'a1) Types.dPair -> part
277 val eject__o__part_no__o__inject__o__sig_to_part : part Types.sig0 -> part
279 val inject__o__sig_to_part : Nat.nat -> part
281 val part_no__o__inject__o__sig_to_part : part -> part
283 val dpi1__o__sig_to_part : (Nat.nat Types.sig0, 'a1) Types.dPair -> part
285 val eject__o__sig_to_part : Nat.nat Types.sig0 Types.sig0 -> part
290 | BVXor of Pointers.pointer Types.option * Pointers.pointer Types.option
292 | BVByte of BitVector.byte
294 | BVptr of Pointers.pointer * part
295 | BVpc of program_counter * part
297 val beval_rect_Type4 :
298 'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
299 Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
300 (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
303 val beval_rect_Type5 :
304 'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
305 Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
306 (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
309 val beval_rect_Type3 :
310 'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
311 Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
312 (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
315 val beval_rect_Type2 :
316 'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
317 Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
318 (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
321 val beval_rect_Type1 :
322 'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
323 Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
324 (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
327 val beval_rect_Type0 :
328 'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
329 Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
330 (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
333 val beval_inv_rect_Type4 :
334 beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
335 Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
336 __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
337 'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1
339 val beval_inv_rect_Type3 :
340 beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
341 Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
342 __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
343 'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1
345 val beval_inv_rect_Type2 :
346 beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
347 Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
348 __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
349 'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1
351 val beval_inv_rect_Type1 :
352 beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
353 Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
354 __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
355 'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1
357 val beval_inv_rect_Type0 :
358 beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
359 Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
360 __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
361 'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1
363 val beval_discr : beval -> beval -> __
365 val beval_jmdiscr : beval -> beval -> __
368 Nat.nat -> Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
371 val pointer_of_bevals : beval List.list -> Pointers.pointer Errors.res
373 val pc_of_bevals : beval List.list -> program_counter Errors.res
375 val bevals_of_pointer : Pointers.pointer -> beval List.list
377 val bevals_of_pc : program_counter -> beval List.list
379 val list_to_pair : 'a1 List.list -> ('a1, 'a1) Types.prod
381 val beval_pair_of_pointer : Pointers.pointer -> (beval, beval) Types.prod
383 val beval_pair_of_pc : program_counter -> (beval, beval) Types.prod
385 val bool_of_beval : beval -> Bool.bool Errors.res
388 ErrorMessages.errorMessage -> beval -> BitVector.byte Errors.res
390 val word_of_list_beval : beval List.list -> Integers.int Errors.res
396 val add_or_sub_rect_Type4 : 'a1 -> 'a1 -> add_or_sub -> 'a1
398 val add_or_sub_rect_Type5 : 'a1 -> 'a1 -> add_or_sub -> 'a1
400 val add_or_sub_rect_Type3 : 'a1 -> 'a1 -> add_or_sub -> 'a1
402 val add_or_sub_rect_Type2 : 'a1 -> 'a1 -> add_or_sub -> 'a1
404 val add_or_sub_rect_Type1 : 'a1 -> 'a1 -> add_or_sub -> 'a1
406 val add_or_sub_rect_Type0 : 'a1 -> 'a1 -> add_or_sub -> 'a1
408 val add_or_sub_inv_rect_Type4 :
409 add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
411 val add_or_sub_inv_rect_Type3 :
412 add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
414 val add_or_sub_inv_rect_Type2 :
415 add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
417 val add_or_sub_inv_rect_Type1 :
418 add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
420 val add_or_sub_inv_rect_Type0 :
421 add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
423 val add_or_sub_discr : add_or_sub -> add_or_sub -> __
425 val add_or_sub_jmdiscr : add_or_sub -> add_or_sub -> __
427 val eq_add_or_sub : add_or_sub -> add_or_sub -> Bool.bool
432 | BBptrcarry of add_or_sub * Pointers.pointer * part * BitVector.bitVector
434 val bebit_rect_Type4 :
435 (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
436 BitVector.bitVector -> 'a1) -> bebit -> 'a1
438 val bebit_rect_Type5 :
439 (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
440 BitVector.bitVector -> 'a1) -> bebit -> 'a1
442 val bebit_rect_Type3 :
443 (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
444 BitVector.bitVector -> 'a1) -> bebit -> 'a1
446 val bebit_rect_Type2 :
447 (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
448 BitVector.bitVector -> 'a1) -> bebit -> 'a1
450 val bebit_rect_Type1 :
451 (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
452 BitVector.bitVector -> 'a1) -> bebit -> 'a1
454 val bebit_rect_Type0 :
455 (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
456 BitVector.bitVector -> 'a1) -> bebit -> 'a1
458 val bebit_inv_rect_Type4 :
459 bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
460 Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
462 val bebit_inv_rect_Type3 :
463 bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
464 Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
466 val bebit_inv_rect_Type2 :
467 bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
468 Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
470 val bebit_inv_rect_Type1 :
471 bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
472 Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
474 val bebit_inv_rect_Type0 :
475 bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
476 Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
478 val bebit_discr : bebit -> bebit -> __
480 val bebit_jmdiscr : bebit -> bebit -> __
483 ErrorMessages.errorMessage -> bebit -> BitVector.bit Errors.res