extracted/joint_semantics.mli

   1 open Preamble
   2
   3 open Extra_bool
   4
   5 open Coqlib
   6
   7 open Values
   8
   9 open FrontEndVal
  10
  11 open Hide
  12
  13 open ByteValues
  14
  15 open Division
  16
  17 open Z
  18
  19 open BitVectorZ
  20
  21 open Pointers
  22
  23 open GenMem
  24
  25 open FrontEndMem
  26
  27 open Proper
  28
  29 open PositiveMap
  30
  31 open Deqsets
  32
  33 open Extralib
  34
  35 open Lists
  36
  37 open Identifiers
  38
  39 open Exp
  40
  41 open Arithmetic
  42
  43 open Vector
  44
  45 open Div_and_mod
  46
  47 open Util
  48
  49 open FoldStuff
  50
  51 open BitVector
  52
  53 open Extranat
  54
  55 open Integers
  56
  57 open AST
  58
  59 open ErrorMessages
  60
  61 open Option
  62
  63 open Setoids
  64
  65 open Monad
  66
  67 open Jmeq
  68
  69 open Russell
  70
  71 open Positive
  72
  73 open PreIdentifiers
  74
  75 open Bool
  76
  77 open Relations
  78
  79 open Nat
  80
  81 open List
  82
  83 open Hints_declaration
  84
  85 open Core_notation
  86
  87 open Pts
  88
  89 open Logic
  90
  91 open Types
  92
  93 open Errors
  94
  95 open Globalenvs
  96
  97 open CostLabel
  98
  99 open Events
 100
 101 open IOMonad
 102
 103 open IO
 104
 105 open BEMem
 106
 107 open String
 108
 109 open Sets
 110
 111 open Listb
 112
 113 open LabelledObjects
 114
 115 open BitVectorTrie
 116
 117 open Graphs
 118
 119 open I8051
 120
 121 open Order
 122
 123 open Registers
 124
 125 open BackEndOps
 126
 127 open Joint
 128
 129 open I8051bis
 130
 131 open ExtraGlobalenvs
 132
 133 type 'f genv_gen = { ge : 'f AST.fundef Globalenvs.genv_t;
 134                      stack_sizes : (AST.ident -> Nat.nat Types.option);
 135                      premain : 'f;
 136                      pc_from_label : (Pointers.block Types.sig0 -> 'f ->
 137                                      Graphs.label ->
 138                                      ByteValues.program_counter Types.option) }
 139
 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) ->
 144   'a1 genv_gen -> 'a2
 145
 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) ->
 150   'a1 genv_gen -> 'a2
 151
 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) ->
 156   'a1 genv_gen -> 'a2
 157
 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) ->
 162   'a1 genv_gen -> 'a2
 163
 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) ->
 168   'a1 genv_gen -> 'a2
 169
 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) ->
 174   'a1 genv_gen -> 'a2
 175
 176 val ge :
 177   AST.ident List.list -> 'a1 genv_gen -> 'a1 AST.fundef Globalenvs.genv_t
 178
 179 val stack_sizes :
 180   AST.ident List.list -> 'a1 genv_gen -> AST.ident -> Nat.nat Types.option
 181
 182 val premain : AST.ident List.list -> 'a1 genv_gen -> 'a1
 183
 184 val pc_from_label :
 185   AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 -> 'a1 ->
 186   Graphs.label -> ByteValues.program_counter Types.option
 187
 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
 193
 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
 199
 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
 205
 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
 211
 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
 217
 218 val genv_gen_discr :
 219   AST.ident List.list -> 'a1 genv_gen -> 'a1 genv_gen -> __
 220
 221 val genv_gen_jmdiscr :
 222   AST.ident List.list -> 'a1 genv_gen -> 'a1 genv_gen -> __
 223
 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
 227
 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
 231
 232 val ge__o__inject :
 233   AST.ident List.list -> 'a1 genv_gen -> 'a1 AST.fundef Globalenvs.genv_t
 234   Types.sig0
 235
 236 val dpi1__o__ge :
 237   AST.ident List.list -> ('a1 genv_gen, 'a2) Types.dPair -> 'a1 AST.fundef
 238   Globalenvs.genv_t
 239
 240 val eject__o__ge :
 241   AST.ident List.list -> 'a1 genv_gen Types.sig0 -> 'a1 AST.fundef
 242   Globalenvs.genv_t
 243
 244 val pre_main_id : AST.ident
 245
 246 val fetch_function :
 247   AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 ->
 248   (AST.ident, 'a1 AST.fundef) Types.prod Errors.res
 249
 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
 253
 254 val code_block_of_block :
 255   Pointers.block -> Pointers.block Types.sig0 Types.option
 256
 257 val block_of_funct_id :
 258   'a1 Globalenvs.genv_t -> PreIdentifiers.identifier -> Pointers.block
 259   Types.sig0 Errors.res
 260
 261 val gen_pc_from_label :
 262   AST.ident List.list -> 'a1 genv_gen -> AST.ident -> Graphs.label ->
 263   ByteValues.program_counter Errors.res
 264
 265 type genv = Joint.joint_closed_internal_function genv_gen
 266
 267 type sem_state_params = { empty_framesT : __;
 268                           empty_regsT : (ByteValues.xpointer -> __);
 269                           load_sp : (__ -> ByteValues.xpointer Errors.res);
 270                           save_sp : (__ -> ByteValues.xpointer -> __) }
 271
 272 val sem_state_params_rect_Type4 :
 273   (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
 274   ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
 275   'a1) -> sem_state_params -> 'a1
 276
 277 val sem_state_params_rect_Type5 :
 278   (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
 279   ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
 280   'a1) -> sem_state_params -> 'a1
 281
 282 val sem_state_params_rect_Type3 :
 283   (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
 284   ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
 285   'a1) -> sem_state_params -> 'a1
 286
 287 val sem_state_params_rect_Type2 :
 288   (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
 289   ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
 290   'a1) -> sem_state_params -> 'a1
 291
 292 val sem_state_params_rect_Type1 :
 293   (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
 294   ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
 295   'a1) -> sem_state_params -> 'a1
 296
 297 val sem_state_params_rect_Type0 :
 298   (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
 299   ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
 300   'a1) -> sem_state_params -> 'a1
 301
 302 type framesT
 303
 304 val empty_framesT : sem_state_params -> __
 305
 306 type regsT
 307
 308 val empty_regsT : sem_state_params -> ByteValues.xpointer -> __
 309
 310 val load_sp : sem_state_params -> __ -> ByteValues.xpointer Errors.res
 311
 312 val save_sp : sem_state_params -> __ -> ByteValues.xpointer -> __
 313
 314 val sem_state_params_inv_rect_Type4 :
 315   sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
 316   -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
 317   __ -> 'a1) -> 'a1
 318
 319 val sem_state_params_inv_rect_Type3 :
 320   sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
 321   -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
 322   __ -> 'a1) -> 'a1
 323
 324 val sem_state_params_inv_rect_Type2 :
 325   sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
 326   -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
 327   __ -> 'a1) -> 'a1
 328
 329 val sem_state_params_inv_rect_Type1 :
 330   sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
 331   -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
 332   __ -> 'a1) -> 'a1
 333
 334 val sem_state_params_inv_rect_Type0 :
 335   sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
 336   -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
 337   __ -> 'a1) -> 'a1
 338
 339 val sem_state_params_jmdiscr : sem_state_params -> sem_state_params -> __
 340
 341 type internal_stack =
 342 | Empty_is
 343 | One_is of ByteValues.beval
 344 | Both_is of ByteValues.beval * ByteValues.beval
 345
 346 val internal_stack_rect_Type4 :
 347   'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
 348   -> 'a1) -> internal_stack -> 'a1
 349
 350 val internal_stack_rect_Type5 :
 351   'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
 352   -> 'a1) -> internal_stack -> 'a1
 353
 354 val internal_stack_rect_Type3 :
 355   'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
 356   -> 'a1) -> internal_stack -> 'a1
 357
 358 val internal_stack_rect_Type2 :
 359   'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
 360   -> 'a1) -> internal_stack -> 'a1
 361
 362 val internal_stack_rect_Type1 :
 363   'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
 364   -> 'a1) -> internal_stack -> 'a1
 365
 366 val internal_stack_rect_Type0 :
 367   'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
 368   -> 'a1) -> internal_stack -> 'a1
 369
 370 val internal_stack_inv_rect_Type4 :
 371   internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
 372   (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1
 373
 374 val internal_stack_inv_rect_Type3 :
 375   internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
 376   (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1
 377
 378 val internal_stack_inv_rect_Type2 :
 379   internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
 380   (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1
 381
 382 val internal_stack_inv_rect_Type1 :
 383   internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
 384   (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1
 385
 386 val internal_stack_inv_rect_Type0 :
 387   internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
 388   (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1
 389
 390 val internal_stack_discr : internal_stack -> internal_stack -> __
 391
 392 val internal_stack_jmdiscr : internal_stack -> internal_stack -> __
 393
 394 val is_push : internal_stack -> ByteValues.beval -> internal_stack Errors.res
 395
 396 val is_pop :
 397   internal_stack -> (ByteValues.beval, internal_stack) Types.prod Errors.res
 398
 399 type state = { st_frms : __ Types.option; istack : internal_stack;
 400                carry : ByteValues.bebit; regs : __; m : BEMem.bemem;
 401                stack_usage : Nat.nat }
 402
 403 val state_rect_Type4 :
 404   sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
 405   -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1
 406
 407 val state_rect_Type5 :
 408   sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
 409   -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1
 410
 411 val state_rect_Type3 :
 412   sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
 413   -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1
 414
 415 val state_rect_Type2 :
 416   sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
 417   -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1
 418
 419 val state_rect_Type1 :
 420   sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
 421   -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1
 422
 423 val state_rect_Type0 :
 424   sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
 425   -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1
 426
 427 val st_frms : sem_state_params -> state -> __ Types.option
 428
 429 val istack : sem_state_params -> state -> internal_stack
 430
 431 val carry : sem_state_params -> state -> ByteValues.bebit
 432
 433 val regs : sem_state_params -> state -> __
 434
 435 val m : sem_state_params -> state -> BEMem.bemem
 436
 437 val stack_usage : sem_state_params -> state -> Nat.nat
 438
 439 val state_inv_rect_Type4 :
 440   sem_state_params -> state -> (__ Types.option -> internal_stack ->
 441   ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1
 442
 443 val state_inv_rect_Type3 :
 444   sem_state_params -> state -> (__ Types.option -> internal_stack ->
 445   ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1
 446
 447 val state_inv_rect_Type2 :
 448   sem_state_params -> state -> (__ Types.option -> internal_stack ->
 449   ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1
 450
 451 val state_inv_rect_Type1 :
 452   sem_state_params -> state -> (__ Types.option -> internal_stack ->
 453   ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1
 454
 455 val state_inv_rect_Type0 :
 456   sem_state_params -> state -> (__ Types.option -> internal_stack ->
 457   ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1
 458
 459 val state_jmdiscr : sem_state_params -> state -> state -> __
 460
 461 val sp : sem_state_params -> state -> ByteValues.xpointer Errors.res
 462
 463 type state_pc = { st_no_pc : state; pc : ByteValues.program_counter;
 464                   last_pop : ByteValues.program_counter }
 465
 466 val state_pc_rect_Type4 :
 467   sem_state_params -> (state -> ByteValues.program_counter ->
 468   ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
 469
 470 val state_pc_rect_Type5 :
 471   sem_state_params -> (state -> ByteValues.program_counter ->
 472   ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
 473
 474 val state_pc_rect_Type3 :
 475   sem_state_params -> (state -> ByteValues.program_counter ->
 476   ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
 477
 478 val state_pc_rect_Type2 :
 479   sem_state_params -> (state -> ByteValues.program_counter ->
 480   ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
 481
 482 val state_pc_rect_Type1 :
 483   sem_state_params -> (state -> ByteValues.program_counter ->
 484   ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
 485
 486 val state_pc_rect_Type0 :
 487   sem_state_params -> (state -> ByteValues.program_counter ->
 488   ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
 489
 490 val st_no_pc : sem_state_params -> state_pc -> state
 491
 492 val pc : sem_state_params -> state_pc -> ByteValues.program_counter
 493
 494 val last_pop : sem_state_params -> state_pc -> ByteValues.program_counter
 495
 496 val state_pc_inv_rect_Type4 :
 497   sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
 498   ByteValues.program_counter -> __ -> 'a1) -> 'a1
 499
 500 val state_pc_inv_rect_Type3 :
 501   sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
 502   ByteValues.program_counter -> __ -> 'a1) -> 'a1
 503
 504 val state_pc_inv_rect_Type2 :
 505   sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
 506   ByteValues.program_counter -> __ -> 'a1) -> 'a1
 507
 508 val state_pc_inv_rect_Type1 :
 509   sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
 510   ByteValues.program_counter -> __ -> 'a1) -> 'a1
 511
 512 val state_pc_inv_rect_Type0 :
 513   sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
 514   ByteValues.program_counter -> __ -> 'a1) -> 'a1
 515
 516 val state_pc_discr : sem_state_params -> state_pc -> state_pc -> __
 517
 518 val state_pc_jmdiscr : sem_state_params -> state_pc -> state_pc -> __
 519
 520 val dpi1__o__st_no_pc__o__inject :
 521   sem_state_params -> (state_pc, 'a1) Types.dPair -> state Types.sig0
 522
 523 val eject__o__st_no_pc__o__inject :
 524   sem_state_params -> state_pc Types.sig0 -> state Types.sig0
 525
 526 val st_no_pc__o__inject : sem_state_params -> state_pc -> state Types.sig0
 527
 528 val dpi1__o__st_no_pc :
 529   sem_state_params -> (state_pc, 'a1) Types.dPair -> state
 530
 531 val eject__o__st_no_pc : sem_state_params -> state_pc Types.sig0 -> state
 532
 533 val init_pc : ByteValues.program_counter
 534
 535 val null_pc : Positive.pos -> ByteValues.program_counter
 536
 537 val set_m : sem_state_params -> BEMem.bemem -> state -> state
 538
 539 val set_regs : sem_state_params -> __ -> state -> state
 540
 541 val set_sp : sem_state_params -> ByteValues.xpointer -> state -> state
 542
 543 val set_carry : sem_state_params -> ByteValues.bebit -> state -> state
 544
 545 val set_istack : sem_state_params -> internal_stack -> state -> state
 546
 547 val set_pc :
 548   sem_state_params -> ByteValues.program_counter -> state_pc -> state_pc
 549
 550 val set_no_pc : sem_state_params -> state -> state_pc -> state_pc
 551
 552 val set_last_pop :
 553   sem_state_params -> state -> ByteValues.program_counter -> state_pc
 554
 555 val set_frms : sem_state_params -> __ -> state -> state
 556
 557 type call_kind =
 558 | PTR
 559 | ID
 560
 561 val call_kind_rect_Type4 : 'a1 -> 'a1 -> call_kind -> 'a1
 562
 563 val call_kind_rect_Type5 : 'a1 -> 'a1 -> call_kind -> 'a1
 564
 565 val call_kind_rect_Type3 : 'a1 -> 'a1 -> call_kind -> 'a1
 566
 567 val call_kind_rect_Type2 : 'a1 -> 'a1 -> call_kind -> 'a1
 568
 569 val call_kind_rect_Type1 : 'a1 -> 'a1 -> call_kind -> 'a1
 570
 571 val call_kind_rect_Type0 : 'a1 -> 'a1 -> call_kind -> 'a1
 572
 573 val call_kind_inv_rect_Type4 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 574
 575 val call_kind_inv_rect_Type3 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 576
 577 val call_kind_inv_rect_Type2 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 578
 579 val call_kind_inv_rect_Type1 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 580
 581 val call_kind_inv_rect_Type0 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 582
 583 val call_kind_discr : call_kind -> call_kind -> __
 584
 585 val call_kind_jmdiscr : call_kind -> call_kind -> __
 586
 587 val kind_of_call :
 588   Joint.unserialized_params -> (AST.ident, (__, __) Types.prod) Types.sum ->
 589   call_kind
 590
 591 type 'f sem_unserialized_params = { st_pars : sem_state_params;
 592                                     acca_store_ : (__ -> ByteValues.beval ->
 593                                                   __ -> __ Errors.res);
 594                                     acca_retrieve_ : (__ -> __ ->
 595                                                      ByteValues.beval
 596                                                      Errors.res);
 597                                     acca_arg_retrieve_ : (__ -> __ ->
 598                                                          ByteValues.beval
 599                                                          Errors.res);
 600                                     accb_store_ : (__ -> ByteValues.beval ->
 601                                                   __ -> __ Errors.res);
 602                                     accb_retrieve_ : (__ -> __ ->
 603                                                      ByteValues.beval
 604                                                      Errors.res);
 605                                     accb_arg_retrieve_ : (__ -> __ ->
 606                                                          ByteValues.beval
 607                                                          Errors.res);
 608                                     dpl_store_ : (__ -> ByteValues.beval ->
 609                                                  __ -> __ Errors.res);
 610                                     dpl_retrieve_ : (__ -> __ ->
 611                                                     ByteValues.beval
 612                                                     Errors.res);
 613                                     dpl_arg_retrieve_ : (__ -> __ ->
 614                                                         ByteValues.beval
 615                                                         Errors.res);
 616                                     dph_store_ : (__ -> ByteValues.beval ->
 617                                                  __ -> __ Errors.res);
 618                                     dph_retrieve_ : (__ -> __ ->
 619                                                     ByteValues.beval
 620                                                     Errors.res);
 621                                     dph_arg_retrieve_ : (__ -> __ ->
 622                                                         ByteValues.beval
 623                                                         Errors.res);
 624                                     snd_arg_retrieve_ : (__ -> __ ->
 625                                                         ByteValues.beval
 626                                                         Errors.res);
 627                                     pair_reg_move_ : (__ -> __ -> __
 628                                                      Errors.res);
 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
 634                                                           -> state -> __ ->
 635                                                           Values.val0
 636                                                           List.list
 637                                                           Errors.res);
 638                                     set_result : (Values.val0 List.list -> __
 639                                                  -> state -> state
 640                                                  Errors.res);
 641                                     call_args_for_main : __;
 642                                     call_dest_for_main : __;
 643                                     read_result : (AST.ident List.list -> 'f
 644                                                   AST.fundef
 645                                                   Globalenvs.genv_t -> __ ->
 646                                                   state -> ByteValues.beval
 647                                                   List.list Errors.res);
 648                                     eval_ext_seq : (AST.ident List.list -> 'f
 649                                                    genv_gen -> __ ->
 650                                                    AST.ident -> state ->
 651                                                    state Errors.res);
 652                                     pop_frame : (AST.ident List.list -> 'f
 653                                                 genv_gen -> AST.ident -> __
 654                                                 -> state -> (state,
 655                                                 ByteValues.program_counter)
 656                                                 Types.prod Errors.res) }
 657
 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
 678
 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
 699
 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
 720
 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
 741
 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
 762
 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
 783
 784 val st_pars :
 785   Joint.unserialized_params -> 'a1 sem_unserialized_params ->
 786   sem_state_params
 787
 788 val acca_store_ :
 789   Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
 790   ByteValues.beval -> __ -> __ Errors.res
 791
 792 val acca_retrieve_ :
 793   Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
 794   ByteValues.beval Errors.res
 795
 796 val acca_arg_retrieve_ :
 797   Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
 798   ByteValues.beval Errors.res
 799
 800 val accb_store_ :
 801   Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
 802   ByteValues.beval -> __ -> __ Errors.res
 803
 804 val accb_retrieve_ :
 805   Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
 806   ByteValues.beval Errors.res
 807
 808 val accb_arg_retrieve_ :
 809   Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
 810   ByteValues.beval Errors.res
 811
 812 val dpl_store_ :
 813   Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
 814   ByteValues.beval -> __ -> __ Errors.res
 815
 816 val dpl_retrieve_ :
 817   Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
 818   ByteValues.beval Errors.res
 819
 820 val dpl_arg_retrieve_ :
 821   Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
 822   ByteValues.beval Errors.res
 823
 824 val dph_store_ :
 825   Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
 826   ByteValues.beval -> __ -> __ Errors.res
 827
 828 val dph_retrieve_ :
 829   Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
 830   ByteValues.beval Errors.res
 831
 832 val dph_arg_retrieve_ :
 833   Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
 834   ByteValues.beval Errors.res
 835
 836 val snd_arg_retrieve_ :
 837   Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
 838   ByteValues.beval Errors.res
 839
 840 val pair_reg_move_ :
 841   Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ -> __
 842   Errors.res
 843
 844 val save_frame :
 845   Joint.unserialized_params -> 'a1 sem_unserialized_params -> call_kind -> __
 846   -> state_pc -> state Errors.res
 847
 848 val setup_call :
 849   Joint.unserialized_params -> 'a1 sem_unserialized_params -> Nat.nat -> __
 850   -> __ -> state -> state Errors.res
 851
 852 val fetch_external_args :
 853   Joint.unserialized_params -> 'a1 sem_unserialized_params ->
 854   AST.external_function -> state -> __ -> Values.val0 List.list Errors.res
 855
 856 val set_result :
 857   Joint.unserialized_params -> 'a1 sem_unserialized_params -> Values.val0
 858   List.list -> __ -> state -> state Errors.res
 859
 860 val call_args_for_main :
 861   Joint.unserialized_params -> 'a1 sem_unserialized_params -> __
 862
 863 val call_dest_for_main :
 864   Joint.unserialized_params -> 'a1 sem_unserialized_params -> __
 865
 866 val read_result :
 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
 870
 871 val eval_ext_seq :
 872   Joint.unserialized_params -> 'a1 sem_unserialized_params -> AST.ident
 873   List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state Errors.res
 874
 875 val pop_frame :
 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
 879
 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
 900
 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
 921
 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
 942
 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
 963
 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
 984
 985 val sem_unserialized_params_jmdiscr :
 986   Joint.unserialized_params -> 'a1 sem_unserialized_params -> 'a1
 987   sem_unserialized_params -> __
 988
 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
 993
 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
 998   Errors.res
 999
1000 val acca_retrieve :
1001   Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1002   ByteValues.beval Errors.res
1003
1004 val acca_store :
1005   Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1006   ByteValues.beval -> state -> state Errors.res
1007
1008 val acca_arg_retrieve :
1009   Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1010   ByteValues.beval Errors.res
1011
1012 val accb_store :
1013   Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1014   ByteValues.beval -> state -> state Errors.res
1015
1016 val accb_retrieve :
1017   Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1018   ByteValues.beval Errors.res
1019
1020 val accb_arg_retrieve :
1021   Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1022   ByteValues.beval Errors.res
1023
1024 val dpl_store :
1025   Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1026   ByteValues.beval -> state -> state Errors.res
1027
1028 val dpl_retrieve :
1029   Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1030   ByteValues.beval Errors.res
1031
1032 val dpl_arg_retrieve :
1033   Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1034   ByteValues.beval Errors.res
1035
1036 val dph_store :
1037   Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1038   ByteValues.beval -> state -> state Errors.res
1039
1040 val dph_retrieve :
1041   Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1042   ByteValues.beval Errors.res
1043
1044 val dph_arg_retrieve :
1045   Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1046   ByteValues.beval Errors.res
1047
1048 val snd_arg_retrieve :
1049   Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1050   ByteValues.beval Errors.res
1051
1052 val pair_reg_move :
1053   Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1054   __
1055
1056 val push : sem_state_params -> state -> ByteValues.beval -> state Errors.res
1057
1058 val pop :
1059   sem_state_params -> state -> (ByteValues.beval, state) Types.prod
1060   Errors.res
1061
1062 val push_ra :
1063   sem_state_params -> state -> ByteValues.program_counter -> state Errors.res
1064
1065 val pop_ra :
1066   sem_state_params -> state -> (state, ByteValues.program_counter) Types.prod
1067   Errors.res
1068
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 -> __) }
1074
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
1079
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
1084
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
1089
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
1094
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
1099
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
1104
1105 val spp : serialized_params -> Joint.params
1106
1107 val msu_pars :
1108   serialized_params -> Joint.joint_closed_internal_function
1109   sem_unserialized_params
1110
1111 val offset_of_point : serialized_params -> __ -> Positive.pos
1112
1113 val point_of_offset : serialized_params -> Positive.pos -> __
1114
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
1119
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
1124
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
1129
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
1134
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
1139
1140 val serialized_params_jmdiscr : serialized_params -> serialized_params -> __
1141
1142 val spp__o__stmt_pars : serialized_params -> Joint.stmt_params
1143
1144 val spp__o__stmt_pars__o__uns_pars : serialized_params -> Joint.uns_params
1145
1146 val spp__o__stmt_pars__o__uns_pars__o__u_pars :
1147   serialized_params -> Joint.unserialized_params
1148
1149 val msu_pars__o__st_pars : serialized_params -> sem_state_params
1150
1151 type sem_params = { spp' : serialized_params;
1152                     pre_main_generator : (Joint.joint_program ->
1153                                          Joint.joint_closed_internal_function) }
1154
1155 val sem_params_rect_Type4 :
1156   (serialized_params -> (Joint.joint_program ->
1157   Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1
1158
1159 val sem_params_rect_Type5 :
1160   (serialized_params -> (Joint.joint_program ->
1161   Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1
1162
1163 val sem_params_rect_Type3 :
1164   (serialized_params -> (Joint.joint_program ->
1165   Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1
1166
1167 val sem_params_rect_Type2 :
1168   (serialized_params -> (Joint.joint_program ->
1169   Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1
1170
1171 val sem_params_rect_Type1 :
1172   (serialized_params -> (Joint.joint_program ->
1173   Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1
1174
1175 val sem_params_rect_Type0 :
1176   (serialized_params -> (Joint.joint_program ->
1177   Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1
1178
1179 val spp' : sem_params -> serialized_params
1180
1181 val pre_main_generator :
1182   sem_params -> Joint.joint_program -> Joint.joint_closed_internal_function
1183
1184 val sem_params_inv_rect_Type4 :
1185   sem_params -> (serialized_params -> (Joint.joint_program ->
1186   Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
1187
1188 val sem_params_inv_rect_Type3 :
1189   sem_params -> (serialized_params -> (Joint.joint_program ->
1190   Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
1191
1192 val sem_params_inv_rect_Type2 :
1193   sem_params -> (serialized_params -> (Joint.joint_program ->
1194   Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
1195
1196 val sem_params_inv_rect_Type1 :
1197   sem_params -> (serialized_params -> (Joint.joint_program ->
1198   Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
1199
1200 val sem_params_inv_rect_Type0 :
1201   sem_params -> (serialized_params -> (Joint.joint_program ->
1202   Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
1203
1204 val sem_params_jmdiscr : sem_params -> sem_params -> __
1205
1206 val spp'__o__msu_pars :
1207   sem_params -> Joint.joint_closed_internal_function sem_unserialized_params
1208
1209 val spp'__o__msu_pars__o__st_pars : sem_params -> sem_state_params
1210
1211 val spp'__o__spp : sem_params -> Joint.params
1212
1213 val spp'__o__spp__o__stmt_pars : sem_params -> Joint.stmt_params
1214
1215 val spp'__o__spp__o__stmt_pars__o__uns_pars : sem_params -> Joint.uns_params
1216
1217 val spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
1218   sem_params -> Joint.unserialized_params
1219
1220 val pc_of_point :
1221   sem_params -> Pointers.block Types.sig0 -> __ -> ByteValues.program_counter
1222
1223 val point_of_pc : sem_params -> ByteValues.program_counter -> __
1224
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
1229
1230 val pc_of_label :
1231   sem_params -> AST.ident List.list -> genv -> Pointers.block Types.sig0 ->
1232   Graphs.label -> ByteValues.program_counter Errors.res
1233
1234 val succ_pc :
1235   sem_params -> ByteValues.program_counter -> __ ->
1236   ByteValues.program_counter
1237
1238 val goto :
1239   sem_params -> AST.ident List.list -> genv -> Graphs.label -> state_pc ->
1240   state_pc Errors.res
1241
1242 val next : sem_params -> __ -> state_pc -> state_pc
1243
1244 val next_of_call_pc :
1245   sem_params -> AST.ident List.list -> genv -> ByteValues.program_counter ->
1246   __ Errors.res
1247
1248 val eval_seq_no_pc :
1249   sem_params -> AST.ident List.list -> genv -> AST.ident -> Joint.joint_seq
1250   -> state -> state Errors.res
1251
1252 val block_of_call :
1253   sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
1254   (__, __) Types.prod) Types.sum -> state -> __
1255
1256 val eval_external_call :
1257   sem_params -> AST.external_function -> __ -> __ -> state -> __
1258
1259 val increment_stack_usage : sem_state_params -> Nat.nat -> state -> state
1260
1261 val decrement_stack_usage : sem_state_params -> Nat.nat -> state -> state
1262
1263 val eval_internal_call :
1264   sem_params -> AST.ident List.list -> genv -> PreIdentifiers.identifier ->
1265   Joint.joint_internal_function -> __ -> state -> __
1266
1267 val is_inl : ('a1, 'a2) Types.sum -> Bool.bool
1268
1269 val eval_call :
1270   sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
1271   (__, __) Types.prod) Types.sum -> __ -> __ -> __ -> state_pc -> __
1272
1273 val eval_statement_no_pc :
1274   sem_params -> AST.ident List.list -> genv -> AST.ident ->
1275   Joint.joint_statement -> state -> state Errors.res
1276
1277 val eval_return :
1278   sem_params -> AST.ident List.list -> genv -> PreIdentifiers.identifier ->
1279   __ -> state -> __
1280
1281 val eval_tailcall :
1282   sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
1283   (__, __) Types.prod) Types.sum -> __ -> PreIdentifiers.identifier -> __ ->
1284   state_pc -> __
1285
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
1290
1291 val eval_state :
1292   sem_params -> AST.ident List.list -> genv -> state_pc -> (IO.io_out,
1293   IO.io_in, state_pc) IOMonad.iO
1294