Changeset 2873 for extracted/joint.ml
 Timestamp:
 Mar 14, 2013, 10:37:39 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/joint.ml
r2867 r2873 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_19 661 > h_Reg x_19661113  Imm x_19 662 > h_Imm x_19662112  Reg x_19830 > h_Reg x_19830 113  Imm x_19831 > h_Imm x_19831 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_19 666 > h_Reg x_19666119  Imm x_19 667 > h_Imm x_19667118  Reg x_19835 > h_Reg x_19835 119  Imm x_19836 > h_Imm x_19836 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_19 671 > h_Reg x_19671125  Imm x_19 672 > h_Imm x_19672124  Reg x_19840 > h_Reg x_19840 125  Imm x_19841 > h_Imm x_19841 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_19 676 > h_Reg x_19676131  Imm x_19 677 > h_Imm x_19677130  Reg x_19845 > h_Reg x_19845 131  Imm x_19846 > h_Imm x_19846 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_19 681 > h_Reg x_19681137  Imm x_19 682 > h_Imm x_19682136  Reg x_19850 > h_Reg x_19850 137  Imm x_19851 > h_Imm x_19851 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_19 686 > h_Reg x_19686143  Imm x_19 687 > h_Imm x_19687142  Reg x_19855 > h_Reg x_19855 143  Imm x_19856 > h_Imm x_19856 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_19 722=326 let rec unserialized_params_rect_Type4 h_mk_unserialized_params x_19891 = 327 327 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = 328 x_19 722328 x_19891 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_19 724=337 let rec unserialized_params_rect_Type5 h_mk_unserialized_params x_19893 = 338 338 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = 339 x_19 724339 x_19893 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_19 726=348 let rec unserialized_params_rect_Type3 h_mk_unserialized_params x_19895 = 349 349 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = 350 x_19 726350 x_19895 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_19 728=359 let rec unserialized_params_rect_Type2 h_mk_unserialized_params x_19897 = 360 360 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = 361 x_19 728361 x_19897 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_19 730=370 let rec unserialized_params_rect_Type1 h_mk_unserialized_params x_19899 = 371 371 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = 372 x_19 730372 x_19899 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_19 732=381 let rec unserialized_params_rect_Type0 h_mk_unserialized_params x_19901 = 382 382 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = 383 x_19 732383 x_19901 384 384 in 385 385 h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __ … … 506 506 (__ > Registers.register List.list) > 'a1) > get_pseudo_reg_functs > 507 507 'a1 **) 508 let rec get_pseudo_reg_functs_rect_Type4 p h_mk_get_pseudo_reg_functs x_19 749=508 let rec get_pseudo_reg_functs_rect_Type4 p h_mk_get_pseudo_reg_functs x_19918 = 509 509 let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args = 510 510 acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs = … … 512 512 snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0; 513 513 f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs = 514 params_regs0 } = x_19 749514 params_regs0 } = x_19918 515 515 in 516 516 h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0 … … 529 529 (__ > Registers.register List.list) > 'a1) > get_pseudo_reg_functs > 530 530 'a1 **) 531 let rec get_pseudo_reg_functs_rect_Type5 p h_mk_get_pseudo_reg_functs x_19 751=531 let rec get_pseudo_reg_functs_rect_Type5 p h_mk_get_pseudo_reg_functs x_19920 = 532 532 let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args = 533 533 acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs = … … 535 535 snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0; 536 536 f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs = 537 params_regs0 } = x_19 751537 params_regs0 } = x_19920 538 538 in 539 539 h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0 … … 552 552 (__ > Registers.register List.list) > 'a1) > get_pseudo_reg_functs > 553 553 'a1 **) 554 let rec get_pseudo_reg_functs_rect_Type3 p h_mk_get_pseudo_reg_functs x_19 753=554 let rec get_pseudo_reg_functs_rect_Type3 p h_mk_get_pseudo_reg_functs x_19922 = 555 555 let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args = 556 556 acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs = … … 558 558 snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0; 559 559 f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs = 560 params_regs0 } = x_19 753560 params_regs0 } = x_19922 561 561 in 562 562 h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0 … … 575 575 (__ > Registers.register List.list) > 'a1) > get_pseudo_reg_functs > 576 576 'a1 **) 577 let rec get_pseudo_reg_functs_rect_Type2 p h_mk_get_pseudo_reg_functs x_19 755=577 let rec get_pseudo_reg_functs_rect_Type2 p h_mk_get_pseudo_reg_functs x_19924 = 578 578 let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args = 579 579 acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs = … … 581 581 snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0; 582 582 f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs = 583 params_regs0 } = x_19 755583 params_regs0 } = x_19924 584 584 in 585 585 h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0 … … 598 598 (__ > Registers.register List.list) > 'a1) > get_pseudo_reg_functs > 599 599 'a1 **) 600 let rec get_pseudo_reg_functs_rect_Type1 p h_mk_get_pseudo_reg_functs x_19 757=600 let rec get_pseudo_reg_functs_rect_Type1 p h_mk_get_pseudo_reg_functs x_19926 = 601 601 let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args = 602 602 acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs = … … 604 604 snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0; 605 605 f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs = 606 params_regs0 } = x_19 757606 params_regs0 } = x_19926 607 607 in 608 608 h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0 … … 621 621 (__ > Registers.register List.list) > 'a1) > get_pseudo_reg_functs > 622 622 'a1 **) 623 let rec get_pseudo_reg_functs_rect_Type0 p h_mk_get_pseudo_reg_functs x_19 759=623 let rec get_pseudo_reg_functs_rect_Type0 p h_mk_get_pseudo_reg_functs x_19928 = 624 624 let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args = 625 625 acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs = … … 627 627 snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0; 628 628 f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs = 629 params_regs0 } = x_19 759629 params_regs0 } = x_19928 630 630 in 631 631 h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0 … … 805 805 (unserialized_params > get_pseudo_reg_functs > 'a1) > uns_params > 806 806 'a1 **) 807 let rec uns_params_rect_Type4 h_mk_uns_params x_19 789=808 let { u_pars = u_pars0; functs = functs0 } = x_19 789in807 let rec uns_params_rect_Type4 h_mk_uns_params x_19958 = 808 let { u_pars = u_pars0; functs = functs0 } = x_19958 in 809 809 h_mk_uns_params u_pars0 functs0 810 810 … … 812 812 (unserialized_params > get_pseudo_reg_functs > 'a1) > uns_params > 813 813 'a1 **) 814 let rec uns_params_rect_Type5 h_mk_uns_params x_19 791=815 let { u_pars = u_pars0; functs = functs0 } = x_19 791in814 let rec uns_params_rect_Type5 h_mk_uns_params x_19960 = 815 let { u_pars = u_pars0; functs = functs0 } = x_19960 in 816 816 h_mk_uns_params u_pars0 functs0 817 817 … … 819 819 (unserialized_params > get_pseudo_reg_functs > 'a1) > uns_params > 820 820 'a1 **) 821 let rec uns_params_rect_Type3 h_mk_uns_params x_19 793=822 let { u_pars = u_pars0; functs = functs0 } = x_19 793in821 let rec uns_params_rect_Type3 h_mk_uns_params x_19962 = 822 let { u_pars = u_pars0; functs = functs0 } = x_19962 in 823 823 h_mk_uns_params u_pars0 functs0 824 824 … … 826 826 (unserialized_params > get_pseudo_reg_functs > 'a1) > uns_params > 827 827 'a1 **) 828 let rec uns_params_rect_Type2 h_mk_uns_params x_19 795=829 let { u_pars = u_pars0; functs = functs0 } = x_19 795in828 let rec uns_params_rect_Type2 h_mk_uns_params x_19964 = 829 let { u_pars = u_pars0; functs = functs0 } = x_19964 in 830 830 h_mk_uns_params u_pars0 functs0 831 831 … … 833 833 (unserialized_params > get_pseudo_reg_functs > 'a1) > uns_params > 834 834 'a1 **) 835 let rec uns_params_rect_Type1 h_mk_uns_params x_19 797=836 let { u_pars = u_pars0; functs = functs0 } = x_19 797in835 let rec uns_params_rect_Type1 h_mk_uns_params x_19966 = 836 let { u_pars = u_pars0; functs = functs0 } = x_19966 in 837 837 h_mk_uns_params u_pars0 functs0 838 838 … … 840 840 (unserialized_params > get_pseudo_reg_functs > 'a1) > uns_params > 841 841 'a1 **) 842 let rec uns_params_rect_Type0 h_mk_uns_params x_19 799=843 let { u_pars = u_pars0; functs = functs0 } = x_19 799in842 let rec uns_params_rect_Type0 h_mk_uns_params x_19968 = 843 let { u_pars = u_pars0; functs = functs0 } = x_19968 in 844 844 h_mk_uns_params u_pars0 functs0 845 845 … … 911 911 'a1) > (__ > 'a1) > joint_seq > 'a1 **) 912 912 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 913  COMMENT x_ 19854 > h_COMMENT x_19854914  MOVE x_ 19855 > h_MOVE x_19855915  POP x_ 19856 > h_POP x_19856916  PUSH x_ 19857 > h_PUSH x_19857917  ADDRESS (i, x_ 19859, x_19858) > h_ADDRESS i __ x_19859 x_19858918  OPACCS (x_ 19865, x_19864, x_19863, x_19862, x_19861) >919 h_OPACCS x_ 19865 x_19864 x_19863 x_19862 x_19861920  OP1 (x_ 19868, x_19867, x_19866) > h_OP1 x_19868 x_19867 x_19866921  OP2 (x_ 19872, x_19871, x_19870, x_19869) >922 h_OP2 x_ 19872 x_19871 x_19870 x_19869913  COMMENT x_20023 > h_COMMENT x_20023 914  MOVE x_20024 > h_MOVE x_20024 915  POP x_20025 > h_POP x_20025 916  PUSH x_20026 > h_PUSH x_20026 917  ADDRESS (i, x_20028, x_20027) > h_ADDRESS i __ x_20028 x_20027 918  OPACCS (x_20034, x_20033, x_20032, x_20031, x_20030) > 919 h_OPACCS x_20034 x_20033 x_20032 x_20031 x_20030 920  OP1 (x_20037, x_20036, x_20035) > h_OP1 x_20037 x_20036 x_20035 921  OP2 (x_20041, x_20040, x_20039, x_20038) > 922 h_OP2 x_20041 x_20040 x_20039 x_20038 923 923  CLEAR_CARRY > h_CLEAR_CARRY 924 924  SET_CARRY > h_SET_CARRY 925  LOAD (x_ 19875, x_19874, x_19873) > h_LOAD x_19875 x_19874 x_19873926  STORE (x_ 19878, x_19877, x_19876) > h_STORE x_19878 x_19877 x_19876927  Extension_seq x_ 19879 > h_extension_seq x_19879925  LOAD (x_20044, x_20043, x_20042) > h_LOAD x_20044 x_20043 x_20042 926  STORE (x_20047, x_20046, x_20045) > h_STORE x_20047 x_20046 x_20045 927  Extension_seq x_20048 > h_extension_seq x_20048 928 928 929 929 (** val joint_seq_rect_Type5 : … … 935 935 'a1) > (__ > 'a1) > joint_seq > 'a1 **) 936 936 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 937  COMMENT x_ 19894 > h_COMMENT x_19894938  MOVE x_ 19895 > h_MOVE x_19895939  POP x_ 19896 > h_POP x_19896940  PUSH x_ 19897 > h_PUSH x_19897941  ADDRESS (i, x_ 19899, x_19898) > h_ADDRESS i __ x_19899 x_19898942  OPACCS (x_ 19905, x_19904, x_19903, x_19902, x_19901) >943 h_OPACCS x_ 19905 x_19904 x_19903 x_19902 x_19901944  OP1 (x_ 19908, x_19907, x_19906) > h_OP1 x_19908 x_19907 x_19906945  OP2 (x_ 19912, x_19911, x_19910, x_19909) >946 h_OP2 x_ 19912 x_19911 x_19910 x_19909937  COMMENT x_20063 > h_COMMENT x_20063 938  MOVE x_20064 > h_MOVE x_20064 939  POP x_20065 > h_POP x_20065 940  PUSH x_20066 > h_PUSH x_20066 941  ADDRESS (i, x_20068, x_20067) > h_ADDRESS i __ x_20068 x_20067 942  OPACCS (x_20074, x_20073, x_20072, x_20071, x_20070) > 943 h_OPACCS x_20074 x_20073 x_20072 x_20071 x_20070 944  OP1 (x_20077, x_20076, x_20075) > h_OP1 x_20077 x_20076 x_20075 945  OP2 (x_20081, x_20080, x_20079, x_20078) > 946 h_OP2 x_20081 x_20080 x_20079 x_20078 947 947  CLEAR_CARRY > h_CLEAR_CARRY 948 948  SET_CARRY > h_SET_CARRY 949  LOAD (x_ 19915, x_19914, x_19913) > h_LOAD x_19915 x_19914 x_19913950  STORE (x_ 19918, x_19917, x_19916) > h_STORE x_19918 x_19917 x_19916951  Extension_seq x_ 19919 > h_extension_seq x_19919949  LOAD (x_20084, x_20083, x_20082) > h_LOAD x_20084 x_20083 x_20082 950  STORE (x_20087, x_20086, x_20085) > h_STORE x_20087 x_20086 x_20085 951  Extension_seq x_20088 > h_extension_seq x_20088 952 952 953 953 (** val joint_seq_rect_Type3 : … … 959 959 'a1) > (__ > 'a1) > joint_seq > 'a1 **) 960 960 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 961  COMMENT x_ 19934 > h_COMMENT x_19934962  MOVE x_ 19935 > h_MOVE x_19935963  POP x_ 19936 > h_POP x_19936964  PUSH x_ 19937 > h_PUSH x_19937965  ADDRESS (i, x_ 19939, x_19938) > h_ADDRESS i __ x_19939 x_19938966  OPACCS (x_ 19945, x_19944, x_19943, x_19942, x_19941) >967 h_OPACCS x_ 19945 x_19944 x_19943 x_19942 x_19941968  OP1 (x_ 19948, x_19947, x_19946) > h_OP1 x_19948 x_19947 x_19946969  OP2 (x_ 19952, x_19951, x_19950, x_19949) >970 h_OP2 x_ 19952 x_19951 x_19950 x_19949961  COMMENT x_20103 > h_COMMENT x_20103 962  MOVE x_20104 > h_MOVE x_20104 963  POP x_20105 > h_POP x_20105 964  PUSH x_20106 > h_PUSH x_20106 965  ADDRESS (i, x_20108, x_20107) > h_ADDRESS i __ x_20108 x_20107 966  OPACCS (x_20114, x_20113, x_20112, x_20111, x_20110) > 967 h_OPACCS x_20114 x_20113 x_20112 x_20111 x_20110 968  OP1 (x_20117, x_20116, x_20115) > h_OP1 x_20117 x_20116 x_20115 969  OP2 (x_20121, x_20120, x_20119, x_20118) > 970 h_OP2 x_20121 x_20120 x_20119 x_20118 971 971  CLEAR_CARRY > h_CLEAR_CARRY 972 972  SET_CARRY > h_SET_CARRY 973  LOAD (x_ 19955, x_19954, x_19953) > h_LOAD x_19955 x_19954 x_19953974  STORE (x_ 19958, x_19957, x_19956) > h_STORE x_19958 x_19957 x_19956975  Extension_seq x_ 19959 > h_extension_seq x_19959973  LOAD (x_20124, x_20123, x_20122) > h_LOAD x_20124 x_20123 x_20122 974  STORE (x_20127, x_20126, x_20125) > h_STORE x_20127 x_20126 x_20125 975  Extension_seq x_20128 > h_extension_seq x_20128 976 976 977 977 (** val joint_seq_rect_Type2 : … … 983 983 'a1) > (__ > 'a1) > joint_seq > 'a1 **) 984 984 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 985  COMMENT x_ 19974 > h_COMMENT x_19974986  MOVE x_ 19975 > h_MOVE x_19975987  POP x_ 19976 > h_POP x_19976988  PUSH x_ 19977 > h_PUSH x_19977989  ADDRESS (i, x_ 19979, x_19978) > h_ADDRESS i __ x_19979 x_19978990  OPACCS (x_ 19985, x_19984, x_19983, x_19982, x_19981) >991 h_OPACCS x_ 19985 x_19984 x_19983 x_19982 x_19981992  OP1 (x_ 19988, x_19987, x_19986) > h_OP1 x_19988 x_19987 x_19986993  OP2 (x_ 19992, x_19991, x_19990, x_19989) >994 h_OP2 x_ 19992 x_19991 x_19990 x_19989985  COMMENT x_20143 > h_COMMENT x_20143 986  MOVE x_20144 > h_MOVE x_20144 987  POP x_20145 > h_POP x_20145 988  PUSH x_20146 > h_PUSH x_20146 989  ADDRESS (i, x_20148, x_20147) > h_ADDRESS i __ x_20148 x_20147 990  OPACCS (x_20154, x_20153, x_20152, x_20151, x_20150) > 991 h_OPACCS x_20154 x_20153 x_20152 x_20151 x_20150 992  OP1 (x_20157, x_20156, x_20155) > h_OP1 x_20157 x_20156 x_20155 993  OP2 (x_20161, x_20160, x_20159, x_20158) > 994 h_OP2 x_20161 x_20160 x_20159 x_20158 995 995  CLEAR_CARRY > h_CLEAR_CARRY 996 996  SET_CARRY > h_SET_CARRY 997  LOAD (x_ 19995, x_19994, x_19993) > h_LOAD x_19995 x_19994 x_19993998  STORE (x_ 19998, x_19997, x_19996) > h_STORE x_19998 x_19997 x_19996999  Extension_seq x_ 19999 > h_extension_seq x_19999997  LOAD (x_20164, x_20163, x_20162) > h_LOAD x_20164 x_20163 x_20162 998  STORE (x_20167, x_20166, x_20165) > h_STORE x_20167 x_20166 x_20165 999  Extension_seq x_20168 > h_extension_seq x_20168 1000 1000 1001 1001 (** val joint_seq_rect_Type1 : … … 1007 1007 'a1) > (__ > 'a1) > joint_seq > 'a1 **) 1008 1008 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 1009  COMMENT x_20 014 > h_COMMENT x_200141010  MOVE x_20 015 > h_MOVE x_200151011  POP x_20 016 > h_POP x_200161012  PUSH x_20 017 > h_PUSH x_200171013  ADDRESS (i, x_20 019, x_20018) > h_ADDRESS i __ x_20019 x_200181014  OPACCS (x_20 025, x_20024, x_20023, x_20022, x_20021) >1015 h_OPACCS x_20 025 x_20024 x_20023 x_20022 x_200211016  OP1 (x_20 028, x_20027, x_20026) > h_OP1 x_20028 x_20027 x_200261017  OP2 (x_20 032, x_20031, x_20030, x_20029) >1018 h_OP2 x_20 032 x_20031 x_20030 x_200291009  COMMENT x_20183 > h_COMMENT x_20183 1010  MOVE x_20184 > h_MOVE x_20184 1011  POP x_20185 > h_POP x_20185 1012  PUSH x_20186 > h_PUSH x_20186 1013  ADDRESS (i, x_20188, x_20187) > h_ADDRESS i __ x_20188 x_20187 1014  OPACCS (x_20194, x_20193, x_20192, x_20191, x_20190) > 1015 h_OPACCS x_20194 x_20193 x_20192 x_20191 x_20190 1016  OP1 (x_20197, x_20196, x_20195) > h_OP1 x_20197 x_20196 x_20195 1017  OP2 (x_20201, x_20200, x_20199, x_20198) > 1018 h_OP2 x_20201 x_20200 x_20199 x_20198 1019 1019  CLEAR_CARRY > h_CLEAR_CARRY 1020 1020  SET_CARRY > h_SET_CARRY 1021  LOAD (x_20 035, x_20034, x_20033) > h_LOAD x_20035 x_20034 x_200331022  STORE (x_20 038, x_20037, x_20036) > h_STORE x_20038 x_20037 x_200361023  Extension_seq x_20 039 > h_extension_seq x_200391021  LOAD (x_20204, x_20203, x_20202) > h_LOAD x_20204 x_20203 x_20202 1022  STORE (x_20207, x_20206, x_20205) > h_STORE x_20207 x_20206 x_20205 1023  Extension_seq x_20208 > h_extension_seq x_20208 1024 1024 1025 1025 (** val joint_seq_rect_Type0 : … … 1031 1031 'a1) > (__ > 'a1) > joint_seq > 'a1 **) 1032 1032 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 1033  COMMENT x_20 054 > h_COMMENT x_200541034  MOVE x_20 055 > h_MOVE x_200551035  POP x_20 056 > h_POP x_200561036  PUSH x_20 057 > h_PUSH x_200571037  ADDRESS (i, x_20 059, x_20058) > h_ADDRESS i __ x_20059 x_200581038  OPACCS (x_20 065, x_20064, x_20063, x_20062, x_20061) >1039 h_OPACCS x_20 065 x_20064 x_20063 x_20062 x_200611040  OP1 (x_20 068, x_20067, x_20066) > h_OP1 x_20068 x_20067 x_200661041  OP2 (x_20 072, x_20071, x_20070, x_20069) >1042 h_OP2 x_20 072 x_20071 x_20070 x_200691033  COMMENT x_20223 > h_COMMENT x_20223 1034  MOVE x_20224 > h_MOVE x_20224 1035  POP x_20225 > h_POP x_20225 1036  PUSH x_20226 > h_PUSH x_20226 1037  ADDRESS (i, x_20228, x_20227) > h_ADDRESS i __ x_20228 x_20227 1038  OPACCS (x_20234, x_20233, x_20232, x_20231, x_20230) > 1039 h_OPACCS x_20234 x_20233 x_20232 x_20231 x_20230 1040  OP1 (x_20237, x_20236, x_20235) > h_OP1 x_20237 x_20236 x_20235 1041  OP2 (x_20241, x_20240, x_20239, x_20238) > 1042 h_OP2 x_20241 x_20240 x_20239 x_20238 1043 1043  CLEAR_CARRY > h_CLEAR_CARRY 1044 1044  SET_CARRY > h_SET_CARRY 1045  LOAD (x_20 075, x_20074, x_20073) > h_LOAD x_20075 x_20074 x_200731046  STORE (x_20 078, x_20077, x_20076) > h_STORE x_20078 x_20077 x_200761047  Extension_seq x_20 079 > h_extension_seq x_200791045  LOAD (x_20244, x_20243, x_20242) > h_LOAD x_20244 x_20243 x_20242 1046  STORE (x_20247, x_20246, x_20245) > h_STORE x_20247 x_20246 x_20245 1047  Extension_seq x_20248 > h_extension_seq x_20248 1048 1048 1049 1049 (** val joint_seq_inv_rect_Type4 : … … 1236 1236 > (__ > Graphs.label > 'a1) > (joint_seq > 'a1) > joint_step > 'a1 **) 1237 1237 let rec joint_step_rect_Type4 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function 1238  COST_LABEL x_20 346 > h_COST_LABEL x_203461239  CALL (x_20 349, x_20348, x_20347) > h_CALL x_20349 x_20348 x_203471240  COND (x_20 351, x_20350) > h_COND x_20351 x_203501241  Step_seq x_20 352 > h_step_seq x_203521238  COST_LABEL x_20515 > h_COST_LABEL x_20515 1239  CALL (x_20518, x_20517, x_20516) > h_CALL x_20518 x_20517 x_20516 1240  COND (x_20520, x_20519) > h_COND x_20520 x_20519 1241  Step_seq x_20521 > h_step_seq x_20521 1242 1242 1243 1243 (** val joint_step_rect_Type5 : … … 1246 1246 > (__ > Graphs.label > 'a1) > (joint_seq > 'a1) > joint_step > 'a1 **) 1247 1247 let rec joint_step_rect_Type5 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function 1248  COST_LABEL x_20 358 > h_COST_LABEL x_203581249  CALL (x_20 361, x_20360, x_20359) > h_CALL x_20361 x_20360 x_203591250  COND (x_20 363, x_20362) > h_COND x_20363 x_203621251  Step_seq x_20 364 > h_step_seq x_203641248  COST_LABEL x_20527 > h_COST_LABEL x_20527 1249  CALL (x_20530, x_20529, x_20528) > h_CALL x_20530 x_20529 x_20528 1250  COND (x_20532, x_20531) > h_COND x_20532 x_20531 1251  Step_seq x_20533 > h_step_seq x_20533 1252 1252 1253 1253 (** val joint_step_rect_Type3 : … … 1256 1256 > (__ > Graphs.label > 'a1) > (joint_seq > 'a1) > joint_step > 'a1 **) 1257 1257 let rec joint_step_rect_Type3 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function 1258  COST_LABEL x_20 370 > h_COST_LABEL x_203701259  CALL (x_20 373, x_20372, x_20371) > h_CALL x_20373 x_20372 x_203711260  COND (x_20 375, x_20374) > h_COND x_20375 x_203741261  Step_seq x_20 376 > h_step_seq x_203761258  COST_LABEL x_20539 > h_COST_LABEL x_20539 1259  CALL (x_20542, x_20541, x_20540) > h_CALL x_20542 x_20541 x_20540 1260  COND (x_20544, x_20543) > h_COND x_20544 x_20543 1261  Step_seq x_20545 > h_step_seq x_20545 1262 1262 1263 1263 (** val joint_step_rect_Type2 : … … 1266 1266 > (__ > Graphs.label > 'a1) > (joint_seq > 'a1) > joint_step > 'a1 **) 1267 1267 let rec joint_step_rect_Type2 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function 1268  COST_LABEL x_20 382 > h_COST_LABEL x_203821269  CALL (x_20 385, x_20384, x_20383) > h_CALL x_20385 x_20384 x_203831270  COND (x_20 387, x_20386) > h_COND x_20387 x_203861271  Step_seq x_20 388 > h_step_seq x_203881268  COST_LABEL x_20551 > h_COST_LABEL x_20551 1269  CALL (x_20554, x_20553, x_20552) > h_CALL x_20554 x_20553 x_20552 1270  COND (x_20556, x_20555) > h_COND x_20556 x_20555 1271  Step_seq x_20557 > h_step_seq x_20557 1272 1272 1273 1273 (** val joint_step_rect_Type1 : … … 1276 1276 > (__ > Graphs.label > 'a1) > (joint_seq > 'a1) > joint_step > 'a1 **) 1277 1277 let rec joint_step_rect_Type1 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function 1278  COST_LABEL x_20 394 > h_COST_LABEL x_203941279  CALL (x_20 397, x_20396, x_20395) > h_CALL x_20397 x_20396 x_203951280  COND (x_20 399, x_20398) > h_COND x_20399 x_203981281  Step_seq x_20 400 > h_step_seq x_204001278  COST_LABEL x_20563 > h_COST_LABEL x_20563 1279  CALL (x_20566, x_20565, x_20564) > h_CALL x_20566 x_20565 x_20564 1280  COND (x_20568, x_20567) > h_COND x_20568 x_20567 1281  Step_seq x_20569 > h_step_seq x_20569 1282 1282 1283 1283 (** val joint_step_rect_Type0 : … … 1286 1286 > (__ > Graphs.label > 'a1) > (joint_seq > 'a1) > joint_step > 'a1 **) 1287 1287 let rec joint_step_rect_Type0 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function 1288  COST_LABEL x_20 406 > h_COST_LABEL x_204061289  CALL (x_20 409, x_20408, x_20407) > h_CALL x_20409 x_20408 x_204071290  COND (x_20 411, x_20410) > h_COND x_20411 x_204101291  Step_seq x_20 412 > h_step_seq x_204121288  COST_LABEL x_20575 > h_COST_LABEL x_20575 1289  CALL (x_20578, x_20577, x_20576) > h_CALL x_20578 x_20577 x_20576 1290  COND (x_20580, x_20579) > h_COND x_20580 x_20579 1291  Step_seq x_20581 > h_step_seq x_20581 1292 1292 1293 1293 (** val joint_step_inv_rect_Type4 : … … 1464 1464 (uns_params > __ > (__ > Graphs.label Types.option) > Bool.bool > 1465 1465 'a1) > stmt_params > 'a1 **) 1466 let rec stmt_params_rect_Type4 h_mk_stmt_params x_20 491=1466 let rec stmt_params_rect_Type4 h_mk_stmt_params x_20660 = 1467 1467 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = 1468 has_fcond0 } = x_20 4911468 has_fcond0 } = x_20660 1469 1469 in 1470 1470 h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0 … … 1473 1473 (uns_params > __ > (__ > Graphs.label Types.option) > Bool.bool > 1474 1474 'a1) > stmt_params > 'a1 **) 1475 let rec stmt_params_rect_Type5 h_mk_stmt_params x_20 493=1475 let rec stmt_params_rect_Type5 h_mk_stmt_params x_20662 = 1476 1476 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = 1477 has_fcond0 } = x_20 4931477 has_fcond0 } = x_20662 1478 1478 in 1479 1479 h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0 … … 1482 1482 (uns_params > __ > (__ > Graphs.label Types.option) > Bool.bool > 1483 1483 'a1) > stmt_params > 'a1 **) 1484 let rec stmt_params_rect_Type3 h_mk_stmt_params x_20 495=1484 let rec stmt_params_rect_Type3 h_mk_stmt_params x_20664 = 1485 1485 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = 1486 has_fcond0 } = x_20 4951486 has_fcond0 } = x_20664 1487 1487 in 1488 1488 h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0 … … 1491 1491 (uns_params > __ > (__ > Graphs.label Types.option) > Bool.bool > 1492 1492 'a1) > stmt_params > 'a1 **) 1493 let rec stmt_params_rect_Type2 h_mk_stmt_params x_20 497=1493 let rec stmt_params_rect_Type2 h_mk_stmt_params x_20666 = 1494 1494 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = 1495 has_fcond0 } = x_20 4971495 has_fcond0 } = x_20666 1496 1496 in 1497 1497 h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0 … … 1500 1500 (uns_params > __ > (__ > Graphs.label Types.option) > Bool.bool > 1501 1501 'a1) > stmt_params > 'a1 **) 1502 let rec stmt_params_rect_Type1 h_mk_stmt_params x_20 499=1502 let rec stmt_params_rect_Type1 h_mk_stmt_params x_20668 = 1503 1503 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = 1504 has_fcond0 } = x_20 4991504 has_fcond0 } = x_20668 1505 1505 in 1506 1506 h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0 … … 1509 1509 (uns_params > __ > (__ > Graphs.label Types.option) > Bool.bool > 1510 1510 'a1) > stmt_params > 'a1 **) 1511 let rec stmt_params_rect_Type0 h_mk_stmt_params x_20 501=1511 let rec stmt_params_rect_Type0 h_mk_stmt_params x_20670 = 1512 1512 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = 1513 has_fcond0 } = x_20 5011513 has_fcond0 } = x_20670 1514 1514 in 1515 1515 h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0 … … 1578 1578 (__, __) Types.prod) Types.sum > __ > 'a1) > joint_fin_step > 'a1 **) 1579 1579 let rec joint_fin_step_rect_Type4 p h_GOTO h_RETURN h_TAILCALL = function 1580  GOTO x_20 525 > h_GOTO x_205251580  GOTO x_20694 > h_GOTO x_20694 1581 1581  RETURN > h_RETURN 1582  TAILCALL (x_20 527, x_20526) > h_TAILCALL __ x_20527 x_205261582  TAILCALL (x_20696, x_20695) > h_TAILCALL __ x_20696 x_20695 1583 1583 1584 1584 (** val joint_fin_step_rect_Type5 : … … 1586 1586 (__, __) Types.prod) Types.sum > __ > 'a1) > joint_fin_step > 'a1 **) 1587 1587 let rec joint_fin_step_rect_Type5 p h_GOTO h_RETURN h_TAILCALL = function 1588  GOTO x_20 533 > h_GOTO x_205331588  GOTO x_20702 > h_GOTO x_20702 1589 1589  RETURN > h_RETURN 1590  TAILCALL (x_20 535, x_20534) > h_TAILCALL __ x_20535 x_205341590  TAILCALL (x_20704, x_20703) > h_TAILCALL __ x_20704 x_20703 1591 1591 1592 1592 (** val joint_fin_step_rect_Type3 : … … 1594 1594 (__, __) Types.prod) Types.sum > __ > 'a1) > joint_fin_step > 'a1 **) 1595 1595 let rec joint_fin_step_rect_Type3 p h_GOTO h_RETURN h_TAILCALL = function 1596  GOTO x_20 541 > h_GOTO x_205411596  GOTO x_20710 > h_GOTO x_20710 1597 1597  RETURN > h_RETURN 1598  TAILCALL (x_20 543, x_20542) > h_TAILCALL __ x_20543 x_205421598  TAILCALL (x_20712, x_20711) > h_TAILCALL __ x_20712 x_20711 1599 1599 1600 1600 (** val joint_fin_step_rect_Type2 : … … 1602 1602 (__, __) Types.prod) Types.sum > __ > 'a1) > joint_fin_step > 'a1 **) 1603 1603 let rec joint_fin_step_rect_Type2 p h_GOTO h_RETURN h_TAILCALL = function 1604  GOTO x_20 549 > h_GOTO x_205491604  GOTO x_20718 > h_GOTO x_20718 1605 1605  RETURN > h_RETURN 1606  TAILCALL (x_20 551, x_20550) > h_TAILCALL __ x_20551 x_205501606  TAILCALL (x_20720, x_20719) > h_TAILCALL __ x_20720 x_20719 1607 1607 1608 1608 (** val joint_fin_step_rect_Type1 : … … 1610 1610 (__, __) Types.prod) Types.sum > __ > 'a1) > joint_fin_step > 'a1 **) 1611 1611 let rec joint_fin_step_rect_Type1 p h_GOTO h_RETURN h_TAILCALL = function 1612  GOTO x_20 557 > h_GOTO x_205571612  GOTO x_20726 > h_GOTO x_20726 1613 1613  RETURN > h_RETURN 1614  TAILCALL (x_20 559, x_20558) > h_TAILCALL __ x_20559 x_205581614  TAILCALL (x_20728, x_20727) > h_TAILCALL __ x_20728 x_20727 1615 1615 1616 1616 (** val joint_fin_step_rect_Type0 : … … 1618 1618 (__, __) Types.prod) Types.sum > __ > 'a1) > joint_fin_step > 'a1 **) 1619 1619 let rec joint_fin_step_rect_Type0 p h_GOTO h_RETURN h_TAILCALL = function 1620  GOTO x_20 565 > h_GOTO x_205651620  GOTO x_20734 > h_GOTO x_20734 1621 1621  RETURN > h_RETURN 1622  TAILCALL (x_20 567, x_20566) > h_TAILCALL __ x_20567 x_205661622  TAILCALL (x_20736, x_20735) > h_TAILCALL __ x_20736 x_20735 1623 1623 1624 1624 (** val joint_fin_step_inv_rect_Type4 : … … 1692 1692 'a1) > joint_statement > 'a1 **) 1693 1693 let rec joint_statement_rect_Type4 p globals h_sequential h_final h_FCOND = function 1694  Sequential (x_20 633, x_20632) > h_sequential x_20633 x_206321695  Final x_20 634 > h_final x_206341696  FCOND (x_20 637, x_20636, x_20635) > h_FCOND __ x_20637 x_20636 x_206351694  Sequential (x_20802, x_20801) > h_sequential x_20802 x_20801 1695  Final x_20803 > h_final x_20803 1696  FCOND (x_20806, x_20805, x_20804) > h_FCOND __ x_20806 x_20805 x_20804 1697 1697 1698 1698 (** val joint_statement_rect_Type5 : … … 1701 1701 'a1) > joint_statement > 'a1 **) 1702 1702 let rec joint_statement_rect_Type5 p globals h_sequential h_final h_FCOND = function 1703  Sequential (x_20 644, x_20643) > h_sequential x_20644 x_206431704  Final x_20 645 > h_final x_206451705  FCOND (x_20 648, x_20647, x_20646) > h_FCOND __ x_20648 x_20647 x_206461703  Sequential (x_20813, x_20812) > h_sequential x_20813 x_20812 1704  Final x_20814 > h_final x_20814 1705  FCOND (x_20817, x_20816, x_20815) > h_FCOND __ x_20817 x_20816 x_20815 1706 1706 1707 1707 (** val joint_statement_rect_Type3 : … … 1710 1710 'a1) > joint_statement > 'a1 **) 1711 1711 let rec joint_statement_rect_Type3 p globals h_sequential h_final h_FCOND = function 1712  Sequential (x_20 655, x_20654) > h_sequential x_20655 x_206541713  Final x_20 656 > h_final x_206561714  FCOND (x_20 659, x_20658, x_20657) > h_FCOND __ x_20659 x_20658 x_206571712  Sequential (x_20824, x_20823) > h_sequential x_20824 x_20823 1713  Final x_20825 > h_final x_20825 1714  FCOND (x_20828, x_20827, x_20826) > h_FCOND __ x_20828 x_20827 x_20826 1715 1715 1716 1716 (** val joint_statement_rect_Type2 : … … 1719 1719 'a1) > joint_statement > 'a1 **) 1720 1720 let rec joint_statement_rect_Type2 p globals h_sequential h_final h_FCOND = function 1721  Sequential (x_20 666, x_20665) > h_sequential x_20666 x_206651722  Final x_20 667 > h_final x_206671723  FCOND (x_20 670, x_20669, x_20668) > h_FCOND __ x_20670 x_20669 x_206681721  Sequential (x_20835, x_20834) > h_sequential x_20835 x_20834 1722  Final x_20836 > h_final x_20836 1723  FCOND (x_20839, x_20838, x_20837) > h_FCOND __ x_20839 x_20838 x_20837 1724 1724 1725 1725 (** val joint_statement_rect_Type1 : … … 1728 1728 'a1) > joint_statement > 'a1 **) 1729 1729 let rec joint_statement_rect_Type1 p globals h_sequential h_final h_FCOND = function 1730  Sequential (x_20 677, x_20676) > h_sequential x_20677 x_206761731  Final x_20 678 > h_final x_206781732  FCOND (x_20 681, x_20680, x_20679) > h_FCOND __ x_20681 x_20680 x_206791730  Sequential (x_20846, x_20845) > h_sequential x_20846 x_20845 1731  Final x_20847 > h_final x_20847 1732  FCOND (x_20850, x_20849, x_20848) > h_FCOND __ x_20850 x_20849 x_20848 1733 1733 1734 1734 (** val joint_statement_rect_Type0 : … … 1737 1737 'a1) > joint_statement > 'a1 **) 1738 1738 let rec joint_statement_rect_Type0 p globals h_sequential h_final h_FCOND = function 1739  Sequential (x_20 688, x_20687) > h_sequential x_20688 x_206871740  Final x_20 689 > h_final x_206891741  FCOND (x_20 692, x_20691, x_20690) > h_FCOND __ x_20692 x_20691 x_206901739  Sequential (x_20857, x_20856) > h_sequential x_20857 x_20856 1740  Final x_20858 > h_final x_20858 1741  FCOND (x_20861, x_20860, x_20859) > h_FCOND __ x_20861 x_20860 x_20859 1742 1742 1743 1743 (** val joint_statement_inv_rect_Type4 : … … 1838 1838 Graphs.label > __ Types.option) > (__ > __ > __) > 'a1) > params > 1839 1839 'a1 **) 1840 let rec params_rect_Type4 h_mk_params x_20 765=1840 let rec params_rect_Type4 h_mk_params x_20934 = 1841 1841 let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label = 1842 point_of_label0; point_of_succ = point_of_succ0 } = x_20 7651842 point_of_label0; point_of_succ = point_of_succ0 } = x_20934 1843 1843 in 1844 1844 h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0 … … 1849 1849 Graphs.label > __ Types.option) > (__ > __ > __) > 'a1) > params > 1850 1850 'a1 **) 1851 let rec params_rect_Type5 h_mk_params x_20 767=1851 let rec params_rect_Type5 h_mk_params x_20936 = 1852 1852 let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label = 1853 point_of_label0; point_of_succ = point_of_succ0 } = x_20 7671853 point_of_label0; point_of_succ = point_of_succ0 } = x_20936 1854 1854 in 1855 1855 h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0 … … 1860 1860 Graphs.label > __ Types.option) > (__ > __ > __) > 'a1) > params > 1861 1861 'a1 **) 1862 let rec params_rect_Type3 h_mk_params x_20 769=1862 let rec params_rect_Type3 h_mk_params x_20938 = 1863 1863 let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label = 1864 point_of_label0; point_of_succ = point_of_succ0 } = x_20 7691864 point_of_label0; point_of_succ = point_of_succ0 } = x_20938 1865 1865 in 1866 1866 h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0 … … 1871 1871 Graphs.label > __ Types.option) > (__ > __ > __) > 'a1) > params > 1872 1872 'a1 **) 1873 let rec params_rect_Type2 h_mk_params x_20 771=1873 let rec params_rect_Type2 h_mk_params x_20940 = 1874 1874 let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label = 1875 point_of_label0; point_of_succ = point_of_succ0 } = x_20 7711875 point_of_label0; point_of_succ = point_of_succ0 } = x_20940 1876 1876 in 1877 1877 h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0 … … 1882 1882 Graphs.label > __ Types.option) > (__ > __ > __) > 'a1) > params > 1883 1883 'a1 **) 1884 let rec params_rect_Type1 h_mk_params x_20 773=1884 let rec params_rect_Type1 h_mk_params x_20942 = 1885 1885 let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label = 1886 point_of_label0; point_of_succ = point_of_succ0 } = x_20 7731886 point_of_label0; point_of_succ = point_of_succ0 } = x_20942 1887 1887 in 1888 1888 h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0 … … 1893 1893 Graphs.label > __ Types.option) > (__ > __ > __) > 'a1) > params > 1894 1894 'a1 **) 1895 let rec params_rect_Type0 h_mk_params x_20 775=1895 let rec params_rect_Type0 h_mk_params x_20944 = 1896 1896 let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label = 1897 point_of_label0; point_of_succ = point_of_succ0 } = x_20 7751897 point_of_label0; point_of_succ = point_of_succ0 } = x_20944 1898 1898 in 1899 1899 h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0 … … 2030 2030 2031 2031 (** val lin_params_rect_Type4 : (uns_params > 'a1) > lin_params > 'a1 **) 2032 let rec lin_params_rect_Type4 h_mk_lin_params x_20 798=2033 let l_u_pars = x_20 798in h_mk_lin_params l_u_pars2032 let rec lin_params_rect_Type4 h_mk_lin_params x_20967 = 2033 let l_u_pars = x_20967 in h_mk_lin_params l_u_pars 2034 2034 2035 2035 (** val lin_params_rect_Type5 : (uns_params > 'a1) > lin_params > 'a1 **) 2036 let rec lin_params_rect_Type5 h_mk_lin_params x_20 800=2037 let l_u_pars = x_20 800in h_mk_lin_params l_u_pars2036 let rec lin_params_rect_Type5 h_mk_lin_params x_20969 = 2037 let l_u_pars = x_20969 in h_mk_lin_params l_u_pars 2038 2038 2039 2039 (** val lin_params_rect_Type3 : (uns_params > 'a1) > lin_params > 'a1 **) 2040 let rec lin_params_rect_Type3 h_mk_lin_params x_20 802=2041 let l_u_pars = x_20 802in h_mk_lin_params l_u_pars2040 let rec lin_params_rect_Type3 h_mk_lin_params x_20971 = 2041 let l_u_pars = x_20971 in h_mk_lin_params l_u_pars 2042 2042 2043 2043 (** val lin_params_rect_Type2 : (uns_params > 'a1) > lin_params > 'a1 **) 2044 let rec lin_params_rect_Type2 h_mk_lin_params x_20 804=2045 let l_u_pars = x_20 804in h_mk_lin_params l_u_pars2044 let rec lin_params_rect_Type2 h_mk_lin_params x_20973 = 2045 let l_u_pars = x_20973 in h_mk_lin_params l_u_pars 2046 2046 2047 2047 (** val lin_params_rect_Type1 : (uns_params > 'a1) > lin_params > 'a1 **) 2048 let rec lin_params_rect_Type1 h_mk_lin_params x_20 806=2049 let l_u_pars = x_20 806in h_mk_lin_params l_u_pars2048 let rec lin_params_rect_Type1 h_mk_lin_params x_20975 = 2049 let l_u_pars = x_20975 in h_mk_lin_params l_u_pars 2050 2050 2051 2051 (** val lin_params_rect_Type0 : (uns_params > 'a1) > lin_params > 'a1 **) 2052 let rec lin_params_rect_Type0 h_mk_lin_params x_20 808=2053 let l_u_pars = x_20 808in h_mk_lin_params l_u_pars2052 let rec lin_params_rect_Type0 h_mk_lin_params x_20977 = 2053 let l_u_pars = x_20977 in h_mk_lin_params l_u_pars 2054 2054 2055 2055 (** val l_u_pars : lin_params > uns_params **) … … 2125 2125 (** val graph_params_rect_Type4 : 2126 2126 (uns_params > 'a1) > graph_params > 'a1 **) 2127 let rec graph_params_rect_Type4 h_mk_graph_params x_20 824=2128 let g_u_pars = x_20 824in h_mk_graph_params g_u_pars2127 let rec graph_params_rect_Type4 h_mk_graph_params x_20993 = 2128 let g_u_pars = x_20993 in h_mk_graph_params g_u_pars 2129 2129 2130 2130 (** val graph_params_rect_Type5 : 2131 2131 (uns_params > 'a1) > graph_params > 'a1 **) 2132 let rec graph_params_rect_Type5 h_mk_graph_params x_20 826=2133 let g_u_pars = x_20 826in h_mk_graph_params g_u_pars2132 let rec graph_params_rect_Type5 h_mk_graph_params x_20995 = 2133 let g_u_pars = x_20995 in h_mk_graph_params g_u_pars 2134 2134 2135 2135 (** val graph_params_rect_Type3 : 2136 2136 (uns_params > 'a1) > graph_params > 'a1 **) 2137 let rec graph_params_rect_Type3 h_mk_graph_params x_20 828=2138 let g_u_pars = x_20 828in h_mk_graph_params g_u_pars2137 let rec graph_params_rect_Type3 h_mk_graph_params x_20997 = 2138 let g_u_pars = x_20997 in h_mk_graph_params g_u_pars 2139 2139 2140 2140 (** val graph_params_rect_Type2 : 2141 2141 (uns_params > 'a1) > graph_params > 'a1 **) 2142 let rec graph_params_rect_Type2 h_mk_graph_params x_20 830=2143 let g_u_pars = x_20 830in h_mk_graph_params g_u_pars2142 let rec graph_params_rect_Type2 h_mk_graph_params x_20999 = 2143 let g_u_pars = x_20999 in h_mk_graph_params g_u_pars 2144 2144 2145 2145 (** val graph_params_rect_Type1 : 2146 2146 (uns_params > 'a1) > graph_params > 'a1 **) 2147 let rec graph_params_rect_Type1 h_mk_graph_params x_2 0832=2148 let g_u_pars = x_2 0832in h_mk_graph_params g_u_pars2147 let rec graph_params_rect_Type1 h_mk_graph_params x_21001 = 2148 let g_u_pars = x_21001 in h_mk_graph_params g_u_pars 2149 2149 2150 2150 (** val graph_params_rect_Type0 : 2151 2151 (uns_params > 'a1) > graph_params > 'a1 **) 2152 let rec graph_params_rect_Type0 h_mk_graph_params x_2 0834=2153 let g_u_pars = x_2 0834in h_mk_graph_params g_u_pars2152 let rec graph_params_rect_Type0 h_mk_graph_params x_21003 = 2153 let g_u_pars = x_21003 in h_mk_graph_params g_u_pars 2154 2154 2155 2155 (** val g_u_pars : graph_params > uns_params **) … … 2221 2221 Identifiers.universe > __ > __ > Nat.nat > Nat.nat > __ > __ > 2222 2222 'a1) > joint_internal_function > 'a1 **) 2223 let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_2 0850=2223 let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_21019 = 2224 2224 let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse = 2225 2225 joint_if_runiverse0; joint_if_result = joint_if_result0; … … 2227 2227 joint_if_stacksize0; joint_if_local_stacksize = 2228 2228 joint_if_local_stacksize0; joint_if_code = joint_if_code0; 2229 joint_if_entry = joint_if_entry0 } = x_2 08502229 joint_if_entry = joint_if_entry0 } = x_21019 2230 2230 in 2231 2231 h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0 … … 2237 2237 Identifiers.universe > __ > __ > Nat.nat > Nat.nat > __ > __ > 2238 2238 'a1) > joint_internal_function > 'a1 **) 2239 let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_2 0852=2239 let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_21021 = 2240 2240 let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse = 2241 2241 joint_if_runiverse0; joint_if_result = joint_if_result0; … … 2243 2243 joint_if_stacksize0; joint_if_local_stacksize = 2244 2244 joint_if_local_stacksize0; joint_if_code = joint_if_code0; 2245 joint_if_entry = joint_if_entry0 } = x_2 08522245 joint_if_entry = joint_if_entry0 } = x_21021 2246 2246 in 2247 2247 h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0 … … 2253 2253 Identifiers.universe > __ > __ > Nat.nat > Nat.nat > __ > __ > 2254 2254 'a1) > joint_internal_function > 'a1 **) 2255 let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_2 0854=2255 let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_21023 = 2256 2256 let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse = 2257 2257 joint_if_runiverse0; joint_if_result = joint_if_result0; … … 2259 2259 joint_if_stacksize0; joint_if_local_stacksize = 2260 2260 joint_if_local_stacksize0; joint_if_code = joint_if_code0; 2261 joint_if_entry = joint_if_entry0 } = x_2 08542261 joint_if_entry = joint_if_entry0 } = x_21023 2262 2262 in 2263 2263 h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0 … … 2269 2269 Identifiers.universe > __ > __ > Nat.nat > Nat.nat > __ > __ > 2270 2270 'a1) > joint_internal_function > 'a1 **) 2271 let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_2 0856=2271 let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_21025 = 2272 2272 let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse = 2273 2273 joint_if_runiverse0; joint_if_result = joint_if_result0; … … 2275 2275 joint_if_stacksize0; joint_if_local_stacksize = 2276 2276 joint_if_local_stacksize0; joint_if_code = joint_if_code0; 2277 joint_if_entry = joint_if_entry0 } = x_2 08562277 joint_if_entry = joint_if_entry0 } = x_21025 2278 2278 in 2279 2279 h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0 … … 2285 2285 Identifiers.universe > __ > __ > Nat.nat > Nat.nat > __ > __ > 2286 2286 'a1) > joint_internal_function > 'a1 **) 2287 let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_2 0858=2287 let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_21027 = 2288 2288 let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse = 2289 2289 joint_if_runiverse0; joint_if_result = joint_if_result0; … … 2291 2291 joint_if_stacksize0; joint_if_local_stacksize = 2292 2292 joint_if_local_stacksize0; joint_if_code = joint_if_code0; 2293 joint_if_entry = joint_if_entry0 } = x_2 08582293 joint_if_entry = joint_if_entry0 } = x_21027 2294 2294 in 2295 2295 h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0 … … 2301 2301 Identifiers.universe > __ > __ > Nat.nat > Nat.nat > __ > __ > 2302 2302 'a1) > joint_internal_function > 'a1 **) 2303 let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_2 0860=2303 let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_21029 = 2304 2304 let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse = 2305 2305 joint_if_runiverse0; joint_if_result = joint_if_result0; … … 2307 2307 joint_if_stacksize0; joint_if_local_stacksize = 2308 2308 joint_if_local_stacksize0; joint_if_code = joint_if_code0; 2309 joint_if_entry = joint_if_entry0 } = x_2 08602309 joint_if_entry = joint_if_entry0 } = x_21029 2310 2310 in 2311 2311 h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
Note: See TracChangeset
for help on using the changeset viewer.