83 open Hints_declaration
133 type 'f genv_gen = { ge : 'f AST.fundef Globalenvs.genv_t;
134 stack_sizes : (AST.ident -> Nat.nat Types.option);
136 pc_from_label : (Pointers.block Types.sig0 -> 'f ->
138 ByteValues.program_counter Types.option) }
140 val genv_gen_rect_Type4 :
141 AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
142 (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 ->
143 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) ->
146 val genv_gen_rect_Type5 :
147 AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
148 (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 ->
149 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) ->
152 val genv_gen_rect_Type3 :
153 AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
154 (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 ->
155 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) ->
158 val genv_gen_rect_Type2 :
159 AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
160 (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 ->
161 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) ->
164 val genv_gen_rect_Type1 :
165 AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
166 (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 ->
167 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) ->
170 val genv_gen_rect_Type0 :
171 AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
172 (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 ->
173 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) ->
177 AST.ident List.list -> 'a1 genv_gen -> 'a1 AST.fundef Globalenvs.genv_t
180 AST.ident List.list -> 'a1 genv_gen -> AST.ident -> Nat.nat Types.option
182 val premain : AST.ident List.list -> 'a1 genv_gen -> 'a1
185 AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 -> 'a1 ->
186 Graphs.label -> ByteValues.program_counter Types.option
188 val genv_gen_inv_rect_Type4 :
189 AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t ->
190 __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
191 Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
192 Types.option) -> __ -> 'a2) -> 'a2
194 val genv_gen_inv_rect_Type3 :
195 AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t ->
196 __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
197 Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
198 Types.option) -> __ -> 'a2) -> 'a2
200 val genv_gen_inv_rect_Type2 :
201 AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t ->
202 __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
203 Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
204 Types.option) -> __ -> 'a2) -> 'a2
206 val genv_gen_inv_rect_Type1 :
207 AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t ->
208 __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
209 Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
210 Types.option) -> __ -> 'a2) -> 'a2
212 val genv_gen_inv_rect_Type0 :
213 AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t ->
214 __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
215 Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
216 Types.option) -> __ -> 'a2) -> 'a2
219 AST.ident List.list -> 'a1 genv_gen -> 'a1 genv_gen -> __
221 val genv_gen_jmdiscr :
222 AST.ident List.list -> 'a1 genv_gen -> 'a1 genv_gen -> __
224 val dpi1__o__ge__o__inject :
225 AST.ident List.list -> ('a1 genv_gen, 'a2) Types.dPair -> 'a1 AST.fundef
226 Globalenvs.genv_t Types.sig0
228 val eject__o__ge__o__inject :
229 AST.ident List.list -> 'a1 genv_gen Types.sig0 -> 'a1 AST.fundef
230 Globalenvs.genv_t Types.sig0
233 AST.ident List.list -> 'a1 genv_gen -> 'a1 AST.fundef Globalenvs.genv_t
237 AST.ident List.list -> ('a1 genv_gen, 'a2) Types.dPair -> 'a1 AST.fundef
241 AST.ident List.list -> 'a1 genv_gen Types.sig0 -> 'a1 AST.fundef
244 val pre_main_id : AST.ident
247 AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 ->
248 (AST.ident, 'a1 AST.fundef) Types.prod Errors.res
250 val fetch_internal_function :
251 AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 ->
252 (AST.ident, 'a1) Types.prod Errors.res
254 val code_block_of_block :
255 Pointers.block -> Pointers.block Types.sig0 Types.option
257 val block_of_funct_id :
258 'a1 Globalenvs.genv_t -> PreIdentifiers.identifier -> Pointers.block
259 Types.sig0 Errors.res
261 val gen_pc_from_label :
262 AST.ident List.list -> 'a1 genv_gen -> AST.ident -> Graphs.label ->
263 ByteValues.program_counter Errors.res
265 type genv = Joint.joint_closed_internal_function genv_gen
267 type sem_state_params = { empty_framesT : __;
268 empty_regsT : (ByteValues.xpointer -> __);
269 load_sp : (__ -> ByteValues.xpointer Errors.res);
270 save_sp : (__ -> ByteValues.xpointer -> __) }
272 val sem_state_params_rect_Type4 :
273 (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
274 ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
275 'a1) -> sem_state_params -> 'a1
277 val sem_state_params_rect_Type5 :
278 (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
279 ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
280 'a1) -> sem_state_params -> 'a1
282 val sem_state_params_rect_Type3 :
283 (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
284 ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
285 'a1) -> sem_state_params -> 'a1
287 val sem_state_params_rect_Type2 :
288 (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
289 ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
290 'a1) -> sem_state_params -> 'a1
292 val sem_state_params_rect_Type1 :
293 (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
294 ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
295 'a1) -> sem_state_params -> 'a1
297 val sem_state_params_rect_Type0 :
298 (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
299 ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
300 'a1) -> sem_state_params -> 'a1
304 val empty_framesT : sem_state_params -> __
308 val empty_regsT : sem_state_params -> ByteValues.xpointer -> __
310 val load_sp : sem_state_params -> __ -> ByteValues.xpointer Errors.res
312 val save_sp : sem_state_params -> __ -> ByteValues.xpointer -> __
314 val sem_state_params_inv_rect_Type4 :
315 sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
316 -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
319 val sem_state_params_inv_rect_Type3 :
320 sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
321 -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
324 val sem_state_params_inv_rect_Type2 :
325 sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
326 -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
329 val sem_state_params_inv_rect_Type1 :
330 sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
331 -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
334 val sem_state_params_inv_rect_Type0 :
335 sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
336 -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
339 val sem_state_params_jmdiscr : sem_state_params -> sem_state_params -> __
341 type internal_stack =
343 | One_is of ByteValues.beval
344 | Both_is of ByteValues.beval * ByteValues.beval
346 val internal_stack_rect_Type4 :
347 'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
348 -> 'a1) -> internal_stack -> 'a1
350 val internal_stack_rect_Type5 :
351 'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
352 -> 'a1) -> internal_stack -> 'a1
354 val internal_stack_rect_Type3 :
355 'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
356 -> 'a1) -> internal_stack -> 'a1
358 val internal_stack_rect_Type2 :
359 'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
360 -> 'a1) -> internal_stack -> 'a1
362 val internal_stack_rect_Type1 :
363 'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
364 -> 'a1) -> internal_stack -> 'a1
366 val internal_stack_rect_Type0 :
367 'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
368 -> 'a1) -> internal_stack -> 'a1
370 val internal_stack_inv_rect_Type4 :
371 internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
372 (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1
374 val internal_stack_inv_rect_Type3 :
375 internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
376 (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1
378 val internal_stack_inv_rect_Type2 :
379 internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
380 (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1
382 val internal_stack_inv_rect_Type1 :
383 internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
384 (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1
386 val internal_stack_inv_rect_Type0 :
387 internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
388 (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1
390 val internal_stack_discr : internal_stack -> internal_stack -> __
392 val internal_stack_jmdiscr : internal_stack -> internal_stack -> __
394 val is_push : internal_stack -> ByteValues.beval -> internal_stack Errors.res
397 internal_stack -> (ByteValues.beval, internal_stack) Types.prod Errors.res
399 type state = { st_frms : __ Types.option; istack : internal_stack;
400 carry : ByteValues.bebit; regs : __; m : BEMem.bemem;
401 stack_usage : Nat.nat }
403 val state_rect_Type4 :
404 sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
405 -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1
407 val state_rect_Type5 :
408 sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
409 -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1
411 val state_rect_Type3 :
412 sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
413 -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1
415 val state_rect_Type2 :
416 sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
417 -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1
419 val state_rect_Type1 :
420 sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
421 -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1
423 val state_rect_Type0 :
424 sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
425 -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1
427 val st_frms : sem_state_params -> state -> __ Types.option
429 val istack : sem_state_params -> state -> internal_stack
431 val carry : sem_state_params -> state -> ByteValues.bebit
433 val regs : sem_state_params -> state -> __
435 val m : sem_state_params -> state -> BEMem.bemem
437 val stack_usage : sem_state_params -> state -> Nat.nat
439 val state_inv_rect_Type4 :
440 sem_state_params -> state -> (__ Types.option -> internal_stack ->
441 ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1
443 val state_inv_rect_Type3 :
444 sem_state_params -> state -> (__ Types.option -> internal_stack ->
445 ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1
447 val state_inv_rect_Type2 :
448 sem_state_params -> state -> (__ Types.option -> internal_stack ->
449 ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1
451 val state_inv_rect_Type1 :
452 sem_state_params -> state -> (__ Types.option -> internal_stack ->
453 ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1
455 val state_inv_rect_Type0 :
456 sem_state_params -> state -> (__ Types.option -> internal_stack ->
457 ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1
459 val state_jmdiscr : sem_state_params -> state -> state -> __
461 val sp : sem_state_params -> state -> ByteValues.xpointer Errors.res
463 type state_pc = { st_no_pc : state; pc : ByteValues.program_counter;
464 last_pop : ByteValues.program_counter }
466 val state_pc_rect_Type4 :
467 sem_state_params -> (state -> ByteValues.program_counter ->
468 ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
470 val state_pc_rect_Type5 :
471 sem_state_params -> (state -> ByteValues.program_counter ->
472 ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
474 val state_pc_rect_Type3 :
475 sem_state_params -> (state -> ByteValues.program_counter ->
476 ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
478 val state_pc_rect_Type2 :
479 sem_state_params -> (state -> ByteValues.program_counter ->
480 ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
482 val state_pc_rect_Type1 :
483 sem_state_params -> (state -> ByteValues.program_counter ->
484 ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
486 val state_pc_rect_Type0 :
487 sem_state_params -> (state -> ByteValues.program_counter ->
488 ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
490 val st_no_pc : sem_state_params -> state_pc -> state
492 val pc : sem_state_params -> state_pc -> ByteValues.program_counter
494 val last_pop : sem_state_params -> state_pc -> ByteValues.program_counter
496 val state_pc_inv_rect_Type4 :
497 sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
498 ByteValues.program_counter -> __ -> 'a1) -> 'a1
500 val state_pc_inv_rect_Type3 :
501 sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
502 ByteValues.program_counter -> __ -> 'a1) -> 'a1
504 val state_pc_inv_rect_Type2 :
505 sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
506 ByteValues.program_counter -> __ -> 'a1) -> 'a1
508 val state_pc_inv_rect_Type1 :
509 sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
510 ByteValues.program_counter -> __ -> 'a1) -> 'a1
512 val state_pc_inv_rect_Type0 :
513 sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
514 ByteValues.program_counter -> __ -> 'a1) -> 'a1
516 val state_pc_discr : sem_state_params -> state_pc -> state_pc -> __
518 val state_pc_jmdiscr : sem_state_params -> state_pc -> state_pc -> __
520 val dpi1__o__st_no_pc__o__inject :
521 sem_state_params -> (state_pc, 'a1) Types.dPair -> state Types.sig0
523 val eject__o__st_no_pc__o__inject :
524 sem_state_params -> state_pc Types.sig0 -> state Types.sig0
526 val st_no_pc__o__inject : sem_state_params -> state_pc -> state Types.sig0
528 val dpi1__o__st_no_pc :
529 sem_state_params -> (state_pc, 'a1) Types.dPair -> state
531 val eject__o__st_no_pc : sem_state_params -> state_pc Types.sig0 -> state
533 val init_pc : ByteValues.program_counter
535 val null_pc : Positive.pos -> ByteValues.program_counter
537 val set_m : sem_state_params -> BEMem.bemem -> state -> state
539 val set_regs : sem_state_params -> __ -> state -> state
541 val set_sp : sem_state_params -> ByteValues.xpointer -> state -> state
543 val set_carry : sem_state_params -> ByteValues.bebit -> state -> state
545 val set_istack : sem_state_params -> internal_stack -> state -> state
548 sem_state_params -> ByteValues.program_counter -> state_pc -> state_pc
550 val set_no_pc : sem_state_params -> state -> state_pc -> state_pc
553 sem_state_params -> state -> ByteValues.program_counter -> state_pc
555 val set_frms : sem_state_params -> __ -> state -> state
561 val call_kind_rect_Type4 : 'a1 -> 'a1 -> call_kind -> 'a1
563 val call_kind_rect_Type5 : 'a1 -> 'a1 -> call_kind -> 'a1
565 val call_kind_rect_Type3 : 'a1 -> 'a1 -> call_kind -> 'a1
567 val call_kind_rect_Type2 : 'a1 -> 'a1 -> call_kind -> 'a1
569 val call_kind_rect_Type1 : 'a1 -> 'a1 -> call_kind -> 'a1
571 val call_kind_rect_Type0 : 'a1 -> 'a1 -> call_kind -> 'a1
573 val call_kind_inv_rect_Type4 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
575 val call_kind_inv_rect_Type3 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
577 val call_kind_inv_rect_Type2 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
579 val call_kind_inv_rect_Type1 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
581 val call_kind_inv_rect_Type0 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
583 val call_kind_discr : call_kind -> call_kind -> __
585 val call_kind_jmdiscr : call_kind -> call_kind -> __
588 Joint.unserialized_params -> (AST.ident, (__, __) Types.prod) Types.sum ->
591 type 'f sem_unserialized_params = { st_pars : sem_state_params;
592 acca_store_ : (__ -> ByteValues.beval ->
593 __ -> __ Errors.res);
594 acca_retrieve_ : (__ -> __ ->
597 acca_arg_retrieve_ : (__ -> __ ->
600 accb_store_ : (__ -> ByteValues.beval ->
601 __ -> __ Errors.res);
602 accb_retrieve_ : (__ -> __ ->
605 accb_arg_retrieve_ : (__ -> __ ->
608 dpl_store_ : (__ -> ByteValues.beval ->
609 __ -> __ Errors.res);
610 dpl_retrieve_ : (__ -> __ ->
613 dpl_arg_retrieve_ : (__ -> __ ->
616 dph_store_ : (__ -> ByteValues.beval ->
617 __ -> __ Errors.res);
618 dph_retrieve_ : (__ -> __ ->
621 dph_arg_retrieve_ : (__ -> __ ->
624 snd_arg_retrieve_ : (__ -> __ ->
627 pair_reg_move_ : (__ -> __ -> __
629 save_frame : (call_kind -> __ -> state_pc
630 -> state Errors.res);
631 setup_call : (Nat.nat -> __ -> __ ->
632 state -> state Errors.res);
633 fetch_external_args : (AST.external_function
638 set_result : (Values.val0 List.list -> __
641 call_args_for_main : __;
642 call_dest_for_main : __;
643 read_result : (AST.ident List.list -> 'f
645 Globalenvs.genv_t -> __ ->
646 state -> ByteValues.beval
647 List.list Errors.res);
648 eval_ext_seq : (AST.ident List.list -> 'f
650 AST.ident -> state ->
652 pop_frame : (AST.ident List.list -> 'f
653 genv_gen -> AST.ident -> __
655 ByteValues.program_counter)
656 Types.prod Errors.res) }
658 val sem_unserialized_params_rect_Type4 :
659 Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
660 -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
661 -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
662 __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
663 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
664 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
665 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
666 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
667 ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
668 -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
669 Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
670 (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
671 -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
672 -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
673 -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
674 genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
675 List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
676 ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1
677 sem_unserialized_params -> 'a2
679 val sem_unserialized_params_rect_Type5 :
680 Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
681 -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
682 -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
683 __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
684 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
685 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
686 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
687 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
688 ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
689 -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
690 Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
691 (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
692 -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
693 -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
694 -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
695 genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
696 List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
697 ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1
698 sem_unserialized_params -> 'a2
700 val sem_unserialized_params_rect_Type3 :
701 Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
702 -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
703 -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
704 __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
705 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
706 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
707 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
708 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
709 ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
710 -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
711 Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
712 (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
713 -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
714 -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
715 -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
716 genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
717 List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
718 ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1
719 sem_unserialized_params -> 'a2
721 val sem_unserialized_params_rect_Type2 :
722 Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
723 -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
724 -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
725 __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
726 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
727 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
728 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
729 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
730 ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
731 -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
732 Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
733 (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
734 -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
735 -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
736 -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
737 genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
738 List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
739 ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1
740 sem_unserialized_params -> 'a2
742 val sem_unserialized_params_rect_Type1 :
743 Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
744 -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
745 -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
746 __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
747 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
748 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
749 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
750 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
751 ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
752 -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
753 Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
754 (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
755 -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
756 -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
757 -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
758 genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
759 List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
760 ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1
761 sem_unserialized_params -> 'a2
763 val sem_unserialized_params_rect_Type0 :
764 Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
765 -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
766 -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
767 __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
768 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
769 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
770 ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
771 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
772 ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
773 -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
774 Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
775 (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
776 -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
777 -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
778 -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
779 genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
780 List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
781 ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1
782 sem_unserialized_params -> 'a2
785 Joint.unserialized_params -> 'a1 sem_unserialized_params ->
789 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
790 ByteValues.beval -> __ -> __ Errors.res
793 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
794 ByteValues.beval Errors.res
796 val acca_arg_retrieve_ :
797 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
798 ByteValues.beval Errors.res
801 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
802 ByteValues.beval -> __ -> __ Errors.res
805 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
806 ByteValues.beval Errors.res
808 val accb_arg_retrieve_ :
809 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
810 ByteValues.beval Errors.res
813 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
814 ByteValues.beval -> __ -> __ Errors.res
817 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
818 ByteValues.beval Errors.res
820 val dpl_arg_retrieve_ :
821 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
822 ByteValues.beval Errors.res
825 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
826 ByteValues.beval -> __ -> __ Errors.res
829 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
830 ByteValues.beval Errors.res
832 val dph_arg_retrieve_ :
833 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
834 ByteValues.beval Errors.res
836 val snd_arg_retrieve_ :
837 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
838 ByteValues.beval Errors.res
841 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ -> __
845 Joint.unserialized_params -> 'a1 sem_unserialized_params -> call_kind -> __
846 -> state_pc -> state Errors.res
849 Joint.unserialized_params -> 'a1 sem_unserialized_params -> Nat.nat -> __
850 -> __ -> state -> state Errors.res
852 val fetch_external_args :
853 Joint.unserialized_params -> 'a1 sem_unserialized_params ->
854 AST.external_function -> state -> __ -> Values.val0 List.list Errors.res
857 Joint.unserialized_params -> 'a1 sem_unserialized_params -> Values.val0
858 List.list -> __ -> state -> state Errors.res
860 val call_args_for_main :
861 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __
863 val call_dest_for_main :
864 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __
867 Joint.unserialized_params -> 'a1 sem_unserialized_params -> AST.ident
868 List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state ->
869 ByteValues.beval List.list Errors.res
872 Joint.unserialized_params -> 'a1 sem_unserialized_params -> AST.ident
873 List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state Errors.res
876 Joint.unserialized_params -> 'a1 sem_unserialized_params -> AST.ident
877 List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
878 ByteValues.program_counter) Types.prod Errors.res
880 val sem_unserialized_params_inv_rect_Type4 :
881 Joint.unserialized_params -> 'a1 sem_unserialized_params ->
882 (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__
883 -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
884 Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
885 -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
886 Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
887 -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
888 Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
889 -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
890 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __
891 Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) ->
892 (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
893 (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
894 -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
895 -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
896 -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
897 genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
898 List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
899 ByteValues.program_counter) Types.prod Errors.res) -> __ -> 'a2) -> 'a2
901 val sem_unserialized_params_inv_rect_Type3 :
902 Joint.unserialized_params -> 'a1 sem_unserialized_params ->
903 (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__
904 -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
905 Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
906 -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
907 Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
908 -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
909 Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
910 -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
911 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __
912 Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) ->
913 (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
914 (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
915 -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
916 -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
917 -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
918 genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
919 List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
920 ByteValues.program_counter) Types.prod Errors.res) -> __ -> 'a2) -> 'a2
922 val sem_unserialized_params_inv_rect_Type2 :
923 Joint.unserialized_params -> 'a1 sem_unserialized_params ->
924 (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__
925 -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
926 Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
927 -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
928 Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
929 -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
930 Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
931 -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
932 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __
933 Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) ->
934 (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
935 (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
936 -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
937 -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
938 -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
939 genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
940 List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
941 ByteValues.program_counter) Types.prod Errors.res) -> __ -> 'a2) -> 'a2
943 val sem_unserialized_params_inv_rect_Type1 :
944 Joint.unserialized_params -> 'a1 sem_unserialized_params ->
945 (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__
946 -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
947 Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
948 -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
949 Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
950 -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
951 Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
952 -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
953 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __
954 Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) ->
955 (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
956 (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
957 -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
958 -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
959 -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
960 genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
961 List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
962 ByteValues.program_counter) Types.prod Errors.res) -> __ -> 'a2) -> 'a2
964 val sem_unserialized_params_inv_rect_Type0 :
965 Joint.unserialized_params -> 'a1 sem_unserialized_params ->
966 (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__
967 -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
968 Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
969 -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
970 Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
971 -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
972 Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
973 -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
974 Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __
975 Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) ->
976 (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
977 (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
978 -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
979 -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
980 -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
981 genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
982 List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
983 ByteValues.program_counter) Types.prod Errors.res) -> __ -> 'a2) -> 'a2
985 val sem_unserialized_params_jmdiscr :
986 Joint.unserialized_params -> 'a1 sem_unserialized_params -> 'a1
987 sem_unserialized_params -> __
989 val helper_def_retrieve :
990 (Joint.unserialized_params -> __ -> __ sem_unserialized_params -> __ -> 'a1
991 -> ByteValues.beval Errors.res) -> Joint.unserialized_params -> 'a2
992 sem_unserialized_params -> state -> 'a1 -> ByteValues.beval Errors.res
994 val helper_def_store :
995 (Joint.unserialized_params -> __ -> __ sem_unserialized_params -> 'a1 ->
996 ByteValues.beval -> __ -> __ Errors.res) -> Joint.unserialized_params ->
997 'a2 sem_unserialized_params -> 'a1 -> ByteValues.beval -> state -> state
1001 Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1002 ByteValues.beval Errors.res
1005 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1006 ByteValues.beval -> state -> state Errors.res
1008 val acca_arg_retrieve :
1009 Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1010 ByteValues.beval Errors.res
1013 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1014 ByteValues.beval -> state -> state Errors.res
1017 Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1018 ByteValues.beval Errors.res
1020 val accb_arg_retrieve :
1021 Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1022 ByteValues.beval Errors.res
1025 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1026 ByteValues.beval -> state -> state Errors.res
1029 Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1030 ByteValues.beval Errors.res
1032 val dpl_arg_retrieve :
1033 Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1034 ByteValues.beval Errors.res
1037 Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1038 ByteValues.beval -> state -> state Errors.res
1041 Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1042 ByteValues.beval Errors.res
1044 val dph_arg_retrieve :
1045 Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1046 ByteValues.beval Errors.res
1048 val snd_arg_retrieve :
1049 Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1050 ByteValues.beval Errors.res
1053 Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1056 val push : sem_state_params -> state -> ByteValues.beval -> state Errors.res
1059 sem_state_params -> state -> (ByteValues.beval, state) Types.prod
1063 sem_state_params -> state -> ByteValues.program_counter -> state Errors.res
1066 sem_state_params -> state -> (state, ByteValues.program_counter) Types.prod
1069 type serialized_params = { spp : Joint.params;
1070 msu_pars : Joint.joint_closed_internal_function
1071 sem_unserialized_params;
1072 offset_of_point : (__ -> Positive.pos);
1073 point_of_offset : (Positive.pos -> __) }
1075 val serialized_params_rect_Type4 :
1076 (Joint.params -> Joint.joint_closed_internal_function
1077 sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1078 __ -> __ -> 'a1) -> serialized_params -> 'a1
1080 val serialized_params_rect_Type5 :
1081 (Joint.params -> Joint.joint_closed_internal_function
1082 sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1083 __ -> __ -> 'a1) -> serialized_params -> 'a1
1085 val serialized_params_rect_Type3 :
1086 (Joint.params -> Joint.joint_closed_internal_function
1087 sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1088 __ -> __ -> 'a1) -> serialized_params -> 'a1
1090 val serialized_params_rect_Type2 :
1091 (Joint.params -> Joint.joint_closed_internal_function
1092 sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1093 __ -> __ -> 'a1) -> serialized_params -> 'a1
1095 val serialized_params_rect_Type1 :
1096 (Joint.params -> Joint.joint_closed_internal_function
1097 sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1098 __ -> __ -> 'a1) -> serialized_params -> 'a1
1100 val serialized_params_rect_Type0 :
1101 (Joint.params -> Joint.joint_closed_internal_function
1102 sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1103 __ -> __ -> 'a1) -> serialized_params -> 'a1
1105 val spp : serialized_params -> Joint.params
1108 serialized_params -> Joint.joint_closed_internal_function
1109 sem_unserialized_params
1111 val offset_of_point : serialized_params -> __ -> Positive.pos
1113 val point_of_offset : serialized_params -> Positive.pos -> __
1115 val serialized_params_inv_rect_Type4 :
1116 serialized_params -> (Joint.params -> Joint.joint_closed_internal_function
1117 sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1118 __ -> __ -> __ -> 'a1) -> 'a1
1120 val serialized_params_inv_rect_Type3 :
1121 serialized_params -> (Joint.params -> Joint.joint_closed_internal_function
1122 sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1123 __ -> __ -> __ -> 'a1) -> 'a1
1125 val serialized_params_inv_rect_Type2 :
1126 serialized_params -> (Joint.params -> Joint.joint_closed_internal_function
1127 sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1128 __ -> __ -> __ -> 'a1) -> 'a1
1130 val serialized_params_inv_rect_Type1 :
1131 serialized_params -> (Joint.params -> Joint.joint_closed_internal_function
1132 sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1133 __ -> __ -> __ -> 'a1) -> 'a1
1135 val serialized_params_inv_rect_Type0 :
1136 serialized_params -> (Joint.params -> Joint.joint_closed_internal_function
1137 sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1138 __ -> __ -> __ -> 'a1) -> 'a1
1140 val serialized_params_jmdiscr : serialized_params -> serialized_params -> __
1142 val spp__o__stmt_pars : serialized_params -> Joint.stmt_params
1144 val spp__o__stmt_pars__o__uns_pars : serialized_params -> Joint.uns_params
1146 val spp__o__stmt_pars__o__uns_pars__o__u_pars :
1147 serialized_params -> Joint.unserialized_params
1149 val msu_pars__o__st_pars : serialized_params -> sem_state_params
1151 type sem_params = { spp' : serialized_params;
1152 pre_main_generator : (Joint.joint_program ->
1153 Joint.joint_closed_internal_function) }
1155 val sem_params_rect_Type4 :
1156 (serialized_params -> (Joint.joint_program ->
1157 Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1
1159 val sem_params_rect_Type5 :
1160 (serialized_params -> (Joint.joint_program ->
1161 Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1
1163 val sem_params_rect_Type3 :
1164 (serialized_params -> (Joint.joint_program ->
1165 Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1
1167 val sem_params_rect_Type2 :
1168 (serialized_params -> (Joint.joint_program ->
1169 Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1
1171 val sem_params_rect_Type1 :
1172 (serialized_params -> (Joint.joint_program ->
1173 Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1
1175 val sem_params_rect_Type0 :
1176 (serialized_params -> (Joint.joint_program ->
1177 Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1
1179 val spp' : sem_params -> serialized_params
1181 val pre_main_generator :
1182 sem_params -> Joint.joint_program -> Joint.joint_closed_internal_function
1184 val sem_params_inv_rect_Type4 :
1185 sem_params -> (serialized_params -> (Joint.joint_program ->
1186 Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
1188 val sem_params_inv_rect_Type3 :
1189 sem_params -> (serialized_params -> (Joint.joint_program ->
1190 Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
1192 val sem_params_inv_rect_Type2 :
1193 sem_params -> (serialized_params -> (Joint.joint_program ->
1194 Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
1196 val sem_params_inv_rect_Type1 :
1197 sem_params -> (serialized_params -> (Joint.joint_program ->
1198 Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
1200 val sem_params_inv_rect_Type0 :
1201 sem_params -> (serialized_params -> (Joint.joint_program ->
1202 Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
1204 val sem_params_jmdiscr : sem_params -> sem_params -> __
1206 val spp'__o__msu_pars :
1207 sem_params -> Joint.joint_closed_internal_function sem_unserialized_params
1209 val spp'__o__msu_pars__o__st_pars : sem_params -> sem_state_params
1211 val spp'__o__spp : sem_params -> Joint.params
1213 val spp'__o__spp__o__stmt_pars : sem_params -> Joint.stmt_params
1215 val spp'__o__spp__o__stmt_pars__o__uns_pars : sem_params -> Joint.uns_params
1217 val spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
1218 sem_params -> Joint.unserialized_params
1221 sem_params -> Pointers.block Types.sig0 -> __ -> ByteValues.program_counter
1223 val point_of_pc : sem_params -> ByteValues.program_counter -> __
1225 val fetch_statement :
1226 sem_params -> AST.ident List.list -> genv -> ByteValues.program_counter ->
1227 ((AST.ident, Joint.joint_closed_internal_function) Types.prod,
1228 Joint.joint_statement) Types.prod Errors.res
1231 sem_params -> AST.ident List.list -> genv -> Pointers.block Types.sig0 ->
1232 Graphs.label -> ByteValues.program_counter Errors.res
1235 sem_params -> ByteValues.program_counter -> __ ->
1236 ByteValues.program_counter
1239 sem_params -> AST.ident List.list -> genv -> Graphs.label -> state_pc ->
1242 val next : sem_params -> __ -> state_pc -> state_pc
1244 val next_of_call_pc :
1245 sem_params -> AST.ident List.list -> genv -> ByteValues.program_counter ->
1248 val eval_seq_no_pc :
1249 sem_params -> AST.ident List.list -> genv -> AST.ident -> Joint.joint_seq
1250 -> state -> state Errors.res
1253 sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
1254 (__, __) Types.prod) Types.sum -> state -> __
1256 val eval_external_call :
1257 sem_params -> AST.external_function -> __ -> __ -> state -> __
1259 val increment_stack_usage : sem_state_params -> Nat.nat -> state -> state
1261 val decrement_stack_usage : sem_state_params -> Nat.nat -> state -> state
1263 val eval_internal_call :
1264 sem_params -> AST.ident List.list -> genv -> PreIdentifiers.identifier ->
1265 Joint.joint_internal_function -> __ -> state -> __
1267 val is_inl : ('a1, 'a2) Types.sum -> Bool.bool
1270 sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
1271 (__, __) Types.prod) Types.sum -> __ -> __ -> __ -> state_pc -> __
1273 val eval_statement_no_pc :
1274 sem_params -> AST.ident List.list -> genv -> AST.ident ->
1275 Joint.joint_statement -> state -> state Errors.res
1278 sem_params -> AST.ident List.list -> genv -> PreIdentifiers.identifier ->
1282 sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
1283 (__, __) Types.prod) Types.sum -> __ -> PreIdentifiers.identifier -> __ ->
1286 val eval_statement_advance :
1287 sem_params -> AST.ident List.list -> genv -> AST.ident ->
1288 Joint.joint_closed_internal_function -> Joint.joint_statement -> state_pc
1289 -> (IO.io_out, IO.io_in, state_pc) IOMonad.iO
1292 sem_params -> AST.ident List.list -> genv -> state_pc -> (IO.io_out,
1293 IO.io_in, state_pc) IOMonad.iO