Changeset 2951 for extracted/joint.ml
 Timestamp:
 Mar 25, 2013, 11:30:01 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/joint.ml
r2873 r2951 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 9830 > h_Reg x_19830113  Imm x_1 9831 > h_Imm x_19831112  Reg x_16908 > h_Reg x_16908 113  Imm x_16909 > h_Imm x_16909 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 9835 > h_Reg x_19835119  Imm x_1 9836 > h_Imm x_19836118  Reg x_16913 > h_Reg x_16913 119  Imm x_16914 > h_Imm x_16914 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 9840 > h_Reg x_19840125  Imm x_1 9841 > h_Imm x_19841124  Reg x_16918 > h_Reg x_16918 125  Imm x_16919 > h_Imm x_16919 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 9845 > h_Reg x_19845131  Imm x_1 9846 > h_Imm x_19846130  Reg x_16923 > h_Reg x_16923 131  Imm x_16924 > h_Imm x_16924 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 9850 > h_Reg x_19850137  Imm x_1 9851 > h_Imm x_19851136  Reg x_16928 > h_Reg x_16928 137  Imm x_16929 > h_Imm x_16929 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 9855 > h_Reg x_19855143  Imm x_1 9856 > h_Imm x_19856142  Reg x_16933 > h_Reg x_16933 143  Imm x_16934 > h_Imm x_16934 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 9891=326 let rec unserialized_params_rect_Type4 h_mk_unserialized_params x_16969 = 327 327 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = 328 x_1 9891328 x_16969 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 9893=337 let rec unserialized_params_rect_Type5 h_mk_unserialized_params x_16971 = 338 338 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = 339 x_1 9893339 x_16971 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 9895=348 let rec unserialized_params_rect_Type3 h_mk_unserialized_params x_16973 = 349 349 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = 350 x_1 9895350 x_16973 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 9897=359 let rec unserialized_params_rect_Type2 h_mk_unserialized_params x_16975 = 360 360 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = 361 x_1 9897361 x_16975 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 9899=370 let rec unserialized_params_rect_Type1 h_mk_unserialized_params x_16977 = 371 371 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = 372 x_1 9899372 x_16977 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 9901=381 let rec unserialized_params_rect_Type0 h_mk_unserialized_params x_16979 = 382 382 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = 383 x_1 9901383 x_16979 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_1 9918=508 let rec get_pseudo_reg_functs_rect_Type4 p h_mk_get_pseudo_reg_functs x_16996 = 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_1 9918514 params_regs0 } = x_16996 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_1 9920=531 let rec get_pseudo_reg_functs_rect_Type5 p h_mk_get_pseudo_reg_functs x_16998 = 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_1 9920537 params_regs0 } = x_16998 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_1 9922=554 let rec get_pseudo_reg_functs_rect_Type3 p h_mk_get_pseudo_reg_functs x_17000 = 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_1 9922560 params_regs0 } = x_17000 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_1 9924=577 let rec get_pseudo_reg_functs_rect_Type2 p h_mk_get_pseudo_reg_functs x_17002 = 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_1 9924583 params_regs0 } = x_17002 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_1 9926=600 let rec get_pseudo_reg_functs_rect_Type1 p h_mk_get_pseudo_reg_functs x_17004 = 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_1 9926606 params_regs0 } = x_17004 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_1 9928=623 let rec get_pseudo_reg_functs_rect_Type0 p h_mk_get_pseudo_reg_functs x_17006 = 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_1 9928629 params_regs0 } = x_17006 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_1 9958=808 let { u_pars = u_pars0; functs = functs0 } = x_1 9958in807 let rec uns_params_rect_Type4 h_mk_uns_params x_17036 = 808 let { u_pars = u_pars0; functs = functs0 } = x_17036 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_1 9960=815 let { u_pars = u_pars0; functs = functs0 } = x_1 9960in814 let rec uns_params_rect_Type5 h_mk_uns_params x_17038 = 815 let { u_pars = u_pars0; functs = functs0 } = x_17038 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_1 9962=822 let { u_pars = u_pars0; functs = functs0 } = x_1 9962in821 let rec uns_params_rect_Type3 h_mk_uns_params x_17040 = 822 let { u_pars = u_pars0; functs = functs0 } = x_17040 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_1 9964=829 let { u_pars = u_pars0; functs = functs0 } = x_1 9964in828 let rec uns_params_rect_Type2 h_mk_uns_params x_17042 = 829 let { u_pars = u_pars0; functs = functs0 } = x_17042 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_1 9966=836 let { u_pars = u_pars0; functs = functs0 } = x_1 9966in835 let rec uns_params_rect_Type1 h_mk_uns_params x_17044 = 836 let { u_pars = u_pars0; functs = functs0 } = x_17044 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_1 9968=843 let { u_pars = u_pars0; functs = functs0 } = x_1 9968in842 let rec uns_params_rect_Type0 h_mk_uns_params x_17046 = 843 let { u_pars = u_pars0; functs = functs0 } = x_17046 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_ 20023 > h_COMMENT x_20023914  MOVE x_ 20024 > h_MOVE x_20024915  POP x_ 20025 > h_POP x_20025916  PUSH x_ 20026 > h_PUSH x_20026917  ADDRESS (i, x_ 20028, x_20027) > h_ADDRESS i __ x_20028 x_20027918  OPACCS (x_ 20034, x_20033, x_20032, x_20031, x_20030) >919 h_OPACCS x_ 20034 x_20033 x_20032 x_20031 x_20030920  OP1 (x_ 20037, x_20036, x_20035) > h_OP1 x_20037 x_20036 x_20035921  OP2 (x_ 20041, x_20040, x_20039, x_20038) >922 h_OP2 x_ 20041 x_20040 x_20039 x_20038913  COMMENT x_17101 > h_COMMENT x_17101 914  MOVE x_17102 > h_MOVE x_17102 915  POP x_17103 > h_POP x_17103 916  PUSH x_17104 > h_PUSH x_17104 917  ADDRESS (i, x_17106, x_17105) > h_ADDRESS i __ x_17106 x_17105 918  OPACCS (x_17112, x_17111, x_17110, x_17109, x_17108) > 919 h_OPACCS x_17112 x_17111 x_17110 x_17109 x_17108 920  OP1 (x_17115, x_17114, x_17113) > h_OP1 x_17115 x_17114 x_17113 921  OP2 (x_17119, x_17118, x_17117, x_17116) > 922 h_OP2 x_17119 x_17118 x_17117 x_17116 923 923  CLEAR_CARRY > h_CLEAR_CARRY 924 924  SET_CARRY > h_SET_CARRY 925  LOAD (x_ 20044, x_20043, x_20042) > h_LOAD x_20044 x_20043 x_20042926  STORE (x_ 20047, x_20046, x_20045) > h_STORE x_20047 x_20046 x_20045927  Extension_seq x_ 20048 > h_extension_seq x_20048925  LOAD (x_17122, x_17121, x_17120) > h_LOAD x_17122 x_17121 x_17120 926  STORE (x_17125, x_17124, x_17123) > h_STORE x_17125 x_17124 x_17123 927  Extension_seq x_17126 > h_extension_seq x_17126 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_ 20063 > h_COMMENT x_20063938  MOVE x_ 20064 > h_MOVE x_20064939  POP x_ 20065 > h_POP x_20065940  PUSH x_ 20066 > h_PUSH x_20066941  ADDRESS (i, x_ 20068, x_20067) > h_ADDRESS i __ x_20068 x_20067942  OPACCS (x_ 20074, x_20073, x_20072, x_20071, x_20070) >943 h_OPACCS x_ 20074 x_20073 x_20072 x_20071 x_20070944  OP1 (x_ 20077, x_20076, x_20075) > h_OP1 x_20077 x_20076 x_20075945  OP2 (x_ 20081, x_20080, x_20079, x_20078) >946 h_OP2 x_ 20081 x_20080 x_20079 x_20078937  COMMENT x_17141 > h_COMMENT x_17141 938  MOVE x_17142 > h_MOVE x_17142 939  POP x_17143 > h_POP x_17143 940  PUSH x_17144 > h_PUSH x_17144 941  ADDRESS (i, x_17146, x_17145) > h_ADDRESS i __ x_17146 x_17145 942  OPACCS (x_17152, x_17151, x_17150, x_17149, x_17148) > 943 h_OPACCS x_17152 x_17151 x_17150 x_17149 x_17148 944  OP1 (x_17155, x_17154, x_17153) > h_OP1 x_17155 x_17154 x_17153 945  OP2 (x_17159, x_17158, x_17157, x_17156) > 946 h_OP2 x_17159 x_17158 x_17157 x_17156 947 947  CLEAR_CARRY > h_CLEAR_CARRY 948 948  SET_CARRY > h_SET_CARRY 949  LOAD (x_ 20084, x_20083, x_20082) > h_LOAD x_20084 x_20083 x_20082950  STORE (x_ 20087, x_20086, x_20085) > h_STORE x_20087 x_20086 x_20085951  Extension_seq x_ 20088 > h_extension_seq x_20088949  LOAD (x_17162, x_17161, x_17160) > h_LOAD x_17162 x_17161 x_17160 950  STORE (x_17165, x_17164, x_17163) > h_STORE x_17165 x_17164 x_17163 951  Extension_seq x_17166 > h_extension_seq x_17166 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_ 20103 > h_COMMENT x_20103962  MOVE x_ 20104 > h_MOVE x_20104963  POP x_ 20105 > h_POP x_20105964  PUSH x_ 20106 > h_PUSH x_20106965  ADDRESS (i, x_ 20108, x_20107) > h_ADDRESS i __ x_20108 x_20107966  OPACCS (x_ 20114, x_20113, x_20112, x_20111, x_20110) >967 h_OPACCS x_ 20114 x_20113 x_20112 x_20111 x_20110968  OP1 (x_ 20117, x_20116, x_20115) > h_OP1 x_20117 x_20116 x_20115969  OP2 (x_ 20121, x_20120, x_20119, x_20118) >970 h_OP2 x_ 20121 x_20120 x_20119 x_20118961  COMMENT x_17181 > h_COMMENT x_17181 962  MOVE x_17182 > h_MOVE x_17182 963  POP x_17183 > h_POP x_17183 964  PUSH x_17184 > h_PUSH x_17184 965  ADDRESS (i, x_17186, x_17185) > h_ADDRESS i __ x_17186 x_17185 966  OPACCS (x_17192, x_17191, x_17190, x_17189, x_17188) > 967 h_OPACCS x_17192 x_17191 x_17190 x_17189 x_17188 968  OP1 (x_17195, x_17194, x_17193) > h_OP1 x_17195 x_17194 x_17193 969  OP2 (x_17199, x_17198, x_17197, x_17196) > 970 h_OP2 x_17199 x_17198 x_17197 x_17196 971 971  CLEAR_CARRY > h_CLEAR_CARRY 972 972  SET_CARRY > h_SET_CARRY 973  LOAD (x_ 20124, x_20123, x_20122) > h_LOAD x_20124 x_20123 x_20122974  STORE (x_ 20127, x_20126, x_20125) > h_STORE x_20127 x_20126 x_20125975  Extension_seq x_ 20128 > h_extension_seq x_20128973  LOAD (x_17202, x_17201, x_17200) > h_LOAD x_17202 x_17201 x_17200 974  STORE (x_17205, x_17204, x_17203) > h_STORE x_17205 x_17204 x_17203 975  Extension_seq x_17206 > h_extension_seq x_17206 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_ 20143 > h_COMMENT x_20143986  MOVE x_ 20144 > h_MOVE x_20144987  POP x_ 20145 > h_POP x_20145988  PUSH x_ 20146 > h_PUSH x_20146989  ADDRESS (i, x_ 20148, x_20147) > h_ADDRESS i __ x_20148 x_20147990  OPACCS (x_ 20154, x_20153, x_20152, x_20151, x_20150) >991 h_OPACCS x_ 20154 x_20153 x_20152 x_20151 x_20150992  OP1 (x_ 20157, x_20156, x_20155) > h_OP1 x_20157 x_20156 x_20155993  OP2 (x_ 20161, x_20160, x_20159, x_20158) >994 h_OP2 x_ 20161 x_20160 x_20159 x_20158985  COMMENT x_17221 > h_COMMENT x_17221 986  MOVE x_17222 > h_MOVE x_17222 987  POP x_17223 > h_POP x_17223 988  PUSH x_17224 > h_PUSH x_17224 989  ADDRESS (i, x_17226, x_17225) > h_ADDRESS i __ x_17226 x_17225 990  OPACCS (x_17232, x_17231, x_17230, x_17229, x_17228) > 991 h_OPACCS x_17232 x_17231 x_17230 x_17229 x_17228 992  OP1 (x_17235, x_17234, x_17233) > h_OP1 x_17235 x_17234 x_17233 993  OP2 (x_17239, x_17238, x_17237, x_17236) > 994 h_OP2 x_17239 x_17238 x_17237 x_17236 995 995  CLEAR_CARRY > h_CLEAR_CARRY 996 996  SET_CARRY > h_SET_CARRY 997  LOAD (x_ 20164, x_20163, x_20162) > h_LOAD x_20164 x_20163 x_20162998  STORE (x_ 20167, x_20166, x_20165) > h_STORE x_20167 x_20166 x_20165999  Extension_seq x_ 20168 > h_extension_seq x_20168997  LOAD (x_17242, x_17241, x_17240) > h_LOAD x_17242 x_17241 x_17240 998  STORE (x_17245, x_17244, x_17243) > h_STORE x_17245 x_17244 x_17243 999  Extension_seq x_17246 > h_extension_seq x_17246 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_ 20183 > h_COMMENT x_201831010  MOVE x_ 20184 > h_MOVE x_201841011  POP x_ 20185 > h_POP x_201851012  PUSH x_ 20186 > h_PUSH x_201861013  ADDRESS (i, x_ 20188, x_20187) > h_ADDRESS i __ x_20188 x_201871014  OPACCS (x_ 20194, x_20193, x_20192, x_20191, x_20190) >1015 h_OPACCS x_ 20194 x_20193 x_20192 x_20191 x_201901016  OP1 (x_ 20197, x_20196, x_20195) > h_OP1 x_20197 x_20196 x_201951017  OP2 (x_ 20201, x_20200, x_20199, x_20198) >1018 h_OP2 x_ 20201 x_20200 x_20199 x_201981009  COMMENT x_17261 > h_COMMENT x_17261 1010  MOVE x_17262 > h_MOVE x_17262 1011  POP x_17263 > h_POP x_17263 1012  PUSH x_17264 > h_PUSH x_17264 1013  ADDRESS (i, x_17266, x_17265) > h_ADDRESS i __ x_17266 x_17265 1014  OPACCS (x_17272, x_17271, x_17270, x_17269, x_17268) > 1015 h_OPACCS x_17272 x_17271 x_17270 x_17269 x_17268 1016  OP1 (x_17275, x_17274, x_17273) > h_OP1 x_17275 x_17274 x_17273 1017  OP2 (x_17279, x_17278, x_17277, x_17276) > 1018 h_OP2 x_17279 x_17278 x_17277 x_17276 1019 1019  CLEAR_CARRY > h_CLEAR_CARRY 1020 1020  SET_CARRY > h_SET_CARRY 1021  LOAD (x_ 20204, x_20203, x_20202) > h_LOAD x_20204 x_20203 x_202021022  STORE (x_ 20207, x_20206, x_20205) > h_STORE x_20207 x_20206 x_202051023  Extension_seq x_ 20208 > h_extension_seq x_202081021  LOAD (x_17282, x_17281, x_17280) > h_LOAD x_17282 x_17281 x_17280 1022  STORE (x_17285, x_17284, x_17283) > h_STORE x_17285 x_17284 x_17283 1023  Extension_seq x_17286 > h_extension_seq x_17286 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_ 20223 > h_COMMENT x_202231034  MOVE x_ 20224 > h_MOVE x_202241035  POP x_ 20225 > h_POP x_202251036  PUSH x_ 20226 > h_PUSH x_202261037  ADDRESS (i, x_ 20228, x_20227) > h_ADDRESS i __ x_20228 x_202271038  OPACCS (x_ 20234, x_20233, x_20232, x_20231, x_20230) >1039 h_OPACCS x_ 20234 x_20233 x_20232 x_20231 x_202301040  OP1 (x_ 20237, x_20236, x_20235) > h_OP1 x_20237 x_20236 x_202351041  OP2 (x_ 20241, x_20240, x_20239, x_20238) >1042 h_OP2 x_ 20241 x_20240 x_20239 x_202381033  COMMENT x_17301 > h_COMMENT x_17301 1034  MOVE x_17302 > h_MOVE x_17302 1035  POP x_17303 > h_POP x_17303 1036  PUSH x_17304 > h_PUSH x_17304 1037  ADDRESS (i, x_17306, x_17305) > h_ADDRESS i __ x_17306 x_17305 1038  OPACCS (x_17312, x_17311, x_17310, x_17309, x_17308) > 1039 h_OPACCS x_17312 x_17311 x_17310 x_17309 x_17308 1040  OP1 (x_17315, x_17314, x_17313) > h_OP1 x_17315 x_17314 x_17313 1041  OP2 (x_17319, x_17318, x_17317, x_17316) > 1042 h_OP2 x_17319 x_17318 x_17317 x_17316 1043 1043  CLEAR_CARRY > h_CLEAR_CARRY 1044 1044  SET_CARRY > h_SET_CARRY 1045  LOAD (x_ 20244, x_20243, x_20242) > h_LOAD x_20244 x_20243 x_202421046  STORE (x_ 20247, x_20246, x_20245) > h_STORE x_20247 x_20246 x_202451047  Extension_seq x_ 20248 > h_extension_seq x_202481045  LOAD (x_17322, x_17321, x_17320) > h_LOAD x_17322 x_17321 x_17320 1046  STORE (x_17325, x_17324, x_17323) > h_STORE x_17325 x_17324 x_17323 1047  Extension_seq x_17326 > h_extension_seq x_17326 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_ 20515 > h_COST_LABEL x_205151239  CALL (x_ 20518, x_20517, x_20516) > h_CALL x_20518 x_20517 x_205161240  COND (x_ 20520, x_20519) > h_COND x_20520 x_205191241  Step_seq x_ 20521 > h_step_seq x_205211238  COST_LABEL x_17593 > h_COST_LABEL x_17593 1239  CALL (x_17596, x_17595, x_17594) > h_CALL x_17596 x_17595 x_17594 1240  COND (x_17598, x_17597) > h_COND x_17598 x_17597 1241  Step_seq x_17599 > h_step_seq x_17599 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_ 20527 > h_COST_LABEL x_205271249  CALL (x_ 20530, x_20529, x_20528) > h_CALL x_20530 x_20529 x_205281250  COND (x_ 20532, x_20531) > h_COND x_20532 x_205311251  Step_seq x_ 20533 > h_step_seq x_205331248  COST_LABEL x_17605 > h_COST_LABEL x_17605 1249  CALL (x_17608, x_17607, x_17606) > h_CALL x_17608 x_17607 x_17606 1250  COND (x_17610, x_17609) > h_COND x_17610 x_17609 1251  Step_seq x_17611 > h_step_seq x_17611 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_ 20539 > h_COST_LABEL x_205391259  CALL (x_ 20542, x_20541, x_20540) > h_CALL x_20542 x_20541 x_205401260  COND (x_ 20544, x_20543) > h_COND x_20544 x_205431261  Step_seq x_ 20545 > h_step_seq x_205451258  COST_LABEL x_17617 > h_COST_LABEL x_17617 1259  CALL (x_17620, x_17619, x_17618) > h_CALL x_17620 x_17619 x_17618 1260  COND (x_17622, x_17621) > h_COND x_17622 x_17621 1261  Step_seq x_17623 > h_step_seq x_17623 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_ 20551 > h_COST_LABEL x_205511269  CALL (x_ 20554, x_20553, x_20552) > h_CALL x_20554 x_20553 x_205521270  COND (x_ 20556, x_20555) > h_COND x_20556 x_205551271  Step_seq x_ 20557 > h_step_seq x_205571268  COST_LABEL x_17629 > h_COST_LABEL x_17629 1269  CALL (x_17632, x_17631, x_17630) > h_CALL x_17632 x_17631 x_17630 1270  COND (x_17634, x_17633) > h_COND x_17634 x_17633 1271  Step_seq x_17635 > h_step_seq x_17635 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_ 20563 > h_COST_LABEL x_205631279  CALL (x_ 20566, x_20565, x_20564) > h_CALL x_20566 x_20565 x_205641280  COND (x_ 20568, x_20567) > h_COND x_20568 x_205671281  Step_seq x_ 20569 > h_step_seq x_205691278  COST_LABEL x_17641 > h_COST_LABEL x_17641 1279  CALL (x_17644, x_17643, x_17642) > h_CALL x_17644 x_17643 x_17642 1280  COND (x_17646, x_17645) > h_COND x_17646 x_17645 1281  Step_seq x_17647 > h_step_seq x_17647 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_ 20575 > h_COST_LABEL x_205751289  CALL (x_ 20578, x_20577, x_20576) > h_CALL x_20578 x_20577 x_205761290  COND (x_ 20580, x_20579) > h_COND x_20580 x_205791291  Step_seq x_ 20581 > h_step_seq x_205811288  COST_LABEL x_17653 > h_COST_LABEL x_17653 1289  CALL (x_17656, x_17655, x_17654) > h_CALL x_17656 x_17655 x_17654 1290  COND (x_17658, x_17657) > h_COND x_17658 x_17657 1291  Step_seq x_17659 > h_step_seq x_17659 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_ 20660=1466 let rec stmt_params_rect_Type4 h_mk_stmt_params x_17738 = 1467 1467 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = 1468 has_fcond0 } = x_ 206601468 has_fcond0 } = x_17738 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_ 20662=1475 let rec stmt_params_rect_Type5 h_mk_stmt_params x_17740 = 1476 1476 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = 1477 has_fcond0 } = x_ 206621477 has_fcond0 } = x_17740 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_ 20664=1484 let rec stmt_params_rect_Type3 h_mk_stmt_params x_17742 = 1485 1485 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = 1486 has_fcond0 } = x_ 206641486 has_fcond0 } = x_17742 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_ 20666=1493 let rec stmt_params_rect_Type2 h_mk_stmt_params x_17744 = 1494 1494 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = 1495 has_fcond0 } = x_ 206661495 has_fcond0 } = x_17744 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_ 20668=1502 let rec stmt_params_rect_Type1 h_mk_stmt_params x_17746 = 1503 1503 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = 1504 has_fcond0 } = x_ 206681504 has_fcond0 } = x_17746 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_ 20670=1511 let rec stmt_params_rect_Type0 h_mk_stmt_params x_17748 = 1512 1512 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = 1513 has_fcond0 } = x_ 206701513 has_fcond0 } = x_17748 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_ 20694 > h_GOTO x_206941580  GOTO x_17772 > h_GOTO x_17772 1581 1581  RETURN > h_RETURN 1582  TAILCALL (x_ 20696, x_20695) > h_TAILCALL __ x_20696 x_206951582  TAILCALL (x_17774, x_17773) > h_TAILCALL __ x_17774 x_17773 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_ 20702 > h_GOTO x_207021588  GOTO x_17780 > h_GOTO x_17780 1589 1589  RETURN > h_RETURN 1590  TAILCALL (x_ 20704, x_20703) > h_TAILCALL __ x_20704 x_207031590  TAILCALL (x_17782, x_17781) > h_TAILCALL __ x_17782 x_17781 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_ 20710 > h_GOTO x_207101596  GOTO x_17788 > h_GOTO x_17788 1597 1597  RETURN > h_RETURN 1598  TAILCALL (x_ 20712, x_20711) > h_TAILCALL __ x_20712 x_207111598  TAILCALL (x_17790, x_17789) > h_TAILCALL __ x_17790 x_17789 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_ 20718 > h_GOTO x_207181604  GOTO x_17796 > h_GOTO x_17796 1605 1605  RETURN > h_RETURN 1606  TAILCALL (x_ 20720, x_20719) > h_TAILCALL __ x_20720 x_207191606  TAILCALL (x_17798, x_17797) > h_TAILCALL __ x_17798 x_17797 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_ 20726 > h_GOTO x_207261612  GOTO x_17804 > h_GOTO x_17804 1613 1613  RETURN > h_RETURN 1614  TAILCALL (x_ 20728, x_20727) > h_TAILCALL __ x_20728 x_207271614  TAILCALL (x_17806, x_17805) > h_TAILCALL __ x_17806 x_17805 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_ 20734 > h_GOTO x_207341620  GOTO x_17812 > h_GOTO x_17812 1621 1621  RETURN > h_RETURN 1622  TAILCALL (x_ 20736, x_20735) > h_TAILCALL __ x_20736 x_207351622  TAILCALL (x_17814, x_17813) > h_TAILCALL __ x_17814 x_17813 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_ 20802, x_20801) > h_sequential x_20802 x_208011695  Final x_ 20803 > h_final x_208031696  FCOND (x_ 20806, x_20805, x_20804) > h_FCOND __ x_20806 x_20805 x_208041694  Sequential (x_17880, x_17879) > h_sequential x_17880 x_17879 1695  Final x_17881 > h_final x_17881 1696  FCOND (x_17884, x_17883, x_17882) > h_FCOND __ x_17884 x_17883 x_17882 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_ 20813, x_20812) > h_sequential x_20813 x_208121704  Final x_ 20814 > h_final x_208141705  FCOND (x_ 20817, x_20816, x_20815) > h_FCOND __ x_20817 x_20816 x_208151703  Sequential (x_17891, x_17890) > h_sequential x_17891 x_17890 1704  Final x_17892 > h_final x_17892 1705  FCOND (x_17895, x_17894, x_17893) > h_FCOND __ x_17895 x_17894 x_17893 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_ 20824, x_20823) > h_sequential x_20824 x_208231713  Final x_ 20825 > h_final x_208251714  FCOND (x_ 20828, x_20827, x_20826) > h_FCOND __ x_20828 x_20827 x_208261712  Sequential (x_17902, x_17901) > h_sequential x_17902 x_17901 1713  Final x_17903 > h_final x_17903 1714  FCOND (x_17906, x_17905, x_17904) > h_FCOND __ x_17906 x_17905 x_17904 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_ 20835, x_20834) > h_sequential x_20835 x_208341722  Final x_ 20836 > h_final x_208361723  FCOND (x_ 20839, x_20838, x_20837) > h_FCOND __ x_20839 x_20838 x_208371721  Sequential (x_17913, x_17912) > h_sequential x_17913 x_17912 1722  Final x_17914 > h_final x_17914 1723  FCOND (x_17917, x_17916, x_17915) > h_FCOND __ x_17917 x_17916 x_17915 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_ 20846, x_20845) > h_sequential x_20846 x_208451731  Final x_ 20847 > h_final x_208471732  FCOND (x_ 20850, x_20849, x_20848) > h_FCOND __ x_20850 x_20849 x_208481730  Sequential (x_17924, x_17923) > h_sequential x_17924 x_17923 1731  Final x_17925 > h_final x_17925 1732  FCOND (x_17928, x_17927, x_17926) > h_FCOND __ x_17928 x_17927 x_17926 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_ 20857, x_20856) > h_sequential x_20857 x_208561740  Final x_ 20858 > h_final x_208581741  FCOND (x_ 20861, x_20860, x_20859) > h_FCOND __ x_20861 x_20860 x_208591739  Sequential (x_17935, x_17934) > h_sequential x_17935 x_17934 1740  Final x_17936 > h_final x_17936 1741  FCOND (x_17939, x_17938, x_17937) > h_FCOND __ x_17939 x_17938 x_17937 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_ 20934=1840 let rec params_rect_Type4 h_mk_params x_18012 = 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_ 209341842 point_of_label0; point_of_succ = point_of_succ0 } = x_18012 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_ 20936=1851 let rec params_rect_Type5 h_mk_params x_18014 = 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_ 209361853 point_of_label0; point_of_succ = point_of_succ0 } = x_18014 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_ 20938=1862 let rec params_rect_Type3 h_mk_params x_18016 = 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_ 209381864 point_of_label0; point_of_succ = point_of_succ0 } = x_18016 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_ 20940=1873 let rec params_rect_Type2 h_mk_params x_18018 = 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_ 209401875 point_of_label0; point_of_succ = point_of_succ0 } = x_18018 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_ 20942=1884 let rec params_rect_Type1 h_mk_params x_18020 = 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_ 209421886 point_of_label0; point_of_succ = point_of_succ0 } = x_18020 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_ 20944=1895 let rec params_rect_Type0 h_mk_params x_18022 = 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_ 209441897 point_of_label0; point_of_succ = point_of_succ0 } = x_18022 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_ 20967=2033 let l_u_pars = x_ 20967in h_mk_lin_params l_u_pars2032 let rec lin_params_rect_Type4 h_mk_lin_params x_18045 = 2033 let l_u_pars = x_18045 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_ 20969=2037 let l_u_pars = x_ 20969in h_mk_lin_params l_u_pars2036 let rec lin_params_rect_Type5 h_mk_lin_params x_18047 = 2037 let l_u_pars = x_18047 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_ 20971=2041 let l_u_pars = x_ 20971in h_mk_lin_params l_u_pars2040 let rec lin_params_rect_Type3 h_mk_lin_params x_18049 = 2041 let l_u_pars = x_18049 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_ 20973=2045 let l_u_pars = x_ 20973in h_mk_lin_params l_u_pars2044 let rec lin_params_rect_Type2 h_mk_lin_params x_18051 = 2045 let l_u_pars = x_18051 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_ 20975=2049 let l_u_pars = x_ 20975in h_mk_lin_params l_u_pars2048 let rec lin_params_rect_Type1 h_mk_lin_params x_18053 = 2049 let l_u_pars = x_18053 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_ 20977=2053 let l_u_pars = x_ 20977in h_mk_lin_params l_u_pars2052 let rec lin_params_rect_Type0 h_mk_lin_params x_18055 = 2053 let l_u_pars = x_18055 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_ 20993=2128 let g_u_pars = x_ 20993in h_mk_graph_params g_u_pars2127 let rec graph_params_rect_Type4 h_mk_graph_params x_18071 = 2128 let g_u_pars = x_18071 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_ 20995=2133 let g_u_pars = x_ 20995in h_mk_graph_params g_u_pars2132 let rec graph_params_rect_Type5 h_mk_graph_params x_18073 = 2133 let g_u_pars = x_18073 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_ 20997=2138 let g_u_pars = x_ 20997in h_mk_graph_params g_u_pars2137 let rec graph_params_rect_Type3 h_mk_graph_params x_18075 = 2138 let g_u_pars = x_18075 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_ 20999=2143 let g_u_pars = x_ 20999in h_mk_graph_params g_u_pars2142 let rec graph_params_rect_Type2 h_mk_graph_params x_18077 = 2143 let g_u_pars = x_18077 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_ 21001=2148 let g_u_pars = x_ 21001in h_mk_graph_params g_u_pars2147 let rec graph_params_rect_Type1 h_mk_graph_params x_18079 = 2148 let g_u_pars = x_18079 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_ 21003=2153 let g_u_pars = x_ 21003in h_mk_graph_params g_u_pars2152 let rec graph_params_rect_Type0 h_mk_graph_params x_18081 = 2153 let g_u_pars = x_18081 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_ 21019=2223 let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_18097 = 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_ 210192229 joint_if_entry = joint_if_entry0 } = x_18097 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_ 21021=2239 let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_18099 = 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_ 210212245 joint_if_entry = joint_if_entry0 } = x_18099 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_ 21023=2255 let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_18101 = 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_ 210232261 joint_if_entry = joint_if_entry0 } = x_18101 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_ 21025=2271 let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_18103 = 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_ 210252277 joint_if_entry = joint_if_entry0 } = x_18103 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_ 21027=2287 let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_18105 = 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_ 210272293 joint_if_entry = joint_if_entry0 } = x_18105 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_ 21029=2303 let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_18107 = 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_ 210292309 joint_if_entry = joint_if_entry0 } = x_18107 2310 2310 in 2311 2311 h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0 … … 2404 2404 (** val good_if_rect_Type4 : 2405 2405 params > AST.ident List.list > joint_internal_function > (__ > __ > 2406 __ > __ > __ > __ >'a1) > 'a1 **)2406 __ > __ > __ > 'a1) > 'a1 **) 2407 2407 let rec good_if_rect_Type4 p globals def h_mk_good_if = 2408 h_mk_good_if __ __ __ __ __ __2408 h_mk_good_if __ __ __ __ __ 2409 2409 2410 2410 (** val good_if_rect_Type5 : 2411 2411 params > AST.ident List.list > joint_internal_function > (__ > __ > 2412 __ > __ > __ > __ >'a1) > 'a1 **)2412 __ > __ > __ > 'a1) > 'a1 **) 2413 2413 let rec good_if_rect_Type5 p globals def h_mk_good_if = 2414 h_mk_good_if __ __ __ __ __ __2414 h_mk_good_if __ __ __ __ __ 2415 2415 2416 2416 (** val good_if_rect_Type3 : 2417 2417 params > AST.ident List.list > joint_internal_function > (__ > __ > 2418 __ > __ > __ > __ >'a1) > 'a1 **)2418 __ > __ > __ > 'a1) > 'a1 **) 2419 2419 let rec good_if_rect_Type3 p globals def h_mk_good_if = 2420 h_mk_good_if __ __ __ __ __ __2420 h_mk_good_if __ __ __ __ __ 2421 2421 2422 2422 (** val good_if_rect_Type2 : 2423 2423 params > AST.ident List.list > joint_internal_function > (__ > __ > 2424 __ > __ > __ > __ >'a1) > 'a1 **)2424 __ > __ > __ > 'a1) > 'a1 **) 2425 2425 let rec good_if_rect_Type2 p globals def h_mk_good_if = 2426 h_mk_good_if __ __ __ __ __ __2426 h_mk_good_if __ __ __ __ __ 2427 2427 2428 2428 (** val good_if_rect_Type1 : 2429 2429 params > AST.ident List.list > joint_internal_function > (__ > __ > 2430 __ > __ > __ > __ >'a1) > 'a1 **)2430 __ > __ > __ > 'a1) > 'a1 **) 2431 2431 let rec good_if_rect_Type1 p globals def h_mk_good_if = 2432 h_mk_good_if __ __ __ __ __ __2432 h_mk_good_if __ __ __ __ __ 2433 2433 2434 2434 (** val good_if_rect_Type0 : 2435 2435 params > AST.ident List.list > joint_internal_function > (__ > __ > 2436 __ > __ > __ > __ >'a1) > 'a1 **)2436 __ > __ > __ > 'a1) > 'a1 **) 2437 2437 let rec good_if_rect_Type0 p globals def h_mk_good_if = 2438 h_mk_good_if __ __ __ __ __ __2438 h_mk_good_if __ __ __ __ __ 2439 2439 2440 2440 (** val good_if_inv_rect_Type4 : 2441 2441 params > AST.ident List.list > joint_internal_function > (__ > __ > 2442 __ > __ > __ > __ > __ >'a1) > 'a1 **)2442 __ > __ > __ > __ > 'a1) > 'a1 **) 2443 2443 let good_if_inv_rect_Type4 x1 x2 x3 h1 = 2444 2444 let hcut = good_if_rect_Type4 x1 x2 x3 h1 in hcut __ … … 2446 2446 (** val good_if_inv_rect_Type3 : 2447 2447 params > AST.ident List.list > joint_internal_function > (__ > __ > 2448 __ > __ > __ > __ > __ >'a1) > 'a1 **)2448 __ > __ > __ > __ > 'a1) > 'a1 **) 2449 2449 let good_if_inv_rect_Type3 x1 x2 x3 h1 = 2450 2450 let hcut = good_if_rect_Type3 x1 x2 x3 h1 in hcut __ … … 2452 2452 (** val good_if_inv_rect_Type2 : 2453 2453 params > AST.ident List.list > joint_internal_function > (__ > __ > 2454 __ > __ > __ > __ > __ >'a1) > 'a1 **)2454 __ > __ > __ > __ > 'a1) > 'a1 **) 2455 2455 let good_if_inv_rect_Type2 x1 x2 x3 h1 = 2456 2456 let hcut = good_if_rect_Type2 x1 x2 x3 h1 in hcut __ … … 2458 2458 (** val good_if_inv_rect_Type1 : 2459 2459 params > AST.ident List.list > joint_internal_function > (__ > __ > 2460 __ > __ > __ > __ > __ >'a1) > 'a1 **)2460 __ > __ > __ > __ > 'a1) > 'a1 **) 2461 2461 let good_if_inv_rect_Type1 x1 x2 x3 h1 = 2462 2462 let hcut = good_if_rect_Type1 x1 x2 x3 h1 in hcut __ … … 2464 2464 (** val good_if_inv_rect_Type0 : 2465 2465 params > AST.ident List.list > joint_internal_function > (__ > __ > 2466 __ > __ > __ > __ > __ >'a1) > 'a1 **)2466 __ > __ > __ > __ > 'a1) > 'a1 **) 2467 2467 let good_if_inv_rect_Type0 x1 x2 x3 h1 = 2468 2468 let hcut = good_if_rect_Type0 x1 x2 x3 h1 in hcut __ 2469 2470 (** val good_if_discr : 2471 params > AST.ident List.list > joint_internal_function > __ **) 2472 let good_if_discr a1 a2 a3 = 2473 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH > dH __ __ __ __ __)) __ 2469 2474 2470 2475 (** val good_if_jmdiscr : 2471 2476 params > AST.ident List.list > joint_internal_function > __ **) 2472 2477 let good_if_jmdiscr a1 a2 a3 = 2473 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH > dH __ __ __ __ __ __)) __2478 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH > dH __ __ __ __ __)) __ 2474 2479 2475 2480 type joint_closed_internal_function = joint_internal_function Types.sig0 … … 2524 2529 type joint_function = joint_closed_internal_function AST.fundef 2525 2530 2526 type joint_program = (joint_function, Nat.nat) AST.program 2531 type joint_program = { joint_prog : (joint_function, AST.init_data List.list) 2532 AST.program; 2533 init_cost_label : CostLabel.costlabel } 2534 2535 (** val joint_program_rect_Type4 : 2536 params > ((joint_function, AST.init_data List.list) AST.program > 2537 CostLabel.costlabel > 'a1) > joint_program > 'a1 **) 2538 let rec joint_program_rect_Type4 p h_mk_joint_program x_18149 = 2539 let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } = 2540 x_18149 2541 in 2542 h_mk_joint_program joint_prog0 init_cost_label0 2543 2544 (** val joint_program_rect_Type5 : 2545 params > ((joint_function, AST.init_data List.list) AST.program > 2546 CostLabel.costlabel > 'a1) > joint_program > 'a1 **) 2547 let rec joint_program_rect_Type5 p h_mk_joint_program x_18151 = 2548 let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } = 2549 x_18151 2550 in 2551 h_mk_joint_program joint_prog0 init_cost_label0 2552 2553 (** val joint_program_rect_Type3 : 2554 params > ((joint_function, AST.init_data List.list) AST.program > 2555 CostLabel.costlabel > 'a1) > joint_program > 'a1 **) 2556 let rec joint_program_rect_Type3 p h_mk_joint_program x_18153 = 2557 let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } = 2558 x_18153 2559 in 2560 h_mk_joint_program joint_prog0 init_cost_label0 2561 2562 (** val joint_program_rect_Type2 : 2563 params > ((joint_function, AST.init_data List.list) AST.program > 2564 CostLabel.costlabel > 'a1) > joint_program > 'a1 **) 2565 let rec joint_program_rect_Type2 p h_mk_joint_program x_18155 = 2566 let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } = 2567 x_18155 2568 in 2569 h_mk_joint_program joint_prog0 init_cost_label0 2570 2571 (** val joint_program_rect_Type1 : 2572 params > ((joint_function, AST.init_data List.list) AST.program > 2573 CostLabel.costlabel > 'a1) > joint_program > 'a1 **) 2574 let rec joint_program_rect_Type1 p h_mk_joint_program x_18157 = 2575 let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } = 2576 x_18157 2577 in 2578 h_mk_joint_program joint_prog0 init_cost_label0 2579 2580 (** val joint_program_rect_Type0 : 2581 params > ((joint_function, AST.init_data List.list) AST.program > 2582 CostLabel.costlabel > 'a1) > joint_program > 'a1 **) 2583 let rec joint_program_rect_Type0 p h_mk_joint_program x_18159 = 2584 let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } = 2585 x_18159 2586 in 2587 h_mk_joint_program joint_prog0 init_cost_label0 2588 2589 (** val joint_prog : 2590 params > joint_program > (joint_function, AST.init_data List.list) 2591 AST.program **) 2592 let rec joint_prog p xxx = 2593 xxx.joint_prog 2594 2595 (** val init_cost_label : params > joint_program > CostLabel.costlabel **) 2596 let rec init_cost_label p xxx = 2597 xxx.init_cost_label 2598 2599 (** val joint_program_inv_rect_Type4 : 2600 params > joint_program > ((joint_function, AST.init_data List.list) 2601 AST.program > CostLabel.costlabel > __ > 'a1) > 'a1 **) 2602 let joint_program_inv_rect_Type4 x1 hterm h1 = 2603 let hcut = joint_program_rect_Type4 x1 h1 hterm in hcut __ 2604 2605 (** val joint_program_inv_rect_Type3 : 2606 params > joint_program > ((joint_function, AST.init_data List.list) 2607 AST.program > CostLabel.costlabel > __ > 'a1) > 'a1 **) 2608 let joint_program_inv_rect_Type3 x1 hterm h1 = 2609 let hcut = joint_program_rect_Type3 x1 h1 hterm in hcut __ 2610 2611 (** val joint_program_inv_rect_Type2 : 2612 params > joint_program > ((joint_function, AST.init_data List.list) 2613 AST.program > CostLabel.costlabel > __ > 'a1) > 'a1 **) 2614 let joint_program_inv_rect_Type2 x1 hterm h1 = 2615 let hcut = joint_program_rect_Type2 x1 h1 hterm in hcut __ 2616 2617 (** val joint_program_inv_rect_Type1 : 2618 params > joint_program > ((joint_function, AST.init_data List.list) 2619 AST.program > CostLabel.costlabel > __ > 'a1) > 'a1 **) 2620 let joint_program_inv_rect_Type1 x1 hterm h1 = 2621 let hcut = joint_program_rect_Type1 x1 h1 hterm in hcut __ 2622 2623 (** val joint_program_inv_rect_Type0 : 2624 params > joint_program > ((joint_function, AST.init_data List.list) 2625 AST.program > CostLabel.costlabel > __ > 'a1) > 'a1 **) 2626 let joint_program_inv_rect_Type0 x1 hterm h1 = 2627 let hcut = joint_program_rect_Type0 x1 h1 hterm in hcut __ 2628 2629 (** val joint_program_discr : 2630 params > joint_program > joint_program > __ **) 2631 let joint_program_discr a1 x y = 2632 Logic.eq_rect_Type2 x 2633 (let { joint_prog = a0; init_cost_label = a10 } = x in 2634 Obj.magic (fun _ dH > dH __ __)) y 2635 2636 (** val joint_program_jmdiscr : 2637 params > joint_program > joint_program > __ **) 2638 let joint_program_jmdiscr a1 x y = 2639 Logic.eq_rect_Type2 x 2640 (let { joint_prog = a0; init_cost_label = a10 } = x in 2641 Obj.magic (fun _ dH > dH __ __)) y 2642 2643 (** val dpi1__o__joint_prog__o__inject : 2644 params > (joint_program, 'a1) Types.dPair > (joint_function, 2645 AST.init_data List.list) AST.program Types.sig0 **) 2646 let dpi1__o__joint_prog__o__inject x0 x3 = 2647 x3.Types.dpi1.joint_prog 2648 2649 (** val eject__o__joint_prog__o__inject : 2650 params > joint_program Types.sig0 > (joint_function, AST.init_data 2651 List.list) AST.program Types.sig0 **) 2652 let eject__o__joint_prog__o__inject x0 x3 = 2653 (Types.pi1 x3).joint_prog 2654 2655 (** val joint_prog__o__inject : 2656 params > joint_program > (joint_function, AST.init_data List.list) 2657 AST.program Types.sig0 **) 2658 let joint_prog__o__inject x0 x2 = 2659 x2.joint_prog 2660 2661 (** val dpi1__o__joint_prog : 2662 params > (joint_program, 'a1) Types.dPair > (joint_function, 2663 AST.init_data List.list) AST.program **) 2664 let dpi1__o__joint_prog x0 x2 = 2665 x2.Types.dpi1.joint_prog 2666 2667 (** val eject__o__joint_prog : 2668 params > joint_program Types.sig0 > (joint_function, AST.init_data 2669 List.list) AST.program **) 2670 let eject__o__joint_prog x0 x2 = 2671 (Types.pi1 x2).joint_prog 2527 2672 2528 2673 type stack_cost_model = (AST.ident, Nat.nat) Types.prod List.list … … 2536 2681 List.Cons ({ Types.fst = id; Types.snd = 2537 2682 (Types.pi1 jif).joint_if_stacksize }, acc) 2538  AST.External x > acc)) List.Nil pr.AST.prog_funct 2683  AST.External x > acc)) List.Nil pr.joint_prog.AST.prog_funct 2684 2685 open Extra_bool 2686 2687 open Coqlib 2688 2689 open Values 2690 2691 open FrontEndVal 2692 2693 open GenMem 2694 2695 open FrontEndMem 2696 2697 open Globalenvs 2539 2698 2540 2699 (** val globals_stacksize : params > joint_program > Nat.nat **) 2541 2700 let globals_stacksize pars p = 2542 2701 List.fold Nat.plus Nat.O (fun entry > Bool.True) (fun entry > 2543 entry.Types.snd) p.AST.prog_vars 2544 2702 Globalenvs.size_init_data_list entry.Types.snd) 2703 p.joint_prog.AST.prog_vars 2704
Note: See TracChangeset
for help on using the changeset viewer.