Changeset 2773 for extracted/joint.ml


Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/joint.ml

    r2743 r2773  
    1717open Extralib
    1818
     19open Lists
     20
     21open Identifiers
     22
     23open Integers
     24
     25open AST
     26
     27open Division
     28
     29open Exp
     30
     31open Arithmetic
     32
    1933open Setoids
    2034
     
    2337open Option
    2438
    25 open Lists
    26 
    27 open Identifiers
    28 
    29 open Integers
    30 
    31 open AST
    32 
    33 open Division
    34 
    35 open Exp
    36 
    37 open Arithmetic
    38 
    3939open Extranat
    4040
     
    8383open BackEndOps
    8484
     85open CostLabel
     86
     87open Order
     88
     89open Registers
     90
     91open I8051
     92
    8593open BitVectorTrie
    86 
    87 open CostLabel
    88 
    89 open Order
    90 
    91 open Registers
    92 
    93 open I8051
    9494
    9595open Graphs
     
    110110    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
    111111let rec argument_rect_Type4 h_Reg h_Imm = function
    112 | Reg x_19390 -> h_Reg x_19390
    113 | Imm x_19391 -> h_Imm x_19391
     112| Reg x_14700 -> h_Reg x_14700
     113| Imm x_14701 -> h_Imm x_14701
    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_19395 -> h_Reg x_19395
    119 | Imm x_19396 -> h_Imm x_19396
     118| Reg x_14705 -> h_Reg x_14705
     119| Imm x_14706 -> h_Imm x_14706
    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_19400 -> h_Reg x_19400
    125 | Imm x_19401 -> h_Imm x_19401
     124| Reg x_14710 -> h_Reg x_14710
     125| Imm x_14711 -> h_Imm x_14711
    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_19405 -> h_Reg x_19405
    131 | Imm x_19406 -> h_Imm x_19406
     130| Reg x_14715 -> h_Reg x_14715
     131| Imm x_14716 -> h_Imm x_14716
    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_19410 -> h_Reg x_19410
    137 | Imm x_19411 -> h_Imm x_19411
     136| Reg x_14720 -> h_Reg x_14720
     137| Imm x_14721 -> h_Imm x_14721
    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_19415 -> h_Reg x_19415
    143 | Imm x_19416 -> h_Imm x_19416
     142| Reg x_14725 -> h_Reg x_14725
     143| Imm x_14726 -> h_Imm x_14726
    144144
    145145(** val argument_inv_rect_Type4 :
     
    324324    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    325325    unserialized_params -> 'a1 **)
    326 let rec unserialized_params_rect_Type4 h_mk_unserialized_params x_19451 =
     326let rec unserialized_params_rect_Type4 h_mk_unserialized_params x_14761 =
    327327  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    328     x_19451
     328    x_14761
    329329  in
    330330  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    335335    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    336336    unserialized_params -> 'a1 **)
    337 let rec unserialized_params_rect_Type5 h_mk_unserialized_params x_19453 =
     337let rec unserialized_params_rect_Type5 h_mk_unserialized_params x_14763 =
    338338  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    339     x_19453
     339    x_14763
    340340  in
    341341  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    346346    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    347347    unserialized_params -> 'a1 **)
    348 let rec unserialized_params_rect_Type3 h_mk_unserialized_params x_19455 =
     348let rec unserialized_params_rect_Type3 h_mk_unserialized_params x_14765 =
    349349  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    350     x_19455
     350    x_14765
    351351  in
    352352  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    357357    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    358358    unserialized_params -> 'a1 **)
    359 let rec unserialized_params_rect_Type2 h_mk_unserialized_params x_19457 =
     359let rec unserialized_params_rect_Type2 h_mk_unserialized_params x_14767 =
    360360  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    361     x_19457
     361    x_14767
    362362  in
    363363  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    368368    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    369369    unserialized_params -> 'a1 **)
    370 let rec unserialized_params_rect_Type1 h_mk_unserialized_params x_19459 =
     370let rec unserialized_params_rect_Type1 h_mk_unserialized_params x_14769 =
    371371  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    372     x_19459
     372    x_14769
    373373  in
    374374  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    379379    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    380380    unserialized_params -> 'a1 **)
    381 let rec unserialized_params_rect_Type0 h_mk_unserialized_params x_19461 =
     381let rec unserialized_params_rect_Type0 h_mk_unserialized_params x_14771 =
    382382  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    383     x_19461
     383    x_14771
    384384  in
    385385  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    489489    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    490490let 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
    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
     491| COMMENT x_14827 -> h_COMMENT x_14827
     492| MOVE x_14828 -> h_MOVE x_14828
     493| POP x_14829 -> h_POP x_14829
     494| PUSH x_14830 -> h_PUSH x_14830
     495| ADDRESS (i, x_14832, x_14831) -> h_ADDRESS i __ x_14832 x_14831
     496| OPACCS (x_14838, x_14837, x_14836, x_14835, x_14834) ->
     497  h_OPACCS x_14838 x_14837 x_14836 x_14835 x_14834
     498| OP1 (x_14841, x_14840, x_14839) -> h_OP1 x_14841 x_14840 x_14839
     499| OP2 (x_14845, x_14844, x_14843, x_14842) ->
     500  h_OP2 x_14845 x_14844 x_14843 x_14842
    501501| CLEAR_CARRY -> h_CLEAR_CARRY
    502502| SET_CARRY -> h_SET_CARRY
    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
     503| LOAD (x_14848, x_14847, x_14846) -> h_LOAD x_14848 x_14847 x_14846
     504| STORE (x_14851, x_14850, x_14849) -> h_STORE x_14851 x_14850 x_14849
     505| Extension_seq x_14852 -> h_extension_seq x_14852
    506506
    507507(** val joint_seq_rect_Type5 :
     
    513513    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    514514let 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
    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
     515| COMMENT x_14867 -> h_COMMENT x_14867
     516| MOVE x_14868 -> h_MOVE x_14868
     517| POP x_14869 -> h_POP x_14869
     518| PUSH x_14870 -> h_PUSH x_14870
     519| ADDRESS (i, x_14872, x_14871) -> h_ADDRESS i __ x_14872 x_14871
     520| OPACCS (x_14878, x_14877, x_14876, x_14875, x_14874) ->
     521  h_OPACCS x_14878 x_14877 x_14876 x_14875 x_14874
     522| OP1 (x_14881, x_14880, x_14879) -> h_OP1 x_14881 x_14880 x_14879
     523| OP2 (x_14885, x_14884, x_14883, x_14882) ->
     524  h_OP2 x_14885 x_14884 x_14883 x_14882
    525525| CLEAR_CARRY -> h_CLEAR_CARRY
    526526| SET_CARRY -> h_SET_CARRY
    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
     527| LOAD (x_14888, x_14887, x_14886) -> h_LOAD x_14888 x_14887 x_14886
     528| STORE (x_14891, x_14890, x_14889) -> h_STORE x_14891 x_14890 x_14889
     529| Extension_seq x_14892 -> h_extension_seq x_14892
    530530
    531531(** val joint_seq_rect_Type3 :
     
    537537    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    538538let 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
    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
     539| COMMENT x_14907 -> h_COMMENT x_14907
     540| MOVE x_14908 -> h_MOVE x_14908
     541| POP x_14909 -> h_POP x_14909
     542| PUSH x_14910 -> h_PUSH x_14910
     543| ADDRESS (i, x_14912, x_14911) -> h_ADDRESS i __ x_14912 x_14911
     544| OPACCS (x_14918, x_14917, x_14916, x_14915, x_14914) ->
     545  h_OPACCS x_14918 x_14917 x_14916 x_14915 x_14914
     546| OP1 (x_14921, x_14920, x_14919) -> h_OP1 x_14921 x_14920 x_14919
     547| OP2 (x_14925, x_14924, x_14923, x_14922) ->
     548  h_OP2 x_14925 x_14924 x_14923 x_14922
    549549| CLEAR_CARRY -> h_CLEAR_CARRY
    550550| SET_CARRY -> h_SET_CARRY
    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
     551| LOAD (x_14928, x_14927, x_14926) -> h_LOAD x_14928 x_14927 x_14926
     552| STORE (x_14931, x_14930, x_14929) -> h_STORE x_14931 x_14930 x_14929
     553| Extension_seq x_14932 -> h_extension_seq x_14932
    554554
    555555(** val joint_seq_rect_Type2 :
     
    561561    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    562562let 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
    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
     563| COMMENT x_14947 -> h_COMMENT x_14947
     564| MOVE x_14948 -> h_MOVE x_14948
     565| POP x_14949 -> h_POP x_14949
     566| PUSH x_14950 -> h_PUSH x_14950
     567| ADDRESS (i, x_14952, x_14951) -> h_ADDRESS i __ x_14952 x_14951
     568| OPACCS (x_14958, x_14957, x_14956, x_14955, x_14954) ->
     569  h_OPACCS x_14958 x_14957 x_14956 x_14955 x_14954
     570| OP1 (x_14961, x_14960, x_14959) -> h_OP1 x_14961 x_14960 x_14959
     571| OP2 (x_14965, x_14964, x_14963, x_14962) ->
     572  h_OP2 x_14965 x_14964 x_14963 x_14962
    573573| CLEAR_CARRY -> h_CLEAR_CARRY
    574574| SET_CARRY -> h_SET_CARRY
    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
     575| LOAD (x_14968, x_14967, x_14966) -> h_LOAD x_14968 x_14967 x_14966
     576| STORE (x_14971, x_14970, x_14969) -> h_STORE x_14971 x_14970 x_14969
     577| Extension_seq x_14972 -> h_extension_seq x_14972
    578578
    579579(** val joint_seq_rect_Type1 :
     
    585585    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    586586let 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
    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
     587| COMMENT x_14987 -> h_COMMENT x_14987
     588| MOVE x_14988 -> h_MOVE x_14988
     589| POP x_14989 -> h_POP x_14989
     590| PUSH x_14990 -> h_PUSH x_14990
     591| ADDRESS (i, x_14992, x_14991) -> h_ADDRESS i __ x_14992 x_14991
     592| OPACCS (x_14998, x_14997, x_14996, x_14995, x_14994) ->
     593  h_OPACCS x_14998 x_14997 x_14996 x_14995 x_14994
     594| OP1 (x_15001, x_15000, x_14999) -> h_OP1 x_15001 x_15000 x_14999
     595| OP2 (x_15005, x_15004, x_15003, x_15002) ->
     596  h_OP2 x_15005 x_15004 x_15003 x_15002
    597597| CLEAR_CARRY -> h_CLEAR_CARRY
    598598| SET_CARRY -> h_SET_CARRY
    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
     599| LOAD (x_15008, x_15007, x_15006) -> h_LOAD x_15008 x_15007 x_15006
     600| STORE (x_15011, x_15010, x_15009) -> h_STORE x_15011 x_15010 x_15009
     601| Extension_seq x_15012 -> h_extension_seq x_15012
    602602
    603603(** val joint_seq_rect_Type0 :
     
    609609    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    610610let 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
    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
     611| COMMENT x_15027 -> h_COMMENT x_15027
     612| MOVE x_15028 -> h_MOVE x_15028
     613| POP x_15029 -> h_POP x_15029
     614| PUSH x_15030 -> h_PUSH x_15030
     615| ADDRESS (i, x_15032, x_15031) -> h_ADDRESS i __ x_15032 x_15031
     616| OPACCS (x_15038, x_15037, x_15036, x_15035, x_15034) ->
     617  h_OPACCS x_15038 x_15037 x_15036 x_15035 x_15034
     618| OP1 (x_15041, x_15040, x_15039) -> h_OP1 x_15041 x_15040 x_15039
     619| OP2 (x_15045, x_15044, x_15043, x_15042) ->
     620  h_OP2 x_15045 x_15044 x_15043 x_15042
    621621| CLEAR_CARRY -> h_CLEAR_CARRY
    622622| SET_CARRY -> h_SET_CARRY
    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
     623| LOAD (x_15048, x_15047, x_15046) -> h_LOAD x_15048 x_15047 x_15046
     624| STORE (x_15051, x_15050, x_15049) -> h_STORE x_15051 x_15050 x_15049
     625| Extension_seq x_15052 -> h_extension_seq x_15052
    626626
    627627(** val joint_seq_inv_rect_Type4 :
     
    785785    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    786786let rec joint_step_rect_Type4 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    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
     787| COST_LABEL x_15319 -> h_COST_LABEL x_15319
     788| CALL (x_15322, x_15321, x_15320) -> h_CALL x_15322 x_15321 x_15320
     789| COND (x_15324, x_15323) -> h_COND x_15324 x_15323
     790| Step_seq x_15325 -> h_step_seq x_15325
    791791
    792792(** val joint_step_rect_Type5 :
     
    795795    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    796796let rec joint_step_rect_Type5 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    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
     797| COST_LABEL x_15331 -> h_COST_LABEL x_15331
     798| CALL (x_15334, x_15333, x_15332) -> h_CALL x_15334 x_15333 x_15332
     799| COND (x_15336, x_15335) -> h_COND x_15336 x_15335
     800| Step_seq x_15337 -> h_step_seq x_15337
    801801
    802802(** val joint_step_rect_Type3 :
     
    805805    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    806806let rec joint_step_rect_Type3 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    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
     807| COST_LABEL x_15343 -> h_COST_LABEL x_15343
     808| CALL (x_15346, x_15345, x_15344) -> h_CALL x_15346 x_15345 x_15344
     809| COND (x_15348, x_15347) -> h_COND x_15348 x_15347
     810| Step_seq x_15349 -> h_step_seq x_15349
    811811
    812812(** val joint_step_rect_Type2 :
     
    815815    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    816816let rec joint_step_rect_Type2 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    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
     817| COST_LABEL x_15355 -> h_COST_LABEL x_15355
     818| CALL (x_15358, x_15357, x_15356) -> h_CALL x_15358 x_15357 x_15356
     819| COND (x_15360, x_15359) -> h_COND x_15360 x_15359
     820| Step_seq x_15361 -> h_step_seq x_15361
    821821
    822822(** val joint_step_rect_Type1 :
     
    825825    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    826826let rec joint_step_rect_Type1 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    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
     827| COST_LABEL x_15367 -> h_COST_LABEL x_15367
     828| CALL (x_15370, x_15369, x_15368) -> h_CALL x_15370 x_15369 x_15368
     829| COND (x_15372, x_15371) -> h_COND x_15372 x_15371
     830| Step_seq x_15373 -> h_step_seq x_15373
    831831
    832832(** val joint_step_rect_Type0 :
     
    835835    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    836836let rec joint_step_rect_Type0 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    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
     837| COST_LABEL x_15379 -> h_COST_LABEL x_15379
     838| CALL (x_15382, x_15381, x_15380) -> h_CALL x_15382 x_15381 x_15380
     839| COND (x_15384, x_15383) -> h_COND x_15384 x_15383
     840| Step_seq x_15385 -> h_step_seq x_15385
    841841
    842842(** val joint_step_inv_rect_Type4 :
     
    995995    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
    996996    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
    997 let rec stmt_params_rect_Type4 h_mk_stmt_params x_20154 =
     997let rec stmt_params_rect_Type4 h_mk_stmt_params x_15464 =
    998998  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    999     has_fcond0 } = x_20154
     999    has_fcond0 } = x_15464
    10001000  in
    10011001  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    10041004    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
    10051005    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
    1006 let rec stmt_params_rect_Type5 h_mk_stmt_params x_20156 =
     1006let rec stmt_params_rect_Type5 h_mk_stmt_params x_15466 =
    10071007  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1008     has_fcond0 } = x_20156
     1008    has_fcond0 } = x_15466
    10091009  in
    10101010  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    10131013    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
    10141014    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
    1015 let rec stmt_params_rect_Type3 h_mk_stmt_params x_20158 =
     1015let rec stmt_params_rect_Type3 h_mk_stmt_params x_15468 =
    10161016  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1017     has_fcond0 } = x_20158
     1017    has_fcond0 } = x_15468
    10181018  in
    10191019  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    10221022    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
    10231023    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
    1024 let rec stmt_params_rect_Type2 h_mk_stmt_params x_20160 =
     1024let rec stmt_params_rect_Type2 h_mk_stmt_params x_15470 =
    10251025  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1026     has_fcond0 } = x_20160
     1026    has_fcond0 } = x_15470
    10271027  in
    10281028  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    10311031    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
    10321032    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
    1033 let rec stmt_params_rect_Type1 h_mk_stmt_params x_20162 =
     1033let rec stmt_params_rect_Type1 h_mk_stmt_params x_15472 =
    10341034  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1035     has_fcond0 } = x_20162
     1035    has_fcond0 } = x_15472
    10361036  in
    10371037  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    10401040    (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
    10411041    Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
    1042 let rec stmt_params_rect_Type0 h_mk_stmt_params x_20164 =
     1042let rec stmt_params_rect_Type0 h_mk_stmt_params x_15474 =
    10431043  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1044     has_fcond0 } = x_20164
     1044    has_fcond0 } = x_15474
    10451045  in
    10461046  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    10501050  xxx.uns_pars
    10511051
    1052 type succ0 = __
     1052type succ = __
    10531053
    10541054(** val succ_label : stmt_params -> __ -> Graphs.label Types.option **)
     
    11051105    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    11061106let rec joint_fin_step_rect_Type4 p h_GOTO h_RETURN h_TAILCALL = function
    1107 | GOTO x_20188 -> h_GOTO x_20188
     1107| GOTO x_15498 -> h_GOTO x_15498
    11081108| RETURN -> h_RETURN
    1109 | TAILCALL (x_20190, x_20189) -> h_TAILCALL __ x_20190 x_20189
     1109| TAILCALL (x_15500, x_15499) -> h_TAILCALL __ x_15500 x_15499
    11101110
    11111111(** val joint_fin_step_rect_Type5 :
     
    11131113    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    11141114let rec joint_fin_step_rect_Type5 p h_GOTO h_RETURN h_TAILCALL = function
    1115 | GOTO x_20196 -> h_GOTO x_20196
     1115| GOTO x_15506 -> h_GOTO x_15506
    11161116| RETURN -> h_RETURN
    1117 | TAILCALL (x_20198, x_20197) -> h_TAILCALL __ x_20198 x_20197
     1117| TAILCALL (x_15508, x_15507) -> h_TAILCALL __ x_15508 x_15507
    11181118
    11191119(** val joint_fin_step_rect_Type3 :
     
    11211121    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    11221122let rec joint_fin_step_rect_Type3 p h_GOTO h_RETURN h_TAILCALL = function
    1123 | GOTO x_20204 -> h_GOTO x_20204
     1123| GOTO x_15514 -> h_GOTO x_15514
    11241124| RETURN -> h_RETURN
    1125 | TAILCALL (x_20206, x_20205) -> h_TAILCALL __ x_20206 x_20205
     1125| TAILCALL (x_15516, x_15515) -> h_TAILCALL __ x_15516 x_15515
    11261126
    11271127(** val joint_fin_step_rect_Type2 :
     
    11291129    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    11301130let rec joint_fin_step_rect_Type2 p h_GOTO h_RETURN h_TAILCALL = function
    1131 | GOTO x_20212 -> h_GOTO x_20212
     1131| GOTO x_15522 -> h_GOTO x_15522
    11321132| RETURN -> h_RETURN
    1133 | TAILCALL (x_20214, x_20213) -> h_TAILCALL __ x_20214 x_20213
     1133| TAILCALL (x_15524, x_15523) -> h_TAILCALL __ x_15524 x_15523
    11341134
    11351135(** val joint_fin_step_rect_Type1 :
     
    11371137    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    11381138let rec joint_fin_step_rect_Type1 p h_GOTO h_RETURN h_TAILCALL = function
    1139 | GOTO x_20220 -> h_GOTO x_20220
     1139| GOTO x_15530 -> h_GOTO x_15530
    11401140| RETURN -> h_RETURN
    1141 | TAILCALL (x_20222, x_20221) -> h_TAILCALL __ x_20222 x_20221
     1141| TAILCALL (x_15532, x_15531) -> h_TAILCALL __ x_15532 x_15531
    11421142
    11431143(** val joint_fin_step_rect_Type0 :
     
    11451145    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    11461146let rec joint_fin_step_rect_Type0 p h_GOTO h_RETURN h_TAILCALL = function
    1147 | GOTO x_20228 -> h_GOTO x_20228
     1147| GOTO x_15538 -> h_GOTO x_15538
    11481148| RETURN -> h_RETURN
    1149 | TAILCALL (x_20230, x_20229) -> h_TAILCALL __ x_20230 x_20229
     1149| TAILCALL (x_15540, x_15539) -> h_TAILCALL __ x_15540 x_15539
    11501150
    11511151(** val joint_fin_step_inv_rect_Type4 :
     
    12191219    'a1) -> joint_statement -> 'a1 **)
    12201220let rec joint_statement_rect_Type4 p globals h_sequential h_final h_FCOND = function
    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
     1221| Sequential (x_15606, x_15605) -> h_sequential x_15606 x_15605
     1222| Final x_15607 -> h_final x_15607
     1223| FCOND (x_15610, x_15609, x_15608) -> h_FCOND __ x_15610 x_15609 x_15608
    12241224
    12251225(** val joint_statement_rect_Type5 :
     
    12281228    'a1) -> joint_statement -> 'a1 **)
    12291229let rec joint_statement_rect_Type5 p globals h_sequential h_final h_FCOND = function
    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
     1230| Sequential (x_15617, x_15616) -> h_sequential x_15617 x_15616
     1231| Final x_15618 -> h_final x_15618
     1232| FCOND (x_15621, x_15620, x_15619) -> h_FCOND __ x_15621 x_15620 x_15619
    12331233
    12341234(** val joint_statement_rect_Type3 :
     
    12371237    'a1) -> joint_statement -> 'a1 **)
    12381238let rec joint_statement_rect_Type3 p globals h_sequential h_final h_FCOND = function
    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
     1239| Sequential (x_15628, x_15627) -> h_sequential x_15628 x_15627
     1240| Final x_15629 -> h_final x_15629
     1241| FCOND (x_15632, x_15631, x_15630) -> h_FCOND __ x_15632 x_15631 x_15630
    12421242
    12431243(** val joint_statement_rect_Type2 :
     
    12461246    'a1) -> joint_statement -> 'a1 **)
    12471247let rec joint_statement_rect_Type2 p globals h_sequential h_final h_FCOND = function
    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
     1248| Sequential (x_15639, x_15638) -> h_sequential x_15639 x_15638
     1249| Final x_15640 -> h_final x_15640
     1250| FCOND (x_15643, x_15642, x_15641) -> h_FCOND __ x_15643 x_15642 x_15641
    12511251
    12521252(** val joint_statement_rect_Type1 :
     
    12551255    'a1) -> joint_statement -> 'a1 **)
    12561256let rec joint_statement_rect_Type1 p globals h_sequential h_final h_FCOND = function
    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
     1257| Sequential (x_15650, x_15649) -> h_sequential x_15650 x_15649
     1258| Final x_15651 -> h_final x_15651
     1259| FCOND (x_15654, x_15653, x_15652) -> h_FCOND __ x_15654 x_15653 x_15652
    12601260
    12611261(** val joint_statement_rect_Type0 :
     
    12641264    'a1) -> joint_statement -> 'a1 **)
    12651265let rec joint_statement_rect_Type0 p globals h_sequential h_final h_FCOND = function
    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
     1266| Sequential (x_15661, x_15660) -> h_sequential x_15661 x_15660
     1267| Final x_15662 -> h_final x_15662
     1268| FCOND (x_15665, x_15664, x_15663) -> h_FCOND __ x_15665 x_15664 x_15663
    12691269
    12701270(** val joint_statement_inv_rect_Type4 :
     
    13651365    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    13661366    'a1 **)
    1367 let rec params_rect_Type4 h_mk_params x_20428 =
     1367let rec params_rect_Type4 h_mk_params x_15738 =
    13681368  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1369     point_of_label0; point_of_succ = point_of_succ0 } = x_20428
     1369    point_of_label0; point_of_succ = point_of_succ0 } = x_15738
    13701370  in
    13711371  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    13761376    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    13771377    'a1 **)
    1378 let rec params_rect_Type5 h_mk_params x_20430 =
     1378let rec params_rect_Type5 h_mk_params x_15740 =
    13791379  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1380     point_of_label0; point_of_succ = point_of_succ0 } = x_20430
     1380    point_of_label0; point_of_succ = point_of_succ0 } = x_15740
    13811381  in
    13821382  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    13871387    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    13881388    'a1 **)
    1389 let rec params_rect_Type3 h_mk_params x_20432 =
     1389let rec params_rect_Type3 h_mk_params x_15742 =
    13901390  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1391     point_of_label0; point_of_succ = point_of_succ0 } = x_20432
     1391    point_of_label0; point_of_succ = point_of_succ0 } = x_15742
    13921392  in
    13931393  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    13981398    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    13991399    'a1 **)
    1400 let rec params_rect_Type2 h_mk_params x_20434 =
     1400let rec params_rect_Type2 h_mk_params x_15744 =
    14011401  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1402     point_of_label0; point_of_succ = point_of_succ0 } = x_20434
     1402    point_of_label0; point_of_succ = point_of_succ0 } = x_15744
    14031403  in
    14041404  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    14091409    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    14101410    'a1 **)
    1411 let rec params_rect_Type1 h_mk_params x_20436 =
     1411let rec params_rect_Type1 h_mk_params x_15746 =
    14121412  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1413     point_of_label0; point_of_succ = point_of_succ0 } = x_20436
     1413    point_of_label0; point_of_succ = point_of_succ0 } = x_15746
    14141414  in
    14151415  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    14201420    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    14211421    'a1 **)
    1422 let rec params_rect_Type0 h_mk_params x_20438 =
     1422let rec params_rect_Type0 h_mk_params x_15748 =
    14231423  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1424     point_of_label0; point_of_succ = point_of_succ0 } = x_20438
     1424    point_of_label0; point_of_succ = point_of_succ0 } = x_15748
    14251425  in
    14261426  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    15281528    stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
    15291529    List.list **)
    1530 let stmt_labels p g0 stmt =
     1530let stmt_labels p g stmt =
    15311531  List.append
    1532     (match stmt_implicit_label p g0 stmt with
     1532    (match stmt_implicit_label p g stmt with
    15331533     | Types.None -> List.Nil
    15341534     | Types.Some l -> List.Cons (l, List.Nil))
    1535     (stmt_explicit_labels p g0 stmt)
     1535    (stmt_explicit_labels p g stmt)
    15361536
    15371537type lin_params =
     
    15411541(** val lin_params_rect_Type4 :
    15421542    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
    1543 let 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
     1543let rec lin_params_rect_Type4 h_mk_lin_params x_15771 =
     1544  let l_u_pars = x_15771 in h_mk_lin_params l_u_pars
    15451545
    15461546(** val lin_params_rect_Type5 :
    15471547    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
    1548 let 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
     1548let rec lin_params_rect_Type5 h_mk_lin_params x_15773 =
     1549  let l_u_pars = x_15773 in h_mk_lin_params l_u_pars
    15501550
    15511551(** val lin_params_rect_Type3 :
    15521552    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
    1553 let 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
     1553let rec lin_params_rect_Type3 h_mk_lin_params x_15775 =
     1554  let l_u_pars = x_15775 in h_mk_lin_params l_u_pars
    15551555
    15561556(** val lin_params_rect_Type2 :
    15571557    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
    1558 let 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
     1558let rec lin_params_rect_Type2 h_mk_lin_params x_15777 =
     1559  let l_u_pars = x_15777 in h_mk_lin_params l_u_pars
    15601560
    15611561(** val lin_params_rect_Type1 :
    15621562    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
    1563 let 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
     1563let rec lin_params_rect_Type1 h_mk_lin_params x_15779 =
     1564  let l_u_pars = x_15779 in h_mk_lin_params l_u_pars
    15651565
    15661566(** val lin_params_rect_Type0 :
    15671567    (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
    1568 let 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
     1568let rec lin_params_rect_Type0 h_mk_lin_params x_15781 =
     1569  let l_u_pars = x_15781 in h_mk_lin_params l_u_pars
    15701570
    15711571(** val l_u_pars : lin_params -> unserialized_params **)
     
    16081608    (fun globals code point ->
    16091609    Obj.magic
    1610       (Monad.m_bind0 (Monad.max_def Option.option0)
     1610      (Monad.m_bind0 (Monad.max_def Option.option)
    16111611        (Obj.magic (List.nth_opt (Obj.magic point) (Obj.magic code)))
    16121612        (fun ls ->
    1613         Monad.m_return0 (Monad.max_def Option.option0) ls.Types.snd)));
     1613        Monad.m_return0 (Monad.max_def Option.option) ls.Types.snd)));
    16141614    point_of_label = (fun globals c lbl ->
    16151615    Util.if_then_else_safe
     
    16171617        (Obj.magic c)) (fun _ ->
    16181618      Obj.magic
    1619         (Monad.m_return0 (Monad.max_def Option.option0)
     1619        (Monad.m_return0 (Monad.max_def Option.option)
    16201620          (LabelledObjects.index_of_label PreIdentifiers.LabelTag lbl
    16211621            (Obj.magic c)))) (fun _ -> Types.None)); point_of_succ =
     
    16371637(** val graph_params_rect_Type4 :
    16381638    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
    1639 let 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
     1639let rec graph_params_rect_Type4 h_mk_graph_params x_15797 =
     1640  let g_u_pars = x_15797 in h_mk_graph_params g_u_pars
    16411641
    16421642(** val graph_params_rect_Type5 :
    16431643    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
    1644 let 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
     1644let rec graph_params_rect_Type5 h_mk_graph_params x_15799 =
     1645  let g_u_pars = x_15799 in h_mk_graph_params g_u_pars
    16461646
    16471647(** val graph_params_rect_Type3 :
    16481648    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
    1649 let 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
     1649let rec graph_params_rect_Type3 h_mk_graph_params x_15801 =
     1650  let g_u_pars = x_15801 in h_mk_graph_params g_u_pars
    16511651
    16521652(** val graph_params_rect_Type2 :
    16531653    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
    1654 let 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
     1654let rec graph_params_rect_Type2 h_mk_graph_params x_15803 =
     1655  let g_u_pars = x_15803 in h_mk_graph_params g_u_pars
    16561656
    16571657(** val graph_params_rect_Type1 :
    16581658    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
    1659 let 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
     1659let rec graph_params_rect_Type1 h_mk_graph_params x_15805 =
     1660  let g_u_pars = x_15805 in h_mk_graph_params g_u_pars
    16611661
    16621662(** val graph_params_rect_Type0 :
    16631663    (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
    1664 let 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
     1664let rec graph_params_rect_Type0 h_mk_graph_params x_15807 =
     1665  let g_u_pars = x_15807 in h_mk_graph_params g_u_pars
    16661666
    16671667(** val g_u_pars : graph_params -> unserialized_params **)
     
    17031703    (Obj.magic (fun x -> Types.Some x)); has_fcond = Bool.False }; stmt_at =
    17041704    (fun globals code ->
    1705     Obj.magic (Identifiers.lookup0 PreIdentifiers.LabelTag (Obj.magic code)));
     1705    Obj.magic (Identifiers.lookup PreIdentifiers.LabelTag (Obj.magic code)));
    17061706    point_of_label = (fun x x0 lbl ->
    1707     Obj.magic (Monad.m_return0 (Monad.max_def Option.option0) lbl));
     1707    Obj.magic (Monad.m_return0 (Monad.max_def Option.option) lbl));
    17081708    point_of_succ = (fun x lbl -> lbl) }
    17091709
     
    17281728    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
    17291729    'a1) -> joint_internal_function -> 'a1 **)
    1730 let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_20513 =
     1730let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_15823 =
    17311731  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    17321732    joint_if_runiverse0; joint_if_result = joint_if_result0;
    17331733    joint_if_params = joint_if_params0; joint_if_stacksize =
    17341734    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
    1735     joint_if_entry0 } = x_20513
     1735    joint_if_entry0 } = x_15823
    17361736  in
    17371737  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    17431743    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
    17441744    'a1) -> joint_internal_function -> 'a1 **)
    1745 let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_20515 =
     1745let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_15825 =
    17461746  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    17471747    joint_if_runiverse0; joint_if_result = joint_if_result0;
    17481748    joint_if_params = joint_if_params0; joint_if_stacksize =
    17491749    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
    1750     joint_if_entry0 } = x_20515
     1750    joint_if_entry0 } = x_15825
    17511751  in
    17521752  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    17581758    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
    17591759    'a1) -> joint_internal_function -> 'a1 **)
    1760 let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_20517 =
     1760let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_15827 =
    17611761  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    17621762    joint_if_runiverse0; joint_if_result = joint_if_result0;
    17631763    joint_if_params = joint_if_params0; joint_if_stacksize =
    17641764    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
    1765     joint_if_entry0 } = x_20517
     1765    joint_if_entry0 } = x_15827
    17661766  in
    17671767  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    17731773    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
    17741774    'a1) -> joint_internal_function -> 'a1 **)
    1775 let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_20519 =
     1775let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_15829 =
    17761776  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    17771777    joint_if_runiverse0; joint_if_result = joint_if_result0;
    17781778    joint_if_params = joint_if_params0; joint_if_stacksize =
    17791779    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
    1780     joint_if_entry0 } = x_20519
     1780    joint_if_entry0 } = x_15829
    17811781  in
    17821782  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    17881788    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
    17891789    'a1) -> joint_internal_function -> 'a1 **)
    1790 let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_20521 =
     1790let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_15831 =
    17911791  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    17921792    joint_if_runiverse0; joint_if_result = joint_if_result0;
    17931793    joint_if_params = joint_if_params0; joint_if_stacksize =
    17941794    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
    1795     joint_if_entry0 } = x_20521
     1795    joint_if_entry0 } = x_15831
    17961796  in
    17971797  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    18031803    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
    18041804    'a1) -> joint_internal_function -> 'a1 **)
    1805 let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_20523 =
     1805let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_15833 =
    18061806  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    18071807    joint_if_runiverse0; joint_if_result = joint_if_result0;
    18081808    joint_if_params = joint_if_params0; joint_if_stacksize =
    18091809    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
    1810     joint_if_entry0 } = x_20523
     1810    joint_if_entry0 } = x_15833
    18111811  in
    18121812  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    19781978    AST.ident List.list -> params -> joint_internal_function -> __ -> __
    19791979    Types.sig0 -> joint_internal_function **)
    1980 let set_joint_code globals pars int_fun graph0 entry =
     1980let set_joint_code globals pars int_fun graph entry =
    19811981  { joint_if_luniverse = int_fun.joint_if_luniverse; joint_if_runiverse =
    19821982    int_fun.joint_if_runiverse; joint_if_result = int_fun.joint_if_result;
    19831983    joint_if_params = int_fun.joint_if_params; joint_if_stacksize =
    1984     int_fun.joint_if_stacksize; joint_if_code = graph0; joint_if_entry =
     1984    int_fun.joint_if_stacksize; joint_if_code = graph; joint_if_entry =
    19851985    entry }
    19861986
     
    19881988    AST.ident List.list -> graph_params -> __ -> joint_internal_function ->
    19891989    joint_internal_function **)
    1990 let set_joint_if_graph globals pars graph0 p =
    1991   set_joint_code globals (graph_params_to_params pars) p graph0
     1990let set_joint_if_graph globals pars graph p =
     1991  set_joint_code globals (graph_params_to_params pars) p graph
    19921992    (Types.pi1 p.joint_if_entry)
    19931993
Note: See TracChangeset for help on using the changeset viewer.