extracted/joint_semantics.ml

   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) ->
 144     'a2) -> 'a1 genv_gen -> 'a2 **)
 145 let rec genv_gen_rect_Type4 globals h_mk_genv_gen x_24476 =
 146   let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0;
 147     pc_from_label = pc_from_label0 } = x_24476
 148   in
 149   h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0
 150
 151 (** val genv_gen_rect_Type5 :
 152     AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
 153     (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0
 154     -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) ->
 155     'a2) -> 'a1 genv_gen -> 'a2 **)
 156 let rec genv_gen_rect_Type5 globals h_mk_genv_gen x_24478 =
 157   let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0;
 158     pc_from_label = pc_from_label0 } = x_24478
 159   in
 160   h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0
 161
 162 (** val genv_gen_rect_Type3 :
 163     AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
 164     (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0
 165     -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) ->
 166     'a2) -> 'a1 genv_gen -> 'a2 **)
 167 let rec genv_gen_rect_Type3 globals h_mk_genv_gen x_24480 =
 168   let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0;
 169     pc_from_label = pc_from_label0 } = x_24480
 170   in
 171   h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0
 172
 173 (** val genv_gen_rect_Type2 :
 174     AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
 175     (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0
 176     -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) ->
 177     'a2) -> 'a1 genv_gen -> 'a2 **)
 178 let rec genv_gen_rect_Type2 globals h_mk_genv_gen x_24482 =
 179   let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0;
 180     pc_from_label = pc_from_label0 } = x_24482
 181   in
 182   h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0
 183
 184 (** val genv_gen_rect_Type1 :
 185     AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
 186     (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0
 187     -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) ->
 188     'a2) -> 'a1 genv_gen -> 'a2 **)
 189 let rec genv_gen_rect_Type1 globals h_mk_genv_gen x_24484 =
 190   let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0;
 191     pc_from_label = pc_from_label0 } = x_24484
 192   in
 193   h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0
 194
 195 (** val genv_gen_rect_Type0 :
 196     AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
 197     (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0
 198     -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) ->
 199     'a2) -> 'a1 genv_gen -> 'a2 **)
 200 let rec genv_gen_rect_Type0 globals h_mk_genv_gen x_24486 =
 201   let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0;
 202     pc_from_label = pc_from_label0 } = x_24486
 203   in
 204   h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0
 205
 206 (** val ge :
 207     AST.ident List.list -> 'a1 genv_gen -> 'a1 AST.fundef Globalenvs.genv_t **)
 208 let rec ge globals xxx =
 209   xxx.ge
 210
 211 (** val stack_sizes :
 212     AST.ident List.list -> 'a1 genv_gen -> AST.ident -> Nat.nat Types.option **)
 213 let rec stack_sizes globals xxx =
 214   xxx.stack_sizes
 215
 216 (** val premain : AST.ident List.list -> 'a1 genv_gen -> 'a1 **)
 217 let rec premain globals xxx =
 218   xxx.premain
 219
 220 (** val pc_from_label :
 221     AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 -> 'a1
 222     -> Graphs.label -> ByteValues.program_counter Types.option **)
 223 let rec pc_from_label globals xxx =
 224   xxx.pc_from_label
 225
 226 (** val genv_gen_inv_rect_Type4 :
 227     AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t
 228     -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
 229     Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
 230     Types.option) -> __ -> 'a2) -> 'a2 **)
 231 let genv_gen_inv_rect_Type4 x2 hterm h1 =
 232   let hcut = genv_gen_rect_Type4 x2 h1 hterm in hcut __
 233
 234 (** val genv_gen_inv_rect_Type3 :
 235     AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t
 236     -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
 237     Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
 238     Types.option) -> __ -> 'a2) -> 'a2 **)
 239 let genv_gen_inv_rect_Type3 x2 hterm h1 =
 240   let hcut = genv_gen_rect_Type3 x2 h1 hterm in hcut __
 241
 242 (** val genv_gen_inv_rect_Type2 :
 243     AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t
 244     -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
 245     Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
 246     Types.option) -> __ -> 'a2) -> 'a2 **)
 247 let genv_gen_inv_rect_Type2 x2 hterm h1 =
 248   let hcut = genv_gen_rect_Type2 x2 h1 hterm in hcut __
 249
 250 (** val genv_gen_inv_rect_Type1 :
 251     AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t
 252     -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
 253     Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
 254     Types.option) -> __ -> 'a2) -> 'a2 **)
 255 let genv_gen_inv_rect_Type1 x2 hterm h1 =
 256   let hcut = genv_gen_rect_Type1 x2 h1 hterm in hcut __
 257
 258 (** val genv_gen_inv_rect_Type0 :
 259     AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t
 260     -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
 261     Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
 262     Types.option) -> __ -> 'a2) -> 'a2 **)
 263 let genv_gen_inv_rect_Type0 x2 hterm h1 =
 264   let hcut = genv_gen_rect_Type0 x2 h1 hterm in hcut __
 265
 266 (** val genv_gen_discr :
 267     AST.ident List.list -> 'a1 genv_gen -> 'a1 genv_gen -> __ **)
 268 let genv_gen_discr a2 x y =
 269   Logic.eq_rect_Type2 x
 270     (let { ge = a0; stack_sizes = a20; premain = a3; pc_from_label = a4 } = x
 271      in
 272     Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
 273
 274 (** val genv_gen_jmdiscr :
 275     AST.ident List.list -> 'a1 genv_gen -> 'a1 genv_gen -> __ **)
 276 let genv_gen_jmdiscr a2 x y =
 277   Logic.eq_rect_Type2 x
 278     (let { ge = a0; stack_sizes = a20; premain = a3; pc_from_label = a4 } = x
 279      in
 280     Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
 281
 282 (** val dpi1__o__ge__o__inject :
 283     AST.ident List.list -> ('a1 genv_gen, 'a2) Types.dPair -> 'a1 AST.fundef
 284     Globalenvs.genv_t Types.sig0 **)
 285 let dpi1__o__ge__o__inject x1 x4 =
 286   x4.Types.dpi1.ge
 287
 288 (** val eject__o__ge__o__inject :
 289     AST.ident List.list -> 'a1 genv_gen Types.sig0 -> 'a1 AST.fundef
 290     Globalenvs.genv_t Types.sig0 **)
 291 let eject__o__ge__o__inject x1 x4 =
 292   (Types.pi1 x4).ge
 293
 294 (** val ge__o__inject :
 295     AST.ident List.list -> 'a1 genv_gen -> 'a1 AST.fundef Globalenvs.genv_t
 296     Types.sig0 **)
 297 let ge__o__inject x1 x3 =
 298   x3.ge
 299
 300 (** val dpi1__o__ge :
 301     AST.ident List.list -> ('a1 genv_gen, 'a2) Types.dPair -> 'a1 AST.fundef
 302     Globalenvs.genv_t **)
 303 let dpi1__o__ge x1 x3 =
 304   x3.Types.dpi1.ge
 305
 306 (** val eject__o__ge :
 307     AST.ident List.list -> 'a1 genv_gen Types.sig0 -> 'a1 AST.fundef
 308     Globalenvs.genv_t **)
 309 let eject__o__ge x1 x3 =
 310   (Types.pi1 x3).ge
 311
 312 (** val pre_main_id : AST.ident **)
 313 let pre_main_id =
 314   Positive.One
 315
 316 (** val fetch_function :
 317     AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 ->
 318     (AST.ident, 'a1 AST.fundef) Types.prod Errors.res **)
 319 let fetch_function g ge0 bl =
 320   match Z.eqZb (Pointers.block_id (Types.pi1 bl))
 321           (Z.zopp (Z.z_of_nat (Nat.S Nat.O))) with
 322   | Bool.True ->
 323     Obj.magic
 324       (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = pre_main_id;
 325         Types.snd = (AST.Internal ge0.premain) })
 326   | Bool.False ->
 327     Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction),
 328       List.Nil))
 329       (Obj.magic
 330         (Monad.m_bind0 (Monad.max_def Option.option)
 331           (Obj.magic (Globalenvs.symbol_for_block ge0.ge (Types.pi1 bl)))
 332           (fun id ->
 333           Monad.m_bind0 (Monad.max_def Option.option)
 334             (Obj.magic (Globalenvs.find_funct_ptr ge0.ge (Types.pi1 bl)))
 335             (fun fd ->
 336             Monad.m_return0 (Monad.max_def Option.option) { Types.fst = id;
 337               Types.snd = fd }))))
 338
 339 (** val fetch_internal_function :
 340     AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 ->
 341     (AST.ident, 'a1) Types.prod Errors.res **)
 342 let fetch_internal_function g ge0 bl =
 343   Obj.magic
 344     (Monad.m_bind2 (Monad.max_def Errors.res0)
 345       (Obj.magic (fetch_function g ge0 bl)) (fun id fd ->
 346       match fd with
 347       | AST.Internal ifd ->
 348         Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = id;
 349           Types.snd = ifd }
 350       | AST.External x ->
 351         Obj.magic (Errors.Error (List.Cons ((Errors.MSG
 352           ErrorMessages.BadFunction), List.Nil)))))
 353
 354 (** val code_block_of_block :
 355     Pointers.block -> Pointers.block Types.sig0 Types.option **)
 356 let code_block_of_block bl =
 357   (match Pointers.block_region bl with
 358    | AST.XData -> (fun _ -> Types.None)
 359    | AST.Code -> (fun _ -> Types.Some bl)) __
 360
 361 (** val block_of_funct_id :
 362     'a1 Globalenvs.genv_t -> PreIdentifiers.identifier -> Pointers.block
 363     Types.sig0 Errors.res **)
 364 let block_of_funct_id ge0 id =
 365   Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction),
 366     (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))
 367     (Obj.magic
 368       (Monad.m_bind0 (Monad.max_def Option.option)
 369         (Obj.magic (Globalenvs.find_symbol ge0 id)) (fun bl ->
 370         Obj.magic (code_block_of_block bl))))
 371
 372 (** val gen_pc_from_label :
 373     AST.ident List.list -> 'a1 genv_gen -> AST.ident -> Graphs.label ->
 374     ByteValues.program_counter Errors.res **)
 375 let gen_pc_from_label g ge0 id lbl =
 376   Obj.magic
 377     (Monad.m_bind0 (Monad.max_def Errors.res0)
 378       (Obj.magic (block_of_funct_id ge0.ge id)) (fun bl ->
 379       Monad.m_bind2 (Monad.max_def Errors.res0)
 380         (Obj.magic (fetch_internal_function g ge0 bl)) (fun ignore f_def ->
 381         Obj.magic
 382           (Errors.opt_to_res (List.Cons ((Errors.MSG
 383             ErrorMessages.LabelNotFound), (List.Cons ((Errors.CTX
 384             (PreIdentifiers.LabelTag, lbl)), List.Nil))))
 385             (ge0.pc_from_label bl f_def lbl)))))
 386
 387 type genv = Joint.joint_closed_internal_function genv_gen
 388
 389 type sem_state_params = { empty_framesT : __;
 390                           empty_regsT : (ByteValues.xpointer -> __);
 391                           load_sp : (__ -> ByteValues.xpointer Errors.res);
 392                           save_sp : (__ -> ByteValues.xpointer -> __) }
 393
 394 (** val sem_state_params_rect_Type4 :
 395     (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
 396     ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
 397     'a1) -> sem_state_params -> 'a1 **)
 398 let rec sem_state_params_rect_Type4 h_mk_sem_state_params x_24507 =
 399   let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
 400     load_sp0; save_sp = save_sp0 } = x_24507
 401   in
 402   h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
 403
 404 (** val sem_state_params_rect_Type5 :
 405     (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
 406     ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
 407     'a1) -> sem_state_params -> 'a1 **)
 408 let rec sem_state_params_rect_Type5 h_mk_sem_state_params x_24509 =
 409   let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
 410     load_sp0; save_sp = save_sp0 } = x_24509
 411   in
 412   h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
 413
 414 (** val sem_state_params_rect_Type3 :
 415     (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
 416     ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
 417     'a1) -> sem_state_params -> 'a1 **)
 418 let rec sem_state_params_rect_Type3 h_mk_sem_state_params x_24511 =
 419   let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
 420     load_sp0; save_sp = save_sp0 } = x_24511
 421   in
 422   h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
 423
 424 (** val sem_state_params_rect_Type2 :
 425     (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
 426     ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
 427     'a1) -> sem_state_params -> 'a1 **)
 428 let rec sem_state_params_rect_Type2 h_mk_sem_state_params x_24513 =
 429   let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
 430     load_sp0; save_sp = save_sp0 } = x_24513
 431   in
 432   h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
 433
 434 (** val sem_state_params_rect_Type1 :
 435     (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
 436     ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
 437     'a1) -> sem_state_params -> 'a1 **)
 438 let rec sem_state_params_rect_Type1 h_mk_sem_state_params x_24515 =
 439   let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
 440     load_sp0; save_sp = save_sp0 } = x_24515
 441   in
 442   h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
 443
 444 (** val sem_state_params_rect_Type0 :
 445     (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
 446     ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
 447     'a1) -> sem_state_params -> 'a1 **)
 448 let rec sem_state_params_rect_Type0 h_mk_sem_state_params x_24517 =
 449   let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
 450     load_sp0; save_sp = save_sp0 } = x_24517
 451   in
 452   h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
 453
 454 type framesT = __
 455
 456 (** val empty_framesT : sem_state_params -> __ **)
 457 let rec empty_framesT xxx =
 458   xxx.empty_framesT
 459
 460 type regsT = __
 461
 462 (** val empty_regsT : sem_state_params -> ByteValues.xpointer -> __ **)
 463 let rec empty_regsT xxx =
 464   xxx.empty_regsT
 465
 466 (** val load_sp :
 467     sem_state_params -> __ -> ByteValues.xpointer Errors.res **)
 468 let rec load_sp xxx =
 469   xxx.load_sp
 470
 471 (** val save_sp : sem_state_params -> __ -> ByteValues.xpointer -> __ **)
 472 let rec save_sp xxx =
 473   xxx.save_sp
 474
 475 (** val sem_state_params_inv_rect_Type4 :
 476     sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
 477     -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __)
 478     -> __ -> 'a1) -> 'a1 **)
 479 let sem_state_params_inv_rect_Type4 hterm h1 =
 480   let hcut = sem_state_params_rect_Type4 h1 hterm in hcut __
 481
 482 (** val sem_state_params_inv_rect_Type3 :
 483     sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
 484     -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __)
 485     -> __ -> 'a1) -> 'a1 **)
 486 let sem_state_params_inv_rect_Type3 hterm h1 =
 487   let hcut = sem_state_params_rect_Type3 h1 hterm in hcut __
 488
 489 (** val sem_state_params_inv_rect_Type2 :
 490     sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
 491     -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __)
 492     -> __ -> 'a1) -> 'a1 **)
 493 let sem_state_params_inv_rect_Type2 hterm h1 =
 494   let hcut = sem_state_params_rect_Type2 h1 hterm in hcut __
 495
 496 (** val sem_state_params_inv_rect_Type1 :
 497     sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
 498     -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __)
 499     -> __ -> 'a1) -> 'a1 **)
 500 let sem_state_params_inv_rect_Type1 hterm h1 =
 501   let hcut = sem_state_params_rect_Type1 h1 hterm in hcut __
 502
 503 (** val sem_state_params_inv_rect_Type0 :
 504     sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
 505     -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __)
 506     -> __ -> 'a1) -> 'a1 **)
 507 let sem_state_params_inv_rect_Type0 hterm h1 =
 508   let hcut = sem_state_params_rect_Type0 h1 hterm in hcut __
 509
 510 (** val sem_state_params_jmdiscr :
 511     sem_state_params -> sem_state_params -> __ **)
 512 let sem_state_params_jmdiscr x y =
 513   Logic.eq_rect_Type2 x
 514     (let { empty_framesT = a1; empty_regsT = a3; load_sp = a4; save_sp =
 515        a5 } = x
 516      in
 517     Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
 518
 519 type internal_stack =
 520 | Empty_is
 521 | One_is of ByteValues.beval
 522 | Both_is of ByteValues.beval * ByteValues.beval
 523
 524 (** val internal_stack_rect_Type4 :
 525     'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
 526     -> 'a1) -> internal_stack -> 'a1 **)
 527 let rec internal_stack_rect_Type4 h_empty_is h_one_is h_both_is = function
 528 | Empty_is -> h_empty_is
 529 | One_is x_24543 -> h_one_is x_24543
 530 | Both_is (x_24545, x_24544) -> h_both_is x_24545 x_24544
 531
 532 (** val internal_stack_rect_Type5 :
 533     'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
 534     -> 'a1) -> internal_stack -> 'a1 **)
 535 let rec internal_stack_rect_Type5 h_empty_is h_one_is h_both_is = function
 536 | Empty_is -> h_empty_is
 537 | One_is x_24550 -> h_one_is x_24550
 538 | Both_is (x_24552, x_24551) -> h_both_is x_24552 x_24551
 539
 540 (** val internal_stack_rect_Type3 :
 541     'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
 542     -> 'a1) -> internal_stack -> 'a1 **)
 543 let rec internal_stack_rect_Type3 h_empty_is h_one_is h_both_is = function
 544 | Empty_is -> h_empty_is
 545 | One_is x_24557 -> h_one_is x_24557
 546 | Both_is (x_24559, x_24558) -> h_both_is x_24559 x_24558
 547
 548 (** val internal_stack_rect_Type2 :
 549     'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
 550     -> 'a1) -> internal_stack -> 'a1 **)
 551 let rec internal_stack_rect_Type2 h_empty_is h_one_is h_both_is = function
 552 | Empty_is -> h_empty_is
 553 | One_is x_24564 -> h_one_is x_24564
 554 | Both_is (x_24566, x_24565) -> h_both_is x_24566 x_24565
 555
 556 (** val internal_stack_rect_Type1 :
 557     'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
 558     -> 'a1) -> internal_stack -> 'a1 **)
 559 let rec internal_stack_rect_Type1 h_empty_is h_one_is h_both_is = function
 560 | Empty_is -> h_empty_is
 561 | One_is x_24571 -> h_one_is x_24571
 562 | Both_is (x_24573, x_24572) -> h_both_is x_24573 x_24572
 563
 564 (** val internal_stack_rect_Type0 :
 565     'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
 566     -> 'a1) -> internal_stack -> 'a1 **)
 567 let rec internal_stack_rect_Type0 h_empty_is h_one_is h_both_is = function
 568 | Empty_is -> h_empty_is
 569 | One_is x_24578 -> h_one_is x_24578
 570 | Both_is (x_24580, x_24579) -> h_both_is x_24580 x_24579
 571
 572 (** val internal_stack_inv_rect_Type4 :
 573     internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
 574     (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1 **)
 575 let internal_stack_inv_rect_Type4 hterm h1 h2 h3 =
 576   let hcut = internal_stack_rect_Type4 h1 h2 h3 hterm in hcut __
 577
 578 (** val internal_stack_inv_rect_Type3 :
 579     internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
 580     (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1 **)
 581 let internal_stack_inv_rect_Type3 hterm h1 h2 h3 =
 582   let hcut = internal_stack_rect_Type3 h1 h2 h3 hterm in hcut __
 583
 584 (** val internal_stack_inv_rect_Type2 :
 585     internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
 586     (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1 **)
 587 let internal_stack_inv_rect_Type2 hterm h1 h2 h3 =
 588   let hcut = internal_stack_rect_Type2 h1 h2 h3 hterm in hcut __
 589
 590 (** val internal_stack_inv_rect_Type1 :
 591     internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
 592     (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1 **)
 593 let internal_stack_inv_rect_Type1 hterm h1 h2 h3 =
 594   let hcut = internal_stack_rect_Type1 h1 h2 h3 hterm in hcut __
 595
 596 (** val internal_stack_inv_rect_Type0 :
 597     internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
 598     (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1 **)
 599 let internal_stack_inv_rect_Type0 hterm h1 h2 h3 =
 600   let hcut = internal_stack_rect_Type0 h1 h2 h3 hterm in hcut __
 601
 602 (** val internal_stack_discr : internal_stack -> internal_stack -> __ **)
 603 let internal_stack_discr x y =
 604   Logic.eq_rect_Type2 x
 605     (match x with
 606      | Empty_is -> Obj.magic (fun _ dH -> dH)
 607      | One_is a0 -> Obj.magic (fun _ dH -> dH __)
 608      | Both_is (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
 609
 610 (** val internal_stack_jmdiscr : internal_stack -> internal_stack -> __ **)
 611 let internal_stack_jmdiscr x y =
 612   Logic.eq_rect_Type2 x
 613     (match x with
 614      | Empty_is -> Obj.magic (fun _ dH -> dH)
 615      | One_is a0 -> Obj.magic (fun _ dH -> dH __)
 616      | Both_is (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
 617
 618 (** val is_push :
 619     internal_stack -> ByteValues.beval -> internal_stack Errors.res **)
 620 let is_push is bv =
 621   match is with
 622   | Empty_is ->
 623     Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) (One_is bv))
 624   | One_is bv' ->
 625     Obj.magic
 626       (Monad.m_return0 (Monad.max_def Errors.res0) (Both_is (bv', bv)))
 627   | Both_is (x, x0) ->
 628     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.InternalStackFull),
 629       List.Nil))
 630
 631 (** val is_pop :
 632     internal_stack -> (ByteValues.beval, internal_stack) Types.prod
 633     Errors.res **)
 634 let is_pop = function
 635 | Empty_is ->
 636   Errors.Error (List.Cons ((Errors.MSG ErrorMessages.InternalStackEmpty),
 637     List.Nil))
 638 | One_is bv' ->
 639   Obj.magic
 640     (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = bv';
 641       Types.snd = Empty_is })
 642 | Both_is (bv, bv') ->
 643   Obj.magic
 644     (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = bv';
 645       Types.snd = (One_is bv) })
 646
 647 type state = { st_frms : __ Types.option; istack : internal_stack;
 648                carry : ByteValues.bebit; regs : __; m : BEMem.bemem;
 649                stack_usage : Nat.nat }
 650
 651 (** val state_rect_Type4 :
 652     sem_state_params -> (__ Types.option -> internal_stack ->
 653     ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
 654 let rec state_rect_Type4 semp h_mk_state x_24628 =
 655   let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
 656     m = m0; stack_usage = stack_usage0 } = x_24628
 657   in
 658   h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
 659
 660 (** val state_rect_Type5 :
 661     sem_state_params -> (__ Types.option -> internal_stack ->
 662     ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
 663 let rec state_rect_Type5 semp h_mk_state x_24630 =
 664   let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
 665     m = m0; stack_usage = stack_usage0 } = x_24630
 666   in
 667   h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
 668
 669 (** val state_rect_Type3 :
 670     sem_state_params -> (__ Types.option -> internal_stack ->
 671     ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
 672 let rec state_rect_Type3 semp h_mk_state x_24632 =
 673   let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
 674     m = m0; stack_usage = stack_usage0 } = x_24632
 675   in
 676   h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
 677
 678 (** val state_rect_Type2 :
 679     sem_state_params -> (__ Types.option -> internal_stack ->
 680     ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
 681 let rec state_rect_Type2 semp h_mk_state x_24634 =
 682   let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
 683     m = m0; stack_usage = stack_usage0 } = x_24634
 684   in
 685   h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
 686
 687 (** val state_rect_Type1 :
 688     sem_state_params -> (__ Types.option -> internal_stack ->
 689     ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
 690 let rec state_rect_Type1 semp h_mk_state x_24636 =
 691   let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
 692     m = m0; stack_usage = stack_usage0 } = x_24636
 693   in
 694   h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
 695
 696 (** val state_rect_Type0 :
 697     sem_state_params -> (__ Types.option -> internal_stack ->
 698     ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
 699 let rec state_rect_Type0 semp h_mk_state x_24638 =
 700   let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
 701     m = m0; stack_usage = stack_usage0 } = x_24638
 702   in
 703   h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
 704
 705 (** val st_frms : sem_state_params -> state -> __ Types.option **)
 706 let rec st_frms semp xxx =
 707   xxx.st_frms
 708
 709 (** val istack : sem_state_params -> state -> internal_stack **)
 710 let rec istack semp xxx =
 711   xxx.istack
 712
 713 (** val carry : sem_state_params -> state -> ByteValues.bebit **)
 714 let rec carry semp xxx =
 715   xxx.carry
 716
 717 (** val regs : sem_state_params -> state -> __ **)
 718 let rec regs semp xxx =
 719   xxx.regs
 720
 721 (** val m : sem_state_params -> state -> BEMem.bemem **)
 722 let rec m semp xxx =
 723   xxx.m
 724
 725 (** val stack_usage : sem_state_params -> state -> Nat.nat **)
 726 let rec stack_usage semp xxx =
 727   xxx.stack_usage
 728
 729 (** val state_inv_rect_Type4 :
 730     sem_state_params -> state -> (__ Types.option -> internal_stack ->
 731     ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1 **)
 732 let state_inv_rect_Type4 x1 hterm h1 =
 733   let hcut = state_rect_Type4 x1 h1 hterm in hcut __
 734
 735 (** val state_inv_rect_Type3 :
 736     sem_state_params -> state -> (__ Types.option -> internal_stack ->
 737     ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1 **)
 738 let state_inv_rect_Type3 x1 hterm h1 =
 739   let hcut = state_rect_Type3 x1 h1 hterm in hcut __
 740
 741 (** val state_inv_rect_Type2 :
 742     sem_state_params -> state -> (__ Types.option -> internal_stack ->
 743     ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1 **)
 744 let state_inv_rect_Type2 x1 hterm h1 =
 745   let hcut = state_rect_Type2 x1 h1 hterm in hcut __
 746
 747 (** val state_inv_rect_Type1 :
 748     sem_state_params -> state -> (__ Types.option -> internal_stack ->
 749     ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1 **)
 750 let state_inv_rect_Type1 x1 hterm h1 =
 751   let hcut = state_rect_Type1 x1 h1 hterm in hcut __
 752
 753 (** val state_inv_rect_Type0 :
 754     sem_state_params -> state -> (__ Types.option -> internal_stack ->
 755     ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1 **)
 756 let state_inv_rect_Type0 x1 hterm h1 =
 757   let hcut = state_rect_Type0 x1 h1 hterm in hcut __
 758
 759 (** val state_jmdiscr : sem_state_params -> state -> state -> __ **)
 760 let state_jmdiscr a1 x y =
 761   Logic.eq_rect_Type2 x
 762     (let { st_frms = a0; istack = a10; carry = a2; regs = a3; m = a4;
 763        stack_usage = a5 } = x
 764      in
 765     Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
 766
 767 (** val sp : sem_state_params -> state -> ByteValues.xpointer Errors.res **)
 768 let sp p st =
 769   p.load_sp st.regs
 770
 771 type state_pc = { st_no_pc : state; pc : ByteValues.program_counter;
 772                   last_pop : ByteValues.program_counter }
 773
 774 (** val state_pc_rect_Type4 :
 775     sem_state_params -> (state -> ByteValues.program_counter ->
 776     ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
 777 let rec state_pc_rect_Type4 semp h_mk_state_pc x_24654 =
 778   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_24654 in
 779   h_mk_state_pc st_no_pc0 pc0 last_pop0
 780
 781 (** val state_pc_rect_Type5 :
 782     sem_state_params -> (state -> ByteValues.program_counter ->
 783     ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
 784 let rec state_pc_rect_Type5 semp h_mk_state_pc x_24656 =
 785   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_24656 in
 786   h_mk_state_pc st_no_pc0 pc0 last_pop0
 787
 788 (** val state_pc_rect_Type3 :
 789     sem_state_params -> (state -> ByteValues.program_counter ->
 790     ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
 791 let rec state_pc_rect_Type3 semp h_mk_state_pc x_24658 =
 792   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_24658 in
 793   h_mk_state_pc st_no_pc0 pc0 last_pop0
 794
 795 (** val state_pc_rect_Type2 :
 796     sem_state_params -> (state -> ByteValues.program_counter ->
 797     ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
 798 let rec state_pc_rect_Type2 semp h_mk_state_pc x_24660 =
 799   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_24660 in
 800   h_mk_state_pc st_no_pc0 pc0 last_pop0
 801
 802 (** val state_pc_rect_Type1 :
 803     sem_state_params -> (state -> ByteValues.program_counter ->
 804     ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
 805 let rec state_pc_rect_Type1 semp h_mk_state_pc x_24662 =
 806   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_24662 in
 807   h_mk_state_pc st_no_pc0 pc0 last_pop0
 808
 809 (** val state_pc_rect_Type0 :
 810     sem_state_params -> (state -> ByteValues.program_counter ->
 811     ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
 812 let rec state_pc_rect_Type0 semp h_mk_state_pc x_24664 =
 813   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_24664 in
 814   h_mk_state_pc st_no_pc0 pc0 last_pop0
 815
 816 (** val st_no_pc : sem_state_params -> state_pc -> state **)
 817 let rec st_no_pc semp xxx =
 818   xxx.st_no_pc
 819
 820 (** val pc : sem_state_params -> state_pc -> ByteValues.program_counter **)
 821 let rec pc semp xxx =
 822   xxx.pc
 823
 824 (** val last_pop :
 825     sem_state_params -> state_pc -> ByteValues.program_counter **)
 826 let rec last_pop semp xxx =
 827   xxx.last_pop
 828
 829 (** val state_pc_inv_rect_Type4 :
 830     sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
 831     ByteValues.program_counter -> __ -> 'a1) -> 'a1 **)
 832 let state_pc_inv_rect_Type4 x1 hterm h1 =
 833   let hcut = state_pc_rect_Type4 x1 h1 hterm in hcut __
 834
 835 (** val state_pc_inv_rect_Type3 :
 836     sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
 837     ByteValues.program_counter -> __ -> 'a1) -> 'a1 **)
 838 let state_pc_inv_rect_Type3 x1 hterm h1 =
 839   let hcut = state_pc_rect_Type3 x1 h1 hterm in hcut __
 840
 841 (** val state_pc_inv_rect_Type2 :
 842     sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
 843     ByteValues.program_counter -> __ -> 'a1) -> 'a1 **)
 844 let state_pc_inv_rect_Type2 x1 hterm h1 =
 845   let hcut = state_pc_rect_Type2 x1 h1 hterm in hcut __
 846
 847 (** val state_pc_inv_rect_Type1 :
 848     sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
 849     ByteValues.program_counter -> __ -> 'a1) -> 'a1 **)
 850 let state_pc_inv_rect_Type1 x1 hterm h1 =
 851   let hcut = state_pc_rect_Type1 x1 h1 hterm in hcut __
 852
 853 (** val state_pc_inv_rect_Type0 :
 854     sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
 855     ByteValues.program_counter -> __ -> 'a1) -> 'a1 **)
 856 let state_pc_inv_rect_Type0 x1 hterm h1 =
 857   let hcut = state_pc_rect_Type0 x1 h1 hterm in hcut __
 858
 859 (** val state_pc_discr : sem_state_params -> state_pc -> state_pc -> __ **)
 860 let state_pc_discr a1 x y =
 861   Logic.eq_rect_Type2 x
 862     (let { st_no_pc = a0; pc = a10; last_pop = a2 } = x in
 863     Obj.magic (fun _ dH -> dH __ __ __)) y
 864
 865 (** val state_pc_jmdiscr : sem_state_params -> state_pc -> state_pc -> __ **)
 866 let state_pc_jmdiscr a1 x y =
 867   Logic.eq_rect_Type2 x
 868     (let { st_no_pc = a0; pc = a10; last_pop = a2 } = x in
 869     Obj.magic (fun _ dH -> dH __ __ __)) y
 870
 871 (** val dpi1__o__st_no_pc__o__inject :
 872     sem_state_params -> (state_pc, 'a1) Types.dPair -> state Types.sig0 **)
 873 let dpi1__o__st_no_pc__o__inject x0 x3 =
 874   x3.Types.dpi1.st_no_pc
 875
 876 (** val eject__o__st_no_pc__o__inject :
 877     sem_state_params -> state_pc Types.sig0 -> state Types.sig0 **)
 878 let eject__o__st_no_pc__o__inject x0 x3 =
 879   (Types.pi1 x3).st_no_pc
 880
 881 (** val st_no_pc__o__inject :
 882     sem_state_params -> state_pc -> state Types.sig0 **)
 883 let st_no_pc__o__inject x0 x2 =
 884   x2.st_no_pc
 885
 886 (** val dpi1__o__st_no_pc :
 887     sem_state_params -> (state_pc, 'a1) Types.dPair -> state **)
 888 let dpi1__o__st_no_pc x0 x2 =
 889   x2.Types.dpi1.st_no_pc
 890
 891 (** val eject__o__st_no_pc :
 892     sem_state_params -> state_pc Types.sig0 -> state **)
 893 let eject__o__st_no_pc x0 x2 =
 894   (Types.pi1 x2).st_no_pc
 895
 896 (** val init_pc : ByteValues.program_counter **)
 897 let init_pc =
 898   { ByteValues.pc_block = (Z.zopp (Z.z_of_nat (Nat.S Nat.O)));
 899     ByteValues.pc_offset = Positive.One }
 900
 901 (** val null_pc : Positive.pos -> ByteValues.program_counter **)
 902 let null_pc pos =
 903   { ByteValues.pc_block = Pointers.dummy_block_code; ByteValues.pc_offset =
 904     pos }
 905
 906 (** val set_m : sem_state_params -> BEMem.bemem -> state -> state **)
 907 let set_m p m0 st =
 908   { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs =
 909     st.regs; m = m0; stack_usage = st.stack_usage }
 910
 911 (** val set_regs : sem_state_params -> __ -> state -> state **)
 912 let set_regs p regs0 st =
 913   { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs = regs0;
 914     m = st.m; stack_usage = st.stack_usage }
 915
 916 (** val set_sp :
 917     sem_state_params -> ByteValues.xpointer -> state -> state **)
 918 let set_sp p sp0 st =
 919   let regs' = p.save_sp st.regs sp0 in
 920   { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs = regs';
 921   m = st.m; stack_usage = st.stack_usage }
 922
 923 (** val set_carry :
 924     sem_state_params -> ByteValues.bebit -> state -> state **)
 925 let set_carry p carry0 st =
 926   { st_frms = st.st_frms; istack = st.istack; carry = carry0; regs = st.regs;
 927     m = st.m; stack_usage = st.stack_usage }
 928
 929 (** val set_istack : sem_state_params -> internal_stack -> state -> state **)
 930 let set_istack p is st =
 931   { st_frms = st.st_frms; istack = is; carry = st.carry; regs = st.regs; m =
 932     st.m; stack_usage = st.stack_usage }
 933
 934 (** val set_pc :
 935     sem_state_params -> ByteValues.program_counter -> state_pc -> state_pc **)
 936 let set_pc p pc0 st =
 937   { st_no_pc = st.st_no_pc; pc = pc0; last_pop = st.last_pop }
 938
 939 (** val set_no_pc : sem_state_params -> state -> state_pc -> state_pc **)
 940 let set_no_pc p s st =
 941   { st_no_pc = s; pc = st.pc; last_pop = st.last_pop }
 942
 943 (** val set_last_pop :
 944     sem_state_params -> state -> ByteValues.program_counter -> state_pc **)
 945 let set_last_pop p st pc0 =
 946   { st_no_pc = st; pc = pc0; last_pop = pc0 }
 947
 948 (** val set_frms : sem_state_params -> __ -> state -> state **)
 949 let set_frms p frms st =
 950   { st_frms = (Types.Some frms); istack = st.istack; carry = st.carry; regs =
 951     st.regs; m = st.m; stack_usage = st.stack_usage }
 952
 953 type call_kind =
 954 | PTR
 955 | ID
 956
 957 (** val call_kind_rect_Type4 : 'a1 -> 'a1 -> call_kind -> 'a1 **)
 958 let rec call_kind_rect_Type4 h_PTR h_ID = function
 959 | PTR -> h_PTR
 960 | ID -> h_ID
 961
 962 (** val call_kind_rect_Type5 : 'a1 -> 'a1 -> call_kind -> 'a1 **)
 963 let rec call_kind_rect_Type5 h_PTR h_ID = function
 964 | PTR -> h_PTR
 965 | ID -> h_ID
 966
 967 (** val call_kind_rect_Type3 : 'a1 -> 'a1 -> call_kind -> 'a1 **)
 968 let rec call_kind_rect_Type3 h_PTR h_ID = function
 969 | PTR -> h_PTR
 970 | ID -> h_ID
 971
 972 (** val call_kind_rect_Type2 : 'a1 -> 'a1 -> call_kind -> 'a1 **)
 973 let rec call_kind_rect_Type2 h_PTR h_ID = function
 974 | PTR -> h_PTR
 975 | ID -> h_ID
 976
 977 (** val call_kind_rect_Type1 : 'a1 -> 'a1 -> call_kind -> 'a1 **)
 978 let rec call_kind_rect_Type1 h_PTR h_ID = function
 979 | PTR -> h_PTR
 980 | ID -> h_ID
 981
 982 (** val call_kind_rect_Type0 : 'a1 -> 'a1 -> call_kind -> 'a1 **)
 983 let rec call_kind_rect_Type0 h_PTR h_ID = function
 984 | PTR -> h_PTR
 985 | ID -> h_ID
 986
 987 (** val call_kind_inv_rect_Type4 :
 988     call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 989 let call_kind_inv_rect_Type4 hterm h1 h2 =
 990   let hcut = call_kind_rect_Type4 h1 h2 hterm in hcut __
 991
 992 (** val call_kind_inv_rect_Type3 :
 993     call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 994 let call_kind_inv_rect_Type3 hterm h1 h2 =
 995   let hcut = call_kind_rect_Type3 h1 h2 hterm in hcut __
 996
 997 (** val call_kind_inv_rect_Type2 :
 998     call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 999 let call_kind_inv_rect_Type2 hterm h1 h2 =
1000   let hcut = call_kind_rect_Type2 h1 h2 hterm in hcut __
1001
1002 (** val call_kind_inv_rect_Type1 :
1003     call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
1004 let call_kind_inv_rect_Type1 hterm h1 h2 =
1005   let hcut = call_kind_rect_Type1 h1 h2 hterm in hcut __
1006
1007 (** val call_kind_inv_rect_Type0 :
1008     call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
1009 let call_kind_inv_rect_Type0 hterm h1 h2 =
1010   let hcut = call_kind_rect_Type0 h1 h2 hterm in hcut __
1011
1012 (** val call_kind_discr : call_kind -> call_kind -> __ **)
1013 let call_kind_discr x y =
1014   Logic.eq_rect_Type2 x
1015     (match x with
1016      | PTR -> Obj.magic (fun _ dH -> dH)
1017      | ID -> Obj.magic (fun _ dH -> dH)) y
1018
1019 (** val call_kind_jmdiscr : call_kind -> call_kind -> __ **)
1020 let call_kind_jmdiscr x y =
1021   Logic.eq_rect_Type2 x
1022     (match x with
1023      | PTR -> Obj.magic (fun _ dH -> dH)
1024      | ID -> Obj.magic (fun _ dH -> dH)) y
1025
1026 (** val kind_of_call :
1027     Joint.unserialized_params -> (AST.ident, (__, __) Types.prod) Types.sum
1028     -> call_kind **)
1029 let kind_of_call p = function
1030 | Types.Inl x -> ID
1031 | Types.Inr x -> PTR
1032
1033 type 'f sem_unserialized_params = { st_pars : sem_state_params;
1034                                     acca_store_ : (__ -> ByteValues.beval ->
1035                                                   __ -> __ Errors.res);
1036                                     acca_retrieve_ : (__ -> __ ->
1037                                                      ByteValues.beval
1038                                                      Errors.res);
1039                                     acca_arg_retrieve_ : (__ -> __ ->
1040                                                          ByteValues.beval
1041                                                          Errors.res);
1042                                     accb_store_ : (__ -> ByteValues.beval ->
1043                                                   __ -> __ Errors.res);
1044                                     accb_retrieve_ : (__ -> __ ->
1045                                                      ByteValues.beval
1046                                                      Errors.res);
1047                                     accb_arg_retrieve_ : (__ -> __ ->
1048                                                          ByteValues.beval
1049                                                          Errors.res);
1050                                     dpl_store_ : (__ -> ByteValues.beval ->
1051                                                  __ -> __ Errors.res);
1052                                     dpl_retrieve_ : (__ -> __ ->
1053                                                     ByteValues.beval
1054                                                     Errors.res);
1055                                     dpl_arg_retrieve_ : (__ -> __ ->
1056                                                         ByteValues.beval
1057                                                         Errors.res);
1058                                     dph_store_ : (__ -> ByteValues.beval ->
1059                                                  __ -> __ Errors.res);
1060                                     dph_retrieve_ : (__ -> __ ->
1061                                                     ByteValues.beval
1062                                                     Errors.res);
1063                                     dph_arg_retrieve_ : (__ -> __ ->
1064                                                         ByteValues.beval
1065                                                         Errors.res);
1066                                     snd_arg_retrieve_ : (__ -> __ ->
1067                                                         ByteValues.beval
1068                                                         Errors.res);
1069                                     pair_reg_move_ : (__ -> __ -> __
1070                                                      Errors.res);
1071                                     save_frame : (call_kind -> __ -> state_pc
1072                                                  -> state Errors.res);
1073                                     setup_call : (Nat.nat -> __ -> __ ->
1074                                                  state -> state Errors.res);
1075                                     fetch_external_args : (AST.external_function
1076                                                           -> state -> __ ->
1077                                                           Values.val0
1078                                                           List.list
1079                                                           Errors.res);
1080                                     set_result : (Values.val0 List.list -> __
1081                                                  -> state -> state
1082                                                  Errors.res);
1083                                     call_args_for_main : __;
1084                                     call_dest_for_main : __;
1085                                     read_result : (AST.ident List.list -> 'f
1086                                                   AST.fundef
1087                                                   Globalenvs.genv_t -> __ ->
1088                                                   state -> ByteValues.beval
1089                                                   List.list Errors.res);
1090                                     eval_ext_seq : (AST.ident List.list -> 'f
1091                                                    genv_gen -> __ ->
1092                                                    AST.ident -> state ->
1093                                                    state Errors.res);
1094                                     pop_frame : (AST.ident List.list -> 'f
1095                                                 genv_gen -> AST.ident -> __
1096                                                 -> state -> (state,
1097                                                 ByteValues.program_counter)
1098                                                 Types.prod Errors.res) }
1099
1100 (** val sem_unserialized_params_rect_Type4 :
1101     Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
1102     -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) ->
1103     (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval ->
1104     __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
1105     -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
1106     __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __
1107     -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1108     Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1109     ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1110     -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1111     Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1112     (AST.external_function -> state -> __ -> Values.val0 List.list
1113     Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1114     -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1115     -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1116     List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1117     Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1118     state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
1119     'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
1120 let rec sem_unserialized_params_rect_Type4 uns_pars h_mk_sem_unserialized_params x_24719 =
1121   let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
1122     acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
1123     accb_store_0; accb_retrieve_ = accb_retrieve_0; accb_arg_retrieve_ =
1124     accb_arg_retrieve_0; dpl_store_ = dpl_store_0; dpl_retrieve_ =
1125     dpl_retrieve_0; dpl_arg_retrieve_ = dpl_arg_retrieve_0; dph_store_ =
1126     dph_store_0; dph_retrieve_ = dph_retrieve_0; dph_arg_retrieve_ =
1127     dph_arg_retrieve_0; snd_arg_retrieve_ = snd_arg_retrieve_0;
1128     pair_reg_move_ = pair_reg_move_0; save_frame = save_frame0; setup_call =
1129     setup_call0; fetch_external_args = fetch_external_args0; set_result =
1130     set_result0; call_args_for_main = call_args_for_main0;
1131     call_dest_for_main = call_dest_for_main0; read_result = read_result0;
1132     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_24719
1133   in
1134   h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
1135     acca_arg_retrieve_0 accb_store_0 accb_retrieve_0 accb_arg_retrieve_0
1136     dpl_store_0 dpl_retrieve_0 dpl_arg_retrieve_0 dph_store_0 dph_retrieve_0
1137     dph_arg_retrieve_0 snd_arg_retrieve_0 pair_reg_move_0 save_frame0
1138     setup_call0 fetch_external_args0 set_result0 call_args_for_main0
1139     call_dest_for_main0 read_result0 eval_ext_seq0 pop_frame0
1140
1141 (** val sem_unserialized_params_rect_Type5 :
1142     Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
1143     -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) ->
1144     (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval ->
1145     __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
1146     -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
1147     __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __
1148     -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1149     Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1150     ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1151     -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1152     Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1153     (AST.external_function -> state -> __ -> Values.val0 List.list
1154     Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1155     -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1156     -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1157     List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1158     Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1159     state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
1160     'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
1161 let rec sem_unserialized_params_rect_Type5 uns_pars h_mk_sem_unserialized_params x_24721 =
1162   let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
1163     acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
1164     accb_store_0; accb_retrieve_ = accb_retrieve_0; accb_arg_retrieve_ =
1165     accb_arg_retrieve_0; dpl_store_ = dpl_store_0; dpl_retrieve_ =
1166     dpl_retrieve_0; dpl_arg_retrieve_ = dpl_arg_retrieve_0; dph_store_ =
1167     dph_store_0; dph_retrieve_ = dph_retrieve_0; dph_arg_retrieve_ =
1168     dph_arg_retrieve_0; snd_arg_retrieve_ = snd_arg_retrieve_0;
1169     pair_reg_move_ = pair_reg_move_0; save_frame = save_frame0; setup_call =
1170     setup_call0; fetch_external_args = fetch_external_args0; set_result =
1171     set_result0; call_args_for_main = call_args_for_main0;
1172     call_dest_for_main = call_dest_for_main0; read_result = read_result0;
1173     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_24721
1174   in
1175   h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
1176     acca_arg_retrieve_0 accb_store_0 accb_retrieve_0 accb_arg_retrieve_0
1177     dpl_store_0 dpl_retrieve_0 dpl_arg_retrieve_0 dph_store_0 dph_retrieve_0
1178     dph_arg_retrieve_0 snd_arg_retrieve_0 pair_reg_move_0 save_frame0
1179     setup_call0 fetch_external_args0 set_result0 call_args_for_main0
1180     call_dest_for_main0 read_result0 eval_ext_seq0 pop_frame0
1181
1182 (** val sem_unserialized_params_rect_Type3 :
1183     Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
1184     -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) ->
1185     (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval ->
1186     __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
1187     -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
1188     __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __
1189     -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1190     Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1191     ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1192     -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1193     Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1194     (AST.external_function -> state -> __ -> Values.val0 List.list
1195     Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1196     -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1197     -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1198     List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1199     Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1200     state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
1201     'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
1202 let rec sem_unserialized_params_rect_Type3 uns_pars h_mk_sem_unserialized_params x_24723 =
1203   let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
1204     acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
1205     accb_store_0; accb_retrieve_ = accb_retrieve_0; accb_arg_retrieve_ =
1206     accb_arg_retrieve_0; dpl_store_ = dpl_store_0; dpl_retrieve_ =
1207     dpl_retrieve_0; dpl_arg_retrieve_ = dpl_arg_retrieve_0; dph_store_ =
1208     dph_store_0; dph_retrieve_ = dph_retrieve_0; dph_arg_retrieve_ =
1209     dph_arg_retrieve_0; snd_arg_retrieve_ = snd_arg_retrieve_0;
1210     pair_reg_move_ = pair_reg_move_0; save_frame = save_frame0; setup_call =
1211     setup_call0; fetch_external_args = fetch_external_args0; set_result =
1212     set_result0; call_args_for_main = call_args_for_main0;
1213     call_dest_for_main = call_dest_for_main0; read_result = read_result0;
1214     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_24723
1215   in
1216   h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
1217     acca_arg_retrieve_0 accb_store_0 accb_retrieve_0 accb_arg_retrieve_0
1218     dpl_store_0 dpl_retrieve_0 dpl_arg_retrieve_0 dph_store_0 dph_retrieve_0
1219     dph_arg_retrieve_0 snd_arg_retrieve_0 pair_reg_move_0 save_frame0
1220     setup_call0 fetch_external_args0 set_result0 call_args_for_main0
1221     call_dest_for_main0 read_result0 eval_ext_seq0 pop_frame0
1222
1223 (** val sem_unserialized_params_rect_Type2 :
1224     Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
1225     -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) ->
1226     (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval ->
1227     __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
1228     -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
1229     __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __
1230     -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1231     Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1232     ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1233     -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1234     Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1235     (AST.external_function -> state -> __ -> Values.val0 List.list
1236     Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1237     -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1238     -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1239     List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1240     Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1241     state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
1242     'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
1243 let rec sem_unserialized_params_rect_Type2 uns_pars h_mk_sem_unserialized_params x_24725 =
1244   let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
1245     acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
1246     accb_store_0; accb_retrieve_ = accb_retrieve_0; accb_arg_retrieve_ =
1247     accb_arg_retrieve_0; dpl_store_ = dpl_store_0; dpl_retrieve_ =
1248     dpl_retrieve_0; dpl_arg_retrieve_ = dpl_arg_retrieve_0; dph_store_ =
1249     dph_store_0; dph_retrieve_ = dph_retrieve_0; dph_arg_retrieve_ =
1250     dph_arg_retrieve_0; snd_arg_retrieve_ = snd_arg_retrieve_0;
1251     pair_reg_move_ = pair_reg_move_0; save_frame = save_frame0; setup_call =
1252     setup_call0; fetch_external_args = fetch_external_args0; set_result =
1253     set_result0; call_args_for_main = call_args_for_main0;
1254     call_dest_for_main = call_dest_for_main0; read_result = read_result0;
1255     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_24725
1256   in
1257   h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
1258     acca_arg_retrieve_0 accb_store_0 accb_retrieve_0 accb_arg_retrieve_0
1259     dpl_store_0 dpl_retrieve_0 dpl_arg_retrieve_0 dph_store_0 dph_retrieve_0
1260     dph_arg_retrieve_0 snd_arg_retrieve_0 pair_reg_move_0 save_frame0
1261     setup_call0 fetch_external_args0 set_result0 call_args_for_main0
1262     call_dest_for_main0 read_result0 eval_ext_seq0 pop_frame0
1263
1264 (** val sem_unserialized_params_rect_Type1 :
1265     Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
1266     -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) ->
1267     (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval ->
1268     __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
1269     -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
1270     __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __
1271     -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1272     Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1273     ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1274     -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1275     Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1276     (AST.external_function -> state -> __ -> Values.val0 List.list
1277     Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1278     -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1279     -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1280     List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1281     Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1282     state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
1283     'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
1284 let rec sem_unserialized_params_rect_Type1 uns_pars h_mk_sem_unserialized_params x_24727 =
1285   let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
1286     acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
1287     accb_store_0; accb_retrieve_ = accb_retrieve_0; accb_arg_retrieve_ =
1288     accb_arg_retrieve_0; dpl_store_ = dpl_store_0; dpl_retrieve_ =
1289     dpl_retrieve_0; dpl_arg_retrieve_ = dpl_arg_retrieve_0; dph_store_ =
1290     dph_store_0; dph_retrieve_ = dph_retrieve_0; dph_arg_retrieve_ =
1291     dph_arg_retrieve_0; snd_arg_retrieve_ = snd_arg_retrieve_0;
1292     pair_reg_move_ = pair_reg_move_0; save_frame = save_frame0; setup_call =
1293     setup_call0; fetch_external_args = fetch_external_args0; set_result =
1294     set_result0; call_args_for_main = call_args_for_main0;
1295     call_dest_for_main = call_dest_for_main0; read_result = read_result0;
1296     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_24727
1297   in
1298   h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
1299     acca_arg_retrieve_0 accb_store_0 accb_retrieve_0 accb_arg_retrieve_0
1300     dpl_store_0 dpl_retrieve_0 dpl_arg_retrieve_0 dph_store_0 dph_retrieve_0
1301     dph_arg_retrieve_0 snd_arg_retrieve_0 pair_reg_move_0 save_frame0
1302     setup_call0 fetch_external_args0 set_result0 call_args_for_main0
1303     call_dest_for_main0 read_result0 eval_ext_seq0 pop_frame0
1304
1305 (** val sem_unserialized_params_rect_Type0 :
1306     Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
1307     -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) ->
1308     (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval ->
1309     __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
1310     -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
1311     __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __
1312     -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1313     Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1314     ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1315     -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1316     Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1317     (AST.external_function -> state -> __ -> Values.val0 List.list
1318     Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1319     -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1320     -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1321     List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1322     Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1323     state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
1324     'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
1325 let rec sem_unserialized_params_rect_Type0 uns_pars h_mk_sem_unserialized_params x_24729 =
1326   let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
1327     acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
1328     accb_store_0; accb_retrieve_ = accb_retrieve_0; accb_arg_retrieve_ =
1329     accb_arg_retrieve_0; dpl_store_ = dpl_store_0; dpl_retrieve_ =
1330     dpl_retrieve_0; dpl_arg_retrieve_ = dpl_arg_retrieve_0; dph_store_ =
1331     dph_store_0; dph_retrieve_ = dph_retrieve_0; dph_arg_retrieve_ =
1332     dph_arg_retrieve_0; snd_arg_retrieve_ = snd_arg_retrieve_0;
1333     pair_reg_move_ = pair_reg_move_0; save_frame = save_frame0; setup_call =
1334     setup_call0; fetch_external_args = fetch_external_args0; set_result =
1335     set_result0; call_args_for_main = call_args_for_main0;
1336     call_dest_for_main = call_dest_for_main0; read_result = read_result0;
1337     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_24729
1338   in
1339   h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
1340     acca_arg_retrieve_0 accb_store_0 accb_retrieve_0 accb_arg_retrieve_0
1341     dpl_store_0 dpl_retrieve_0 dpl_arg_retrieve_0 dph_store_0 dph_retrieve_0
1342     dph_arg_retrieve_0 snd_arg_retrieve_0 pair_reg_move_0 save_frame0
1343     setup_call0 fetch_external_args0 set_result0 call_args_for_main0
1344     call_dest_for_main0 read_result0 eval_ext_seq0 pop_frame0
1345
1346 (** val st_pars :
1347     Joint.unserialized_params -> 'a1 sem_unserialized_params ->
1348     sem_state_params **)
1349 let rec st_pars uns_pars xxx =
1350   xxx.st_pars
1351
1352 (** val acca_store_ :
1353     Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1354     ByteValues.beval -> __ -> __ Errors.res **)
1355 let rec acca_store_ uns_pars xxx =
1356   xxx.acca_store_
1357
1358 (** val acca_retrieve_ :
1359     Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1360     ByteValues.beval Errors.res **)
1361 let rec acca_retrieve_ uns_pars xxx =
1362   xxx.acca_retrieve_
1363
1364 (** val acca_arg_retrieve_ :
1365     Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1366     ByteValues.beval Errors.res **)
1367 let rec acca_arg_retrieve_ uns_pars xxx =
1368   xxx.acca_arg_retrieve_
1369
1370 (** val accb_store_ :
1371     Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1372     ByteValues.beval -> __ -> __ Errors.res **)
1373 let rec accb_store_ uns_pars xxx =
1374   xxx.accb_store_
1375
1376 (** val accb_retrieve_ :
1377     Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1378     ByteValues.beval Errors.res **)
1379 let rec accb_retrieve_ uns_pars xxx =
1380   xxx.accb_retrieve_
1381
1382 (** val accb_arg_retrieve_ :
1383     Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1384     ByteValues.beval Errors.res **)
1385 let rec accb_arg_retrieve_ uns_pars xxx =
1386   xxx.accb_arg_retrieve_
1387
1388 (** val dpl_store_ :
1389     Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1390     ByteValues.beval -> __ -> __ Errors.res **)
1391 let rec dpl_store_ uns_pars xxx =
1392   xxx.dpl_store_
1393
1394 (** val dpl_retrieve_ :
1395     Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1396     ByteValues.beval Errors.res **)
1397 let rec dpl_retrieve_ uns_pars xxx =
1398   xxx.dpl_retrieve_
1399
1400 (** val dpl_arg_retrieve_ :
1401     Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1402     ByteValues.beval Errors.res **)
1403 let rec dpl_arg_retrieve_ uns_pars xxx =
1404   xxx.dpl_arg_retrieve_
1405
1406 (** val dph_store_ :
1407     Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1408     ByteValues.beval -> __ -> __ Errors.res **)
1409 let rec dph_store_ uns_pars xxx =
1410   xxx.dph_store_
1411
1412 (** val dph_retrieve_ :
1413     Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1414     ByteValues.beval Errors.res **)
1415 let rec dph_retrieve_ uns_pars xxx =
1416   xxx.dph_retrieve_
1417
1418 (** val dph_arg_retrieve_ :
1419     Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1420     ByteValues.beval Errors.res **)
1421 let rec dph_arg_retrieve_ uns_pars xxx =
1422   xxx.dph_arg_retrieve_
1423
1424 (** val snd_arg_retrieve_ :
1425     Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1426     ByteValues.beval Errors.res **)
1427 let rec snd_arg_retrieve_ uns_pars xxx =
1428   xxx.snd_arg_retrieve_
1429
1430 (** val pair_reg_move_ :
1431     Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
1432     __ Errors.res **)
1433 let rec pair_reg_move_ uns_pars xxx =
1434   xxx.pair_reg_move_
1435
1436 (** val save_frame :
1437     Joint.unserialized_params -> 'a1 sem_unserialized_params -> call_kind ->
1438     __ -> state_pc -> state Errors.res **)
1439 let rec save_frame uns_pars xxx =
1440   xxx.save_frame
1441
1442 (** val setup_call :
1443     Joint.unserialized_params -> 'a1 sem_unserialized_params -> Nat.nat -> __
1444     -> __ -> state -> state Errors.res **)
1445 let rec setup_call uns_pars xxx =
1446   xxx.setup_call
1447
1448 (** val fetch_external_args :
1449     Joint.unserialized_params -> 'a1 sem_unserialized_params ->
1450     AST.external_function -> state -> __ -> Values.val0 List.list Errors.res **)
1451 let rec fetch_external_args uns_pars xxx =
1452   xxx.fetch_external_args
1453
1454 (** val set_result :
1455     Joint.unserialized_params -> 'a1 sem_unserialized_params -> Values.val0
1456     List.list -> __ -> state -> state Errors.res **)
1457 let rec set_result uns_pars xxx =
1458   xxx.set_result
1459
1460 (** val call_args_for_main :
1461     Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ **)
1462 let rec call_args_for_main uns_pars xxx =
1463   xxx.call_args_for_main
1464
1465 (** val call_dest_for_main :
1466     Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ **)
1467 let rec call_dest_for_main uns_pars xxx =
1468   xxx.call_dest_for_main
1469
1470 (** val read_result :
1471     Joint.unserialized_params -> 'a1 sem_unserialized_params -> AST.ident
1472     List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state ->
1473     ByteValues.beval List.list Errors.res **)
1474 let rec read_result uns_pars xxx =
1475   xxx.read_result
1476
1477 (** val eval_ext_seq :
1478     Joint.unserialized_params -> 'a1 sem_unserialized_params -> AST.ident
1479     List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state Errors.res **)
1480 let rec eval_ext_seq uns_pars xxx =
1481   xxx.eval_ext_seq
1482
1483 (** val pop_frame :
1484     Joint.unserialized_params -> 'a1 sem_unserialized_params -> AST.ident
1485     List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
1486     ByteValues.program_counter) Types.prod Errors.res **)
1487 let rec pop_frame uns_pars xxx =
1488   xxx.pop_frame
1489
1490 (** val sem_unserialized_params_inv_rect_Type4 :
1491     Joint.unserialized_params -> 'a1 sem_unserialized_params ->
1492     (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) ->
1493     (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1494     ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1495     Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1496     ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1497     Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1498     ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1499     Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1500     ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1501     -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1502     Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1503     (AST.external_function -> state -> __ -> Values.val0 List.list
1504     Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1505     -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1506     -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1507     List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1508     Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1509     state -> (state, ByteValues.program_counter) Types.prod Errors.res) -> __
1510     -> 'a2) -> 'a2 **)
1511 let sem_unserialized_params_inv_rect_Type4 x1 hterm h1 =
1512   let hcut = sem_unserialized_params_rect_Type4 x1 h1 hterm in hcut __
1513
1514 (** val sem_unserialized_params_inv_rect_Type3 :
1515     Joint.unserialized_params -> 'a1 sem_unserialized_params ->
1516     (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) ->
1517     (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1518     ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1519     Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1520     ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1521     Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1522     ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1523     Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1524     ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1525     -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1526     Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1527     (AST.external_function -> state -> __ -> Values.val0 List.list
1528     Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1529     -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1530     -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1531     List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1532     Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1533     state -> (state, ByteValues.program_counter) Types.prod Errors.res) -> __
1534     -> 'a2) -> 'a2 **)
1535 let sem_unserialized_params_inv_rect_Type3 x1 hterm h1 =
1536   let hcut = sem_unserialized_params_rect_Type3 x1 h1 hterm in hcut __
1537
1538 (** val sem_unserialized_params_inv_rect_Type2 :
1539     Joint.unserialized_params -> 'a1 sem_unserialized_params ->
1540     (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) ->
1541     (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1542     ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1543     Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1544     ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1545     Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1546     ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1547     Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1548     ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1549     -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1550     Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1551     (AST.external_function -> state -> __ -> Values.val0 List.list
1552     Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1553     -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1554     -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1555     List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1556     Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1557     state -> (state, ByteValues.program_counter) Types.prod Errors.res) -> __
1558     -> 'a2) -> 'a2 **)
1559 let sem_unserialized_params_inv_rect_Type2 x1 hterm h1 =
1560   let hcut = sem_unserialized_params_rect_Type2 x1 h1 hterm in hcut __
1561
1562 (** val sem_unserialized_params_inv_rect_Type1 :
1563     Joint.unserialized_params -> 'a1 sem_unserialized_params ->
1564     (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) ->
1565     (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1566     ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1567     Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1568     ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1569     Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1570     ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1571     Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1572     ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1573     -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1574     Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1575     (AST.external_function -> state -> __ -> Values.val0 List.list
1576     Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1577     -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1578     -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1579     List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1580     Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1581     state -> (state, ByteValues.program_counter) Types.prod Errors.res) -> __
1582     -> 'a2) -> 'a2 **)
1583 let sem_unserialized_params_inv_rect_Type1 x1 hterm h1 =
1584   let hcut = sem_unserialized_params_rect_Type1 x1 h1 hterm in hcut __
1585
1586 (** val sem_unserialized_params_inv_rect_Type0 :
1587     Joint.unserialized_params -> 'a1 sem_unserialized_params ->
1588     (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) ->
1589     (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1590     ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1591     Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1592     ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1593     Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1594     ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
1595     Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
1596     ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
1597     -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
1598     Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
1599     (AST.external_function -> state -> __ -> Values.val0 List.list
1600     Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res)
1601     -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t
1602     -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident
1603     List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state
1604     Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ ->
1605     state -> (state, ByteValues.program_counter) Types.prod Errors.res) -> __
1606     -> 'a2) -> 'a2 **)
1607 let sem_unserialized_params_inv_rect_Type0 x1 hterm h1 =
1608   let hcut = sem_unserialized_params_rect_Type0 x1 h1 hterm in hcut __
1609
1610 (** val sem_unserialized_params_jmdiscr :
1611     Joint.unserialized_params -> 'a1 sem_unserialized_params -> 'a1
1612     sem_unserialized_params -> __ **)
1613 let sem_unserialized_params_jmdiscr a1 x y =
1614   Logic.eq_rect_Type2 x
1615     (let { st_pars = a0; acca_store_ = a10; acca_retrieve_ = a20;
1616        acca_arg_retrieve_ = a3; accb_store_ = a4; accb_retrieve_ = a5;
1617        accb_arg_retrieve_ = a6; dpl_store_ = a7; dpl_retrieve_ = a8;
1618        dpl_arg_retrieve_ = a9; dph_store_ = a100; dph_retrieve_ = a11;
1619        dph_arg_retrieve_ = a12; snd_arg_retrieve_ = a13; pair_reg_move_ =
1620        a14; save_frame = a15; setup_call = a16; fetch_external_args = a17;
1621        set_result = a18; call_args_for_main = a19; call_dest_for_main = a200;
1622        read_result = a21; eval_ext_seq = a22; pop_frame = a23 } = x
1623      in
1624     Obj.magic (fun _ dH ->
1625       dH __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __
1626         __)) y
1627
1628 (** val helper_def_retrieve :
1629     (Joint.unserialized_params -> __ -> __ sem_unserialized_params -> __ ->
1630     'a1 -> ByteValues.beval Errors.res) -> Joint.unserialized_params -> 'a2
1631     sem_unserialized_params -> state -> 'a1 -> ByteValues.beval Errors.res **)
1632 let helper_def_retrieve f up p st =
1633   Obj.magic f up __ p st.regs
1634
1635 (** val helper_def_store :
1636     (Joint.unserialized_params -> __ -> __ sem_unserialized_params -> 'a1 ->
1637     ByteValues.beval -> __ -> __ Errors.res) -> Joint.unserialized_params ->
1638     'a2 sem_unserialized_params -> 'a1 -> ByteValues.beval -> state -> state
1639     Errors.res **)
1640 let helper_def_store f up p x v st =
1641   Obj.magic
1642     (Monad.m_bind0 (Monad.max_def Errors.res0)
1643       (Obj.magic f up __ p x v st.regs) (fun r ->
1644       Monad.m_return0 (Monad.max_def Errors.res0) (set_regs p.st_pars r st)))
1645
1646 (** val acca_retrieve :
1647     Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1648     -> ByteValues.beval Errors.res **)
1649 let acca_retrieve up p x x0 =
1650   helper_def_retrieve (fun x1 _ -> acca_retrieve_ x1) up p x x0
1651
1652 (** val acca_store :
1653     Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1654     ByteValues.beval -> state -> state Errors.res **)
1655 let acca_store up p x x0 x1 =
1656   helper_def_store (fun x2 _ -> acca_store_ x2) up p x x0 x1
1657
1658 (** val acca_arg_retrieve :
1659     Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1660     -> ByteValues.beval Errors.res **)
1661 let acca_arg_retrieve up p x x0 =
1662   helper_def_retrieve (fun x1 _ -> acca_arg_retrieve_ x1) up p x x0
1663
1664 (** val accb_store :
1665     Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1666     ByteValues.beval -> state -> state Errors.res **)
1667 let accb_store up p x x0 x1 =
1668   helper_def_store (fun x2 _ -> accb_store_ x2) up p x x0 x1
1669
1670 (** val accb_retrieve :
1671     Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1672     -> ByteValues.beval Errors.res **)
1673 let accb_retrieve up p x x0 =
1674   helper_def_retrieve (fun x1 _ -> accb_retrieve_ x1) up p x x0
1675
1676 (** val accb_arg_retrieve :
1677     Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1678     -> ByteValues.beval Errors.res **)
1679 let accb_arg_retrieve up p x x0 =
1680   helper_def_retrieve (fun x1 _ -> accb_arg_retrieve_ x1) up p x x0
1681
1682 (** val dpl_store :
1683     Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1684     ByteValues.beval -> state -> state Errors.res **)
1685 let dpl_store up p x x0 x1 =
1686   helper_def_store (fun x2 _ -> dpl_store_ x2) up p x x0 x1
1687
1688 (** val dpl_retrieve :
1689     Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1690     -> ByteValues.beval Errors.res **)
1691 let dpl_retrieve up p x x0 =
1692   helper_def_retrieve (fun x1 _ -> dpl_retrieve_ x1) up p x x0
1693
1694 (** val dpl_arg_retrieve :
1695     Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1696     -> ByteValues.beval Errors.res **)
1697 let dpl_arg_retrieve up p x x0 =
1698   helper_def_retrieve (fun x1 _ -> dpl_arg_retrieve_ x1) up p x x0
1699
1700 (** val dph_store :
1701     Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1702     ByteValues.beval -> state -> state Errors.res **)
1703 let dph_store up p x x0 x1 =
1704   helper_def_store (fun x2 _ -> dph_store_ x2) up p x x0 x1
1705
1706 (** val dph_retrieve :
1707     Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1708     -> ByteValues.beval Errors.res **)
1709 let dph_retrieve up p x x0 =
1710   helper_def_retrieve (fun x1 _ -> dph_retrieve_ x1) up p x x0
1711
1712 (** val dph_arg_retrieve :
1713     Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1714     -> ByteValues.beval Errors.res **)
1715 let dph_arg_retrieve up p x x0 =
1716   helper_def_retrieve (fun x1 _ -> dph_arg_retrieve_ x1) up p x x0
1717
1718 (** val snd_arg_retrieve :
1719     Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1720     -> ByteValues.beval Errors.res **)
1721 let snd_arg_retrieve up p x x0 =
1722   helper_def_retrieve (fun x1 _ -> snd_arg_retrieve_ x1) up p x x0
1723
1724 (** val pair_reg_move :
1725     Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __
1726     -> __ **)
1727 let pair_reg_move up p st pm =
1728   Monad.m_bind0 (Monad.max_def Errors.res0)
1729     (Obj.magic (p.pair_reg_move_ st.regs pm)) (fun r ->
1730     Monad.m_return0 (Monad.max_def Errors.res0) (set_regs p.st_pars r st))
1731
1732 (** val push :
1733     sem_state_params -> state -> ByteValues.beval -> state Errors.res **)
1734 let push p st v =
1735   Obj.magic
1736     (Monad.m_bind0 (Monad.max_def Errors.res0)
1737       (Obj.magic (is_push st.istack v)) (fun is ->
1738       Monad.m_return0 (Monad.max_def Errors.res0) (set_istack p is st)))
1739
1740 (** val pop :
1741     sem_state_params -> state -> (ByteValues.beval, state) Types.prod
1742     Errors.res **)
1743 let pop p st =
1744   Obj.magic
1745     (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (is_pop st.istack))
1746       (fun bv is ->
1747       Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = bv;
1748         Types.snd = (set_istack p is st) }))
1749
1750 (** val push_ra :
1751     sem_state_params -> state -> ByteValues.program_counter -> state
1752     Errors.res **)
1753 let push_ra p st l =
1754   let { Types.fst = addrl; Types.snd = addrh } =
1755     ByteValues.beval_pair_of_pc l
1756   in
1757   Obj.magic
1758     (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (push p st addrl))
1759       (fun st' -> Obj.magic (push p st' addrh)))
1760
1761 (** val pop_ra :
1762     sem_state_params -> state -> (state, ByteValues.program_counter)
1763     Types.prod Errors.res **)
1764 let pop_ra p st =
1765   Obj.magic
1766     (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (pop p st))
1767       (fun addrh st' ->
1768       Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (pop p st'))
1769         (fun addrl st'' ->
1770         Monad.m_bind0 (Monad.max_def Errors.res0)
1771           (Obj.magic
1772             (ByteValues.pc_of_bevals (List.Cons (addrl, (List.Cons (addrh,
1773               List.Nil)))))) (fun pr ->
1774           Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = st'';
1775             Types.snd = pr }))))
1776
1777 type serialized_params = { spp : Joint.params;
1778                            msu_pars : Joint.joint_closed_internal_function
1779                                       sem_unserialized_params;
1780                            offset_of_point : (__ -> Positive.pos);
1781                            point_of_offset : (Positive.pos -> __) }
1782
1783 (** val serialized_params_rect_Type4 :
1784     (Joint.params -> Joint.joint_closed_internal_function
1785     sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1786     -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
1787 let rec serialized_params_rect_Type4 h_mk_serialized_params x_24799 =
1788   let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
1789     point_of_offset = point_of_offset0 } = x_24799
1790   in
1791   h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
1792     __
1793
1794 (** val serialized_params_rect_Type5 :
1795     (Joint.params -> Joint.joint_closed_internal_function
1796     sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1797     -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
1798 let rec serialized_params_rect_Type5 h_mk_serialized_params x_24801 =
1799   let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
1800     point_of_offset = point_of_offset0 } = x_24801
1801   in
1802   h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
1803     __
1804
1805 (** val serialized_params_rect_Type3 :
1806     (Joint.params -> Joint.joint_closed_internal_function
1807     sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1808     -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
1809 let rec serialized_params_rect_Type3 h_mk_serialized_params x_24803 =
1810   let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
1811     point_of_offset = point_of_offset0 } = x_24803
1812   in
1813   h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
1814     __
1815
1816 (** val serialized_params_rect_Type2 :
1817     (Joint.params -> Joint.joint_closed_internal_function
1818     sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1819     -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
1820 let rec serialized_params_rect_Type2 h_mk_serialized_params x_24805 =
1821   let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
1822     point_of_offset = point_of_offset0 } = x_24805
1823   in
1824   h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
1825     __
1826
1827 (** val serialized_params_rect_Type1 :
1828     (Joint.params -> Joint.joint_closed_internal_function
1829     sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1830     -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
1831 let rec serialized_params_rect_Type1 h_mk_serialized_params x_24807 =
1832   let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
1833     point_of_offset = point_of_offset0 } = x_24807
1834   in
1835   h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
1836     __
1837
1838 (** val serialized_params_rect_Type0 :
1839     (Joint.params -> Joint.joint_closed_internal_function
1840     sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
1841     -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
1842 let rec serialized_params_rect_Type0 h_mk_serialized_params x_24809 =
1843   let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
1844     point_of_offset = point_of_offset0 } = x_24809
1845   in
1846   h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
1847     __
1848
1849 (** val spp : serialized_params -> Joint.params **)
1850 let rec spp xxx =
1851   xxx.spp
1852
1853 (** val msu_pars :
1854     serialized_params -> Joint.joint_closed_internal_function
1855     sem_unserialized_params **)
1856 let rec msu_pars xxx =
1857   xxx.msu_pars
1858
1859 (** val offset_of_point : serialized_params -> __ -> Positive.pos **)
1860 let rec offset_of_point xxx =
1861   xxx.offset_of_point
1862
1863 (** val point_of_offset : serialized_params -> Positive.pos -> __ **)
1864 let rec point_of_offset xxx =
1865   xxx.point_of_offset
1866
1867 (** val serialized_params_inv_rect_Type4 :
1868     serialized_params -> (Joint.params ->
1869     Joint.joint_closed_internal_function sem_unserialized_params -> (__ ->
1870     Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1871 let serialized_params_inv_rect_Type4 hterm h1 =
1872   let hcut = serialized_params_rect_Type4 h1 hterm in hcut __
1873
1874 (** val serialized_params_inv_rect_Type3 :
1875     serialized_params -> (Joint.params ->
1876     Joint.joint_closed_internal_function sem_unserialized_params -> (__ ->
1877     Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1878 let serialized_params_inv_rect_Type3 hterm h1 =
1879   let hcut = serialized_params_rect_Type3 h1 hterm in hcut __
1880
1881 (** val serialized_params_inv_rect_Type2 :
1882     serialized_params -> (Joint.params ->
1883     Joint.joint_closed_internal_function sem_unserialized_params -> (__ ->
1884     Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1885 let serialized_params_inv_rect_Type2 hterm h1 =
1886   let hcut = serialized_params_rect_Type2 h1 hterm in hcut __
1887
1888 (** val serialized_params_inv_rect_Type1 :
1889     serialized_params -> (Joint.params ->
1890     Joint.joint_closed_internal_function sem_unserialized_params -> (__ ->
1891     Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1892 let serialized_params_inv_rect_Type1 hterm h1 =
1893   let hcut = serialized_params_rect_Type1 h1 hterm in hcut __
1894
1895 (** val serialized_params_inv_rect_Type0 :
1896     serialized_params -> (Joint.params ->
1897     Joint.joint_closed_internal_function sem_unserialized_params -> (__ ->
1898     Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1899 let serialized_params_inv_rect_Type0 hterm h1 =
1900   let hcut = serialized_params_rect_Type0 h1 hterm in hcut __
1901
1902 (** val serialized_params_jmdiscr :
1903     serialized_params -> serialized_params -> __ **)
1904 let serialized_params_jmdiscr x y =
1905   Logic.eq_rect_Type2 x
1906     (let { spp = a0; msu_pars = a1; offset_of_point = a2; point_of_offset =
1907        a3 } = x
1908      in
1909     Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
1910
1911 (** val spp__o__stmt_pars : serialized_params -> Joint.stmt_params **)
1912 let spp__o__stmt_pars x0 =
1913   x0.spp.Joint.stmt_pars
1914
1915 (** val spp__o__stmt_pars__o__uns_pars :
1916     serialized_params -> Joint.uns_params **)
1917 let spp__o__stmt_pars__o__uns_pars x0 =
1918   Joint.stmt_pars__o__uns_pars x0.spp
1919
1920 (** val spp__o__stmt_pars__o__uns_pars__o__u_pars :
1921     serialized_params -> Joint.unserialized_params **)
1922 let spp__o__stmt_pars__o__uns_pars__o__u_pars x0 =
1923   Joint.stmt_pars__o__uns_pars__o__u_pars x0.spp
1924
1925 (** val msu_pars__o__st_pars : serialized_params -> sem_state_params **)
1926 let msu_pars__o__st_pars x0 =
1927   x0.msu_pars.st_pars
1928
1929 type sem_params = { spp' : serialized_params;
1930                     pre_main_generator : (Joint.joint_program ->
1931                                          Joint.joint_closed_internal_function) }
1932
1933 (** val sem_params_rect_Type4 :
1934     (serialized_params -> (Joint.joint_program ->
1935     Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
1936 let rec sem_params_rect_Type4 h_mk_sem_params x_24827 =
1937   let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_24827 in
1938   h_mk_sem_params spp'0 pre_main_generator0
1939
1940 (** val sem_params_rect_Type5 :
1941     (serialized_params -> (Joint.joint_program ->
1942     Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
1943 let rec sem_params_rect_Type5 h_mk_sem_params x_24829 =
1944   let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_24829 in
1945   h_mk_sem_params spp'0 pre_main_generator0
1946
1947 (** val sem_params_rect_Type3 :
1948     (serialized_params -> (Joint.joint_program ->
1949     Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
1950 let rec sem_params_rect_Type3 h_mk_sem_params x_24831 =
1951   let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_24831 in
1952   h_mk_sem_params spp'0 pre_main_generator0
1953
1954 (** val sem_params_rect_Type2 :
1955     (serialized_params -> (Joint.joint_program ->
1956     Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
1957 let rec sem_params_rect_Type2 h_mk_sem_params x_24833 =
1958   let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_24833 in
1959   h_mk_sem_params spp'0 pre_main_generator0
1960
1961 (** val sem_params_rect_Type1 :
1962     (serialized_params -> (Joint.joint_program ->
1963     Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
1964 let rec sem_params_rect_Type1 h_mk_sem_params x_24835 =
1965   let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_24835 in
1966   h_mk_sem_params spp'0 pre_main_generator0
1967
1968 (** val sem_params_rect_Type0 :
1969     (serialized_params -> (Joint.joint_program ->
1970     Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
1971 let rec sem_params_rect_Type0 h_mk_sem_params x_24837 =
1972   let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_24837 in
1973   h_mk_sem_params spp'0 pre_main_generator0
1974
1975 (** val spp' : sem_params -> serialized_params **)
1976 let rec spp' xxx =
1977   xxx.spp'
1978
1979 (** val pre_main_generator :
1980     sem_params -> Joint.joint_program -> Joint.joint_closed_internal_function **)
1981 let rec pre_main_generator xxx =
1982   xxx.pre_main_generator
1983
1984 (** val sem_params_inv_rect_Type4 :
1985     sem_params -> (serialized_params -> (Joint.joint_program ->
1986     Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
1987 let sem_params_inv_rect_Type4 hterm h1 =
1988   let hcut = sem_params_rect_Type4 h1 hterm in hcut __
1989
1990 (** val sem_params_inv_rect_Type3 :
1991     sem_params -> (serialized_params -> (Joint.joint_program ->
1992     Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
1993 let sem_params_inv_rect_Type3 hterm h1 =
1994   let hcut = sem_params_rect_Type3 h1 hterm in hcut __
1995
1996 (** val sem_params_inv_rect_Type2 :
1997     sem_params -> (serialized_params -> (Joint.joint_program ->
1998     Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
1999 let sem_params_inv_rect_Type2 hterm h1 =
2000   let hcut = sem_params_rect_Type2 h1 hterm in hcut __
2001
2002 (** val sem_params_inv_rect_Type1 :
2003     sem_params -> (serialized_params -> (Joint.joint_program ->
2004     Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
2005 let sem_params_inv_rect_Type1 hterm h1 =
2006   let hcut = sem_params_rect_Type1 h1 hterm in hcut __
2007
2008 (** val sem_params_inv_rect_Type0 :
2009     sem_params -> (serialized_params -> (Joint.joint_program ->
2010     Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
2011 let sem_params_inv_rect_Type0 hterm h1 =
2012   let hcut = sem_params_rect_Type0 h1 hterm in hcut __
2013
2014 (** val sem_params_jmdiscr : sem_params -> sem_params -> __ **)
2015 let sem_params_jmdiscr x y =
2016   Logic.eq_rect_Type2 x
2017     (let { spp' = a0; pre_main_generator = a1 } = x in
2018     Obj.magic (fun _ dH -> dH __ __)) y
2019
2020 (** val spp'__o__msu_pars :
2021     sem_params -> Joint.joint_closed_internal_function
2022     sem_unserialized_params **)
2023 let spp'__o__msu_pars x0 =
2024   x0.spp'.msu_pars
2025
2026 (** val spp'__o__msu_pars__o__st_pars : sem_params -> sem_state_params **)
2027 let spp'__o__msu_pars__o__st_pars x0 =
2028   msu_pars__o__st_pars x0.spp'
2029
2030 (** val spp'__o__spp : sem_params -> Joint.params **)
2031 let spp'__o__spp x0 =
2032   x0.spp'.spp
2033
2034 (** val spp'__o__spp__o__stmt_pars : sem_params -> Joint.stmt_params **)
2035 let spp'__o__spp__o__stmt_pars x0 =
2036   spp__o__stmt_pars x0.spp'
2037
2038 (** val spp'__o__spp__o__stmt_pars__o__uns_pars :
2039     sem_params -> Joint.uns_params **)
2040 let spp'__o__spp__o__stmt_pars__o__uns_pars x0 =
2041   spp__o__stmt_pars__o__uns_pars x0.spp'
2042
2043 (** val spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
2044     sem_params -> Joint.unserialized_params **)
2045 let spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 =
2046   spp__o__stmt_pars__o__uns_pars__o__u_pars x0.spp'
2047
2048 (** val pc_of_point :
2049     sem_params -> Pointers.block Types.sig0 -> __ ->
2050     ByteValues.program_counter **)
2051 let pc_of_point p bl pt =
2052   { ByteValues.pc_block = bl; ByteValues.pc_offset =
2053     (p.spp'.offset_of_point pt) }
2054
2055 (** val point_of_pc : sem_params -> ByteValues.program_counter -> __ **)
2056 let point_of_pc p ptr =
2057   p.spp'.point_of_offset ptr.ByteValues.pc_offset
2058
2059 (** val fetch_statement :
2060     sem_params -> AST.ident List.list -> genv -> ByteValues.program_counter
2061     -> ((AST.ident, Joint.joint_closed_internal_function) Types.prod,
2062     Joint.joint_statement) Types.prod Errors.res **)
2063 let fetch_statement p globals ge0 ptr =
2064   Obj.magic
2065     (Monad.m_bind2 (Monad.max_def Errors.res0)
2066       (Obj.magic
2067         (fetch_internal_function globals ge0 ptr.ByteValues.pc_block))
2068       (fun id fn ->
2069       let pt = point_of_pc p ptr in
2070       Monad.m_bind0 (Monad.max_def Errors.res0)
2071         (Obj.magic
2072           (Errors.opt_to_res
2073             (Errors.msg ErrorMessages.ProgramCounterOutOfCode)
2074             ((spp'__o__spp p).Joint.stmt_at globals
2075               (Types.pi1 fn).Joint.joint_if_code pt))) (fun stmt ->
2076         Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
2077           { Types.fst = id; Types.snd = fn }; Types.snd = stmt })))
2078
2079 (** val pc_of_label :
2080     sem_params -> AST.ident List.list -> genv -> Pointers.block Types.sig0 ->
2081     Graphs.label -> ByteValues.program_counter Errors.res **)
2082 let pc_of_label p globals ge0 bl lbl =
2083   Obj.magic
2084     (Monad.m_bind2 (Monad.max_def Errors.res0)
2085       (Obj.magic (fetch_internal_function globals ge0 bl)) (fun i fn ->
2086       Monad.m_bind0 (Monad.max_def Errors.res0)
2087         (Obj.magic
2088           (Errors.opt_to_res (List.Cons ((Errors.MSG
2089             ErrorMessages.LabelNotFound), (List.Cons ((Errors.CTX
2090             (PreIdentifiers.LabelTag, lbl)), List.Nil))))
2091             ((spp'__o__spp p).Joint.point_of_label globals
2092               (Types.pi1 fn).Joint.joint_if_code lbl))) (fun pt ->
2093         Monad.m_return0 (Monad.max_def Errors.res0) { ByteValues.pc_block =
2094           bl; ByteValues.pc_offset = (p.spp'.offset_of_point pt) })))
2095
2096 (** val succ_pc :
2097     sem_params -> ByteValues.program_counter -> __ ->
2098     ByteValues.program_counter **)
2099 let succ_pc p ptr nxt =
2100   let curr = point_of_pc p ptr in
2101   pc_of_point p ptr.ByteValues.pc_block
2102     ((spp'__o__spp p).Joint.point_of_succ curr nxt)
2103
2104 (** val goto :
2105     sem_params -> AST.ident List.list -> genv -> Graphs.label -> state_pc ->
2106     state_pc Errors.res **)
2107 let goto p globals ge0 l st =
2108   Obj.magic
2109     (Monad.m_bind0 (Monad.max_def Errors.res0)
2110       (Obj.magic (pc_of_label p globals ge0 st.pc.ByteValues.pc_block l))
2111       (fun newpc ->
2112       Monad.m_return0 (Monad.max_def Errors.res0)
2113         (set_pc (spp'__o__msu_pars__o__st_pars p) newpc st)))
2114
2115 (** val next : sem_params -> __ -> state_pc -> state_pc **)
2116 let next p l st =
2117   let newpc = succ_pc p st.pc l in
2118   set_pc (spp'__o__msu_pars__o__st_pars p) newpc st
2119
2120 (** val next_of_call_pc :
2121     sem_params -> AST.ident List.list -> genv -> ByteValues.program_counter
2122     -> __ Errors.res **)
2123 let next_of_call_pc p globals ge0 pc0 =
2124   Obj.magic
2125     (Monad.m_bind2 (Monad.max_def Errors.res0)
2126       (Obj.magic (fetch_statement p globals ge0 pc0)) (fun id_fn stmt ->
2127       match stmt with
2128       | Joint.Sequential (s, nxt) ->
2129         (match s with
2130          | Joint.COST_LABEL x ->
2131            Obj.magic (Errors.Error (List.Cons ((Errors.MSG
2132              ErrorMessages.NoSuccessor), List.Nil)))
2133          | Joint.CALL (x, x0, x1) ->
2134            Monad.m_return0 (Monad.max_def Errors.res0) nxt
2135          | Joint.COND (x, x0) ->
2136            Obj.magic (Errors.Error (List.Cons ((Errors.MSG
2137              ErrorMessages.NoSuccessor), List.Nil)))
2138          | Joint.Step_seq x ->
2139            Obj.magic (Errors.Error (List.Cons ((Errors.MSG
2140              ErrorMessages.NoSuccessor), List.Nil))))
2141       | Joint.Final x ->
2142         Obj.magic (Errors.Error (List.Cons ((Errors.MSG
2143           ErrorMessages.NoSuccessor), List.Nil)))
2144       | Joint.FCOND (x0, x1, x2) ->
2145         Obj.magic (Errors.Error (List.Cons ((Errors.MSG
2146           ErrorMessages.NoSuccessor), List.Nil)))))
2147
2148 (** val eval_seq_no_pc :
2149     sem_params -> AST.ident List.list -> genv -> AST.ident -> Joint.joint_seq
2150     -> state -> state Errors.res **)
2151 let eval_seq_no_pc p globals ge0 curr_id seq st =
2152   match seq with
2153   | Joint.COMMENT x ->
2154     Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st)
2155   | Joint.MOVE dst_src ->
2156     Obj.magic
2157       (pair_reg_move (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2158         p.spp'.msu_pars st dst_src)
2159   | Joint.POP dst ->
2160     Obj.magic
2161       (Monad.m_bind2 (Monad.max_def Errors.res0)
2162         (Obj.magic (pop (spp'__o__msu_pars__o__st_pars p) st)) (fun v st' ->
2163         Obj.magic
2164           (acca_store (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2165             (spp'__o__msu_pars p) dst v st')))
2166   | Joint.PUSH src ->
2167     Obj.magic
2168       (Monad.m_bind0 (Monad.max_def Errors.res0)
2169         (Obj.magic
2170           (acca_arg_retrieve
2171             (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2172             p.spp'.msu_pars st src)) (fun v ->
2173         Obj.magic (push (spp'__o__msu_pars__o__st_pars p) st v)))
2174   | Joint.ADDRESS (id, off, ldest, hdest) ->
2175     let addr_block = Option.opt_safe (Globalenvs.find_symbol ge0.ge id) in
2176     let { Types.fst = laddr; Types.snd = haddr } =
2177       ByteValues.beval_pair_of_pointer { Pointers.pblock = addr_block;
2178         Pointers.poff = off }
2179     in
2180     Obj.magic
2181       (Monad.m_bind0 (Monad.max_def Errors.res0)
2182         (Obj.magic
2183           (dpl_store (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
2184             p.spp'.msu_pars ldest laddr st)) (fun st' ->
2185         Obj.magic
2186           (dph_store (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
2187             p.spp'.msu_pars hdest haddr st')))
2188   | Joint.OPACCS (op, dacc_a_reg, dacc_b_reg, sacc_a_reg, sacc_b_reg) ->
2189     Obj.magic
2190       (Monad.m_bind0 (Monad.max_def Errors.res0)
2191         (Obj.magic
2192           (acca_arg_retrieve
2193             (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2194             p.spp'.msu_pars st sacc_a_reg)) (fun v1 ->
2195         Monad.m_bind0 (Monad.max_def Errors.res0)
2196           (Obj.magic
2197             (accb_arg_retrieve
2198               (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2199               p.spp'.msu_pars st sacc_b_reg)) (fun v2 ->
2200           Monad.m_bind2 (Monad.max_def Errors.res0)
2201             (Obj.magic (BackEndOps.be_opaccs op v1 v2)) (fun v1' v2' ->
2202             Monad.m_bind0 (Monad.max_def Errors.res0)
2203               (Obj.magic
2204                 (acca_store
2205                   (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
2206                   p.spp'.msu_pars dacc_a_reg v1' st)) (fun st' ->
2207               Obj.magic
2208                 (accb_store
2209                   (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
2210                   p.spp'.msu_pars dacc_b_reg v2' st'))))))
2211   | Joint.OP1 (op, dacc_a, sacc_a) ->
2212     Obj.magic
2213       (Monad.m_bind0 (Monad.max_def Errors.res0)
2214         (Obj.magic
2215           (acca_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2216             p.spp'.msu_pars st sacc_a)) (fun v ->
2217         Monad.m_bind0 (Monad.max_def Errors.res0)
2218           (Obj.magic (BackEndOps.be_op1 op v)) (fun v' ->
2219           Obj.magic
2220             (acca_store
2221               (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
2222               p.spp'.msu_pars dacc_a v' st))))
2223   | Joint.OP2 (op, dacc_a, sacc_a, src) ->
2224     Obj.magic
2225       (Monad.m_bind0 (Monad.max_def Errors.res0)
2226         (Obj.magic
2227           (acca_arg_retrieve
2228             (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2229             p.spp'.msu_pars st sacc_a)) (fun v1 ->
2230         Monad.m_bind0 (Monad.max_def Errors.res0)
2231           (Obj.magic
2232             (snd_arg_retrieve
2233               (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2234               p.spp'.msu_pars st src)) (fun v2 ->
2235           Monad.m_bind2 (Monad.max_def Errors.res0)
2236             (Obj.magic (BackEndOps.be_op2 st.carry op v1 v2))
2237             (fun v' carry0 ->
2238             Monad.m_bind0 (Monad.max_def Errors.res0)
2239               (Obj.magic
2240                 (acca_store
2241                   (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
2242                   p.spp'.msu_pars dacc_a v' st)) (fun st' ->
2243               Monad.m_return0 (Monad.max_def Errors.res0)
2244                 (set_carry p.spp'.msu_pars.st_pars carry0 st'))))))
2245   | Joint.CLEAR_CARRY ->
2246     Obj.magic
2247       (Monad.m_return0 (Monad.max_def Errors.res0)
2248         (set_carry (spp'__o__msu_pars__o__st_pars p) (ByteValues.BBbit
2249           Bool.False) st))
2250   | Joint.SET_CARRY ->
2251     Obj.magic
2252       (Monad.m_return0 (Monad.max_def Errors.res0)
2253         (set_carry (spp'__o__msu_pars__o__st_pars p) (ByteValues.BBbit
2254           Bool.True) st))
2255   | Joint.LOAD (dst, addrl, addrh) ->
2256     Obj.magic
2257       (Monad.m_bind0 (Monad.max_def Errors.res0)
2258         (Obj.magic
2259           (dph_arg_retrieve
2260             (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2261             p.spp'.msu_pars st addrh)) (fun vaddrh ->
2262         Monad.m_bind0 (Monad.max_def Errors.res0)
2263           (Obj.magic
2264             (dpl_arg_retrieve
2265               (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2266               p.spp'.msu_pars st addrl)) (fun vaddrl ->
2267           Monad.m_bind0 (Monad.max_def Errors.res0)
2268             (Obj.magic
2269               (BEMem.pointer_of_address { Types.fst = vaddrl; Types.snd =
2270                 vaddrh })) (fun vaddr ->
2271             Monad.m_bind0 (Monad.max_def Errors.res0)
2272               (Obj.magic
2273                 (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
2274                   (GenMem.beloadv st.m vaddr))) (fun v ->
2275               Obj.magic
2276                 (acca_store
2277                   (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
2278                   p.spp'.msu_pars dst v st))))))
2279   | Joint.STORE (addrl, addrh, src) ->
2280     Obj.magic
2281       (Monad.m_bind0 (Monad.max_def Errors.res0)
2282         (Obj.magic
2283           (dph_arg_retrieve
2284             (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2285             p.spp'.msu_pars st addrh)) (fun vaddrh ->
2286         Monad.m_bind0 (Monad.max_def Errors.res0)
2287           (Obj.magic
2288             (dpl_arg_retrieve
2289               (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2290               p.spp'.msu_pars st addrl)) (fun vaddrl ->
2291           Monad.m_bind0 (Monad.max_def Errors.res0)
2292             (Obj.magic
2293               (BEMem.pointer_of_address { Types.fst = vaddrl; Types.snd =
2294                 vaddrh })) (fun vaddr ->
2295             Monad.m_bind0 (Monad.max_def Errors.res0)
2296               (Obj.magic
2297                 (acca_arg_retrieve
2298                   (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2299                   p.spp'.msu_pars st src)) (fun v ->
2300               Monad.m_bind0 (Monad.max_def Errors.res0)
2301                 (Obj.magic
2302                   (Errors.opt_to_res (Errors.msg ErrorMessages.FailedStore)
2303                     (GenMem.bestorev st.m vaddr v))) (fun m' ->
2304                 Monad.m_return0 (Monad.max_def Errors.res0)
2305                   (set_m (spp'__o__msu_pars__o__st_pars p) m' st)))))))
2306   | Joint.Extension_seq c ->
2307     p.spp'.msu_pars.eval_ext_seq globals ge0 c curr_id st
2308
2309 (** val block_of_call :
2310     sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
2311     (__, __) Types.prod) Types.sum -> state -> __ **)
2312 let block_of_call p globals ge0 f st =
2313   Monad.m_bind0 (Monad.max_def Errors.res0)
2314     (match f with
2315      | Types.Inl id ->
2316        Obj.magic
2317          (Errors.opt_to_res (List.Cons ((Errors.MSG
2318            ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
2319            (PreIdentifiers.SymbolTag, id)), List.Nil))))
2320            (Globalenvs.find_symbol ge0.ge id))
2321      | Types.Inr addr ->
2322        Monad.m_bind0 (Monad.max_def Errors.res0)
2323          (Obj.magic
2324            (dpl_arg_retrieve
2325              (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2326              p.spp'.msu_pars st addr.Types.fst)) (fun addr_l ->
2327          Monad.m_bind0 (Monad.max_def Errors.res0)
2328            (Obj.magic
2329              (dph_arg_retrieve
2330                (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2331                p.spp'.msu_pars st addr.Types.snd)) (fun addr_h ->
2332            Monad.m_bind0 (Monad.max_def Errors.res0)
2333              (Obj.magic
2334                (ByteValues.pointer_of_bevals (List.Cons (addr_l, (List.Cons
2335                  (addr_h, List.Nil)))))) (fun ptr ->
2336              match BitVector.eq_bv Pointers.offset_size
2337                      (BitVector.zero Pointers.offset_size)
2338                      (Pointers.offv ptr.Pointers.poff) with
2339              | Bool.True ->
2340                Monad.m_return0 (Monad.max_def Errors.res0)
2341                  ptr.Pointers.pblock
2342              | Bool.False ->
2343                Obj.magic (Errors.Error (List.Cons ((Errors.MSG
2344                  ErrorMessages.BadFunction), (List.Cons ((Errors.MSG
2345                  ErrorMessages.BadPointer), List.Nil))))))))) (fun bl ->
2346     Obj.magic
2347       (Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction),
2348         (List.Cons ((Errors.MSG ErrorMessages.BadPointer), List.Nil))))
2349         (code_block_of_block bl)))
2350
2351 (** val eval_external_call :
2352     sem_params -> AST.external_function -> __ -> __ -> state -> __ **)
2353 let eval_external_call p fn args dest st =
2354   Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2355     (let x =
2356        IOMonad.err_to_io
2357          ((spp'__o__msu_pars p).fetch_external_args fn st args)
2358      in
2359     Obj.magic x) (fun params ->
2360     Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2361       (let x =
2362          IOMonad.err_to_io
2363            (IO.check_eventval_list params fn.AST.ef_sig.AST.sig_args)
2364        in
2365       Obj.magic x) (fun evargs ->
2366       Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2367         (Obj.magic
2368           (IO.do_io fn.AST.ef_id evargs (AST.proj_sig_res fn.AST.ef_sig)))
2369         (fun evres ->
2370         let vs = List.Cons
2371           ((IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres), List.Nil)
2372         in
2373         Obj.magic
2374           (IOMonad.err_to_io ((spp'__o__msu_pars p).set_result vs dest st)))))
2375
2376 (** val increment_stack_usage :
2377     sem_state_params -> Nat.nat -> state -> state **)
2378 let increment_stack_usage p n st =
2379   { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs =
2380     st.regs; m = st.m; stack_usage = (Nat.plus n st.stack_usage) }
2381
2382 (** val decrement_stack_usage :
2383     sem_state_params -> Nat.nat -> state -> state **)
2384 let decrement_stack_usage p n st =
2385   { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs =
2386     st.regs; m = st.m; stack_usage = (Nat.minus st.stack_usage n) }
2387
2388 (** val eval_internal_call :
2389     sem_params -> AST.ident List.list -> genv -> PreIdentifiers.identifier ->
2390     Joint.joint_internal_function -> __ -> state -> __ **)
2391 let eval_internal_call p globals ge0 i fn args st =
2392   Monad.m_bind0 (Monad.max_def Errors.res0)
2393     (Obj.magic
2394       (Errors.opt_to_res (List.Cons ((Errors.MSG
2395         ErrorMessages.MissingStackSize), (List.Cons ((Errors.CTX
2396         (PreIdentifiers.SymbolTag, i)), List.Nil)))) (ge0.stack_sizes i)))
2397     (fun stack_size ->
2398     Monad.m_bind0 (Monad.max_def Errors.res0)
2399       (Obj.magic
2400         (p.spp'.msu_pars.setup_call stack_size fn.Joint.joint_if_params args
2401           st)) (fun st' ->
2402       Monad.m_return0 (Monad.max_def Errors.res0)
2403         (increment_stack_usage p.spp'.msu_pars.st_pars stack_size st')))
2404
2405 (** val is_inl : ('a1, 'a2) Types.sum -> Bool.bool **)
2406 let is_inl = function
2407 | Types.Inl x0 -> Bool.True
2408 | Types.Inr x0 -> Bool.False
2409
2410 (** val eval_call :
2411     sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
2412     (__, __) Types.prod) Types.sum -> __ -> __ -> __ -> state_pc -> __ **)
2413 let eval_call p globals ge0 f args dest nxt st =
2414   Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2415     (let x =
2416        IOMonad.err_to_io
2417          (Obj.magic (block_of_call p globals ge0 f st.st_no_pc))
2418      in
2419     Obj.magic x) (fun bl ->
2420     Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
2421       (let x = IOMonad.err_to_io (fetch_function globals ge0 bl) in
2422       Obj.magic x) (fun i fd ->
2423       match fd with
2424       | AST.Internal ifd ->
2425         Obj.magic
2426           (IOMonad.err_to_io
2427             (Obj.magic
2428               (Monad.m_bind0 (Monad.max_def Errors.res0)
2429                 (Obj.magic
2430                   (p.spp'.msu_pars.save_frame
2431                     (kind_of_call
2432                       (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp) f)
2433                     dest st)) (fun st' ->
2434                 Monad.m_bind0 (Monad.max_def Errors.res0)
2435                   (eval_internal_call p globals ge0 i (Types.pi1 ifd) args
2436                     st') (fun st'' ->
2437                   let pc0 =
2438                     pc_of_point p bl (Types.pi1 ifd).Joint.joint_if_entry
2439                   in
2440                   Monad.m_return0 (Monad.max_def Errors.res0) { st_no_pc =
2441                     st''; pc = pc0; last_pop = st.last_pop })))))
2442       | AST.External efd ->
2443         Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2444           (eval_external_call p efd args dest st.st_no_pc) (fun st' ->
2445           Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { st_no_pc = st';
2446             pc = (succ_pc p st.pc nxt); last_pop = st.last_pop })))
2447
2448 (** val eval_statement_no_pc :
2449     sem_params -> AST.ident List.list -> genv -> AST.ident ->
2450     Joint.joint_statement -> state -> state Errors.res **)
2451 let eval_statement_no_pc p globals ge0 curr_id s st =
2452   match s with
2453   | Joint.Sequential (s0, next0) ->
2454     (match s0 with
2455      | Joint.COST_LABEL x ->
2456        Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st)
2457      | Joint.CALL (x, x0, x1) ->
2458        Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st)
2459      | Joint.COND (x, x0) ->
2460        Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st)
2461      | Joint.Step_seq s1 -> eval_seq_no_pc p globals ge0 curr_id s1 st)
2462   | Joint.Final x ->
2463     Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st)
2464   | Joint.FCOND (x0, x1, x2) ->
2465     Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st)
2466
2467 (** val eval_return :
2468     sem_params -> AST.ident List.list -> genv -> PreIdentifiers.identifier ->
2469     __ -> state -> __ **)
2470 let eval_return p globals ge0 curr_id curr_ret st =
2471   Monad.m_bind0 (Monad.max_def Errors.res0)
2472     (Obj.magic
2473       (Errors.opt_to_res (List.Cons ((Errors.MSG
2474         ErrorMessages.MissingStackSize), (List.Cons ((Errors.CTX
2475         (PreIdentifiers.SymbolTag, curr_id)), List.Nil))))
2476         (ge0.stack_sizes curr_id))) (fun stack_size ->
2477     Monad.m_bind2 (Monad.max_def Errors.res0)
2478       (Obj.magic (p.spp'.msu_pars.pop_frame globals ge0 curr_id curr_ret st))
2479       (fun st' call_pc ->
2480       Monad.m_bind0 (Monad.max_def Errors.res0)
2481         (Obj.magic (next_of_call_pc p globals ge0 call_pc)) (fun nxt ->
2482         let st'' =
2483           set_last_pop p.spp'.msu_pars.st_pars
2484             (decrement_stack_usage p.spp'.msu_pars.st_pars stack_size st')
2485             call_pc
2486         in
2487         Monad.m_return0 (Monad.max_def Errors.res0) (next p nxt st''))))
2488
2489 (** val eval_tailcall :
2490     sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
2491     (__, __) Types.prod) Types.sum -> __ -> PreIdentifiers.identifier -> __
2492     -> state_pc -> __ **)
2493 let eval_tailcall p globals ge0 f args curr_f curr_ret st =
2494   Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2495     (let x =
2496        IOMonad.err_to_io
2497          (Obj.magic (block_of_call p globals ge0 f st.st_no_pc))
2498      in
2499     Obj.magic x) (fun bl ->
2500     Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
2501       (let x = IOMonad.err_to_io (fetch_function globals ge0 bl) in
2502       Obj.magic x) (fun i fd ->
2503       match fd with
2504       | AST.Internal ifd ->
2505         Obj.magic
2506           (IOMonad.err_to_io
2507             (Obj.magic
2508               (Monad.m_bind0 (Monad.max_def Errors.res0)
2509                 (Obj.magic
2510                   (Errors.opt_to_res (List.Cons ((Errors.MSG
2511                     ErrorMessages.MissingStackSize), (List.Cons ((Errors.CTX
2512                     (PreIdentifiers.SymbolTag, curr_f)), List.Nil))))
2513                     (ge0.stack_sizes curr_f))) (fun stack_size ->
2514                 let st' =
2515                   decrement_stack_usage (spp'__o__msu_pars__o__st_pars p)
2516                     stack_size st.st_no_pc
2517                 in
2518                 Monad.m_bind0 (Monad.max_def Errors.res0)
2519                   (eval_internal_call p globals ge0 i (Types.pi1 ifd) args
2520                     st') (fun st'' ->
2521                   let pc0 =
2522                     pc_of_point p bl (Types.pi1 ifd).Joint.joint_if_entry
2523                   in
2524                   Monad.m_return0 (Monad.max_def Errors.res0) { st_no_pc =
2525                     st''; pc = pc0; last_pop = st.last_pop })))))
2526       | AST.External efd ->
2527         Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2528           (eval_external_call p efd args curr_ret st.st_no_pc) (fun st' ->
2529           Obj.magic
2530             (IOMonad.err_to_io
2531               (Obj.magic
2532                 (eval_return p globals ge0 curr_f curr_ret st.st_no_pc))))))
2533
2534 (** val eval_statement_advance :
2535     sem_params -> AST.ident List.list -> genv -> AST.ident ->
2536     Joint.joint_closed_internal_function -> Joint.joint_statement -> state_pc
2537     -> (IO.io_out, IO.io_in, state_pc) IOMonad.iO **)
2538 let eval_statement_advance p g ge0 curr_id curr_fn s st =
2539   match s with
2540   | Joint.Sequential (s0, nxt) ->
2541     (match s0 with
2542      | Joint.COST_LABEL x ->
2543        Obj.magic
2544          (Monad.m_return0 (Monad.max_def IOMonad.iOMonad) (next p nxt st))
2545      | Joint.CALL (f, args, dest) ->
2546        Obj.magic (eval_call p g ge0 f args dest nxt st)
2547      | Joint.COND (a, l) ->
2548        IOMonad.err_to_io
2549          (Obj.magic
2550            (Monad.m_bind0 (Monad.max_def Errors.res0)
2551              (Obj.magic
2552                (acca_retrieve
2553                  (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2554                  p.spp'.msu_pars st.st_no_pc a)) (fun v ->
2555              Monad.m_bind0 (Monad.max_def Errors.res0)
2556                (Obj.magic (ByteValues.bool_of_beval v)) (fun b ->
2557                match b with
2558                | Bool.True -> Obj.magic (goto p g ge0 l st)
2559                | Bool.False ->
2560                  Monad.m_return0 (Monad.max_def Errors.res0) (next p nxt st)))))
2561      | Joint.Step_seq x ->
2562        Obj.magic
2563          (Monad.m_return0 (Monad.max_def IOMonad.iOMonad) (next p nxt st)))
2564   | Joint.Final s0 ->
2565     let curr_ret = (Types.pi1 curr_fn).Joint.joint_if_result in
2566     (match s0 with
2567      | Joint.GOTO l -> IOMonad.err_to_io (goto p g ge0 l st)
2568      | Joint.RETURN ->
2569        IOMonad.err_to_io
2570          (Obj.magic (eval_return p g ge0 curr_id curr_ret st.st_no_pc))
2571      | Joint.TAILCALL (f, args) ->
2572        Obj.magic (eval_tailcall p g ge0 f args curr_id curr_ret st))
2573   | Joint.FCOND (a, lbltrue, lblfalse) ->
2574     IOMonad.err_to_io
2575       (Obj.magic
2576         (Monad.m_bind0 (Monad.max_def Errors.res0)
2577           (Obj.magic
2578             (acca_retrieve
2579               (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
2580               p.spp'.msu_pars st.st_no_pc a)) (fun v ->
2581           Monad.m_bind0 (Monad.max_def Errors.res0)
2582             (Obj.magic (ByteValues.bool_of_beval v)) (fun b ->
2583             match b with
2584             | Bool.True -> Obj.magic (goto p g ge0 lbltrue st)
2585             | Bool.False -> Obj.magic (goto p g ge0 lblfalse st)))))
2586
2587 (** val eval_state :
2588     sem_params -> AST.ident List.list -> genv -> state_pc -> (IO.io_out,
2589     IO.io_in, state_pc) IOMonad.iO **)
2590 let eval_state p globals ge0 st =
2591   Obj.magic
2592     (Monad.m_bind3 (Monad.max_def IOMonad.iOMonad)
2593       (let x = IOMonad.err_to_io (fetch_statement p globals ge0 st.pc) in
2594       Obj.magic x) (fun id fn s ->
2595       Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
2596         (let x =
2597            IOMonad.err_to_io
2598              (eval_statement_no_pc p globals ge0 id s st.st_no_pc)
2599          in
2600         Obj.magic x) (fun st' ->
2601         let st'' = set_no_pc (spp'__o__msu_pars__o__st_pars p) st' st in
2602         Obj.magic (eval_statement_advance p globals ge0 id fn s st''))))
2603