Changeset 2773 for extracted/joint.ml
 Timestamp:
 Mar 4, 2013, 10:03:33 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/joint.ml
r2743 r2773 17 17 open Extralib 18 18 19 open Lists 20 21 open Identifiers 22 23 open Integers 24 25 open AST 26 27 open Division 28 29 open Exp 30 31 open Arithmetic 32 19 33 open Setoids 20 34 … … 23 37 open Option 24 38 25 open Lists26 27 open Identifiers28 29 open Integers30 31 open AST32 33 open Division34 35 open Exp36 37 open Arithmetic38 39 39 open Extranat 40 40 … … 83 83 open BackEndOps 84 84 85 open CostLabel 86 87 open Order 88 89 open Registers 90 91 open I8051 92 85 93 open BitVectorTrie 86 87 open CostLabel88 89 open Order90 91 open Registers92 93 open I805194 94 95 95 open Graphs … … 110 110 ('a1 > 'a2) > (BitVector.byte > 'a2) > 'a1 argument > 'a2 **) 111 111 let rec argument_rect_Type4 h_Reg h_Imm = function 112  Reg x_1 9390 > h_Reg x_19390113  Imm x_1 9391 > h_Imm x_19391112  Reg x_14700 > h_Reg x_14700 113  Imm x_14701 > h_Imm x_14701 114 114 115 115 (** val argument_rect_Type5 : 116 116 ('a1 > 'a2) > (BitVector.byte > 'a2) > 'a1 argument > 'a2 **) 117 117 let rec argument_rect_Type5 h_Reg h_Imm = function 118  Reg x_1 9395 > h_Reg x_19395119  Imm x_1 9396 > h_Imm x_19396118  Reg x_14705 > h_Reg x_14705 119  Imm x_14706 > h_Imm x_14706 120 120 121 121 (** val argument_rect_Type3 : 122 122 ('a1 > 'a2) > (BitVector.byte > 'a2) > 'a1 argument > 'a2 **) 123 123 let rec argument_rect_Type3 h_Reg h_Imm = function 124  Reg x_1 9400 > h_Reg x_19400125  Imm x_1 9401 > h_Imm x_19401124  Reg x_14710 > h_Reg x_14710 125  Imm x_14711 > h_Imm x_14711 126 126 127 127 (** val argument_rect_Type2 : 128 128 ('a1 > 'a2) > (BitVector.byte > 'a2) > 'a1 argument > 'a2 **) 129 129 let rec argument_rect_Type2 h_Reg h_Imm = function 130  Reg x_1 9405 > h_Reg x_19405131  Imm x_1 9406 > h_Imm x_19406130  Reg x_14715 > h_Reg x_14715 131  Imm x_14716 > h_Imm x_14716 132 132 133 133 (** val argument_rect_Type1 : 134 134 ('a1 > 'a2) > (BitVector.byte > 'a2) > 'a1 argument > 'a2 **) 135 135 let rec argument_rect_Type1 h_Reg h_Imm = function 136  Reg x_1 9410 > h_Reg x_19410137  Imm x_1 9411 > h_Imm x_19411136  Reg x_14720 > h_Reg x_14720 137  Imm x_14721 > h_Imm x_14721 138 138 139 139 (** val argument_rect_Type0 : 140 140 ('a1 > 'a2) > (BitVector.byte > 'a2) > 'a1 argument > 'a2 **) 141 141 let rec argument_rect_Type0 h_Reg h_Imm = function 142  Reg x_1 9415 > h_Reg x_19415143  Imm x_1 9416 > h_Imm x_19416142  Reg x_14725 > h_Reg x_14725 143  Imm x_14726 > h_Imm x_14726 144 144 145 145 (** val argument_inv_rect_Type4 : … … 324 324 __ > (__ > Graphs.label List.list) > Bool.bool > __ > 'a1) > 325 325 unserialized_params > 'a1 **) 326 let rec unserialized_params_rect_Type4 h_mk_unserialized_params x_1 9451 =326 let rec unserialized_params_rect_Type4 h_mk_unserialized_params x_14761 = 327 327 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = 328 x_1 9451328 x_14761 329 329 in 330 330 h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __ … … 335 335 __ > (__ > Graphs.label List.list) > Bool.bool > __ > 'a1) > 336 336 unserialized_params > 'a1 **) 337 let rec unserialized_params_rect_Type5 h_mk_unserialized_params x_1 9453 =337 let rec unserialized_params_rect_Type5 h_mk_unserialized_params x_14763 = 338 338 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = 339 x_1 9453339 x_14763 340 340 in 341 341 h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __ … … 346 346 __ > (__ > Graphs.label List.list) > Bool.bool > __ > 'a1) > 347 347 unserialized_params > 'a1 **) 348 let rec unserialized_params_rect_Type3 h_mk_unserialized_params x_1 9455 =348 let rec unserialized_params_rect_Type3 h_mk_unserialized_params x_14765 = 349 349 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = 350 x_1 9455350 x_14765 351 351 in 352 352 h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __ … … 357 357 __ > (__ > Graphs.label List.list) > Bool.bool > __ > 'a1) > 358 358 unserialized_params > 'a1 **) 359 let rec unserialized_params_rect_Type2 h_mk_unserialized_params x_1 9457 =359 let rec unserialized_params_rect_Type2 h_mk_unserialized_params x_14767 = 360 360 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = 361 x_1 9457361 x_14767 362 362 in 363 363 h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __ … … 368 368 __ > (__ > Graphs.label List.list) > Bool.bool > __ > 'a1) > 369 369 unserialized_params > 'a1 **) 370 let rec unserialized_params_rect_Type1 h_mk_unserialized_params x_1 9459 =370 let rec unserialized_params_rect_Type1 h_mk_unserialized_params x_14769 = 371 371 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = 372 x_1 9459372 x_14769 373 373 in 374 374 h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __ … … 379 379 __ > (__ > Graphs.label List.list) > Bool.bool > __ > 'a1) > 380 380 unserialized_params > 'a1 **) 381 let rec unserialized_params_rect_Type0 h_mk_unserialized_params x_1 9461 =381 let rec unserialized_params_rect_Type0 h_mk_unserialized_params x_14771 = 382 382 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = 383 x_1 9461383 x_14771 384 384 in 385 385 h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __ … … 489 489 'a1) > (__ > 'a1) > joint_seq > 'a1 **) 490 490 let 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_1 9517 > h_COMMENT x_19517492  MOVE x_1 9518 > h_MOVE x_19518493  POP x_1 9519 > h_POP x_19519494  PUSH x_1 9520 > h_PUSH x_19520495  ADDRESS (i, x_1 9522, x_19521) > h_ADDRESS i __ x_19522 x_19521496  OPACCS (x_1 9528, x_19527, x_19526, x_19525, x_19524) >497 h_OPACCS x_1 9528 x_19527 x_19526 x_19525 x_19524498  OP1 (x_1 9531, x_19530, x_19529) > h_OP1 x_19531 x_19530 x_19529499  OP2 (x_1 9535, x_19534, x_19533, x_19532) >500 h_OP2 x_1 9535 x_19534 x_19533 x_19532491  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 501 501  CLEAR_CARRY > h_CLEAR_CARRY 502 502  SET_CARRY > h_SET_CARRY 503  LOAD (x_1 9538, x_19537, x_19536) > h_LOAD x_19538 x_19537 x_19536504  STORE (x_1 9541, x_19540, x_19539) > h_STORE x_19541 x_19540 x_19539505  Extension_seq x_1 9542 > h_extension_seq x_19542503  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 506 506 507 507 (** val joint_seq_rect_Type5 : … … 513 513 'a1) > (__ > 'a1) > joint_seq > 'a1 **) 514 514 let 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_1 9557 > h_COMMENT x_19557516  MOVE x_1 9558 > h_MOVE x_19558517  POP x_1 9559 > h_POP x_19559518  PUSH x_1 9560 > h_PUSH x_19560519  ADDRESS (i, x_1 9562, x_19561) > h_ADDRESS i __ x_19562 x_19561520  OPACCS (x_1 9568, x_19567, x_19566, x_19565, x_19564) >521 h_OPACCS x_1 9568 x_19567 x_19566 x_19565 x_19564522  OP1 (x_1 9571, x_19570, x_19569) > h_OP1 x_19571 x_19570 x_19569523  OP2 (x_1 9575, x_19574, x_19573, x_19572) >524 h_OP2 x_1 9575 x_19574 x_19573 x_19572515  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 525 525  CLEAR_CARRY > h_CLEAR_CARRY 526 526  SET_CARRY > h_SET_CARRY 527  LOAD (x_1 9578, x_19577, x_19576) > h_LOAD x_19578 x_19577 x_19576528  STORE (x_1 9581, x_19580, x_19579) > h_STORE x_19581 x_19580 x_19579529  Extension_seq x_1 9582 > h_extension_seq x_19582527  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 530 530 531 531 (** val joint_seq_rect_Type3 : … … 537 537 'a1) > (__ > 'a1) > joint_seq > 'a1 **) 538 538 let 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_1 9597 > h_COMMENT x_19597540  MOVE x_1 9598 > h_MOVE x_19598541  POP x_1 9599 > h_POP x_19599542  PUSH x_1 9600 > h_PUSH x_19600543  ADDRESS (i, x_1 9602, x_19601) > h_ADDRESS i __ x_19602 x_19601544  OPACCS (x_1 9608, x_19607, x_19606, x_19605, x_19604) >545 h_OPACCS x_1 9608 x_19607 x_19606 x_19605 x_19604546  OP1 (x_1 9611, x_19610, x_19609) > h_OP1 x_19611 x_19610 x_19609547  OP2 (x_1 9615, x_19614, x_19613, x_19612) >548 h_OP2 x_1 9615 x_19614 x_19613 x_19612539  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 549 549  CLEAR_CARRY > h_CLEAR_CARRY 550 550  SET_CARRY > h_SET_CARRY 551  LOAD (x_1 9618, x_19617, x_19616) > h_LOAD x_19618 x_19617 x_19616552  STORE (x_1 9621, x_19620, x_19619) > h_STORE x_19621 x_19620 x_19619553  Extension_seq x_1 9622 > h_extension_seq x_19622551  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 554 554 555 555 (** val joint_seq_rect_Type2 : … … 561 561 'a1) > (__ > 'a1) > joint_seq > 'a1 **) 562 562 let 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_1 9637 > h_COMMENT x_19637564  MOVE x_1 9638 > h_MOVE x_19638565  POP x_1 9639 > h_POP x_19639566  PUSH x_1 9640 > h_PUSH x_19640567  ADDRESS (i, x_1 9642, x_19641) > h_ADDRESS i __ x_19642 x_19641568  OPACCS (x_1 9648, x_19647, x_19646, x_19645, x_19644) >569 h_OPACCS x_1 9648 x_19647 x_19646 x_19645 x_19644570  OP1 (x_1 9651, x_19650, x_19649) > h_OP1 x_19651 x_19650 x_19649571  OP2 (x_1 9655, x_19654, x_19653, x_19652) >572 h_OP2 x_1 9655 x_19654 x_19653 x_19652563  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 573 573  CLEAR_CARRY > h_CLEAR_CARRY 574 574  SET_CARRY > h_SET_CARRY 575  LOAD (x_1 9658, x_19657, x_19656) > h_LOAD x_19658 x_19657 x_19656576  STORE (x_1 9661, x_19660, x_19659) > h_STORE x_19661 x_19660 x_19659577  Extension_seq x_1 9662 > h_extension_seq x_19662575  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 578 578 579 579 (** val joint_seq_rect_Type1 : … … 585 585 'a1) > (__ > 'a1) > joint_seq > 'a1 **) 586 586 let 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_1 9677 > h_COMMENT x_19677588  MOVE x_1 9678 > h_MOVE x_19678589  POP x_1 9679 > h_POP x_19679590  PUSH x_1 9680 > h_PUSH x_19680591  ADDRESS (i, x_1 9682, x_19681) > h_ADDRESS i __ x_19682 x_19681592  OPACCS (x_1 9688, x_19687, x_19686, x_19685, x_19684) >593 h_OPACCS x_1 9688 x_19687 x_19686 x_19685 x_19684594  OP1 (x_1 9691, x_19690, x_19689) > h_OP1 x_19691 x_19690 x_19689595  OP2 (x_1 9695, x_19694, x_19693, x_19692) >596 h_OP2 x_1 9695 x_19694 x_19693 x_19692587  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 597 597  CLEAR_CARRY > h_CLEAR_CARRY 598 598  SET_CARRY > h_SET_CARRY 599  LOAD (x_1 9698, x_19697, x_19696) > h_LOAD x_19698 x_19697 x_19696600  STORE (x_1 9701, x_19700, x_19699) > h_STORE x_19701 x_19700 x_19699601  Extension_seq x_1 9702 > h_extension_seq x_19702599  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 602 602 603 603 (** val joint_seq_rect_Type0 : … … 609 609 'a1) > (__ > 'a1) > joint_seq > 'a1 **) 610 610 let 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_1 9717 > h_COMMENT x_19717612  MOVE x_1 9718 > h_MOVE x_19718613  POP x_1 9719 > h_POP x_19719614  PUSH x_1 9720 > h_PUSH x_19720615  ADDRESS (i, x_1 9722, x_19721) > h_ADDRESS i __ x_19722 x_19721616  OPACCS (x_1 9728, x_19727, x_19726, x_19725, x_19724) >617 h_OPACCS x_1 9728 x_19727 x_19726 x_19725 x_19724618  OP1 (x_1 9731, x_19730, x_19729) > h_OP1 x_19731 x_19730 x_19729619  OP2 (x_1 9735, x_19734, x_19733, x_19732) >620 h_OP2 x_1 9735 x_19734 x_19733 x_19732611  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 621 621  CLEAR_CARRY > h_CLEAR_CARRY 622 622  SET_CARRY > h_SET_CARRY 623  LOAD (x_1 9738, x_19737, x_19736) > h_LOAD x_19738 x_19737 x_19736624  STORE (x_1 9741, x_19740, x_19739) > h_STORE x_19741 x_19740 x_19739625  Extension_seq x_1 9742 > h_extension_seq x_19742623  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 626 626 627 627 (** val joint_seq_inv_rect_Type4 : … … 785 785 > (__ > Graphs.label > 'a1) > (joint_seq > 'a1) > joint_step > 'a1 **) 786 786 let 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_20009788  CALL (x_ 20012, x_20011, x_20010) > h_CALL x_20012 x_20011 x_20010789  COND (x_ 20014, x_20013) > h_COND x_20014 x_20013790  Step_seq x_ 20015 > h_step_seq x_20015787  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 791 791 792 792 (** val joint_step_rect_Type5 : … … 795 795 > (__ > Graphs.label > 'a1) > (joint_seq > 'a1) > joint_step > 'a1 **) 796 796 let 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_20021798  CALL (x_ 20024, x_20023, x_20022) > h_CALL x_20024 x_20023 x_20022799  COND (x_ 20026, x_20025) > h_COND x_20026 x_20025800  Step_seq x_ 20027 > h_step_seq x_20027797  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 801 801 802 802 (** val joint_step_rect_Type3 : … … 805 805 > (__ > Graphs.label > 'a1) > (joint_seq > 'a1) > joint_step > 'a1 **) 806 806 let 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_20033808  CALL (x_ 20036, x_20035, x_20034) > h_CALL x_20036 x_20035 x_20034809  COND (x_ 20038, x_20037) > h_COND x_20038 x_20037810  Step_seq x_ 20039 > h_step_seq x_20039807  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 811 811 812 812 (** val joint_step_rect_Type2 : … … 815 815 > (__ > Graphs.label > 'a1) > (joint_seq > 'a1) > joint_step > 'a1 **) 816 816 let 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_20045818  CALL (x_ 20048, x_20047, x_20046) > h_CALL x_20048 x_20047 x_20046819  COND (x_ 20050, x_20049) > h_COND x_20050 x_20049820  Step_seq x_ 20051 > h_step_seq x_20051817  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 821 821 822 822 (** val joint_step_rect_Type1 : … … 825 825 > (__ > Graphs.label > 'a1) > (joint_seq > 'a1) > joint_step > 'a1 **) 826 826 let 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_20057828  CALL (x_ 20060, x_20059, x_20058) > h_CALL x_20060 x_20059 x_20058829  COND (x_ 20062, x_20061) > h_COND x_20062 x_20061830  Step_seq x_ 20063 > h_step_seq x_20063827  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 831 831 832 832 (** val joint_step_rect_Type0 : … … 835 835 > (__ > Graphs.label > 'a1) > (joint_seq > 'a1) > joint_step > 'a1 **) 836 836 let 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_20069838  CALL (x_ 20072, x_20071, x_20070) > h_CALL x_20072 x_20071 x_20070839  COND (x_ 20074, x_20073) > h_COND x_20074 x_20073840  Step_seq x_ 20075 > h_step_seq x_20075837  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 841 841 842 842 (** val joint_step_inv_rect_Type4 : … … 995 995 (unserialized_params > __ > (__ > Graphs.label Types.option) > 996 996 Bool.bool > 'a1) > stmt_params > 'a1 **) 997 let rec stmt_params_rect_Type4 h_mk_stmt_params x_ 20154 =997 let rec stmt_params_rect_Type4 h_mk_stmt_params x_15464 = 998 998 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = 999 has_fcond0 } = x_ 20154999 has_fcond0 } = x_15464 1000 1000 in 1001 1001 h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0 … … 1004 1004 (unserialized_params > __ > (__ > Graphs.label Types.option) > 1005 1005 Bool.bool > 'a1) > stmt_params > 'a1 **) 1006 let rec stmt_params_rect_Type5 h_mk_stmt_params x_ 20156 =1006 let rec stmt_params_rect_Type5 h_mk_stmt_params x_15466 = 1007 1007 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = 1008 has_fcond0 } = x_ 201561008 has_fcond0 } = x_15466 1009 1009 in 1010 1010 h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0 … … 1013 1013 (unserialized_params > __ > (__ > Graphs.label Types.option) > 1014 1014 Bool.bool > 'a1) > stmt_params > 'a1 **) 1015 let rec stmt_params_rect_Type3 h_mk_stmt_params x_ 20158 =1015 let rec stmt_params_rect_Type3 h_mk_stmt_params x_15468 = 1016 1016 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = 1017 has_fcond0 } = x_ 201581017 has_fcond0 } = x_15468 1018 1018 in 1019 1019 h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0 … … 1022 1022 (unserialized_params > __ > (__ > Graphs.label Types.option) > 1023 1023 Bool.bool > 'a1) > stmt_params > 'a1 **) 1024 let rec stmt_params_rect_Type2 h_mk_stmt_params x_ 20160 =1024 let rec stmt_params_rect_Type2 h_mk_stmt_params x_15470 = 1025 1025 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = 1026 has_fcond0 } = x_ 201601026 has_fcond0 } = x_15470 1027 1027 in 1028 1028 h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0 … … 1031 1031 (unserialized_params > __ > (__ > Graphs.label Types.option) > 1032 1032 Bool.bool > 'a1) > stmt_params > 'a1 **) 1033 let rec stmt_params_rect_Type1 h_mk_stmt_params x_ 20162 =1033 let rec stmt_params_rect_Type1 h_mk_stmt_params x_15472 = 1034 1034 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = 1035 has_fcond0 } = x_ 201621035 has_fcond0 } = x_15472 1036 1036 in 1037 1037 h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0 … … 1040 1040 (unserialized_params > __ > (__ > Graphs.label Types.option) > 1041 1041 Bool.bool > 'a1) > stmt_params > 'a1 **) 1042 let rec stmt_params_rect_Type0 h_mk_stmt_params x_ 20164 =1042 let rec stmt_params_rect_Type0 h_mk_stmt_params x_15474 = 1043 1043 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = 1044 has_fcond0 } = x_ 201641044 has_fcond0 } = x_15474 1045 1045 in 1046 1046 h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0 … … 1050 1050 xxx.uns_pars 1051 1051 1052 type succ 0= __1052 type succ = __ 1053 1053 1054 1054 (** val succ_label : stmt_params > __ > Graphs.label Types.option **) … … 1105 1105 (__, __) Types.prod) Types.sum > __ > 'a1) > joint_fin_step > 'a1 **) 1106 1106 let rec joint_fin_step_rect_Type4 p h_GOTO h_RETURN h_TAILCALL = function 1107  GOTO x_ 20188 > h_GOTO x_201881107  GOTO x_15498 > h_GOTO x_15498 1108 1108  RETURN > h_RETURN 1109  TAILCALL (x_ 20190, x_20189) > h_TAILCALL __ x_20190 x_201891109  TAILCALL (x_15500, x_15499) > h_TAILCALL __ x_15500 x_15499 1110 1110 1111 1111 (** val joint_fin_step_rect_Type5 : … … 1113 1113 (__, __) Types.prod) Types.sum > __ > 'a1) > joint_fin_step > 'a1 **) 1114 1114 let rec joint_fin_step_rect_Type5 p h_GOTO h_RETURN h_TAILCALL = function 1115  GOTO x_ 20196 > h_GOTO x_201961115  GOTO x_15506 > h_GOTO x_15506 1116 1116  RETURN > h_RETURN 1117  TAILCALL (x_ 20198, x_20197) > h_TAILCALL __ x_20198 x_201971117  TAILCALL (x_15508, x_15507) > h_TAILCALL __ x_15508 x_15507 1118 1118 1119 1119 (** val joint_fin_step_rect_Type3 : … … 1121 1121 (__, __) Types.prod) Types.sum > __ > 'a1) > joint_fin_step > 'a1 **) 1122 1122 let rec joint_fin_step_rect_Type3 p h_GOTO h_RETURN h_TAILCALL = function 1123  GOTO x_ 20204 > h_GOTO x_202041123  GOTO x_15514 > h_GOTO x_15514 1124 1124  RETURN > h_RETURN 1125  TAILCALL (x_ 20206, x_20205) > h_TAILCALL __ x_20206 x_202051125  TAILCALL (x_15516, x_15515) > h_TAILCALL __ x_15516 x_15515 1126 1126 1127 1127 (** val joint_fin_step_rect_Type2 : … … 1129 1129 (__, __) Types.prod) Types.sum > __ > 'a1) > joint_fin_step > 'a1 **) 1130 1130 let rec joint_fin_step_rect_Type2 p h_GOTO h_RETURN h_TAILCALL = function 1131  GOTO x_ 20212 > h_GOTO x_202121131  GOTO x_15522 > h_GOTO x_15522 1132 1132  RETURN > h_RETURN 1133  TAILCALL (x_ 20214, x_20213) > h_TAILCALL __ x_20214 x_202131133  TAILCALL (x_15524, x_15523) > h_TAILCALL __ x_15524 x_15523 1134 1134 1135 1135 (** val joint_fin_step_rect_Type1 : … … 1137 1137 (__, __) Types.prod) Types.sum > __ > 'a1) > joint_fin_step > 'a1 **) 1138 1138 let rec joint_fin_step_rect_Type1 p h_GOTO h_RETURN h_TAILCALL = function 1139  GOTO x_ 20220 > h_GOTO x_202201139  GOTO x_15530 > h_GOTO x_15530 1140 1140  RETURN > h_RETURN 1141  TAILCALL (x_ 20222, x_20221) > h_TAILCALL __ x_20222 x_202211141  TAILCALL (x_15532, x_15531) > h_TAILCALL __ x_15532 x_15531 1142 1142 1143 1143 (** val joint_fin_step_rect_Type0 : … … 1145 1145 (__, __) Types.prod) Types.sum > __ > 'a1) > joint_fin_step > 'a1 **) 1146 1146 let rec joint_fin_step_rect_Type0 p h_GOTO h_RETURN h_TAILCALL = function 1147  GOTO x_ 20228 > h_GOTO x_202281147  GOTO x_15538 > h_GOTO x_15538 1148 1148  RETURN > h_RETURN 1149  TAILCALL (x_ 20230, x_20229) > h_TAILCALL __ x_20230 x_202291149  TAILCALL (x_15540, x_15539) > h_TAILCALL __ x_15540 x_15539 1150 1150 1151 1151 (** val joint_fin_step_inv_rect_Type4 : … … 1219 1219 'a1) > joint_statement > 'a1 **) 1220 1220 let 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_202951222  Final x_ 20297 > h_final x_202971223  FCOND (x_ 20300, x_20299, x_20298) > h_FCOND __ x_20300 x_20299 x_202981221  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 1224 1224 1225 1225 (** val joint_statement_rect_Type5 : … … 1228 1228 'a1) > joint_statement > 'a1 **) 1229 1229 let 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_203061231  Final x_ 20308 > h_final x_203081232  FCOND (x_ 20311, x_20310, x_20309) > h_FCOND __ x_20311 x_20310 x_203091230  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 1233 1233 1234 1234 (** val joint_statement_rect_Type3 : … … 1237 1237 'a1) > joint_statement > 'a1 **) 1238 1238 let 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_203171240  Final x_ 20319 > h_final x_203191241  FCOND (x_ 20322, x_20321, x_20320) > h_FCOND __ x_20322 x_20321 x_203201239  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 1242 1242 1243 1243 (** val joint_statement_rect_Type2 : … … 1246 1246 'a1) > joint_statement > 'a1 **) 1247 1247 let 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_203281249  Final x_ 20330 > h_final x_203301250  FCOND (x_ 20333, x_20332, x_20331) > h_FCOND __ x_20333 x_20332 x_203311248  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 1251 1251 1252 1252 (** val joint_statement_rect_Type1 : … … 1255 1255 'a1) > joint_statement > 'a1 **) 1256 1256 let 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_203391258  Final x_ 20341 > h_final x_203411259  FCOND (x_ 20344, x_20343, x_20342) > h_FCOND __ x_20344 x_20343 x_203421257  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 1260 1260 1261 1261 (** val joint_statement_rect_Type0 : … … 1264 1264 'a1) > joint_statement > 'a1 **) 1265 1265 let 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_203501267  Final x_ 20352 > h_final x_203521268  FCOND (x_ 20355, x_20354, x_20353) > h_FCOND __ x_20355 x_20354 x_203531266  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 1269 1269 1270 1270 (** val joint_statement_inv_rect_Type4 : … … 1365 1365 Graphs.label > __ Types.option) > (__ > __ > __) > 'a1) > params > 1366 1366 'a1 **) 1367 let rec params_rect_Type4 h_mk_params x_ 20428 =1367 let rec params_rect_Type4 h_mk_params x_15738 = 1368 1368 let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label = 1369 point_of_label0; point_of_succ = point_of_succ0 } = x_ 204281369 point_of_label0; point_of_succ = point_of_succ0 } = x_15738 1370 1370 in 1371 1371 h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0 … … 1376 1376 Graphs.label > __ Types.option) > (__ > __ > __) > 'a1) > params > 1377 1377 'a1 **) 1378 let rec params_rect_Type5 h_mk_params x_ 20430 =1378 let rec params_rect_Type5 h_mk_params x_15740 = 1379 1379 let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label = 1380 point_of_label0; point_of_succ = point_of_succ0 } = x_ 204301380 point_of_label0; point_of_succ = point_of_succ0 } = x_15740 1381 1381 in 1382 1382 h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0 … … 1387 1387 Graphs.label > __ Types.option) > (__ > __ > __) > 'a1) > params > 1388 1388 'a1 **) 1389 let rec params_rect_Type3 h_mk_params x_ 20432 =1389 let rec params_rect_Type3 h_mk_params x_15742 = 1390 1390 let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label = 1391 point_of_label0; point_of_succ = point_of_succ0 } = x_ 204321391 point_of_label0; point_of_succ = point_of_succ0 } = x_15742 1392 1392 in 1393 1393 h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0 … … 1398 1398 Graphs.label > __ Types.option) > (__ > __ > __) > 'a1) > params > 1399 1399 'a1 **) 1400 let rec params_rect_Type2 h_mk_params x_ 20434 =1400 let rec params_rect_Type2 h_mk_params x_15744 = 1401 1401 let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label = 1402 point_of_label0; point_of_succ = point_of_succ0 } = x_ 204341402 point_of_label0; point_of_succ = point_of_succ0 } = x_15744 1403 1403 in 1404 1404 h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0 … … 1409 1409 Graphs.label > __ Types.option) > (__ > __ > __) > 'a1) > params > 1410 1410 'a1 **) 1411 let rec params_rect_Type1 h_mk_params x_ 20436 =1411 let rec params_rect_Type1 h_mk_params x_15746 = 1412 1412 let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label = 1413 point_of_label0; point_of_succ = point_of_succ0 } = x_ 204361413 point_of_label0; point_of_succ = point_of_succ0 } = x_15746 1414 1414 in 1415 1415 h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0 … … 1420 1420 Graphs.label > __ Types.option) > (__ > __ > __) > 'a1) > params > 1421 1421 'a1 **) 1422 let rec params_rect_Type0 h_mk_params x_ 20438 =1422 let rec params_rect_Type0 h_mk_params x_15748 = 1423 1423 let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label = 1424 point_of_label0; point_of_succ = point_of_succ0 } = x_ 204381424 point_of_label0; point_of_succ = point_of_succ0 } = x_15748 1425 1425 in 1426 1426 h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0 … … 1528 1528 stmt_params > AST.ident List.list > joint_statement > Graphs.label 1529 1529 List.list **) 1530 let stmt_labels p g 0stmt =1530 let stmt_labels p g stmt = 1531 1531 List.append 1532 (match stmt_implicit_label p g 0stmt with1532 (match stmt_implicit_label p g stmt with 1533 1533  Types.None > List.Nil 1534 1534  Types.Some l > List.Cons (l, List.Nil)) 1535 (stmt_explicit_labels p g 0stmt)1535 (stmt_explicit_labels p g stmt) 1536 1536 1537 1537 type lin_params = … … 1541 1541 (** val lin_params_rect_Type4 : 1542 1542 (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_pars1543 let 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 1545 1545 1546 1546 (** val lin_params_rect_Type5 : 1547 1547 (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_pars1548 let 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 1550 1550 1551 1551 (** val lin_params_rect_Type3 : 1552 1552 (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_pars1553 let 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 1555 1555 1556 1556 (** val lin_params_rect_Type2 : 1557 1557 (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_pars1558 let 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 1560 1560 1561 1561 (** val lin_params_rect_Type1 : 1562 1562 (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_pars1563 let 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 1565 1565 1566 1566 (** val lin_params_rect_Type0 : 1567 1567 (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_pars1568 let 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 1570 1570 1571 1571 (** val l_u_pars : lin_params > unserialized_params **) … … 1608 1608 (fun globals code point > 1609 1609 Obj.magic 1610 (Monad.m_bind0 (Monad.max_def Option.option 0)1610 (Monad.m_bind0 (Monad.max_def Option.option) 1611 1611 (Obj.magic (List.nth_opt (Obj.magic point) (Obj.magic code))) 1612 1612 (fun ls > 1613 Monad.m_return0 (Monad.max_def Option.option 0) ls.Types.snd)));1613 Monad.m_return0 (Monad.max_def Option.option) ls.Types.snd))); 1614 1614 point_of_label = (fun globals c lbl > 1615 1615 Util.if_then_else_safe … … 1617 1617 (Obj.magic c)) (fun _ > 1618 1618 Obj.magic 1619 (Monad.m_return0 (Monad.max_def Option.option 0)1619 (Monad.m_return0 (Monad.max_def Option.option) 1620 1620 (LabelledObjects.index_of_label PreIdentifiers.LabelTag lbl 1621 1621 (Obj.magic c)))) (fun _ > Types.None)); point_of_succ = … … 1637 1637 (** val graph_params_rect_Type4 : 1638 1638 (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_pars1639 let 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 1641 1641 1642 1642 (** val graph_params_rect_Type5 : 1643 1643 (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_pars1644 let 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 1646 1646 1647 1647 (** val graph_params_rect_Type3 : 1648 1648 (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_pars1649 let 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 1651 1651 1652 1652 (** val graph_params_rect_Type2 : 1653 1653 (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_pars1654 let 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 1656 1656 1657 1657 (** val graph_params_rect_Type1 : 1658 1658 (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_pars1659 let 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 1661 1661 1662 1662 (** val graph_params_rect_Type0 : 1663 1663 (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_pars1664 let 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 1666 1666 1667 1667 (** val g_u_pars : graph_params > unserialized_params **) … … 1703 1703 (Obj.magic (fun x > Types.Some x)); has_fcond = Bool.False }; stmt_at = 1704 1704 (fun globals code > 1705 Obj.magic (Identifiers.lookup 0PreIdentifiers.LabelTag (Obj.magic code)));1705 Obj.magic (Identifiers.lookup PreIdentifiers.LabelTag (Obj.magic code))); 1706 1706 point_of_label = (fun x x0 lbl > 1707 Obj.magic (Monad.m_return0 (Monad.max_def Option.option 0) lbl));1707 Obj.magic (Monad.m_return0 (Monad.max_def Option.option) lbl)); 1708 1708 point_of_succ = (fun x lbl > lbl) } 1709 1709 … … 1728 1728 Identifiers.universe > __ > __ > Nat.nat > __ > __ Types.sig0 > 1729 1729 'a1) > joint_internal_function > 'a1 **) 1730 let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_ 20513 =1730 let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_15823 = 1731 1731 let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse = 1732 1732 joint_if_runiverse0; joint_if_result = joint_if_result0; 1733 1733 joint_if_params = joint_if_params0; joint_if_stacksize = 1734 1734 joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry = 1735 joint_if_entry0 } = x_ 205131735 joint_if_entry0 } = x_15823 1736 1736 in 1737 1737 h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0 … … 1743 1743 Identifiers.universe > __ > __ > Nat.nat > __ > __ Types.sig0 > 1744 1744 'a1) > joint_internal_function > 'a1 **) 1745 let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_ 20515 =1745 let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_15825 = 1746 1746 let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse = 1747 1747 joint_if_runiverse0; joint_if_result = joint_if_result0; 1748 1748 joint_if_params = joint_if_params0; joint_if_stacksize = 1749 1749 joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry = 1750 joint_if_entry0 } = x_ 205151750 joint_if_entry0 } = x_15825 1751 1751 in 1752 1752 h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0 … … 1758 1758 Identifiers.universe > __ > __ > Nat.nat > __ > __ Types.sig0 > 1759 1759 'a1) > joint_internal_function > 'a1 **) 1760 let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_ 20517 =1760 let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_15827 = 1761 1761 let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse = 1762 1762 joint_if_runiverse0; joint_if_result = joint_if_result0; 1763 1763 joint_if_params = joint_if_params0; joint_if_stacksize = 1764 1764 joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry = 1765 joint_if_entry0 } = x_ 205171765 joint_if_entry0 } = x_15827 1766 1766 in 1767 1767 h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0 … … 1773 1773 Identifiers.universe > __ > __ > Nat.nat > __ > __ Types.sig0 > 1774 1774 'a1) > joint_internal_function > 'a1 **) 1775 let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_ 20519 =1775 let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_15829 = 1776 1776 let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse = 1777 1777 joint_if_runiverse0; joint_if_result = joint_if_result0; 1778 1778 joint_if_params = joint_if_params0; joint_if_stacksize = 1779 1779 joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry = 1780 joint_if_entry0 } = x_ 205191780 joint_if_entry0 } = x_15829 1781 1781 in 1782 1782 h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0 … … 1788 1788 Identifiers.universe > __ > __ > Nat.nat > __ > __ Types.sig0 > 1789 1789 'a1) > joint_internal_function > 'a1 **) 1790 let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_ 20521 =1790 let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_15831 = 1791 1791 let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse = 1792 1792 joint_if_runiverse0; joint_if_result = joint_if_result0; 1793 1793 joint_if_params = joint_if_params0; joint_if_stacksize = 1794 1794 joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry = 1795 joint_if_entry0 } = x_ 205211795 joint_if_entry0 } = x_15831 1796 1796 in 1797 1797 h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0 … … 1803 1803 Identifiers.universe > __ > __ > Nat.nat > __ > __ Types.sig0 > 1804 1804 'a1) > joint_internal_function > 'a1 **) 1805 let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_ 20523 =1805 let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_15833 = 1806 1806 let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse = 1807 1807 joint_if_runiverse0; joint_if_result = joint_if_result0; 1808 1808 joint_if_params = joint_if_params0; joint_if_stacksize = 1809 1809 joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry = 1810 joint_if_entry0 } = x_ 205231810 joint_if_entry0 } = x_15833 1811 1811 in 1812 1812 h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0 … … 1978 1978 AST.ident List.list > params > joint_internal_function > __ > __ 1979 1979 Types.sig0 > joint_internal_function **) 1980 let set_joint_code globals pars int_fun graph 0entry =1980 let set_joint_code globals pars int_fun graph entry = 1981 1981 { joint_if_luniverse = int_fun.joint_if_luniverse; joint_if_runiverse = 1982 1982 int_fun.joint_if_runiverse; joint_if_result = int_fun.joint_if_result; 1983 1983 joint_if_params = int_fun.joint_if_params; joint_if_stacksize = 1984 int_fun.joint_if_stacksize; joint_if_code = graph 0; joint_if_entry =1984 int_fun.joint_if_stacksize; joint_if_code = graph; joint_if_entry = 1985 1985 entry } 1986 1986 … … 1988 1988 AST.ident List.list > graph_params > __ > joint_internal_function > 1989 1989 joint_internal_function **) 1990 let set_joint_if_graph globals pars graph 0p =1991 set_joint_code globals (graph_params_to_params pars) p graph 01990 let set_joint_if_graph globals pars graph p = 1991 set_joint_code globals (graph_params_to_params pars) p graph 1992 1992 (Types.pi1 p.joint_if_entry) 1993 1993
Note: See TracChangeset
for help on using the changeset viewer.