Changeset 2730 for extracted/joint.ml


Ignore:
Timestamp:
Feb 25, 2013, 9:54:49 PM (7 years ago)
Author:
sacerdot
Message:

Exported again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/joint.ml

    r2717 r2730  
    110110    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
    111111let rec argument_rect_Type4 h_Reg h_Imm = function
    112 | Reg x_16310 -> h_Reg x_16310
    113 | Imm x_16311 -> h_Imm x_16311
     112| Reg x_6298 -> h_Reg x_6298
     113| Imm x_6299 -> h_Imm x_6299
    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_16315 -> h_Reg x_16315
    119 | Imm x_16316 -> h_Imm x_16316
     118| Reg x_6303 -> h_Reg x_6303
     119| Imm x_6304 -> h_Imm x_6304
    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_16320 -> h_Reg x_16320
    125 | Imm x_16321 -> h_Imm x_16321
     124| Reg x_6308 -> h_Reg x_6308
     125| Imm x_6309 -> h_Imm x_6309
    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_16325 -> h_Reg x_16325
    131 | Imm x_16326 -> h_Imm x_16326
     130| Reg x_6313 -> h_Reg x_6313
     131| Imm x_6314 -> h_Imm x_6314
    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_16330 -> h_Reg x_16330
    137 | Imm x_16331 -> h_Imm x_16331
     136| Reg x_6318 -> h_Reg x_6318
     137| Imm x_6319 -> h_Imm x_6319
    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_16335 -> h_Reg x_16335
    143 | Imm x_16336 -> h_Imm x_16336
     142| Reg x_6323 -> h_Reg x_6323
     143| Imm x_6324 -> h_Imm x_6324
    144144
    145145(** val argument_inv_rect_Type4 :
     
    224224    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    225225    unserialized_params -> 'a1 **)
    226 let rec unserialized_params_rect_Type4 h_mk_unserialized_params x_16371 =
     226let rec unserialized_params_rect_Type4 h_mk_unserialized_params x_6359 =
    227227  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    228     x_16371
     228    x_6359
    229229  in
    230230  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    235235    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    236236    unserialized_params -> 'a1 **)
    237 let rec unserialized_params_rect_Type5 h_mk_unserialized_params x_16373 =
     237let rec unserialized_params_rect_Type5 h_mk_unserialized_params x_6361 =
    238238  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    239     x_16373
     239    x_6361
    240240  in
    241241  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    246246    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    247247    unserialized_params -> 'a1 **)
    248 let rec unserialized_params_rect_Type3 h_mk_unserialized_params x_16375 =
     248let rec unserialized_params_rect_Type3 h_mk_unserialized_params x_6363 =
    249249  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    250     x_16375
     250    x_6363
    251251  in
    252252  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    257257    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    258258    unserialized_params -> 'a1 **)
    259 let rec unserialized_params_rect_Type2 h_mk_unserialized_params x_16377 =
     259let rec unserialized_params_rect_Type2 h_mk_unserialized_params x_6365 =
    260260  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    261     x_16377
     261    x_6365
    262262  in
    263263  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    268268    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    269269    unserialized_params -> 'a1 **)
    270 let rec unserialized_params_rect_Type1 h_mk_unserialized_params x_16379 =
     270let rec unserialized_params_rect_Type1 h_mk_unserialized_params x_6367 =
    271271  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    272     x_16379
     272    x_6367
    273273  in
    274274  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    279279    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    280280    unserialized_params -> 'a1 **)
    281 let rec unserialized_params_rect_Type0 h_mk_unserialized_params x_16381 =
     281let rec unserialized_params_rect_Type0 h_mk_unserialized_params x_6369 =
    282282  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    283     x_16381
     283    x_6369
    284284  in
    285285  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    389389    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    390390let 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_16437 -> h_COMMENT x_16437
    392 | MOVE x_16438 -> h_MOVE x_16438
    393 | POP x_16439 -> h_POP x_16439
    394 | PUSH x_16440 -> h_PUSH x_16440
    395 | ADDRESS (i, x_16442, x_16441) -> h_ADDRESS i __ x_16442 x_16441
    396 | OPACCS (x_16448, x_16447, x_16446, x_16445, x_16444) ->
    397   h_OPACCS x_16448 x_16447 x_16446 x_16445 x_16444
    398 | OP1 (x_16451, x_16450, x_16449) -> h_OP1 x_16451 x_16450 x_16449
    399 | OP2 (x_16455, x_16454, x_16453, x_16452) ->
    400   h_OP2 x_16455 x_16454 x_16453 x_16452
     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
    401400| CLEAR_CARRY -> h_CLEAR_CARRY
    402401| SET_CARRY -> h_SET_CARRY
    403 | LOAD (x_16458, x_16457, x_16456) -> h_LOAD x_16458 x_16457 x_16456
    404 | STORE (x_16461, x_16460, x_16459) -> h_STORE x_16461 x_16460 x_16459
    405 | Extension_seq x_16462 -> h_extension_seq x_16462
     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
    406405
    407406(** val joint_seq_rect_Type5 :
     
    413412    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    414413let 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
    415 | COMMENT x_16477 -> h_COMMENT x_16477
    416 | MOVE x_16478 -> h_MOVE x_16478
    417 | POP x_16479 -> h_POP x_16479
    418 | PUSH x_16480 -> h_PUSH x_16480
    419 | ADDRESS (i, x_16482, x_16481) -> h_ADDRESS i __ x_16482 x_16481
    420 | OPACCS (x_16488, x_16487, x_16486, x_16485, x_16484) ->
    421   h_OPACCS x_16488 x_16487 x_16486 x_16485 x_16484
    422 | OP1 (x_16491, x_16490, x_16489) -> h_OP1 x_16491 x_16490 x_16489
    423 | OP2 (x_16495, x_16494, x_16493, x_16492) ->
    424   h_OP2 x_16495 x_16494 x_16493 x_16492
     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
    425423| CLEAR_CARRY -> h_CLEAR_CARRY
    426424| SET_CARRY -> h_SET_CARRY
    427 | LOAD (x_16498, x_16497, x_16496) -> h_LOAD x_16498 x_16497 x_16496
    428 | STORE (x_16501, x_16500, x_16499) -> h_STORE x_16501 x_16500 x_16499
    429 | Extension_seq x_16502 -> h_extension_seq x_16502
     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
    430428
    431429(** val joint_seq_rect_Type3 :
     
    437435    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    438436let 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
    439 | COMMENT x_16517 -> h_COMMENT x_16517
    440 | MOVE x_16518 -> h_MOVE x_16518
    441 | POP x_16519 -> h_POP x_16519
    442 | PUSH x_16520 -> h_PUSH x_16520
    443 | ADDRESS (i, x_16522, x_16521) -> h_ADDRESS i __ x_16522 x_16521
    444 | OPACCS (x_16528, x_16527, x_16526, x_16525, x_16524) ->
    445   h_OPACCS x_16528 x_16527 x_16526 x_16525 x_16524
    446 | OP1 (x_16531, x_16530, x_16529) -> h_OP1 x_16531 x_16530 x_16529
    447 | OP2 (x_16535, x_16534, x_16533, x_16532) ->
    448   h_OP2 x_16535 x_16534 x_16533 x_16532
     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
    449446| CLEAR_CARRY -> h_CLEAR_CARRY
    450447| SET_CARRY -> h_SET_CARRY
    451 | LOAD (x_16538, x_16537, x_16536) -> h_LOAD x_16538 x_16537 x_16536
    452 | STORE (x_16541, x_16540, x_16539) -> h_STORE x_16541 x_16540 x_16539
    453 | Extension_seq x_16542 -> h_extension_seq x_16542
     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
    454451
    455452(** val joint_seq_rect_Type2 :
     
    461458    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    462459let 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
    463 | COMMENT x_16557 -> h_COMMENT x_16557
    464 | MOVE x_16558 -> h_MOVE x_16558
    465 | POP x_16559 -> h_POP x_16559
    466 | PUSH x_16560 -> h_PUSH x_16560
    467 | ADDRESS (i, x_16562, x_16561) -> h_ADDRESS i __ x_16562 x_16561
    468 | OPACCS (x_16568, x_16567, x_16566, x_16565, x_16564) ->
    469   h_OPACCS x_16568 x_16567 x_16566 x_16565 x_16564
    470 | OP1 (x_16571, x_16570, x_16569) -> h_OP1 x_16571 x_16570 x_16569
    471 | OP2 (x_16575, x_16574, x_16573, x_16572) ->
    472   h_OP2 x_16575 x_16574 x_16573 x_16572
     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
    473469| CLEAR_CARRY -> h_CLEAR_CARRY
    474470| SET_CARRY -> h_SET_CARRY
    475 | LOAD (x_16578, x_16577, x_16576) -> h_LOAD x_16578 x_16577 x_16576
    476 | STORE (x_16581, x_16580, x_16579) -> h_STORE x_16581 x_16580 x_16579
    477 | Extension_seq x_16582 -> h_extension_seq x_16582
     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
    478474
    479475(** val joint_seq_rect_Type1 :
     
    485481    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    486482let 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
    487 | COMMENT x_16597 -> h_COMMENT x_16597
    488 | MOVE x_16598 -> h_MOVE x_16598
    489 | POP x_16599 -> h_POP x_16599
    490 | PUSH x_16600 -> h_PUSH x_16600
    491 | ADDRESS (i, x_16602, x_16601) -> h_ADDRESS i __ x_16602 x_16601
    492 | OPACCS (x_16608, x_16607, x_16606, x_16605, x_16604) ->
    493   h_OPACCS x_16608 x_16607 x_16606 x_16605 x_16604
    494 | OP1 (x_16611, x_16610, x_16609) -> h_OP1 x_16611 x_16610 x_16609
    495 | OP2 (x_16615, x_16614, x_16613, x_16612) ->
    496   h_OP2 x_16615 x_16614 x_16613 x_16612
     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
    497492| CLEAR_CARRY -> h_CLEAR_CARRY
    498493| SET_CARRY -> h_SET_CARRY
    499 | LOAD (x_16618, x_16617, x_16616) -> h_LOAD x_16618 x_16617 x_16616
    500 | STORE (x_16621, x_16620, x_16619) -> h_STORE x_16621 x_16620 x_16619
    501 | Extension_seq x_16622 -> h_extension_seq x_16622
     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
    502497
    503498(** val joint_seq_rect_Type0 :
     
    509504    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    510505let 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
    511 | COMMENT x_16637 -> h_COMMENT x_16637
    512 | MOVE x_16638 -> h_MOVE x_16638
    513 | POP x_16639 -> h_POP x_16639
    514 | PUSH x_16640 -> h_PUSH x_16640
    515 | ADDRESS (i, x_16642, x_16641) -> h_ADDRESS i __ x_16642 x_16641
    516 | OPACCS (x_16648, x_16647, x_16646, x_16645, x_16644) ->
    517   h_OPACCS x_16648 x_16647 x_16646 x_16645 x_16644
    518 | OP1 (x_16651, x_16650, x_16649) -> h_OP1 x_16651 x_16650 x_16649
    519 | OP2 (x_16655, x_16654, x_16653, x_16652) ->
    520   h_OP2 x_16655 x_16654 x_16653 x_16652
     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
    521515| CLEAR_CARRY -> h_CLEAR_CARRY
    522516| SET_CARRY -> h_SET_CARRY
    523 | LOAD (x_16658, x_16657, x_16656) -> h_LOAD x_16658 x_16657 x_16656
    524 | STORE (x_16661, x_16660, x_16659) -> h_STORE x_16661 x_16660 x_16659
    525 | Extension_seq x_16662 -> h_extension_seq x_16662
     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
    526520
    527521(** val joint_seq_inv_rect_Type4 :
     
    657651    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    658652let rec joint_step_rect_Type4 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    659 | COST_LABEL x_16929 -> h_COST_LABEL x_16929
    660 | CALL (x_16932, x_16931, x_16930) -> h_CALL x_16932 x_16931 x_16930
    661 | COND (x_16934, x_16933) -> h_COND x_16934 x_16933
    662 | Step_seq x_16935 -> h_step_seq x_16935
     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
    663657
    664658(** val joint_step_rect_Type5 :
     
    667661    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    668662let rec joint_step_rect_Type5 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    669 | COST_LABEL x_16941 -> h_COST_LABEL x_16941
    670 | CALL (x_16944, x_16943, x_16942) -> h_CALL x_16944 x_16943 x_16942
    671 | COND (x_16946, x_16945) -> h_COND x_16946 x_16945
    672 | Step_seq x_16947 -> h_step_seq x_16947
     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
    673667
    674668(** val joint_step_rect_Type3 :
     
    677671    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    678672let rec joint_step_rect_Type3 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    679 | COST_LABEL x_16953 -> h_COST_LABEL x_16953
    680 | CALL (x_16956, x_16955, x_16954) -> h_CALL x_16956 x_16955 x_16954
    681 | COND (x_16958, x_16957) -> h_COND x_16958 x_16957
    682 | Step_seq x_16959 -> h_step_seq x_16959
     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
    683677
    684678(** val joint_step_rect_Type2 :
     
    687681    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    688682let rec joint_step_rect_Type2 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    689 | COST_LABEL x_16965 -> h_COST_LABEL x_16965
    690 | CALL (x_16968, x_16967, x_16966) -> h_CALL x_16968 x_16967 x_16966
    691 | COND (x_16970, x_16969) -> h_COND x_16970 x_16969
    692 | Step_seq x_16971 -> h_step_seq x_16971
     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
    693687
    694688(** val joint_step_rect_Type1 :
     
    697691    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    698692let rec joint_step_rect_Type1 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    699 | COST_LABEL x_16977 -> h_COST_LABEL x_16977
    700 | CALL (x_16980, x_16979, x_16978) -> h_CALL x_16980 x_16979 x_16978
    701 | COND (x_16982, x_16981) -> h_COND x_16982 x_16981
    702 | Step_seq x_16983 -> h_step_seq x_16983
     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
    703697
    704698(** val joint_step_rect_Type0 :
     
    707701    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    708702let rec joint_step_rect_Type0 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    709 | COST_LABEL x_16989 -> h_COST_LABEL x_16989
    710 | CALL (x_16992, x_16991, x_16990) -> h_CALL x_16992 x_16991 x_16990
    711 | COND (x_16994, x_16993) -> h_COND x_16994 x_16993
    712 | Step_seq x_16995 -> h_step_seq x_16995
     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
    713707
    714708(** val joint_step_inv_rect_Type4 :
     
    804798    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
    805799    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
    806 let rec stmt_params_rect_Type4 h_mk_stmt_params x_17074 =
     800let rec stmt_params_rect_Type4 h_mk_stmt_params x_7062 =
    807801  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    808     has_fcond0 } = x_17074
     802    has_fcond0 } = x_7062
    809803  in
    810804  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    813807    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
    814808    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
    815 let rec stmt_params_rect_Type5 h_mk_stmt_params x_17076 =
     809let rec stmt_params_rect_Type5 h_mk_stmt_params x_7064 =
    816810  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    817     has_fcond0 } = x_17076
     811    has_fcond0 } = x_7064
    818812  in
    819813  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    822816    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
    823817    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
    824 let rec stmt_params_rect_Type3 h_mk_stmt_params x_17078 =
     818let rec stmt_params_rect_Type3 h_mk_stmt_params x_7066 =
    825819  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    826     has_fcond0 } = x_17078
     820    has_fcond0 } = x_7066
    827821  in
    828822  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    831825    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
    832826    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
    833 let rec stmt_params_rect_Type2 h_mk_stmt_params x_17080 =
     827let rec stmt_params_rect_Type2 h_mk_stmt_params x_7068 =
    834828  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    835     has_fcond0 } = x_17080
     829    has_fcond0 } = x_7068
    836830  in
    837831  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    840834    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
    841835    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
    842 let rec stmt_params_rect_Type1 h_mk_stmt_params x_17082 =
     836let rec stmt_params_rect_Type1 h_mk_stmt_params x_7070 =
    843837  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    844     has_fcond0 } = x_17082
     838    has_fcond0 } = x_7070
    845839  in
    846840  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    849843    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
    850844    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
    851 let rec stmt_params_rect_Type0 h_mk_stmt_params x_17084 =
     845let rec stmt_params_rect_Type0 h_mk_stmt_params x_7072 =
    852846  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    853     has_fcond0 } = x_17084
     847    has_fcond0 } = x_7072
    854848  in
    855849  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    914908    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    915909let rec joint_fin_step_rect_Type4 p h_GOTO h_RETURN h_TAILCALL = function
    916 | GOTO x_17108 -> h_GOTO x_17108
     910| GOTO x_7096 -> h_GOTO x_7096
    917911| RETURN -> h_RETURN
    918 | TAILCALL (x_17110, x_17109) -> h_TAILCALL __ x_17110 x_17109
     912| TAILCALL (x_7098, x_7097) -> h_TAILCALL __ x_7098 x_7097
    919913
    920914(** val joint_fin_step_rect_Type5 :
     
    922916    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    923917let rec joint_fin_step_rect_Type5 p h_GOTO h_RETURN h_TAILCALL = function
    924 | GOTO x_17116 -> h_GOTO x_17116
     918| GOTO x_7104 -> h_GOTO x_7104
    925919| RETURN -> h_RETURN
    926 | TAILCALL (x_17118, x_17117) -> h_TAILCALL __ x_17118 x_17117
     920| TAILCALL (x_7106, x_7105) -> h_TAILCALL __ x_7106 x_7105
    927921
    928922(** val joint_fin_step_rect_Type3 :
     
    930924    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    931925let rec joint_fin_step_rect_Type3 p h_GOTO h_RETURN h_TAILCALL = function
    932 | GOTO x_17124 -> h_GOTO x_17124
     926| GOTO x_7112 -> h_GOTO x_7112
    933927| RETURN -> h_RETURN
    934 | TAILCALL (x_17126, x_17125) -> h_TAILCALL __ x_17126 x_17125
     928| TAILCALL (x_7114, x_7113) -> h_TAILCALL __ x_7114 x_7113
    935929
    936930(** val joint_fin_step_rect_Type2 :
     
    938932    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    939933let rec joint_fin_step_rect_Type2 p h_GOTO h_RETURN h_TAILCALL = function
    940 | GOTO x_17132 -> h_GOTO x_17132
     934| GOTO x_7120 -> h_GOTO x_7120
    941935| RETURN -> h_RETURN
    942 | TAILCALL (x_17134, x_17133) -> h_TAILCALL __ x_17134 x_17133
     936| TAILCALL (x_7122, x_7121) -> h_TAILCALL __ x_7122 x_7121
    943937
    944938(** val joint_fin_step_rect_Type1 :
     
    946940    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    947941let rec joint_fin_step_rect_Type1 p h_GOTO h_RETURN h_TAILCALL = function
    948 | GOTO x_17140 -> h_GOTO x_17140
     942| GOTO x_7128 -> h_GOTO x_7128
    949943| RETURN -> h_RETURN
    950 | TAILCALL (x_17142, x_17141) -> h_TAILCALL __ x_17142 x_17141
     944| TAILCALL (x_7130, x_7129) -> h_TAILCALL __ x_7130 x_7129
    951945
    952946(** val joint_fin_step_rect_Type0 :
     
    954948    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    955949let rec joint_fin_step_rect_Type0 p h_GOTO h_RETURN h_TAILCALL = function
    956 | GOTO x_17148 -> h_GOTO x_17148
     950| GOTO x_7136 -> h_GOTO x_7136
    957951| RETURN -> h_RETURN
    958 | TAILCALL (x_17150, x_17149) -> h_TAILCALL __ x_17150 x_17149
     952| TAILCALL (x_7138, x_7137) -> h_TAILCALL __ x_7138 x_7137
    959953
    960954(** val joint_fin_step_inv_rect_Type4 :
     
    10281022    'a1) -> joint_statement -> 'a1 **)
    10291023let rec joint_statement_rect_Type4 p globals h_sequential h_final h_FCOND = function
    1030 | Sequential (x_17216, x_17215) -> h_sequential x_17216 x_17215
    1031 | Final x_17217 -> h_final x_17217
    1032 | FCOND (x_17220, x_17219, x_17218) -> h_FCOND __ x_17220 x_17219 x_17218
     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
    10331027
    10341028(** val joint_statement_rect_Type5 :
     
    10371031    'a1) -> joint_statement -> 'a1 **)
    10381032let rec joint_statement_rect_Type5 p globals h_sequential h_final h_FCOND = function
    1039 | Sequential (x_17227, x_17226) -> h_sequential x_17227 x_17226
    1040 | Final x_17228 -> h_final x_17228
    1041 | FCOND (x_17231, x_17230, x_17229) -> h_FCOND __ x_17231 x_17230 x_17229
     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
    10421036
    10431037(** val joint_statement_rect_Type3 :
     
    10461040    'a1) -> joint_statement -> 'a1 **)
    10471041let rec joint_statement_rect_Type3 p globals h_sequential h_final h_FCOND = function
    1048 | Sequential (x_17238, x_17237) -> h_sequential x_17238 x_17237
    1049 | Final x_17239 -> h_final x_17239
    1050 | FCOND (x_17242, x_17241, x_17240) -> h_FCOND __ x_17242 x_17241 x_17240
     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
    10511045
    10521046(** val joint_statement_rect_Type2 :
     
    10551049    'a1) -> joint_statement -> 'a1 **)
    10561050let rec joint_statement_rect_Type2 p globals h_sequential h_final h_FCOND = function
    1057 | Sequential (x_17249, x_17248) -> h_sequential x_17249 x_17248
    1058 | Final x_17250 -> h_final x_17250
    1059 | FCOND (x_17253, x_17252, x_17251) -> h_FCOND __ x_17253 x_17252 x_17251
     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
    10601054
    10611055(** val joint_statement_rect_Type1 :
     
    10641058    'a1) -> joint_statement -> 'a1 **)
    10651059let rec joint_statement_rect_Type1 p globals h_sequential h_final h_FCOND = function
    1066 | Sequential (x_17260, x_17259) -> h_sequential x_17260 x_17259
    1067 | Final x_17261 -> h_final x_17261
    1068 | FCOND (x_17264, x_17263, x_17262) -> h_FCOND __ x_17264 x_17263 x_17262
     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
    10691063
    10701064(** val joint_statement_rect_Type0 :
     
    10731067    'a1) -> joint_statement -> 'a1 **)
    10741068let rec joint_statement_rect_Type0 p globals h_sequential h_final h_FCOND = function
    1075 | Sequential (x_17271, x_17270) -> h_sequential x_17271 x_17270
    1076 | Final x_17272 -> h_final x_17272
    1077 | FCOND (x_17275, x_17274, x_17273) -> h_FCOND __ x_17275 x_17274 x_17273
     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
    10781072
    10791073(** val joint_statement_inv_rect_Type4 :
     
    11441138    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    11451139    'a1 **)
    1146 let rec params_rect_Type4 h_mk_params x_17348 =
     1140let rec params_rect_Type4 h_mk_params x_7336 =
    11471141  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1148     point_of_label0; point_of_succ = point_of_succ0 } = x_17348
     1142    point_of_label0; point_of_succ = point_of_succ0 } = x_7336
    11491143  in
    11501144  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    11551149    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    11561150    'a1 **)
    1157 let rec params_rect_Type5 h_mk_params x_17350 =
     1151let rec params_rect_Type5 h_mk_params x_7338 =
    11581152  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1159     point_of_label0; point_of_succ = point_of_succ0 } = x_17350
     1153    point_of_label0; point_of_succ = point_of_succ0 } = x_7338
    11601154  in
    11611155  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    11661160    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    11671161    'a1 **)
    1168 let rec params_rect_Type3 h_mk_params x_17352 =
     1162let rec params_rect_Type3 h_mk_params x_7340 =
    11691163  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1170     point_of_label0; point_of_succ = point_of_succ0 } = x_17352
     1164    point_of_label0; point_of_succ = point_of_succ0 } = x_7340
    11711165  in
    11721166  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    11771171    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    11781172    'a1 **)
    1179 let rec params_rect_Type2 h_mk_params x_17354 =
     1173let rec params_rect_Type2 h_mk_params x_7342 =
    11801174  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1181     point_of_label0; point_of_succ = point_of_succ0 } = x_17354
     1175    point_of_label0; point_of_succ = point_of_succ0 } = x_7342
    11821176  in
    11831177  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    11881182    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    11891183    'a1 **)
    1190 let rec params_rect_Type1 h_mk_params x_17356 =
     1184let rec params_rect_Type1 h_mk_params x_7344 =
    11911185  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1192     point_of_label0; point_of_succ = point_of_succ0 } = x_17356
     1186    point_of_label0; point_of_succ = point_of_succ0 } = x_7344
    11931187  in
    11941188  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    11991193    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    12001194    'a1 **)
    1201 let rec params_rect_Type0 h_mk_params x_17358 =
     1195let rec params_rect_Type0 h_mk_params x_7346 =
    12021196  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1203     point_of_label0; point_of_succ = point_of_succ0 } = x_17358
     1197    point_of_label0; point_of_succ = point_of_succ0 } = x_7346
    12041198  in
    12051199  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    13201314(** val lin_params_rect_Type4 :
    13211315    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
    1322 let rec lin_params_rect_Type4 h_mk_lin_params x_17381 =
    1323   let l_u_pars = x_17381 in h_mk_lin_params l_u_pars
     1316let 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
    13241318
    13251319(** val lin_params_rect_Type5 :
    13261320    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
    1327 let rec lin_params_rect_Type5 h_mk_lin_params x_17383 =
    1328   let l_u_pars = x_17383 in h_mk_lin_params l_u_pars
     1321let 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
    13291323
    13301324(** val lin_params_rect_Type3 :
    13311325    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
    1332 let rec lin_params_rect_Type3 h_mk_lin_params x_17385 =
    1333   let l_u_pars = x_17385 in h_mk_lin_params l_u_pars
     1326let 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
    13341328
    13351329(** val lin_params_rect_Type2 :
    13361330    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
    1337 let rec lin_params_rect_Type2 h_mk_lin_params x_17387 =
    1338   let l_u_pars = x_17387 in h_mk_lin_params l_u_pars
     1331let 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
    13391333
    13401334(** val lin_params_rect_Type1 :
    13411335    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
    1342 let rec lin_params_rect_Type1 h_mk_lin_params x_17389 =
    1343   let l_u_pars = x_17389 in h_mk_lin_params l_u_pars
     1336let 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
    13441338
    13451339(** val lin_params_rect_Type0 :
    13461340    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
    1347 let rec lin_params_rect_Type0 h_mk_lin_params x_17391 =
    1348   let l_u_pars = x_17391 in h_mk_lin_params l_u_pars
     1341let 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
    13491343
    13501344(** val l_u_pars : lin_params -> unserialized_params **)
     
    14071401(** val graph_params_rect_Type4 :
    14081402    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
    1409 let rec graph_params_rect_Type4 h_mk_graph_params x_17407 =
    1410   let g_u_pars = x_17407 in h_mk_graph_params g_u_pars
     1403let 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
    14111405
    14121406(** val graph_params_rect_Type5 :
    14131407    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
    1414 let rec graph_params_rect_Type5 h_mk_graph_params x_17409 =
    1415   let g_u_pars = x_17409 in h_mk_graph_params g_u_pars
     1408let 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
    14161410
    14171411(** val graph_params_rect_Type3 :
    14181412    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
    1419 let rec graph_params_rect_Type3 h_mk_graph_params x_17411 =
    1420   let g_u_pars = x_17411 in h_mk_graph_params g_u_pars
     1413let 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
    14211415
    14221416(** val graph_params_rect_Type2 :
    14231417    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
    1424 let rec graph_params_rect_Type2 h_mk_graph_params x_17413 =
    1425   let g_u_pars = x_17413 in h_mk_graph_params g_u_pars
     1418let 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
    14261420
    14271421(** val graph_params_rect_Type1 :
    14281422    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
    1429 let rec graph_params_rect_Type1 h_mk_graph_params x_17415 =
    1430   let g_u_pars = x_17415 in h_mk_graph_params g_u_pars
     1423let 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
    14311425
    14321426(** val graph_params_rect_Type0 :
    14331427    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
    1434 let rec graph_params_rect_Type0 h_mk_graph_params x_17417 =
    1435   let g_u_pars = x_17417 in h_mk_graph_params g_u_pars
     1428let 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
    14361430
    14371431(** val g_u_pars : graph_params -> unserialized_params **)
     
    14891483    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
    14901484    'a1) -> joint_internal_function -> 'a1 **)
    1491 let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_17433 =
     1485let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_7421 =
    14921486  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    14931487    joint_if_runiverse0; joint_if_result = joint_if_result0;
    14941488    joint_if_params = joint_if_params0; joint_if_stacksize =
    14951489    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
    1496     joint_if_entry0 } = x_17433
     1490    joint_if_entry0 } = x_7421
    14971491  in
    14981492  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    15041498    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
    15051499    'a1) -> joint_internal_function -> 'a1 **)
    1506 let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_17435 =
     1500let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_7423 =
    15071501  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    15081502    joint_if_runiverse0; joint_if_result = joint_if_result0;
    15091503    joint_if_params = joint_if_params0; joint_if_stacksize =
    15101504    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
    1511     joint_if_entry0 } = x_17435
     1505    joint_if_entry0 } = x_7423
    15121506  in
    15131507  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    15191513    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
    15201514    'a1) -> joint_internal_function -> 'a1 **)
    1521 let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_17437 =
     1515let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_7425 =
    15221516  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    15231517    joint_if_runiverse0; joint_if_result = joint_if_result0;
    15241518    joint_if_params = joint_if_params0; joint_if_stacksize =
    15251519    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
    1526     joint_if_entry0 } = x_17437
     1520    joint_if_entry0 } = x_7425
    15271521  in
    15281522  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    15341528    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
    15351529    'a1) -> joint_internal_function -> 'a1 **)
    1536 let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_17439 =
     1530let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_7427 =
    15371531  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    15381532    joint_if_runiverse0; joint_if_result = joint_if_result0;
    15391533    joint_if_params = joint_if_params0; joint_if_stacksize =
    15401534    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
    1541     joint_if_entry0 } = x_17439
     1535    joint_if_entry0 } = x_7427
    15421536  in
    15431537  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    15491543    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
    15501544    'a1) -> joint_internal_function -> 'a1 **)
    1551 let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_17441 =
     1545let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_7429 =
    15521546  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    15531547    joint_if_runiverse0; joint_if_result = joint_if_result0;
    15541548    joint_if_params = joint_if_params0; joint_if_stacksize =
    15551549    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
    1556     joint_if_entry0 } = x_17441
     1550    joint_if_entry0 } = x_7429
    15571551  in
    15581552  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    15641558    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
    15651559    'a1) -> joint_internal_function -> 'a1 **)
    1566 let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_17443 =
     1560let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_7431 =
    15671561  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    15681562    joint_if_runiverse0; joint_if_result = joint_if_result0;
    15691563    joint_if_params = joint_if_params0; joint_if_stacksize =
    15701564    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
    1571     joint_if_entry0 } = x_17443
     1565    joint_if_entry0 } = x_7431
    15721566  in
    15731567  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
Note: See TracChangeset for help on using the changeset viewer.