Changeset 2743 for extracted/joint.ml


Ignore:
Timestamp:
Feb 27, 2013, 9:27:58 PM (7 years ago)
Author:
sacerdot
Message:

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/joint.ml

    r2730 r2743  
    110110    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
    111111let rec argument_rect_Type4 h_Reg h_Imm = function
    112 | Reg x_6298 -> h_Reg x_6298
    113 | Imm x_6299 -> h_Imm x_6299
     112| Reg x_19390 -> h_Reg x_19390
     113| Imm x_19391 -> h_Imm x_19391
    114114
    115115(** val argument_rect_Type5 :
    116116    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
    117117let rec argument_rect_Type5 h_Reg h_Imm = function
    118 | Reg x_6303 -> h_Reg x_6303
    119 | Imm x_6304 -> h_Imm x_6304
     118| Reg x_19395 -> h_Reg x_19395
     119| Imm x_19396 -> h_Imm x_19396
    120120
    121121(** val argument_rect_Type3 :
    122122    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
    123123let rec argument_rect_Type3 h_Reg h_Imm = function
    124 | Reg x_6308 -> h_Reg x_6308
    125 | Imm x_6309 -> h_Imm x_6309
     124| Reg x_19400 -> h_Reg x_19400
     125| Imm x_19401 -> h_Imm x_19401
    126126
    127127(** val argument_rect_Type2 :
    128128    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
    129129let rec argument_rect_Type2 h_Reg h_Imm = function
    130 | Reg x_6313 -> h_Reg x_6313
    131 | Imm x_6314 -> h_Imm x_6314
     130| Reg x_19405 -> h_Reg x_19405
     131| Imm x_19406 -> h_Imm x_19406
    132132
    133133(** val argument_rect_Type1 :
    134134    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
    135135let rec argument_rect_Type1 h_Reg h_Imm = function
    136 | Reg x_6318 -> h_Reg x_6318
    137 | Imm x_6319 -> h_Imm x_6319
     136| Reg x_19410 -> h_Reg x_19410
     137| Imm x_19411 -> h_Imm x_19411
    138138
    139139(** val argument_rect_Type0 :
    140140    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
    141141let rec argument_rect_Type0 h_Reg h_Imm = function
    142 | Reg x_6323 -> h_Reg x_6323
    143 | Imm x_6324 -> h_Imm x_6324
     142| Reg x_19415 -> h_Reg x_19415
     143| Imm x_19416 -> h_Imm x_19416
    144144
    145145(** val argument_inv_rect_Type4 :
     
    193193  Reg x
    194194
     195(** val dpi1__o__reg_to_psd_argument__o__inject :
     196    (Registers.register, 'a1) Types.dPair -> psd_argument Types.sig0 **)
     197let dpi1__o__reg_to_psd_argument__o__inject x2 =
     198  psd_argument_from_reg x2.Types.dpi1
     199
     200(** val eject__o__reg_to_psd_argument__o__inject :
     201    Registers.register Types.sig0 -> psd_argument Types.sig0 **)
     202let eject__o__reg_to_psd_argument__o__inject x2 =
     203  psd_argument_from_reg (Types.pi1 x2)
     204
     205(** val reg_to_psd_argument__o__inject :
     206    Registers.register -> psd_argument Types.sig0 **)
     207let reg_to_psd_argument__o__inject x1 =
     208  psd_argument_from_reg x1
     209
     210(** val dpi1__o__reg_to_psd_argument :
     211    (Registers.register, 'a1) Types.dPair -> psd_argument **)
     212let dpi1__o__reg_to_psd_argument x1 =
     213  psd_argument_from_reg x1.Types.dpi1
     214
     215(** val eject__o__reg_to_psd_argument :
     216    Registers.register Types.sig0 -> psd_argument **)
     217let eject__o__reg_to_psd_argument x1 =
     218  psd_argument_from_reg (Types.pi1 x1)
     219
    195220(** val psd_argument_from_byte : BitVector.byte -> psd_argument **)
    196221let psd_argument_from_byte x =
    197222  Imm x
    198223
     224(** val dpi1__o__byte_to_psd_argument__o__inject :
     225    (BitVector.byte, 'a1) Types.dPair -> psd_argument Types.sig0 **)
     226let dpi1__o__byte_to_psd_argument__o__inject x2 =
     227  psd_argument_from_byte x2.Types.dpi1
     228
     229(** val eject__o__byte_to_psd_argument__o__inject :
     230    BitVector.byte Types.sig0 -> psd_argument Types.sig0 **)
     231let eject__o__byte_to_psd_argument__o__inject x2 =
     232  psd_argument_from_byte (Types.pi1 x2)
     233
     234(** val byte_to_psd_argument__o__inject :
     235    BitVector.byte -> psd_argument Types.sig0 **)
     236let byte_to_psd_argument__o__inject x1 =
     237  psd_argument_from_byte x1
     238
     239(** val dpi1__o__byte_to_psd_argument :
     240    (BitVector.byte, 'a1) Types.dPair -> psd_argument **)
     241let dpi1__o__byte_to_psd_argument x1 =
     242  psd_argument_from_byte x1.Types.dpi1
     243
     244(** val eject__o__byte_to_psd_argument :
     245    BitVector.byte Types.sig0 -> psd_argument **)
     246let eject__o__byte_to_psd_argument x1 =
     247  psd_argument_from_byte (Types.pi1 x1)
     248
    199249type hdw_argument = I8051.register argument
    200250
     
    203253  Reg x
    204254
     255(** val dpi1__o__reg_to_hdw_argument__o__inject :
     256    (I8051.register, 'a1) Types.dPair -> hdw_argument Types.sig0 **)
     257let dpi1__o__reg_to_hdw_argument__o__inject x2 =
     258  hdw_argument_from_reg x2.Types.dpi1
     259
     260(** val eject__o__reg_to_hdw_argument__o__inject :
     261    I8051.register Types.sig0 -> hdw_argument Types.sig0 **)
     262let eject__o__reg_to_hdw_argument__o__inject x2 =
     263  hdw_argument_from_reg (Types.pi1 x2)
     264
     265(** val reg_to_hdw_argument__o__inject :
     266    I8051.register -> hdw_argument Types.sig0 **)
     267let reg_to_hdw_argument__o__inject x1 =
     268  hdw_argument_from_reg x1
     269
     270(** val dpi1__o__reg_to_hdw_argument :
     271    (I8051.register, 'a1) Types.dPair -> hdw_argument **)
     272let dpi1__o__reg_to_hdw_argument x1 =
     273  hdw_argument_from_reg x1.Types.dpi1
     274
     275(** val eject__o__reg_to_hdw_argument :
     276    I8051.register Types.sig0 -> hdw_argument **)
     277let eject__o__reg_to_hdw_argument x1 =
     278  hdw_argument_from_reg (Types.pi1 x1)
     279
    205280(** val hdw_argument_from_byte : BitVector.byte -> hdw_argument **)
    206281let hdw_argument_from_byte x =
    207282  Imm x
     283
     284(** val dpi1__o__byte_to_hdw_argument__o__inject :
     285    (BitVector.byte, 'a1) Types.dPair -> psd_argument Types.sig0 **)
     286let dpi1__o__byte_to_hdw_argument__o__inject x2 =
     287  psd_argument_from_byte x2.Types.dpi1
     288
     289(** val eject__o__byte_to_hdw_argument__o__inject :
     290    BitVector.byte Types.sig0 -> psd_argument Types.sig0 **)
     291let eject__o__byte_to_hdw_argument__o__inject x2 =
     292  psd_argument_from_byte (Types.pi1 x2)
     293
     294(** val byte_to_hdw_argument__o__inject :
     295    BitVector.byte -> psd_argument Types.sig0 **)
     296let byte_to_hdw_argument__o__inject x1 =
     297  psd_argument_from_byte x1
     298
     299(** val dpi1__o__byte_to_hdw_argument :
     300    (BitVector.byte, 'a1) Types.dPair -> psd_argument **)
     301let dpi1__o__byte_to_hdw_argument x1 =
     302  psd_argument_from_byte x1.Types.dpi1
     303
     304(** val eject__o__byte_to_hdw_argument :
     305    BitVector.byte Types.sig0 -> psd_argument **)
     306let eject__o__byte_to_hdw_argument x1 =
     307  psd_argument_from_byte (Types.pi1 x1)
    208308
    209309(** val byte_of_nat : Nat.nat -> BitVector.byte **)
     
    224324    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    225325    unserialized_params -> 'a1 **)
    226 let rec unserialized_params_rect_Type4 h_mk_unserialized_params x_6359 =
     326let rec unserialized_params_rect_Type4 h_mk_unserialized_params x_19451 =
    227327  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    228     x_6359
     328    x_19451
    229329  in
    230330  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    235335    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    236336    unserialized_params -> 'a1 **)
    237 let rec unserialized_params_rect_Type5 h_mk_unserialized_params x_6361 =
     337let rec unserialized_params_rect_Type5 h_mk_unserialized_params x_19453 =
    238338  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    239     x_6361
     339    x_19453
    240340  in
    241341  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    246346    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    247347    unserialized_params -> 'a1 **)
    248 let rec unserialized_params_rect_Type3 h_mk_unserialized_params x_6363 =
     348let rec unserialized_params_rect_Type3 h_mk_unserialized_params x_19455 =
    249349  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    250     x_6363
     350    x_19455
    251351  in
    252352  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    257357    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    258358    unserialized_params -> 'a1 **)
    259 let rec unserialized_params_rect_Type2 h_mk_unserialized_params x_6365 =
     359let rec unserialized_params_rect_Type2 h_mk_unserialized_params x_19457 =
    260360  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    261     x_6365
     361    x_19457
    262362  in
    263363  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    268368    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    269369    unserialized_params -> 'a1 **)
    270 let rec unserialized_params_rect_Type1 h_mk_unserialized_params x_6367 =
     370let rec unserialized_params_rect_Type1 h_mk_unserialized_params x_19459 =
    271371  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    272     x_6367
     372    x_19459
    273373  in
    274374  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    279379    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    280380    unserialized_params -> 'a1 **)
    281 let rec unserialized_params_rect_Type0 h_mk_unserialized_params x_6369 =
     381let rec unserialized_params_rect_Type0 h_mk_unserialized_params x_19461 =
    282382  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    283     x_6369
     383    x_19461
    284384  in
    285385  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    389489    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    390490let rec joint_seq_rect_Type4 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
    391 | COMMENT x_6425 -> h_COMMENT x_6425
    392 | MOVE x_6426 -> h_MOVE x_6426
    393 | POP x_6427 -> h_POP x_6427
    394 | PUSH x_6428 -> h_PUSH x_6428
    395 | ADDRESS (i, x_6430, x_6429) -> h_ADDRESS i __ x_6430 x_6429
    396 | OPACCS (x_6436, x_6435, x_6434, x_6433, x_6432) ->
    397   h_OPACCS x_6436 x_6435 x_6434 x_6433 x_6432
    398 | OP1 (x_6439, x_6438, x_6437) -> h_OP1 x_6439 x_6438 x_6437
    399 | OP2 (x_6443, x_6442, x_6441, x_6440) -> h_OP2 x_6443 x_6442 x_6441 x_6440
     491| COMMENT x_19517 -> h_COMMENT x_19517
     492| MOVE x_19518 -> h_MOVE x_19518
     493| POP x_19519 -> h_POP x_19519
     494| PUSH x_19520 -> h_PUSH x_19520
     495| ADDRESS (i, x_19522, x_19521) -> h_ADDRESS i __ x_19522 x_19521
     496| OPACCS (x_19528, x_19527, x_19526, x_19525, x_19524) ->
     497  h_OPACCS x_19528 x_19527 x_19526 x_19525 x_19524
     498| OP1 (x_19531, x_19530, x_19529) -> h_OP1 x_19531 x_19530 x_19529
     499| OP2 (x_19535, x_19534, x_19533, x_19532) ->
     500  h_OP2 x_19535 x_19534 x_19533 x_19532
    400501| CLEAR_CARRY -> h_CLEAR_CARRY
    401502| SET_CARRY -> h_SET_CARRY
    402 | LOAD (x_6446, x_6445, x_6444) -> h_LOAD x_6446 x_6445 x_6444
    403 | STORE (x_6449, x_6448, x_6447) -> h_STORE x_6449 x_6448 x_6447
    404 | Extension_seq x_6450 -> h_extension_seq x_6450
     503| LOAD (x_19538, x_19537, x_19536) -> h_LOAD x_19538 x_19537 x_19536
     504| STORE (x_19541, x_19540, x_19539) -> h_STORE x_19541 x_19540 x_19539
     505| Extension_seq x_19542 -> h_extension_seq x_19542
    405506
    406507(** val joint_seq_rect_Type5 :
     
    412513    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    413514let rec joint_seq_rect_Type5 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
    414 | COMMENT x_6465 -> h_COMMENT x_6465
    415 | MOVE x_6466 -> h_MOVE x_6466
    416 | POP x_6467 -> h_POP x_6467
    417 | PUSH x_6468 -> h_PUSH x_6468
    418 | ADDRESS (i, x_6470, x_6469) -> h_ADDRESS i __ x_6470 x_6469
    419 | OPACCS (x_6476, x_6475, x_6474, x_6473, x_6472) ->
    420   h_OPACCS x_6476 x_6475 x_6474 x_6473 x_6472
    421 | OP1 (x_6479, x_6478, x_6477) -> h_OP1 x_6479 x_6478 x_6477
    422 | OP2 (x_6483, x_6482, x_6481, x_6480) -> h_OP2 x_6483 x_6482 x_6481 x_6480
     515| COMMENT x_19557 -> h_COMMENT x_19557
     516| MOVE x_19558 -> h_MOVE x_19558
     517| POP x_19559 -> h_POP x_19559
     518| PUSH x_19560 -> h_PUSH x_19560
     519| ADDRESS (i, x_19562, x_19561) -> h_ADDRESS i __ x_19562 x_19561
     520| OPACCS (x_19568, x_19567, x_19566, x_19565, x_19564) ->
     521  h_OPACCS x_19568 x_19567 x_19566 x_19565 x_19564
     522| OP1 (x_19571, x_19570, x_19569) -> h_OP1 x_19571 x_19570 x_19569
     523| OP2 (x_19575, x_19574, x_19573, x_19572) ->
     524  h_OP2 x_19575 x_19574 x_19573 x_19572
    423525| CLEAR_CARRY -> h_CLEAR_CARRY
    424526| SET_CARRY -> h_SET_CARRY
    425 | LOAD (x_6486, x_6485, x_6484) -> h_LOAD x_6486 x_6485 x_6484
    426 | STORE (x_6489, x_6488, x_6487) -> h_STORE x_6489 x_6488 x_6487
    427 | Extension_seq x_6490 -> h_extension_seq x_6490
     527| LOAD (x_19578, x_19577, x_19576) -> h_LOAD x_19578 x_19577 x_19576
     528| STORE (x_19581, x_19580, x_19579) -> h_STORE x_19581 x_19580 x_19579
     529| Extension_seq x_19582 -> h_extension_seq x_19582
    428530
    429531(** val joint_seq_rect_Type3 :
     
    435537    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    436538let rec joint_seq_rect_Type3 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
    437 | COMMENT x_6505 -> h_COMMENT x_6505
    438 | MOVE x_6506 -> h_MOVE x_6506
    439 | POP x_6507 -> h_POP x_6507
    440 | PUSH x_6508 -> h_PUSH x_6508
    441 | ADDRESS (i, x_6510, x_6509) -> h_ADDRESS i __ x_6510 x_6509
    442 | OPACCS (x_6516, x_6515, x_6514, x_6513, x_6512) ->
    443   h_OPACCS x_6516 x_6515 x_6514 x_6513 x_6512
    444 | OP1 (x_6519, x_6518, x_6517) -> h_OP1 x_6519 x_6518 x_6517
    445 | OP2 (x_6523, x_6522, x_6521, x_6520) -> h_OP2 x_6523 x_6522 x_6521 x_6520
     539| COMMENT x_19597 -> h_COMMENT x_19597
     540| MOVE x_19598 -> h_MOVE x_19598
     541| POP x_19599 -> h_POP x_19599
     542| PUSH x_19600 -> h_PUSH x_19600
     543| ADDRESS (i, x_19602, x_19601) -> h_ADDRESS i __ x_19602 x_19601
     544| OPACCS (x_19608, x_19607, x_19606, x_19605, x_19604) ->
     545  h_OPACCS x_19608 x_19607 x_19606 x_19605 x_19604
     546| OP1 (x_19611, x_19610, x_19609) -> h_OP1 x_19611 x_19610 x_19609
     547| OP2 (x_19615, x_19614, x_19613, x_19612) ->
     548  h_OP2 x_19615 x_19614 x_19613 x_19612
    446549| CLEAR_CARRY -> h_CLEAR_CARRY
    447550| SET_CARRY -> h_SET_CARRY
    448 | LOAD (x_6526, x_6525, x_6524) -> h_LOAD x_6526 x_6525 x_6524
    449 | STORE (x_6529, x_6528, x_6527) -> h_STORE x_6529 x_6528 x_6527
    450 | Extension_seq x_6530 -> h_extension_seq x_6530
     551| LOAD (x_19618, x_19617, x_19616) -> h_LOAD x_19618 x_19617 x_19616
     552| STORE (x_19621, x_19620, x_19619) -> h_STORE x_19621 x_19620 x_19619
     553| Extension_seq x_19622 -> h_extension_seq x_19622
    451554
    452555(** val joint_seq_rect_Type2 :
     
    458561    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    459562let rec joint_seq_rect_Type2 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
    460 | COMMENT x_6545 -> h_COMMENT x_6545
    461 | MOVE x_6546 -> h_MOVE x_6546
    462 | POP x_6547 -> h_POP x_6547
    463 | PUSH x_6548 -> h_PUSH x_6548
    464 | ADDRESS (i, x_6550, x_6549) -> h_ADDRESS i __ x_6550 x_6549
    465 | OPACCS (x_6556, x_6555, x_6554, x_6553, x_6552) ->
    466   h_OPACCS x_6556 x_6555 x_6554 x_6553 x_6552
    467 | OP1 (x_6559, x_6558, x_6557) -> h_OP1 x_6559 x_6558 x_6557
    468 | OP2 (x_6563, x_6562, x_6561, x_6560) -> h_OP2 x_6563 x_6562 x_6561 x_6560
     563| COMMENT x_19637 -> h_COMMENT x_19637
     564| MOVE x_19638 -> h_MOVE x_19638
     565| POP x_19639 -> h_POP x_19639
     566| PUSH x_19640 -> h_PUSH x_19640
     567| ADDRESS (i, x_19642, x_19641) -> h_ADDRESS i __ x_19642 x_19641
     568| OPACCS (x_19648, x_19647, x_19646, x_19645, x_19644) ->
     569  h_OPACCS x_19648 x_19647 x_19646 x_19645 x_19644
     570| OP1 (x_19651, x_19650, x_19649) -> h_OP1 x_19651 x_19650 x_19649
     571| OP2 (x_19655, x_19654, x_19653, x_19652) ->
     572  h_OP2 x_19655 x_19654 x_19653 x_19652
    469573| CLEAR_CARRY -> h_CLEAR_CARRY
    470574| SET_CARRY -> h_SET_CARRY
    471 | LOAD (x_6566, x_6565, x_6564) -> h_LOAD x_6566 x_6565 x_6564
    472 | STORE (x_6569, x_6568, x_6567) -> h_STORE x_6569 x_6568 x_6567
    473 | Extension_seq x_6570 -> h_extension_seq x_6570
     575| LOAD (x_19658, x_19657, x_19656) -> h_LOAD x_19658 x_19657 x_19656
     576| STORE (x_19661, x_19660, x_19659) -> h_STORE x_19661 x_19660 x_19659
     577| Extension_seq x_19662 -> h_extension_seq x_19662
    474578
    475579(** val joint_seq_rect_Type1 :
     
    481585    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    482586let rec joint_seq_rect_Type1 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
    483 | COMMENT x_6585 -> h_COMMENT x_6585
    484 | MOVE x_6586 -> h_MOVE x_6586
    485 | POP x_6587 -> h_POP x_6587
    486 | PUSH x_6588 -> h_PUSH x_6588
    487 | ADDRESS (i, x_6590, x_6589) -> h_ADDRESS i __ x_6590 x_6589
    488 | OPACCS (x_6596, x_6595, x_6594, x_6593, x_6592) ->
    489   h_OPACCS x_6596 x_6595 x_6594 x_6593 x_6592
    490 | OP1 (x_6599, x_6598, x_6597) -> h_OP1 x_6599 x_6598 x_6597
    491 | OP2 (x_6603, x_6602, x_6601, x_6600) -> h_OP2 x_6603 x_6602 x_6601 x_6600
     587| COMMENT x_19677 -> h_COMMENT x_19677
     588| MOVE x_19678 -> h_MOVE x_19678
     589| POP x_19679 -> h_POP x_19679
     590| PUSH x_19680 -> h_PUSH x_19680
     591| ADDRESS (i, x_19682, x_19681) -> h_ADDRESS i __ x_19682 x_19681
     592| OPACCS (x_19688, x_19687, x_19686, x_19685, x_19684) ->
     593  h_OPACCS x_19688 x_19687 x_19686 x_19685 x_19684
     594| OP1 (x_19691, x_19690, x_19689) -> h_OP1 x_19691 x_19690 x_19689
     595| OP2 (x_19695, x_19694, x_19693, x_19692) ->
     596  h_OP2 x_19695 x_19694 x_19693 x_19692
    492597| CLEAR_CARRY -> h_CLEAR_CARRY
    493598| SET_CARRY -> h_SET_CARRY
    494 | LOAD (x_6606, x_6605, x_6604) -> h_LOAD x_6606 x_6605 x_6604
    495 | STORE (x_6609, x_6608, x_6607) -> h_STORE x_6609 x_6608 x_6607
    496 | Extension_seq x_6610 -> h_extension_seq x_6610
     599| LOAD (x_19698, x_19697, x_19696) -> h_LOAD x_19698 x_19697 x_19696
     600| STORE (x_19701, x_19700, x_19699) -> h_STORE x_19701 x_19700 x_19699
     601| Extension_seq x_19702 -> h_extension_seq x_19702
    497602
    498603(** val joint_seq_rect_Type0 :
     
    504609    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    505610let rec joint_seq_rect_Type0 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
    506 | COMMENT x_6625 -> h_COMMENT x_6625
    507 | MOVE x_6626 -> h_MOVE x_6626
    508 | POP x_6627 -> h_POP x_6627
    509 | PUSH x_6628 -> h_PUSH x_6628
    510 | ADDRESS (i, x_6630, x_6629) -> h_ADDRESS i __ x_6630 x_6629
    511 | OPACCS (x_6636, x_6635, x_6634, x_6633, x_6632) ->
    512   h_OPACCS x_6636 x_6635 x_6634 x_6633 x_6632
    513 | OP1 (x_6639, x_6638, x_6637) -> h_OP1 x_6639 x_6638 x_6637
    514 | OP2 (x_6643, x_6642, x_6641, x_6640) -> h_OP2 x_6643 x_6642 x_6641 x_6640
     611| COMMENT x_19717 -> h_COMMENT x_19717
     612| MOVE x_19718 -> h_MOVE x_19718
     613| POP x_19719 -> h_POP x_19719
     614| PUSH x_19720 -> h_PUSH x_19720
     615| ADDRESS (i, x_19722, x_19721) -> h_ADDRESS i __ x_19722 x_19721
     616| OPACCS (x_19728, x_19727, x_19726, x_19725, x_19724) ->
     617  h_OPACCS x_19728 x_19727 x_19726 x_19725 x_19724
     618| OP1 (x_19731, x_19730, x_19729) -> h_OP1 x_19731 x_19730 x_19729
     619| OP2 (x_19735, x_19734, x_19733, x_19732) ->
     620  h_OP2 x_19735 x_19734 x_19733 x_19732
    515621| CLEAR_CARRY -> h_CLEAR_CARRY
    516622| SET_CARRY -> h_SET_CARRY
    517 | LOAD (x_6646, x_6645, x_6644) -> h_LOAD x_6646 x_6645 x_6644
    518 | STORE (x_6649, x_6648, x_6647) -> h_STORE x_6649 x_6648 x_6647
    519 | Extension_seq x_6650 -> h_extension_seq x_6650
     623| LOAD (x_19738, x_19737, x_19736) -> h_LOAD x_19738 x_19737 x_19736
     624| STORE (x_19741, x_19740, x_19739) -> h_STORE x_19741 x_19740 x_19739
     625| Extension_seq x_19742 -> h_extension_seq x_19742
    520626
    521627(** val joint_seq_inv_rect_Type4 :
     
    640746  COMMENT String.EmptyString
    641747
     748(** val dpi1__o__extension_seq_to_seq__o__inject :
     749    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
     750    joint_seq Types.sig0 **)
     751let dpi1__o__extension_seq_to_seq__o__inject x0 x1 x4 =
     752  Extension_seq x4.Types.dpi1
     753
     754(** val eject__o__extension_seq_to_seq__o__inject :
     755    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq
     756    Types.sig0 **)
     757let eject__o__extension_seq_to_seq__o__inject x0 x1 x4 =
     758  Extension_seq (Types.pi1 x4)
     759
     760(** val extension_seq_to_seq__o__inject :
     761    unserialized_params -> AST.ident List.list -> __ -> joint_seq Types.sig0 **)
     762let extension_seq_to_seq__o__inject x0 x1 x3 =
     763  Extension_seq x3
     764
     765(** val dpi1__o__extension_seq_to_seq :
     766    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
     767    joint_seq **)
     768let dpi1__o__extension_seq_to_seq x0 x1 x3 =
     769  Extension_seq x3.Types.dpi1
     770
     771(** val eject__o__extension_seq_to_seq :
     772    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq **)
     773let eject__o__extension_seq_to_seq x0 x1 x3 =
     774  Extension_seq (Types.pi1 x3)
     775
    642776type joint_step =
    643777| COST_LABEL of CostLabel.costlabel
     
    651785    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    652786let rec joint_step_rect_Type4 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    653 | COST_LABEL x_6917 -> h_COST_LABEL x_6917
    654 | CALL (x_6920, x_6919, x_6918) -> h_CALL x_6920 x_6919 x_6918
    655 | COND (x_6922, x_6921) -> h_COND x_6922 x_6921
    656 | Step_seq x_6923 -> h_step_seq x_6923
     787| COST_LABEL x_20009 -> h_COST_LABEL x_20009
     788| CALL (x_20012, x_20011, x_20010) -> h_CALL x_20012 x_20011 x_20010
     789| COND (x_20014, x_20013) -> h_COND x_20014 x_20013
     790| Step_seq x_20015 -> h_step_seq x_20015
    657791
    658792(** val joint_step_rect_Type5 :
     
    661795    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    662796let rec joint_step_rect_Type5 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    663 | COST_LABEL x_6929 -> h_COST_LABEL x_6929
    664 | CALL (x_6932, x_6931, x_6930) -> h_CALL x_6932 x_6931 x_6930
    665 | COND (x_6934, x_6933) -> h_COND x_6934 x_6933
    666 | Step_seq x_6935 -> h_step_seq x_6935
     797| COST_LABEL x_20021 -> h_COST_LABEL x_20021
     798| CALL (x_20024, x_20023, x_20022) -> h_CALL x_20024 x_20023 x_20022
     799| COND (x_20026, x_20025) -> h_COND x_20026 x_20025
     800| Step_seq x_20027 -> h_step_seq x_20027
    667801
    668802(** val joint_step_rect_Type3 :
     
    671805    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    672806let rec joint_step_rect_Type3 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    673 | COST_LABEL x_6941 -> h_COST_LABEL x_6941
    674 | CALL (x_6944, x_6943, x_6942) -> h_CALL x_6944 x_6943 x_6942
    675 | COND (x_6946, x_6945) -> h_COND x_6946 x_6945
    676 | Step_seq x_6947 -> h_step_seq x_6947
     807| COST_LABEL x_20033 -> h_COST_LABEL x_20033
     808| CALL (x_20036, x_20035, x_20034) -> h_CALL x_20036 x_20035 x_20034
     809| COND (x_20038, x_20037) -> h_COND x_20038 x_20037
     810| Step_seq x_20039 -> h_step_seq x_20039
    677811
    678812(** val joint_step_rect_Type2 :
     
    681815    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    682816let rec joint_step_rect_Type2 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    683 | COST_LABEL x_6953 -> h_COST_LABEL x_6953
    684 | CALL (x_6956, x_6955, x_6954) -> h_CALL x_6956 x_6955 x_6954
    685 | COND (x_6958, x_6957) -> h_COND x_6958 x_6957
    686 | Step_seq x_6959 -> h_step_seq x_6959
     817| COST_LABEL x_20045 -> h_COST_LABEL x_20045
     818| CALL (x_20048, x_20047, x_20046) -> h_CALL x_20048 x_20047 x_20046
     819| COND (x_20050, x_20049) -> h_COND x_20050 x_20049
     820| Step_seq x_20051 -> h_step_seq x_20051
    687821
    688822(** val joint_step_rect_Type1 :
     
    691825    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    692826let rec joint_step_rect_Type1 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    693 | COST_LABEL x_6965 -> h_COST_LABEL x_6965
    694 | CALL (x_6968, x_6967, x_6966) -> h_CALL x_6968 x_6967 x_6966
    695 | COND (x_6970, x_6969) -> h_COND x_6970 x_6969
    696 | Step_seq x_6971 -> h_step_seq x_6971
     827| COST_LABEL x_20057 -> h_COST_LABEL x_20057
     828| CALL (x_20060, x_20059, x_20058) -> h_CALL x_20060 x_20059 x_20058
     829| COND (x_20062, x_20061) -> h_COND x_20062 x_20061
     830| Step_seq x_20063 -> h_step_seq x_20063
    697831
    698832(** val joint_step_rect_Type0 :
     
    701835    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    702836let rec joint_step_rect_Type0 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    703 | COST_LABEL x_6977 -> h_COST_LABEL x_6977
    704 | CALL (x_6980, x_6979, x_6978) -> h_CALL x_6980 x_6979 x_6978
    705 | COND (x_6982, x_6981) -> h_COND x_6982 x_6981
    706 | Step_seq x_6983 -> h_step_seq x_6983
     837| COST_LABEL x_20069 -> h_COST_LABEL x_20069
     838| CALL (x_20072, x_20071, x_20070) -> h_CALL x_20072 x_20071 x_20070
     839| COND (x_20074, x_20073) -> h_COND x_20074 x_20073
     840| Step_seq x_20075 -> h_step_seq x_20075
    707841
    708842(** val joint_step_inv_rect_Type4 :
     
    767901     | COND (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
    768902     | Step_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
     903
     904(** val dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject :
     905    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
     906    joint_step Types.sig0 **)
     907let dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x4 =
     908  Step_seq (dpi1__o__extension_seq_to_seq x0 x1 x4)
     909
     910(** val eject__o__extension_seq_to_seq__o__seq_to_step__o__inject :
     911    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step
     912    Types.sig0 **)
     913let eject__o__extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x4 =
     914  Step_seq (eject__o__extension_seq_to_seq x0 x1 x4)
     915
     916(** val extension_seq_to_seq__o__seq_to_step__o__inject :
     917    unserialized_params -> AST.ident List.list -> __ -> joint_step Types.sig0 **)
     918let extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x2 =
     919  Step_seq (Extension_seq x2)
     920
     921(** val dpi1__o__seq_to_step__o__inject :
     922    unserialized_params -> AST.ident List.list -> (joint_seq, 'a1)
     923    Types.dPair -> joint_step Types.sig0 **)
     924let dpi1__o__seq_to_step__o__inject x0 x1 x4 =
     925  Step_seq x4.Types.dpi1
     926
     927(** val eject__o__seq_to_step__o__inject :
     928    unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
     929    joint_step Types.sig0 **)
     930let eject__o__seq_to_step__o__inject x0 x1 x4 =
     931  Step_seq (Types.pi1 x4)
     932
     933(** val seq_to_step__o__inject :
     934    unserialized_params -> AST.ident List.list -> joint_seq -> joint_step
     935    Types.sig0 **)
     936let seq_to_step__o__inject x0 x1 x3 =
     937  Step_seq x3
     938
     939(** val dpi1__o__extension_seq_to_seq__o__seq_to_step :
     940    unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
     941    joint_step **)
     942let dpi1__o__extension_seq_to_seq__o__seq_to_step x0 x1 x3 =
     943  Step_seq (dpi1__o__extension_seq_to_seq x0 x1 x3)
     944
     945(** val eject__o__extension_seq_to_seq__o__seq_to_step :
     946    unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step **)
     947let eject__o__extension_seq_to_seq__o__seq_to_step x0 x1 x3 =
     948  Step_seq (eject__o__extension_seq_to_seq x0 x1 x3)
     949
     950(** val extension_seq_to_seq__o__seq_to_step :
     951    unserialized_params -> AST.ident List.list -> __ -> joint_step **)
     952let extension_seq_to_seq__o__seq_to_step x0 x1 x2 =
     953  Step_seq (Extension_seq x2)
     954
     955(** val dpi1__o__seq_to_step :
     956    unserialized_params -> AST.ident List.list -> (joint_seq, 'a1)
     957    Types.dPair -> joint_step **)
     958let dpi1__o__seq_to_step x0 x1 x3 =
     959  Step_seq x3.Types.dpi1
     960
     961(** val eject__o__seq_to_step :
     962    unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
     963    joint_step **)
     964let eject__o__seq_to_step x0 x1 x3 =
     965  Step_seq (Types.pi1 x3)
    769966
    770967(** val step_labels :
     
    798995    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
    799996    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
    800 let rec stmt_params_rect_Type4 h_mk_stmt_params x_7062 =
     997let rec stmt_params_rect_Type4 h_mk_stmt_params x_20154 =
    801998  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    802     has_fcond0 } = x_7062
     999    has_fcond0 } = x_20154
    8031000  in
    8041001  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    8071004    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
    8081005    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
    809 let rec stmt_params_rect_Type5 h_mk_stmt_params x_7064 =
     1006let rec stmt_params_rect_Type5 h_mk_stmt_params x_20156 =
    8101007  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    811     has_fcond0 } = x_7064
     1008    has_fcond0 } = x_20156
    8121009  in
    8131010  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    8161013    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
    8171014    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
    818 let rec stmt_params_rect_Type3 h_mk_stmt_params x_7066 =
     1015let rec stmt_params_rect_Type3 h_mk_stmt_params x_20158 =
    8191016  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    820     has_fcond0 } = x_7066
     1017    has_fcond0 } = x_20158
    8211018  in
    8221019  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    8251022    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
    8261023    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
    827 let rec stmt_params_rect_Type2 h_mk_stmt_params x_7068 =
     1024let rec stmt_params_rect_Type2 h_mk_stmt_params x_20160 =
    8281025  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    829     has_fcond0 } = x_7068
     1026    has_fcond0 } = x_20160
    8301027  in
    8311028  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    8341031    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
    8351032    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
    836 let rec stmt_params_rect_Type1 h_mk_stmt_params x_7070 =
     1033let rec stmt_params_rect_Type1 h_mk_stmt_params x_20162 =
    8371034  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    838     has_fcond0 } = x_7070
     1035    has_fcond0 } = x_20162
    8391036  in
    8401037  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    8431040    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
    8441041    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
    845 let rec stmt_params_rect_Type0 h_mk_stmt_params x_7072 =
     1042let rec stmt_params_rect_Type0 h_mk_stmt_params x_20164 =
    8461043  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    847     has_fcond0 } = x_7072
     1044    has_fcond0 } = x_20164
    8481045  in
    8491046  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    9081105    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    9091106let rec joint_fin_step_rect_Type4 p h_GOTO h_RETURN h_TAILCALL = function
    910 | GOTO x_7096 -> h_GOTO x_7096
     1107| GOTO x_20188 -> h_GOTO x_20188
    9111108| RETURN -> h_RETURN
    912 | TAILCALL (x_7098, x_7097) -> h_TAILCALL __ x_7098 x_7097
     1109| TAILCALL (x_20190, x_20189) -> h_TAILCALL __ x_20190 x_20189
    9131110
    9141111(** val joint_fin_step_rect_Type5 :
     
    9161113    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    9171114let rec joint_fin_step_rect_Type5 p h_GOTO h_RETURN h_TAILCALL = function
    918 | GOTO x_7104 -> h_GOTO x_7104
     1115| GOTO x_20196 -> h_GOTO x_20196
    9191116| RETURN -> h_RETURN
    920 | TAILCALL (x_7106, x_7105) -> h_TAILCALL __ x_7106 x_7105
     1117| TAILCALL (x_20198, x_20197) -> h_TAILCALL __ x_20198 x_20197
    9211118
    9221119(** val joint_fin_step_rect_Type3 :
     
    9241121    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    9251122let rec joint_fin_step_rect_Type3 p h_GOTO h_RETURN h_TAILCALL = function
    926 | GOTO x_7112 -> h_GOTO x_7112
     1123| GOTO x_20204 -> h_GOTO x_20204
    9271124| RETURN -> h_RETURN
    928 | TAILCALL (x_7114, x_7113) -> h_TAILCALL __ x_7114 x_7113
     1125| TAILCALL (x_20206, x_20205) -> h_TAILCALL __ x_20206 x_20205
    9291126
    9301127(** val joint_fin_step_rect_Type2 :
     
    9321129    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    9331130let rec joint_fin_step_rect_Type2 p h_GOTO h_RETURN h_TAILCALL = function
    934 | GOTO x_7120 -> h_GOTO x_7120
     1131| GOTO x_20212 -> h_GOTO x_20212
    9351132| RETURN -> h_RETURN
    936 | TAILCALL (x_7122, x_7121) -> h_TAILCALL __ x_7122 x_7121
     1133| TAILCALL (x_20214, x_20213) -> h_TAILCALL __ x_20214 x_20213
    9371134
    9381135(** val joint_fin_step_rect_Type1 :
     
    9401137    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    9411138let rec joint_fin_step_rect_Type1 p h_GOTO h_RETURN h_TAILCALL = function
    942 | GOTO x_7128 -> h_GOTO x_7128
     1139| GOTO x_20220 -> h_GOTO x_20220
    9431140| RETURN -> h_RETURN
    944 | TAILCALL (x_7130, x_7129) -> h_TAILCALL __ x_7130 x_7129
     1141| TAILCALL (x_20222, x_20221) -> h_TAILCALL __ x_20222 x_20221
    9451142
    9461143(** val joint_fin_step_rect_Type0 :
     
    9481145    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    9491146let rec joint_fin_step_rect_Type0 p h_GOTO h_RETURN h_TAILCALL = function
    950 | GOTO x_7136 -> h_GOTO x_7136
     1147| GOTO x_20228 -> h_GOTO x_20228
    9511148| RETURN -> h_RETURN
    952 | TAILCALL (x_7138, x_7137) -> h_TAILCALL __ x_7138 x_7137
     1149| TAILCALL (x_20230, x_20229) -> h_TAILCALL __ x_20230 x_20229
    9531150
    9541151(** val joint_fin_step_inv_rect_Type4 :
     
    10221219    'a1) -> joint_statement -> 'a1 **)
    10231220let rec joint_statement_rect_Type4 p globals h_sequential h_final h_FCOND = function
    1024 | Sequential (x_7204, x_7203) -> h_sequential x_7204 x_7203
    1025 | Final x_7205 -> h_final x_7205
    1026 | FCOND (x_7208, x_7207, x_7206) -> h_FCOND __ x_7208 x_7207 x_7206
     1221| Sequential (x_20296, x_20295) -> h_sequential x_20296 x_20295
     1222| Final x_20297 -> h_final x_20297
     1223| FCOND (x_20300, x_20299, x_20298) -> h_FCOND __ x_20300 x_20299 x_20298
    10271224
    10281225(** val joint_statement_rect_Type5 :
     
    10311228    'a1) -> joint_statement -> 'a1 **)
    10321229let rec joint_statement_rect_Type5 p globals h_sequential h_final h_FCOND = function
    1033 | Sequential (x_7215, x_7214) -> h_sequential x_7215 x_7214
    1034 | Final x_7216 -> h_final x_7216
    1035 | FCOND (x_7219, x_7218, x_7217) -> h_FCOND __ x_7219 x_7218 x_7217
     1230| Sequential (x_20307, x_20306) -> h_sequential x_20307 x_20306
     1231| Final x_20308 -> h_final x_20308
     1232| FCOND (x_20311, x_20310, x_20309) -> h_FCOND __ x_20311 x_20310 x_20309
    10361233
    10371234(** val joint_statement_rect_Type3 :
     
    10401237    'a1) -> joint_statement -> 'a1 **)
    10411238let rec joint_statement_rect_Type3 p globals h_sequential h_final h_FCOND = function
    1042 | Sequential (x_7226, x_7225) -> h_sequential x_7226 x_7225
    1043 | Final x_7227 -> h_final x_7227
    1044 | FCOND (x_7230, x_7229, x_7228) -> h_FCOND __ x_7230 x_7229 x_7228
     1239| Sequential (x_20318, x_20317) -> h_sequential x_20318 x_20317
     1240| Final x_20319 -> h_final x_20319
     1241| FCOND (x_20322, x_20321, x_20320) -> h_FCOND __ x_20322 x_20321 x_20320
    10451242
    10461243(** val joint_statement_rect_Type2 :
     
    10491246    'a1) -> joint_statement -> 'a1 **)
    10501247let rec joint_statement_rect_Type2 p globals h_sequential h_final h_FCOND = function
    1051 | Sequential (x_7237, x_7236) -> h_sequential x_7237 x_7236
    1052 | Final x_7238 -> h_final x_7238
    1053 | FCOND (x_7241, x_7240, x_7239) -> h_FCOND __ x_7241 x_7240 x_7239
     1248| Sequential (x_20329, x_20328) -> h_sequential x_20329 x_20328
     1249| Final x_20330 -> h_final x_20330
     1250| FCOND (x_20333, x_20332, x_20331) -> h_FCOND __ x_20333 x_20332 x_20331
    10541251
    10551252(** val joint_statement_rect_Type1 :
     
    10581255    'a1) -> joint_statement -> 'a1 **)
    10591256let rec joint_statement_rect_Type1 p globals h_sequential h_final h_FCOND = function
    1060 | Sequential (x_7248, x_7247) -> h_sequential x_7248 x_7247
    1061 | Final x_7249 -> h_final x_7249
    1062 | FCOND (x_7252, x_7251, x_7250) -> h_FCOND __ x_7252 x_7251 x_7250
     1257| Sequential (x_20340, x_20339) -> h_sequential x_20340 x_20339
     1258| Final x_20341 -> h_final x_20341
     1259| FCOND (x_20344, x_20343, x_20342) -> h_FCOND __ x_20344 x_20343 x_20342
    10631260
    10641261(** val joint_statement_rect_Type0 :
     
    10671264    'a1) -> joint_statement -> 'a1 **)
    10681265let rec joint_statement_rect_Type0 p globals h_sequential h_final h_FCOND = function
    1069 | Sequential (x_7259, x_7258) -> h_sequential x_7259 x_7258
    1070 | Final x_7260 -> h_final x_7260
    1071 | FCOND (x_7263, x_7262, x_7261) -> h_FCOND __ x_7263 x_7262 x_7261
     1266| Sequential (x_20351, x_20350) -> h_sequential x_20351 x_20350
     1267| Final x_20352 -> h_final x_20352
     1268| FCOND (x_20355, x_20354, x_20353) -> h_FCOND __ x_20355 x_20354 x_20353
    10721269
    10731270(** val joint_statement_inv_rect_Type4 :
     
    11261323     | FCOND (a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
    11271324
     1325(** val dpi1__o__fin_step_to_stmt__o__inject :
     1326    stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair
     1327    -> joint_statement Types.sig0 **)
     1328let dpi1__o__fin_step_to_stmt__o__inject x0 x1 x4 =
     1329  Final x4.Types.dpi1
     1330
     1331(** val eject__o__fin_step_to_stmt__o__inject :
     1332    stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
     1333    joint_statement Types.sig0 **)
     1334let eject__o__fin_step_to_stmt__o__inject x0 x1 x4 =
     1335  Final (Types.pi1 x4)
     1336
     1337(** val fin_step_to_stmt__o__inject :
     1338    stmt_params -> AST.ident List.list -> joint_fin_step -> joint_statement
     1339    Types.sig0 **)
     1340let fin_step_to_stmt__o__inject x0 x1 x3 =
     1341  Final x3
     1342
     1343(** val dpi1__o__fin_step_to_stmt :
     1344    stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair
     1345    -> joint_statement **)
     1346let dpi1__o__fin_step_to_stmt x0 x1 x3 =
     1347  Final x3.Types.dpi1
     1348
     1349(** val eject__o__fin_step_to_stmt :
     1350    stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
     1351    joint_statement **)
     1352let eject__o__fin_step_to_stmt x0 x1 x3 =
     1353  Final (Types.pi1 x3)
     1354
    11281355type params = { stmt_pars : stmt_params;
    11291356                stmt_at : (AST.ident List.list -> __ -> __ -> joint_statement
     
    11381365    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    11391366    'a1 **)
    1140 let rec params_rect_Type4 h_mk_params x_7336 =
     1367let rec params_rect_Type4 h_mk_params x_20428 =
    11411368  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1142     point_of_label0; point_of_succ = point_of_succ0 } = x_7336
     1369    point_of_label0; point_of_succ = point_of_succ0 } = x_20428
    11431370  in
    11441371  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    11491376    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    11501377    'a1 **)
    1151 let rec params_rect_Type5 h_mk_params x_7338 =
     1378let rec params_rect_Type5 h_mk_params x_20430 =
    11521379  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1153     point_of_label0; point_of_succ = point_of_succ0 } = x_7338
     1380    point_of_label0; point_of_succ = point_of_succ0 } = x_20430
    11541381  in
    11551382  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    11601387    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    11611388    'a1 **)
    1162 let rec params_rect_Type3 h_mk_params x_7340 =
     1389let rec params_rect_Type3 h_mk_params x_20432 =
    11631390  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1164     point_of_label0; point_of_succ = point_of_succ0 } = x_7340
     1391    point_of_label0; point_of_succ = point_of_succ0 } = x_20432
    11651392  in
    11661393  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    11711398    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    11721399    'a1 **)
    1173 let rec params_rect_Type2 h_mk_params x_7342 =
     1400let rec params_rect_Type2 h_mk_params x_20434 =
    11741401  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1175     point_of_label0; point_of_succ = point_of_succ0 } = x_7342
     1402    point_of_label0; point_of_succ = point_of_succ0 } = x_20434
    11761403  in
    11771404  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    11821409    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    11831410    'a1 **)
    1184 let rec params_rect_Type1 h_mk_params x_7344 =
     1411let rec params_rect_Type1 h_mk_params x_20436 =
    11851412  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1186     point_of_label0; point_of_succ = point_of_succ0 } = x_7344
     1413    point_of_label0; point_of_succ = point_of_succ0 } = x_20436
    11871414  in
    11881415  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    11931420    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    11941421    'a1 **)
    1195 let rec params_rect_Type0 h_mk_params x_7346 =
     1422let rec params_rect_Type0 h_mk_params x_20438 =
    11961423  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1197     point_of_label0; point_of_succ = point_of_succ0 } = x_7346
     1424    point_of_label0; point_of_succ = point_of_succ0 } = x_20438
    11981425  in
    11991426  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    13141541(** val lin_params_rect_Type4 :
    13151542    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
    1316 let rec lin_params_rect_Type4 h_mk_lin_params x_7369 =
    1317   let l_u_pars = x_7369 in h_mk_lin_params l_u_pars
     1543let rec lin_params_rect_Type4 h_mk_lin_params x_20461 =
     1544  let l_u_pars = x_20461 in h_mk_lin_params l_u_pars
    13181545
    13191546(** val lin_params_rect_Type5 :
    13201547    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
    1321 let rec lin_params_rect_Type5 h_mk_lin_params x_7371 =
    1322   let l_u_pars = x_7371 in h_mk_lin_params l_u_pars
     1548let rec lin_params_rect_Type5 h_mk_lin_params x_20463 =
     1549  let l_u_pars = x_20463 in h_mk_lin_params l_u_pars
    13231550
    13241551(** val lin_params_rect_Type3 :
    13251552    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
    1326 let rec lin_params_rect_Type3 h_mk_lin_params x_7373 =
    1327   let l_u_pars = x_7373 in h_mk_lin_params l_u_pars
     1553let rec lin_params_rect_Type3 h_mk_lin_params x_20465 =
     1554  let l_u_pars = x_20465 in h_mk_lin_params l_u_pars
    13281555
    13291556(** val lin_params_rect_Type2 :
    13301557    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
    1331 let rec lin_params_rect_Type2 h_mk_lin_params x_7375 =
    1332   let l_u_pars = x_7375 in h_mk_lin_params l_u_pars
     1558let rec lin_params_rect_Type2 h_mk_lin_params x_20467 =
     1559  let l_u_pars = x_20467 in h_mk_lin_params l_u_pars
    13331560
    13341561(** val lin_params_rect_Type1 :
    13351562    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
    1336 let rec lin_params_rect_Type1 h_mk_lin_params x_7377 =
    1337   let l_u_pars = x_7377 in h_mk_lin_params l_u_pars
     1563let rec lin_params_rect_Type1 h_mk_lin_params x_20469 =
     1564  let l_u_pars = x_20469 in h_mk_lin_params l_u_pars
    13381565
    13391566(** val lin_params_rect_Type0 :
    13401567    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
    1341 let rec lin_params_rect_Type0 h_mk_lin_params x_7379 =
    1342   let l_u_pars = x_7379 in h_mk_lin_params l_u_pars
     1568let rec lin_params_rect_Type0 h_mk_lin_params x_20471 =
     1569  let l_u_pars = x_20471 in h_mk_lin_params l_u_pars
    13431570
    13441571(** val l_u_pars : lin_params -> unserialized_params **)
     
    13951622    (fun current x -> Obj.magic (Nat.S (Obj.magic current))) }
    13961623
     1624(** val lp_to_p__o__stmt_pars : lin_params -> stmt_params **)
     1625let lp_to_p__o__stmt_pars x0 =
     1626  (lin_params_to_params x0).stmt_pars
     1627
     1628(** val lp_to_p__o__stmt_pars__o__uns_pars :
     1629    lin_params -> unserialized_params **)
     1630let lp_to_p__o__stmt_pars__o__uns_pars x0 =
     1631  stmt_pars__o__uns_pars (lin_params_to_params x0)
     1632
    13971633type graph_params =
    13981634  unserialized_params
     
    14011637(** val graph_params_rect_Type4 :
    14021638    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
    1403 let rec graph_params_rect_Type4 h_mk_graph_params x_7395 =
    1404   let g_u_pars = x_7395 in h_mk_graph_params g_u_pars
     1639let rec graph_params_rect_Type4 h_mk_graph_params x_20487 =
     1640  let g_u_pars = x_20487 in h_mk_graph_params g_u_pars
    14051641
    14061642(** val graph_params_rect_Type5 :
    14071643    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
    1408 let rec graph_params_rect_Type5 h_mk_graph_params x_7397 =
    1409   let g_u_pars = x_7397 in h_mk_graph_params g_u_pars
     1644let rec graph_params_rect_Type5 h_mk_graph_params x_20489 =
     1645  let g_u_pars = x_20489 in h_mk_graph_params g_u_pars
    14101646
    14111647(** val graph_params_rect_Type3 :
    14121648    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
    1413 let rec graph_params_rect_Type3 h_mk_graph_params x_7399 =
    1414   let g_u_pars = x_7399 in h_mk_graph_params g_u_pars
     1649let rec graph_params_rect_Type3 h_mk_graph_params x_20491 =
     1650  let g_u_pars = x_20491 in h_mk_graph_params g_u_pars
    14151651
    14161652(** val graph_params_rect_Type2 :
    14171653    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
    1418 let rec graph_params_rect_Type2 h_mk_graph_params x_7401 =
    1419   let g_u_pars = x_7401 in h_mk_graph_params g_u_pars
     1654let rec graph_params_rect_Type2 h_mk_graph_params x_20493 =
     1655  let g_u_pars = x_20493 in h_mk_graph_params g_u_pars
    14201656
    14211657(** val graph_params_rect_Type1 :
    14221658    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
    1423 let rec graph_params_rect_Type1 h_mk_graph_params x_7403 =
    1424   let g_u_pars = x_7403 in h_mk_graph_params g_u_pars
     1659let rec graph_params_rect_Type1 h_mk_graph_params x_20495 =
     1660  let g_u_pars = x_20495 in h_mk_graph_params g_u_pars
    14251661
    14261662(** val graph_params_rect_Type0 :
    14271663    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
    1428 let rec graph_params_rect_Type0 h_mk_graph_params x_7405 =
    1429   let g_u_pars = x_7405 in h_mk_graph_params g_u_pars
     1664let rec graph_params_rect_Type0 h_mk_graph_params x_20497 =
     1665  let g_u_pars = x_20497 in h_mk_graph_params g_u_pars
    14301666
    14311667(** val g_u_pars : graph_params -> unserialized_params **)
     
    14721708    point_of_succ = (fun x lbl -> lbl) }
    14731709
     1710(** val gp_to_p__o__stmt_pars : graph_params -> stmt_params **)
     1711let gp_to_p__o__stmt_pars x0 =
     1712  (graph_params_to_params x0).stmt_pars
     1713
     1714(** val gp_to_p__o__stmt_pars__o__uns_pars :
     1715    graph_params -> unserialized_params **)
     1716let gp_to_p__o__stmt_pars__o__uns_pars x0 =
     1717  stmt_pars__o__uns_pars (graph_params_to_params x0)
     1718
    14741719type joint_internal_function = { joint_if_luniverse : Identifiers.universe;
    14751720                                 joint_if_runiverse : Identifiers.universe;
     
    14831728    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
    14841729    'a1) -> joint_internal_function -> 'a1 **)
    1485 let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_7421 =
     1730let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_20513 =
    14861731  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    14871732    joint_if_runiverse0; joint_if_result = joint_if_result0;
    14881733    joint_if_params = joint_if_params0; joint_if_stacksize =
    14891734    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
    1490     joint_if_entry0 } = x_7421
     1735    joint_if_entry0 } = x_20513
    14911736  in
    14921737  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    14981743    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
    14991744    'a1) -> joint_internal_function -> 'a1 **)
    1500 let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_7423 =
     1745let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_20515 =
    15011746  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    15021747    joint_if_runiverse0; joint_if_result = joint_if_result0;
    15031748    joint_if_params = joint_if_params0; joint_if_stacksize =
    15041749    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
    1505     joint_if_entry0 } = x_7423
     1750    joint_if_entry0 } = x_20515
    15061751  in
    15071752  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    15131758    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
    15141759    'a1) -> joint_internal_function -> 'a1 **)
    1515 let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_7425 =
     1760let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_20517 =
    15161761  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    15171762    joint_if_runiverse0; joint_if_result = joint_if_result0;
    15181763    joint_if_params = joint_if_params0; joint_if_stacksize =
    15191764    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
    1520     joint_if_entry0 } = x_7425
     1765    joint_if_entry0 } = x_20517
    15211766  in
    15221767  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    15281773    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
    15291774    'a1) -> joint_internal_function -> 'a1 **)
    1530 let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_7427 =
     1775let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_20519 =
    15311776  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    15321777    joint_if_runiverse0; joint_if_result = joint_if_result0;
    15331778    joint_if_params = joint_if_params0; joint_if_stacksize =
    15341779    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
    1535     joint_if_entry0 } = x_7427
     1780    joint_if_entry0 } = x_20519
    15361781  in
    15371782  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    15431788    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
    15441789    'a1) -> joint_internal_function -> 'a1 **)
    1545 let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_7429 =
     1790let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_20521 =
    15461791  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    15471792    joint_if_runiverse0; joint_if_result = joint_if_result0;
    15481793    joint_if_params = joint_if_params0; joint_if_stacksize =
    15491794    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
    1550     joint_if_entry0 } = x_7429
     1795    joint_if_entry0 } = x_20521
    15511796  in
    15521797  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    15581803    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
    15591804    'a1) -> joint_internal_function -> 'a1 **)
    1560 let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_7431 =
     1805let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_20523 =
    15611806  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    15621807    joint_if_runiverse0; joint_if_result = joint_if_result0;
    15631808    joint_if_params = joint_if_params0; joint_if_stacksize =
    15641809    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
    1565     joint_if_entry0 } = x_7431
     1810    joint_if_entry0 } = x_20523
    15661811  in
    15671812  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    17842029type joint_program = (joint_function, Nat.nat) AST.program
    17852030
    1786 let lp_to_p__o__stmt_pars _ = assert false
Note: See TracChangeset for help on using the changeset viewer.