Changeset 2867 for extracted/joint.ml
 Timestamp:
 Mar 13, 2013, 11:12:29 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/joint.ml
r2854 r2867 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_ 7 > h_Reg x_7113  Imm x_ 8 > h_Imm x_8112  Reg x_19661 > h_Reg x_19661 113  Imm x_19662 > h_Imm x_19662 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 2 > h_Reg x_12119  Imm x_1 3 > h_Imm x_13118  Reg x_19666 > h_Reg x_19666 119  Imm x_19667 > h_Imm x_19667 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 7 > h_Reg x_17125  Imm x_1 8 > h_Imm x_18124  Reg x_19671 > h_Reg x_19671 125  Imm x_19672 > h_Imm x_19672 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_ 22 > h_Reg x_22131  Imm x_ 23 > h_Imm x_23130  Reg x_19676 > h_Reg x_19676 131  Imm x_19677 > h_Imm x_19677 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_ 27 > h_Reg x_27137  Imm x_ 28 > h_Imm x_28136  Reg x_19681 > h_Reg x_19681 137  Imm x_19682 > h_Imm x_19682 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_ 32 > h_Reg x_32143  Imm x_ 33 > h_Imm x_33142  Reg x_19686 > h_Reg x_19686 143  Imm x_19687 > h_Imm x_19687 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_ 68=326 let rec unserialized_params_rect_Type4 h_mk_unserialized_params x_19722 = 327 327 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = 328 x_ 68328 x_19722 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_ 70=337 let rec unserialized_params_rect_Type5 h_mk_unserialized_params x_19724 = 338 338 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = 339 x_ 70339 x_19724 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_ 72=348 let rec unserialized_params_rect_Type3 h_mk_unserialized_params x_19726 = 349 349 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = 350 x_ 72350 x_19726 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_ 74=359 let rec unserialized_params_rect_Type2 h_mk_unserialized_params x_19728 = 360 360 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = 361 x_ 74361 x_19728 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_ 76=370 let rec unserialized_params_rect_Type1 h_mk_unserialized_params x_19730 = 371 371 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = 372 x_ 76372 x_19730 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_ 78=381 let rec unserialized_params_rect_Type0 h_mk_unserialized_params x_19732 = 382 382 let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = 383 x_ 78383 x_19732 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_ 95=508 let rec get_pseudo_reg_functs_rect_Type4 p h_mk_get_pseudo_reg_functs x_19749 = 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_ 95514 params_regs0 } = x_19749 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_ 97=531 let rec get_pseudo_reg_functs_rect_Type5 p h_mk_get_pseudo_reg_functs x_19751 = 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_ 97537 params_regs0 } = x_19751 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_ 99=554 let rec get_pseudo_reg_functs_rect_Type3 p h_mk_get_pseudo_reg_functs x_19753 = 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_ 99560 params_regs0 } = x_19753 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 01=577 let rec get_pseudo_reg_functs_rect_Type2 p h_mk_get_pseudo_reg_functs x_19755 = 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 01583 params_regs0 } = x_19755 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 03=600 let rec get_pseudo_reg_functs_rect_Type1 p h_mk_get_pseudo_reg_functs x_19757 = 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 03606 params_regs0 } = x_19757 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 05=623 let rec get_pseudo_reg_functs_rect_Type0 p h_mk_get_pseudo_reg_functs x_19759 = 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 05629 params_regs0 } = x_19759 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 35=808 let { u_pars = u_pars0; functs = functs0 } = x_1 35in807 let rec uns_params_rect_Type4 h_mk_uns_params x_19789 = 808 let { u_pars = u_pars0; functs = functs0 } = x_19789 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 37=815 let { u_pars = u_pars0; functs = functs0 } = x_1 37in814 let rec uns_params_rect_Type5 h_mk_uns_params x_19791 = 815 let { u_pars = u_pars0; functs = functs0 } = x_19791 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 39=822 let { u_pars = u_pars0; functs = functs0 } = x_1 39in821 let rec uns_params_rect_Type3 h_mk_uns_params x_19793 = 822 let { u_pars = u_pars0; functs = functs0 } = x_19793 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 41=829 let { u_pars = u_pars0; functs = functs0 } = x_1 41in828 let rec uns_params_rect_Type2 h_mk_uns_params x_19795 = 829 let { u_pars = u_pars0; functs = functs0 } = x_19795 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 43=836 let { u_pars = u_pars0; functs = functs0 } = x_1 43in835 let rec uns_params_rect_Type1 h_mk_uns_params x_19797 = 836 let { u_pars = u_pars0; functs = functs0 } = x_19797 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 45=843 let { u_pars = u_pars0; functs = functs0 } = x_1 45in842 let rec uns_params_rect_Type0 h_mk_uns_params x_19799 = 843 let { u_pars = u_pars0; functs = functs0 } = x_19799 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_200 > h_COMMENT x_200 914  MOVE x_201 > h_MOVE x_201 915  POP x_202 > h_POP x_202 916  PUSH x_203 > h_PUSH x_203 917  ADDRESS (i, x_205, x_204) > h_ADDRESS i __ x_205 x_204 918  OPACCS (x_211, x_210, x_209, x_208, x_207) > 919 h_OPACCS x_211 x_210 x_209 x_208 x_207 920  OP1 (x_214, x_213, x_212) > h_OP1 x_214 x_213 x_212 921  OP2 (x_218, x_217, x_216, x_215) > h_OP2 x_218 x_217 x_216 x_215 913  COMMENT x_19854 > h_COMMENT x_19854 914  MOVE x_19855 > h_MOVE x_19855 915  POP x_19856 > h_POP x_19856 916  PUSH x_19857 > h_PUSH x_19857 917  ADDRESS (i, x_19859, x_19858) > h_ADDRESS i __ x_19859 x_19858 918  OPACCS (x_19865, x_19864, x_19863, x_19862, x_19861) > 919 h_OPACCS x_19865 x_19864 x_19863 x_19862 x_19861 920  OP1 (x_19868, x_19867, x_19866) > h_OP1 x_19868 x_19867 x_19866 921  OP2 (x_19872, x_19871, x_19870, x_19869) > 922 h_OP2 x_19872 x_19871 x_19870 x_19869 922 923  CLEAR_CARRY > h_CLEAR_CARRY 923 924  SET_CARRY > h_SET_CARRY 924  LOAD (x_ 221, x_220, x_219) > h_LOAD x_221 x_220 x_219925  STORE (x_ 224, x_223, x_222) > h_STORE x_224 x_223 x_222926  Extension_seq x_ 225 > h_extension_seq x_225925  LOAD (x_19875, x_19874, x_19873) > h_LOAD x_19875 x_19874 x_19873 926  STORE (x_19878, x_19877, x_19876) > h_STORE x_19878 x_19877 x_19876 927  Extension_seq x_19879 > h_extension_seq x_19879 927 928 928 929 (** val joint_seq_rect_Type5 : … … 934 935 'a1) > (__ > 'a1) > joint_seq > 'a1 **) 935 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 936  COMMENT x_240 > h_COMMENT x_240 937  MOVE x_241 > h_MOVE x_241 938  POP x_242 > h_POP x_242 939  PUSH x_243 > h_PUSH x_243 940  ADDRESS (i, x_245, x_244) > h_ADDRESS i __ x_245 x_244 941  OPACCS (x_251, x_250, x_249, x_248, x_247) > 942 h_OPACCS x_251 x_250 x_249 x_248 x_247 943  OP1 (x_254, x_253, x_252) > h_OP1 x_254 x_253 x_252 944  OP2 (x_258, x_257, x_256, x_255) > h_OP2 x_258 x_257 x_256 x_255 937  COMMENT x_19894 > h_COMMENT x_19894 938  MOVE x_19895 > h_MOVE x_19895 939  POP x_19896 > h_POP x_19896 940  PUSH x_19897 > h_PUSH x_19897 941  ADDRESS (i, x_19899, x_19898) > h_ADDRESS i __ x_19899 x_19898 942  OPACCS (x_19905, x_19904, x_19903, x_19902, x_19901) > 943 h_OPACCS x_19905 x_19904 x_19903 x_19902 x_19901 944  OP1 (x_19908, x_19907, x_19906) > h_OP1 x_19908 x_19907 x_19906 945  OP2 (x_19912, x_19911, x_19910, x_19909) > 946 h_OP2 x_19912 x_19911 x_19910 x_19909 945 947  CLEAR_CARRY > h_CLEAR_CARRY 946 948  SET_CARRY > h_SET_CARRY 947  LOAD (x_ 261, x_260, x_259) > h_LOAD x_261 x_260 x_259948  STORE (x_ 264, x_263, x_262) > h_STORE x_264 x_263 x_262949  Extension_seq x_ 265 > h_extension_seq x_265949  LOAD (x_19915, x_19914, x_19913) > h_LOAD x_19915 x_19914 x_19913 950  STORE (x_19918, x_19917, x_19916) > h_STORE x_19918 x_19917 x_19916 951  Extension_seq x_19919 > h_extension_seq x_19919 950 952 951 953 (** val joint_seq_rect_Type3 : … … 957 959 'a1) > (__ > 'a1) > joint_seq > 'a1 **) 958 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 959  COMMENT x_280 > h_COMMENT x_280 960  MOVE x_281 > h_MOVE x_281 961  POP x_282 > h_POP x_282 962  PUSH x_283 > h_PUSH x_283 963  ADDRESS (i, x_285, x_284) > h_ADDRESS i __ x_285 x_284 964  OPACCS (x_291, x_290, x_289, x_288, x_287) > 965 h_OPACCS x_291 x_290 x_289 x_288 x_287 966  OP1 (x_294, x_293, x_292) > h_OP1 x_294 x_293 x_292 967  OP2 (x_298, x_297, x_296, x_295) > h_OP2 x_298 x_297 x_296 x_295 961  COMMENT x_19934 > h_COMMENT x_19934 962  MOVE x_19935 > h_MOVE x_19935 963  POP x_19936 > h_POP x_19936 964  PUSH x_19937 > h_PUSH x_19937 965  ADDRESS (i, x_19939, x_19938) > h_ADDRESS i __ x_19939 x_19938 966  OPACCS (x_19945, x_19944, x_19943, x_19942, x_19941) > 967 h_OPACCS x_19945 x_19944 x_19943 x_19942 x_19941 968  OP1 (x_19948, x_19947, x_19946) > h_OP1 x_19948 x_19947 x_19946 969  OP2 (x_19952, x_19951, x_19950, x_19949) > 970 h_OP2 x_19952 x_19951 x_19950 x_19949 968 971  CLEAR_CARRY > h_CLEAR_CARRY 969 972  SET_CARRY > h_SET_CARRY 970  LOAD (x_ 301, x_300, x_299) > h_LOAD x_301 x_300 x_299971  STORE (x_ 304, x_303, x_302) > h_STORE x_304 x_303 x_302972  Extension_seq x_ 305 > h_extension_seq x_305973  LOAD (x_19955, x_19954, x_19953) > h_LOAD x_19955 x_19954 x_19953 974  STORE (x_19958, x_19957, x_19956) > h_STORE x_19958 x_19957 x_19956 975  Extension_seq x_19959 > h_extension_seq x_19959 973 976 974 977 (** val joint_seq_rect_Type2 : … … 980 983 'a1) > (__ > 'a1) > joint_seq > 'a1 **) 981 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 982  COMMENT x_320 > h_COMMENT x_320 983  MOVE x_321 > h_MOVE x_321 984  POP x_322 > h_POP x_322 985  PUSH x_323 > h_PUSH x_323 986  ADDRESS (i, x_325, x_324) > h_ADDRESS i __ x_325 x_324 987  OPACCS (x_331, x_330, x_329, x_328, x_327) > 988 h_OPACCS x_331 x_330 x_329 x_328 x_327 989  OP1 (x_334, x_333, x_332) > h_OP1 x_334 x_333 x_332 990  OP2 (x_338, x_337, x_336, x_335) > h_OP2 x_338 x_337 x_336 x_335 985  COMMENT x_19974 > h_COMMENT x_19974 986  MOVE x_19975 > h_MOVE x_19975 987  POP x_19976 > h_POP x_19976 988  PUSH x_19977 > h_PUSH x_19977 989  ADDRESS (i, x_19979, x_19978) > h_ADDRESS i __ x_19979 x_19978 990  OPACCS (x_19985, x_19984, x_19983, x_19982, x_19981) > 991 h_OPACCS x_19985 x_19984 x_19983 x_19982 x_19981 992  OP1 (x_19988, x_19987, x_19986) > h_OP1 x_19988 x_19987 x_19986 993  OP2 (x_19992, x_19991, x_19990, x_19989) > 994 h_OP2 x_19992 x_19991 x_19990 x_19989 991 995  CLEAR_CARRY > h_CLEAR_CARRY 992 996  SET_CARRY > h_SET_CARRY 993  LOAD (x_ 341, x_340, x_339) > h_LOAD x_341 x_340 x_339994  STORE (x_ 344, x_343, x_342) > h_STORE x_344 x_343 x_342995  Extension_seq x_ 345 > h_extension_seq x_345997  LOAD (x_19995, x_19994, x_19993) > h_LOAD x_19995 x_19994 x_19993 998  STORE (x_19998, x_19997, x_19996) > h_STORE x_19998 x_19997 x_19996 999  Extension_seq x_19999 > h_extension_seq x_19999 996 1000 997 1001 (** val joint_seq_rect_Type1 : … … 1003 1007 'a1) > (__ > 'a1) > joint_seq > 'a1 **) 1004 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 1005  COMMENT x_360 > h_COMMENT x_360 1006  MOVE x_361 > h_MOVE x_361 1007  POP x_362 > h_POP x_362 1008  PUSH x_363 > h_PUSH x_363 1009  ADDRESS (i, x_365, x_364) > h_ADDRESS i __ x_365 x_364 1010  OPACCS (x_371, x_370, x_369, x_368, x_367) > 1011 h_OPACCS x_371 x_370 x_369 x_368 x_367 1012  OP1 (x_374, x_373, x_372) > h_OP1 x_374 x_373 x_372 1013  OP2 (x_378, x_377, x_376, x_375) > h_OP2 x_378 x_377 x_376 x_375 1009  COMMENT x_20014 > h_COMMENT x_20014 1010  MOVE x_20015 > h_MOVE x_20015 1011  POP x_20016 > h_POP x_20016 1012  PUSH x_20017 > h_PUSH x_20017 1013  ADDRESS (i, x_20019, x_20018) > h_ADDRESS i __ x_20019 x_20018 1014  OPACCS (x_20025, x_20024, x_20023, x_20022, x_20021) > 1015 h_OPACCS x_20025 x_20024 x_20023 x_20022 x_20021 1016  OP1 (x_20028, x_20027, x_20026) > h_OP1 x_20028 x_20027 x_20026 1017  OP2 (x_20032, x_20031, x_20030, x_20029) > 1018 h_OP2 x_20032 x_20031 x_20030 x_20029 1014 1019  CLEAR_CARRY > h_CLEAR_CARRY 1015 1020  SET_CARRY > h_SET_CARRY 1016  LOAD (x_ 381, x_380, x_379) > h_LOAD x_381 x_380 x_3791017  STORE (x_ 384, x_383, x_382) > h_STORE x_384 x_383 x_3821018  Extension_seq x_ 385 > h_extension_seq x_3851021  LOAD (x_20035, x_20034, x_20033) > h_LOAD x_20035 x_20034 x_20033 1022  STORE (x_20038, x_20037, x_20036) > h_STORE x_20038 x_20037 x_20036 1023  Extension_seq x_20039 > h_extension_seq x_20039 1019 1024 1020 1025 (** val joint_seq_rect_Type0 : … … 1026 1031 'a1) > (__ > 'a1) > joint_seq > 'a1 **) 1027 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 1028  COMMENT x_400 > h_COMMENT x_400 1029  MOVE x_401 > h_MOVE x_401 1030  POP x_402 > h_POP x_402 1031  PUSH x_403 > h_PUSH x_403 1032  ADDRESS (i, x_405, x_404) > h_ADDRESS i __ x_405 x_404 1033  OPACCS (x_411, x_410, x_409, x_408, x_407) > 1034 h_OPACCS x_411 x_410 x_409 x_408 x_407 1035  OP1 (x_414, x_413, x_412) > h_OP1 x_414 x_413 x_412 1036  OP2 (x_418, x_417, x_416, x_415) > h_OP2 x_418 x_417 x_416 x_415 1033  COMMENT x_20054 > h_COMMENT x_20054 1034  MOVE x_20055 > h_MOVE x_20055 1035  POP x_20056 > h_POP x_20056 1036  PUSH x_20057 > h_PUSH x_20057 1037  ADDRESS (i, x_20059, x_20058) > h_ADDRESS i __ x_20059 x_20058 1038  OPACCS (x_20065, x_20064, x_20063, x_20062, x_20061) > 1039 h_OPACCS x_20065 x_20064 x_20063 x_20062 x_20061 1040  OP1 (x_20068, x_20067, x_20066) > h_OP1 x_20068 x_20067 x_20066 1041  OP2 (x_20072, x_20071, x_20070, x_20069) > 1042 h_OP2 x_20072 x_20071 x_20070 x_20069 1037 1043  CLEAR_CARRY > h_CLEAR_CARRY 1038 1044  SET_CARRY > h_SET_CARRY 1039  LOAD (x_ 421, x_420, x_419) > h_LOAD x_421 x_420 x_4191040  STORE (x_ 424, x_423, x_422) > h_STORE x_424 x_423 x_4221041  Extension_seq x_ 425 > h_extension_seq x_4251045  LOAD (x_20075, x_20074, x_20073) > h_LOAD x_20075 x_20074 x_20073 1046  STORE (x_20078, x_20077, x_20076) > h_STORE x_20078 x_20077 x_20076 1047  Extension_seq x_20079 > h_extension_seq x_20079 1042 1048 1043 1049 (** val joint_seq_inv_rect_Type4 : … … 1230 1236 > (__ > Graphs.label > 'a1) > (joint_seq > 'a1) > joint_step > 'a1 **) 1231 1237 let rec joint_step_rect_Type4 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function 1232  COST_LABEL x_ 692 > h_COST_LABEL x_6921233  CALL (x_ 695, x_694, x_693) > h_CALL x_695 x_694 x_6931234  COND (x_ 697, x_696) > h_COND x_697 x_6961235  Step_seq x_ 698 > h_step_seq x_6981238  COST_LABEL x_20346 > h_COST_LABEL x_20346 1239  CALL (x_20349, x_20348, x_20347) > h_CALL x_20349 x_20348 x_20347 1240  COND (x_20351, x_20350) > h_COND x_20351 x_20350 1241  Step_seq x_20352 > h_step_seq x_20352 1236 1242 1237 1243 (** val joint_step_rect_Type5 : … … 1240 1246 > (__ > Graphs.label > 'a1) > (joint_seq > 'a1) > joint_step > 'a1 **) 1241 1247 let rec joint_step_rect_Type5 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function 1242  COST_LABEL x_ 704 > h_COST_LABEL x_7041243  CALL (x_ 707, x_706, x_705) > h_CALL x_707 x_706 x_7051244  COND (x_ 709, x_708) > h_COND x_709 x_7081245  Step_seq x_ 710 > h_step_seq x_7101248  COST_LABEL x_20358 > h_COST_LABEL x_20358 1249  CALL (x_20361, x_20360, x_20359) > h_CALL x_20361 x_20360 x_20359 1250  COND (x_20363, x_20362) > h_COND x_20363 x_20362 1251  Step_seq x_20364 > h_step_seq x_20364 1246 1252 1247 1253 (** val joint_step_rect_Type3 : … … 1250 1256 > (__ > Graphs.label > 'a1) > (joint_seq > 'a1) > joint_step > 'a1 **) 1251 1257 let rec joint_step_rect_Type3 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function 1252  COST_LABEL x_ 716 > h_COST_LABEL x_7161253  CALL (x_ 719, x_718, x_717) > h_CALL x_719 x_718 x_7171254  COND (x_ 721, x_720) > h_COND x_721 x_7201255  Step_seq x_ 722 > h_step_seq x_7221258  COST_LABEL x_20370 > h_COST_LABEL x_20370 1259  CALL (x_20373, x_20372, x_20371) > h_CALL x_20373 x_20372 x_20371 1260  COND (x_20375, x_20374) > h_COND x_20375 x_20374 1261  Step_seq x_20376 > h_step_seq x_20376 1256 1262 1257 1263 (** val joint_step_rect_Type2 : … … 1260 1266 > (__ > Graphs.label > 'a1) > (joint_seq > 'a1) > joint_step > 'a1 **) 1261 1267 let rec joint_step_rect_Type2 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function 1262  COST_LABEL x_ 728 > h_COST_LABEL x_7281263  CALL (x_ 731, x_730, x_729) > h_CALL x_731 x_730 x_7291264  COND (x_ 733, x_732) > h_COND x_733 x_7321265  Step_seq x_ 734 > h_step_seq x_7341268  COST_LABEL x_20382 > h_COST_LABEL x_20382 1269  CALL (x_20385, x_20384, x_20383) > h_CALL x_20385 x_20384 x_20383 1270  COND (x_20387, x_20386) > h_COND x_20387 x_20386 1271  Step_seq x_20388 > h_step_seq x_20388 1266 1272 1267 1273 (** val joint_step_rect_Type1 : … … 1270 1276 > (__ > Graphs.label > 'a1) > (joint_seq > 'a1) > joint_step > 'a1 **) 1271 1277 let rec joint_step_rect_Type1 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function 1272  COST_LABEL x_ 740 > h_COST_LABEL x_7401273  CALL (x_ 743, x_742, x_741) > h_CALL x_743 x_742 x_7411274  COND (x_ 745, x_744) > h_COND x_745 x_7441275  Step_seq x_ 746 > h_step_seq x_7461278  COST_LABEL x_20394 > h_COST_LABEL x_20394 1279  CALL (x_20397, x_20396, x_20395) > h_CALL x_20397 x_20396 x_20395 1280  COND (x_20399, x_20398) > h_COND x_20399 x_20398 1281  Step_seq x_20400 > h_step_seq x_20400 1276 1282 1277 1283 (** val joint_step_rect_Type0 : … … 1280 1286 > (__ > Graphs.label > 'a1) > (joint_seq > 'a1) > joint_step > 'a1 **) 1281 1287 let rec joint_step_rect_Type0 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function 1282  COST_LABEL x_ 752 > h_COST_LABEL x_7521283  CALL (x_ 755, x_754, x_753) > h_CALL x_755 x_754 x_7531284  COND (x_ 757, x_756) > h_COND x_757 x_7561285  Step_seq x_ 758 > h_step_seq x_7581288  COST_LABEL x_20406 > h_COST_LABEL x_20406 1289  CALL (x_20409, x_20408, x_20407) > h_CALL x_20409 x_20408 x_20407 1290  COND (x_20411, x_20410) > h_COND x_20411 x_20410 1291  Step_seq x_20412 > h_step_seq x_20412 1286 1292 1287 1293 (** val joint_step_inv_rect_Type4 : … … 1458 1464 (uns_params > __ > (__ > Graphs.label Types.option) > Bool.bool > 1459 1465 'a1) > stmt_params > 'a1 **) 1460 let rec stmt_params_rect_Type4 h_mk_stmt_params x_ 837=1466 let rec stmt_params_rect_Type4 h_mk_stmt_params x_20491 = 1461 1467 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = 1462 has_fcond0 } = x_ 8371468 has_fcond0 } = x_20491 1463 1469 in 1464 1470 h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0 … … 1467 1473 (uns_params > __ > (__ > Graphs.label Types.option) > Bool.bool > 1468 1474 'a1) > stmt_params > 'a1 **) 1469 let rec stmt_params_rect_Type5 h_mk_stmt_params x_ 839=1475 let rec stmt_params_rect_Type5 h_mk_stmt_params x_20493 = 1470 1476 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = 1471 has_fcond0 } = x_ 8391477 has_fcond0 } = x_20493 1472 1478 in 1473 1479 h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0 … … 1476 1482 (uns_params > __ > (__ > Graphs.label Types.option) > Bool.bool > 1477 1483 'a1) > stmt_params > 'a1 **) 1478 let rec stmt_params_rect_Type3 h_mk_stmt_params x_ 841=1484 let rec stmt_params_rect_Type3 h_mk_stmt_params x_20495 = 1479 1485 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = 1480 has_fcond0 } = x_ 8411486 has_fcond0 } = x_20495 1481 1487 in 1482 1488 h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0 … … 1485 1491 (uns_params > __ > (__ > Graphs.label Types.option) > Bool.bool > 1486 1492 'a1) > stmt_params > 'a1 **) 1487 let rec stmt_params_rect_Type2 h_mk_stmt_params x_ 843=1493 let rec stmt_params_rect_Type2 h_mk_stmt_params x_20497 = 1488 1494 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = 1489 has_fcond0 } = x_ 8431495 has_fcond0 } = x_20497 1490 1496 in 1491 1497 h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0 … … 1494 1500 (uns_params > __ > (__ > Graphs.label Types.option) > Bool.bool > 1495 1501 'a1) > stmt_params > 'a1 **) 1496 let rec stmt_params_rect_Type1 h_mk_stmt_params x_ 845=1502 let rec stmt_params_rect_Type1 h_mk_stmt_params x_20499 = 1497 1503 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = 1498 has_fcond0 } = x_ 8451504 has_fcond0 } = x_20499 1499 1505 in 1500 1506 h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0 … … 1503 1509 (uns_params > __ > (__ > Graphs.label Types.option) > Bool.bool > 1504 1510 'a1) > stmt_params > 'a1 **) 1505 let rec stmt_params_rect_Type0 h_mk_stmt_params x_ 847=1511 let rec stmt_params_rect_Type0 h_mk_stmt_params x_20501 = 1506 1512 let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = 1507 has_fcond0 } = x_ 8471513 has_fcond0 } = x_20501 1508 1514 in 1509 1515 h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0 … … 1572 1578 (__, __) Types.prod) Types.sum > __ > 'a1) > joint_fin_step > 'a1 **) 1573 1579 let rec joint_fin_step_rect_Type4 p h_GOTO h_RETURN h_TAILCALL = function 1574  GOTO x_ 871 > h_GOTO x_8711580  GOTO x_20525 > h_GOTO x_20525 1575 1581  RETURN > h_RETURN 1576  TAILCALL (x_ 873, x_872) > h_TAILCALL __ x_873 x_8721582  TAILCALL (x_20527, x_20526) > h_TAILCALL __ x_20527 x_20526 1577 1583 1578 1584 (** val joint_fin_step_rect_Type5 : … … 1580 1586 (__, __) Types.prod) Types.sum > __ > 'a1) > joint_fin_step > 'a1 **) 1581 1587 let rec joint_fin_step_rect_Type5 p h_GOTO h_RETURN h_TAILCALL = function 1582  GOTO x_ 879 > h_GOTO x_8791588  GOTO x_20533 > h_GOTO x_20533 1583 1589  RETURN > h_RETURN 1584  TAILCALL (x_ 881, x_880) > h_TAILCALL __ x_881 x_8801590  TAILCALL (x_20535, x_20534) > h_TAILCALL __ x_20535 x_20534 1585 1591 1586 1592 (** val joint_fin_step_rect_Type3 : … … 1588 1594 (__, __) Types.prod) Types.sum > __ > 'a1) > joint_fin_step > 'a1 **) 1589 1595 let rec joint_fin_step_rect_Type3 p h_GOTO h_RETURN h_TAILCALL = function 1590  GOTO x_ 887 > h_GOTO x_8871596  GOTO x_20541 > h_GOTO x_20541 1591 1597  RETURN > h_RETURN 1592  TAILCALL (x_ 889, x_888) > h_TAILCALL __ x_889 x_8881598  TAILCALL (x_20543, x_20542) > h_TAILCALL __ x_20543 x_20542 1593 1599 1594 1600 (** val joint_fin_step_rect_Type2 : … … 1596 1602 (__, __) Types.prod) Types.sum > __ > 'a1) > joint_fin_step > 'a1 **) 1597 1603 let rec joint_fin_step_rect_Type2 p h_GOTO h_RETURN h_TAILCALL = function 1598  GOTO x_ 895 > h_GOTO x_8951604  GOTO x_20549 > h_GOTO x_20549 1599 1605  RETURN > h_RETURN 1600  TAILCALL (x_ 897, x_896) > h_TAILCALL __ x_897 x_8961606  TAILCALL (x_20551, x_20550) > h_TAILCALL __ x_20551 x_20550 1601 1607 1602 1608 (** val joint_fin_step_rect_Type1 : … … 1604 1610 (__, __) Types.prod) Types.sum > __ > 'a1) > joint_fin_step > 'a1 **) 1605 1611 let rec joint_fin_step_rect_Type1 p h_GOTO h_RETURN h_TAILCALL = function 1606  GOTO x_ 903 > h_GOTO x_9031612  GOTO x_20557 > h_GOTO x_20557 1607 1613  RETURN > h_RETURN 1608  TAILCALL (x_ 905, x_904) > h_TAILCALL __ x_905 x_9041614  TAILCALL (x_20559, x_20558) > h_TAILCALL __ x_20559 x_20558 1609 1615 1610 1616 (** val joint_fin_step_rect_Type0 : … … 1612 1618 (__, __) Types.prod) Types.sum > __ > 'a1) > joint_fin_step > 'a1 **) 1613 1619 let rec joint_fin_step_rect_Type0 p h_GOTO h_RETURN h_TAILCALL = function 1614  GOTO x_ 911 > h_GOTO x_9111620  GOTO x_20565 > h_GOTO x_20565 1615 1621  RETURN > h_RETURN 1616  TAILCALL (x_ 913, x_912) > h_TAILCALL __ x_913 x_9121622  TAILCALL (x_20567, x_20566) > h_TAILCALL __ x_20567 x_20566 1617 1623 1618 1624 (** val joint_fin_step_inv_rect_Type4 : … … 1686 1692 'a1) > joint_statement > 'a1 **) 1687 1693 let rec joint_statement_rect_Type4 p globals h_sequential h_final h_FCOND = function 1688  Sequential (x_ 979, x_978) > h_sequential x_979 x_9781689  Final x_ 980 > h_final x_9801690  FCOND (x_ 983, x_982, x_981) > h_FCOND __ x_983 x_982 x_9811694  Sequential (x_20633, x_20632) > h_sequential x_20633 x_20632 1695  Final x_20634 > h_final x_20634 1696  FCOND (x_20637, x_20636, x_20635) > h_FCOND __ x_20637 x_20636 x_20635 1691 1697 1692 1698 (** val joint_statement_rect_Type5 : … … 1695 1701 'a1) > joint_statement > 'a1 **) 1696 1702 let rec joint_statement_rect_Type5 p globals h_sequential h_final h_FCOND = function 1697  Sequential (x_ 990, x_989) > h_sequential x_990 x_9891698  Final x_ 991 > h_final x_9911699  FCOND (x_ 994, x_993, x_992) > h_FCOND __ x_994 x_993 x_9921703  Sequential (x_20644, x_20643) > h_sequential x_20644 x_20643 1704  Final x_20645 > h_final x_20645 1705  FCOND (x_20648, x_20647, x_20646) > h_FCOND __ x_20648 x_20647 x_20646 1700 1706 1701 1707 (** val joint_statement_rect_Type3 : … … 1704 1710 'a1) > joint_statement > 'a1 **) 1705 1711 let rec joint_statement_rect_Type3 p globals h_sequential h_final h_FCOND = function 1706  Sequential (x_ 1001, x_1000) > h_sequential x_1001 x_10001707  Final x_ 1002 > h_final x_10021708  FCOND (x_ 1005, x_1004, x_1003) > h_FCOND __ x_1005 x_1004 x_10031712  Sequential (x_20655, x_20654) > h_sequential x_20655 x_20654 1713  Final x_20656 > h_final x_20656 1714  FCOND (x_20659, x_20658, x_20657) > h_FCOND __ x_20659 x_20658 x_20657 1709 1715 1710 1716 (** val joint_statement_rect_Type2 : … … 1713 1719 'a1) > joint_statement > 'a1 **) 1714 1720 let rec joint_statement_rect_Type2 p globals h_sequential h_final h_FCOND = function 1715  Sequential (x_ 1012, x_1011) > h_sequential x_1012 x_10111716  Final x_ 1013 > h_final x_10131717  FCOND (x_ 1016, x_1015, x_1014) > h_FCOND __ x_1016 x_1015 x_10141721  Sequential (x_20666, x_20665) > h_sequential x_20666 x_20665 1722  Final x_20667 > h_final x_20667 1723  FCOND (x_20670, x_20669, x_20668) > h_FCOND __ x_20670 x_20669 x_20668 1718 1724 1719 1725 (** val joint_statement_rect_Type1 : … … 1722 1728 'a1) > joint_statement > 'a1 **) 1723 1729 let rec joint_statement_rect_Type1 p globals h_sequential h_final h_FCOND = function 1724  Sequential (x_ 1023, x_1022) > h_sequential x_1023 x_10221725  Final x_ 1024 > h_final x_10241726  FCOND (x_ 1027, x_1026, x_1025) > h_FCOND __ x_1027 x_1026 x_10251730  Sequential (x_20677, x_20676) > h_sequential x_20677 x_20676 1731  Final x_20678 > h_final x_20678 1732  FCOND (x_20681, x_20680, x_20679) > h_FCOND __ x_20681 x_20680 x_20679 1727 1733 1728 1734 (** val joint_statement_rect_Type0 : … … 1731 1737 'a1) > joint_statement > 'a1 **) 1732 1738 let rec joint_statement_rect_Type0 p globals h_sequential h_final h_FCOND = function 1733  Sequential (x_ 1034, x_1033) > h_sequential x_1034 x_10331734  Final x_ 1035 > h_final x_10351735  FCOND (x_ 1038, x_1037, x_1036) > h_FCOND __ x_1038 x_1037 x_10361739  Sequential (x_20688, x_20687) > h_sequential x_20688 x_20687 1740  Final x_20689 > h_final x_20689 1741  FCOND (x_20692, x_20691, x_20690) > h_FCOND __ x_20692 x_20691 x_20690 1736 1742 1737 1743 (** val joint_statement_inv_rect_Type4 : … … 1832 1838 Graphs.label > __ Types.option) > (__ > __ > __) > 'a1) > params > 1833 1839 'a1 **) 1834 let rec params_rect_Type4 h_mk_params x_ 1111=1840 let rec params_rect_Type4 h_mk_params x_20765 = 1835 1841 let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label = 1836 point_of_label0; point_of_succ = point_of_succ0 } = x_ 11111842 point_of_label0; point_of_succ = point_of_succ0 } = x_20765 1837 1843 in 1838 1844 h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0 … … 1843 1849 Graphs.label > __ Types.option) > (__ > __ > __) > 'a1) > params > 1844 1850 'a1 **) 1845 let rec params_rect_Type5 h_mk_params x_ 1113=1851 let rec params_rect_Type5 h_mk_params x_20767 = 1846 1852 let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label = 1847 point_of_label0; point_of_succ = point_of_succ0 } = x_ 11131853 point_of_label0; point_of_succ = point_of_succ0 } = x_20767 1848 1854 in 1849 1855 h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0 … … 1854 1860 Graphs.label > __ Types.option) > (__ > __ > __) > 'a1) > params > 1855 1861 'a1 **) 1856 let rec params_rect_Type3 h_mk_params x_ 1115=1862 let rec params_rect_Type3 h_mk_params x_20769 = 1857 1863 let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label = 1858 point_of_label0; point_of_succ = point_of_succ0 } = x_ 11151864 point_of_label0; point_of_succ = point_of_succ0 } = x_20769 1859 1865 in 1860 1866 h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0 … … 1865 1871 Graphs.label > __ Types.option) > (__ > __ > __) > 'a1) > params > 1866 1872 'a1 **) 1867 let rec params_rect_Type2 h_mk_params x_ 1117=1873 let rec params_rect_Type2 h_mk_params x_20771 = 1868 1874 let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label = 1869 point_of_label0; point_of_succ = point_of_succ0 } = x_ 11171875 point_of_label0; point_of_succ = point_of_succ0 } = x_20771 1870 1876 in 1871 1877 h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0 … … 1876 1882 Graphs.label > __ Types.option) > (__ > __ > __) > 'a1) > params > 1877 1883 'a1 **) 1878 let rec params_rect_Type1 h_mk_params x_ 1119=1884 let rec params_rect_Type1 h_mk_params x_20773 = 1879 1885 let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label = 1880 point_of_label0; point_of_succ = point_of_succ0 } = x_ 11191886 point_of_label0; point_of_succ = point_of_succ0 } = x_20773 1881 1887 in 1882 1888 h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0 … … 1887 1893 Graphs.label > __ Types.option) > (__ > __ > __) > 'a1) > params > 1888 1894 'a1 **) 1889 let rec params_rect_Type0 h_mk_params x_ 1121=1895 let rec params_rect_Type0 h_mk_params x_20775 = 1890 1896 let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label = 1891 point_of_label0; point_of_succ = point_of_succ0 } = x_ 11211897 point_of_label0; point_of_succ = point_of_succ0 } = x_20775 1892 1898 in 1893 1899 h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0 … … 2024 2030 2025 2031 (** val lin_params_rect_Type4 : (uns_params > 'a1) > lin_params > 'a1 **) 2026 let rec lin_params_rect_Type4 h_mk_lin_params x_ 1144=2027 let l_u_pars = x_ 1144in h_mk_lin_params l_u_pars2032 let rec lin_params_rect_Type4 h_mk_lin_params x_20798 = 2033 let l_u_pars = x_20798 in h_mk_lin_params l_u_pars 2028 2034 2029 2035 (** val lin_params_rect_Type5 : (uns_params > 'a1) > lin_params > 'a1 **) 2030 let rec lin_params_rect_Type5 h_mk_lin_params x_ 1146=2031 let l_u_pars = x_ 1146in h_mk_lin_params l_u_pars2036 let rec lin_params_rect_Type5 h_mk_lin_params x_20800 = 2037 let l_u_pars = x_20800 in h_mk_lin_params l_u_pars 2032 2038 2033 2039 (** val lin_params_rect_Type3 : (uns_params > 'a1) > lin_params > 'a1 **) 2034 let rec lin_params_rect_Type3 h_mk_lin_params x_ 1148=2035 let l_u_pars = x_ 1148in h_mk_lin_params l_u_pars2040 let rec lin_params_rect_Type3 h_mk_lin_params x_20802 = 2041 let l_u_pars = x_20802 in h_mk_lin_params l_u_pars 2036 2042 2037 2043 (** val lin_params_rect_Type2 : (uns_params > 'a1) > lin_params > 'a1 **) 2038 let rec lin_params_rect_Type2 h_mk_lin_params x_ 1150=2039 let l_u_pars = x_ 1150in h_mk_lin_params l_u_pars2044 let rec lin_params_rect_Type2 h_mk_lin_params x_20804 = 2045 let l_u_pars = x_20804 in h_mk_lin_params l_u_pars 2040 2046 2041 2047 (** val lin_params_rect_Type1 : (uns_params > 'a1) > lin_params > 'a1 **) 2042 let rec lin_params_rect_Type1 h_mk_lin_params x_ 1152=2043 let l_u_pars = x_ 1152in h_mk_lin_params l_u_pars2048 let rec lin_params_rect_Type1 h_mk_lin_params x_20806 = 2049 let l_u_pars = x_20806 in h_mk_lin_params l_u_pars 2044 2050 2045 2051 (** val lin_params_rect_Type0 : (uns_params > 'a1) > lin_params > 'a1 **) 2046 let rec lin_params_rect_Type0 h_mk_lin_params x_ 1154=2047 let l_u_pars = x_ 1154in h_mk_lin_params l_u_pars2052 let rec lin_params_rect_Type0 h_mk_lin_params x_20808 = 2053 let l_u_pars = x_20808 in h_mk_lin_params l_u_pars 2048 2054 2049 2055 (** val l_u_pars : lin_params > uns_params **) … … 2119 2125 (** val graph_params_rect_Type4 : 2120 2126 (uns_params > 'a1) > graph_params > 'a1 **) 2121 let rec graph_params_rect_Type4 h_mk_graph_params x_ 1170=2122 let g_u_pars = x_ 1170in h_mk_graph_params g_u_pars2127 let rec graph_params_rect_Type4 h_mk_graph_params x_20824 = 2128 let g_u_pars = x_20824 in h_mk_graph_params g_u_pars 2123 2129 2124 2130 (** val graph_params_rect_Type5 : 2125 2131 (uns_params > 'a1) > graph_params > 'a1 **) 2126 let rec graph_params_rect_Type5 h_mk_graph_params x_ 1172=2127 let g_u_pars = x_ 1172in h_mk_graph_params g_u_pars2132 let rec graph_params_rect_Type5 h_mk_graph_params x_20826 = 2133 let g_u_pars = x_20826 in h_mk_graph_params g_u_pars 2128 2134 2129 2135 (** val graph_params_rect_Type3 : 2130 2136 (uns_params > 'a1) > graph_params > 'a1 **) 2131 let rec graph_params_rect_Type3 h_mk_graph_params x_ 1174=2132 let g_u_pars = x_ 1174in h_mk_graph_params g_u_pars2137 let rec graph_params_rect_Type3 h_mk_graph_params x_20828 = 2138 let g_u_pars = x_20828 in h_mk_graph_params g_u_pars 2133 2139 2134 2140 (** val graph_params_rect_Type2 : 2135 2141 (uns_params > 'a1) > graph_params > 'a1 **) 2136 let rec graph_params_rect_Type2 h_mk_graph_params x_ 1176=2137 let g_u_pars = x_ 1176in h_mk_graph_params g_u_pars2142 let rec graph_params_rect_Type2 h_mk_graph_params x_20830 = 2143 let g_u_pars = x_20830 in h_mk_graph_params g_u_pars 2138 2144 2139 2145 (** val graph_params_rect_Type1 : 2140 2146 (uns_params > 'a1) > graph_params > 'a1 **) 2141 let rec graph_params_rect_Type1 h_mk_graph_params x_ 1178=2142 let g_u_pars = x_ 1178in h_mk_graph_params g_u_pars2147 let rec graph_params_rect_Type1 h_mk_graph_params x_20832 = 2148 let g_u_pars = x_20832 in h_mk_graph_params g_u_pars 2143 2149 2144 2150 (** val graph_params_rect_Type0 : 2145 2151 (uns_params > 'a1) > graph_params > 'a1 **) 2146 let rec graph_params_rect_Type0 h_mk_graph_params x_ 1180=2147 let g_u_pars = x_ 1180in h_mk_graph_params g_u_pars2152 let rec graph_params_rect_Type0 h_mk_graph_params x_20834 = 2153 let g_u_pars = x_20834 in h_mk_graph_params g_u_pars 2148 2154 2149 2155 (** val g_u_pars : graph_params > uns_params **) … … 2215 2221 Identifiers.universe > __ > __ > Nat.nat > Nat.nat > __ > __ > 2216 2222 'a1) > joint_internal_function > 'a1 **) 2217 let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_ 1196=2223 let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_20850 = 2218 2224 let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse = 2219 2225 joint_if_runiverse0; joint_if_result = joint_if_result0; … … 2221 2227 joint_if_stacksize0; joint_if_local_stacksize = 2222 2228 joint_if_local_stacksize0; joint_if_code = joint_if_code0; 2223 joint_if_entry = joint_if_entry0 } = x_ 11962229 joint_if_entry = joint_if_entry0 } = x_20850 2224 2230 in 2225 2231 h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0 … … 2231 2237 Identifiers.universe > __ > __ > Nat.nat > Nat.nat > __ > __ > 2232 2238 'a1) > joint_internal_function > 'a1 **) 2233 let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_ 1198=2239 let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_20852 = 2234 2240 let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse = 2235 2241 joint_if_runiverse0; joint_if_result = joint_if_result0; … … 2237 2243 joint_if_stacksize0; joint_if_local_stacksize = 2238 2244 joint_if_local_stacksize0; joint_if_code = joint_if_code0; 2239 joint_if_entry = joint_if_entry0 } = x_ 11982245 joint_if_entry = joint_if_entry0 } = x_20852 2240 2246 in 2241 2247 h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0 … … 2247 2253 Identifiers.universe > __ > __ > Nat.nat > Nat.nat > __ > __ > 2248 2254 'a1) > joint_internal_function > 'a1 **) 2249 let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_ 1200=2255 let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_20854 = 2250 2256 let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse = 2251 2257 joint_if_runiverse0; joint_if_result = joint_if_result0; … … 2253 2259 joint_if_stacksize0; joint_if_local_stacksize = 2254 2260 joint_if_local_stacksize0; joint_if_code = joint_if_code0; 2255 joint_if_entry = joint_if_entry0 } = x_ 12002261 joint_if_entry = joint_if_entry0 } = x_20854 2256 2262 in 2257 2263 h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0 … … 2263 2269 Identifiers.universe > __ > __ > Nat.nat > Nat.nat > __ > __ > 2264 2270 'a1) > joint_internal_function > 'a1 **) 2265 let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_ 1202=2271 let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_20856 = 2266 2272 let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse = 2267 2273 joint_if_runiverse0; joint_if_result = joint_if_result0; … … 2269 2275 joint_if_stacksize0; joint_if_local_stacksize = 2270 2276 joint_if_local_stacksize0; joint_if_code = joint_if_code0; 2271 joint_if_entry = joint_if_entry0 } = x_ 12022277 joint_if_entry = joint_if_entry0 } = x_20856 2272 2278 in 2273 2279 h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0 … … 2279 2285 Identifiers.universe > __ > __ > Nat.nat > Nat.nat > __ > __ > 2280 2286 'a1) > joint_internal_function > 'a1 **) 2281 let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_ 1204=2287 let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_20858 = 2282 2288 let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse = 2283 2289 joint_if_runiverse0; joint_if_result = joint_if_result0; … … 2285 2291 joint_if_stacksize0; joint_if_local_stacksize = 2286 2292 joint_if_local_stacksize0; joint_if_code = joint_if_code0; 2287 joint_if_entry = joint_if_entry0 } = x_ 12042293 joint_if_entry = joint_if_entry0 } = x_20858 2288 2294 in 2289 2295 h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0 … … 2295 2301 Identifiers.universe > __ > __ > Nat.nat > Nat.nat > __ > __ > 2296 2302 'a1) > joint_internal_function > 'a1 **) 2297 let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_ 1206=2303 let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_20860 = 2298 2304 let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse = 2299 2305 joint_if_runiverse0; joint_if_result = joint_if_result0; … … 2301 2307 joint_if_stacksize0; joint_if_local_stacksize = 2302 2308 joint_if_local_stacksize0; joint_if_code = joint_if_code0; 2303 joint_if_entry = joint_if_entry0 } = x_ 12062309 joint_if_entry = joint_if_entry0 } = x_20860 2304 2310 in 2305 2311 h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0 … … 2398 2404 (** val good_if_rect_Type4 : 2399 2405 params > AST.ident List.list > joint_internal_function > (__ > __ > 2400 __ > __ > __ > 'a1) > 'a1 **)2406 __ > __ > __ > __ > 'a1) > 'a1 **) 2401 2407 let rec good_if_rect_Type4 p globals def h_mk_good_if = 2402 h_mk_good_if __ __ __ __ __ 2408 h_mk_good_if __ __ __ __ __ __ 2403 2409 2404 2410 (** val good_if_rect_Type5 : 2405 2411 params > AST.ident List.list > joint_internal_function > (__ > __ > 2406 __ > __ > __ > 'a1) > 'a1 **)2412 __ > __ > __ > __ > 'a1) > 'a1 **) 2407 2413 let rec good_if_rect_Type5 p globals def h_mk_good_if = 2408 h_mk_good_if __ __ __ __ __ 2414 h_mk_good_if __ __ __ __ __ __ 2409 2415 2410 2416 (** val good_if_rect_Type3 : 2411 2417 params > AST.ident List.list > joint_internal_function > (__ > __ > 2412 __ > __ > __ > 'a1) > 'a1 **)2418 __ > __ > __ > __ > 'a1) > 'a1 **) 2413 2419 let rec good_if_rect_Type3 p globals def h_mk_good_if = 2414 h_mk_good_if __ __ __ __ __ 2420 h_mk_good_if __ __ __ __ __ __ 2415 2421 2416 2422 (** val good_if_rect_Type2 : 2417 2423 params > AST.ident List.list > joint_internal_function > (__ > __ > 2418 __ > __ > __ > 'a1) > 'a1 **)2424 __ > __ > __ > __ > 'a1) > 'a1 **) 2419 2425 let rec good_if_rect_Type2 p globals def h_mk_good_if = 2420 h_mk_good_if __ __ __ __ __ 2426 h_mk_good_if __ __ __ __ __ __ 2421 2427 2422 2428 (** val good_if_rect_Type1 : 2423 2429 params > AST.ident List.list > joint_internal_function > (__ > __ > 2424 __ > __ > __ > 'a1) > 'a1 **)2430 __ > __ > __ > __ > 'a1) > 'a1 **) 2425 2431 let rec good_if_rect_Type1 p globals def h_mk_good_if = 2426 h_mk_good_if __ __ __ __ __ 2432 h_mk_good_if __ __ __ __ __ __ 2427 2433 2428 2434 (** val good_if_rect_Type0 : 2429 2435 params > AST.ident List.list > joint_internal_function > (__ > __ > 2430 __ > __ > __ > 'a1) > 'a1 **)2436 __ > __ > __ > __ > 'a1) > 'a1 **) 2431 2437 let rec good_if_rect_Type0 p globals def h_mk_good_if = 2432 h_mk_good_if __ __ __ __ __ 2438 h_mk_good_if __ __ __ __ __ __ 2433 2439 2434 2440 (** val good_if_inv_rect_Type4 : 2435 2441 params > AST.ident List.list > joint_internal_function > (__ > __ > 2436 __ > __ > __ > __ > 'a1) > 'a1 **)2442 __ > __ > __ > __ > __ > 'a1) > 'a1 **) 2437 2443 let good_if_inv_rect_Type4 x1 x2 x3 h1 = 2438 2444 let hcut = good_if_rect_Type4 x1 x2 x3 h1 in hcut __ … … 2440 2446 (** val good_if_inv_rect_Type3 : 2441 2447 params > AST.ident List.list > joint_internal_function > (__ > __ > 2442 __ > __ > __ > __ > 'a1) > 'a1 **)2448 __ > __ > __ > __ > __ > 'a1) > 'a1 **) 2443 2449 let good_if_inv_rect_Type3 x1 x2 x3 h1 = 2444 2450 let hcut = good_if_rect_Type3 x1 x2 x3 h1 in hcut __ … … 2446 2452 (** val good_if_inv_rect_Type2 : 2447 2453 params > AST.ident List.list > joint_internal_function > (__ > __ > 2448 __ > __ > __ > __ > 'a1) > 'a1 **)2454 __ > __ > __ > __ > __ > 'a1) > 'a1 **) 2449 2455 let good_if_inv_rect_Type2 x1 x2 x3 h1 = 2450 2456 let hcut = good_if_rect_Type2 x1 x2 x3 h1 in hcut __ … … 2452 2458 (** val good_if_inv_rect_Type1 : 2453 2459 params > AST.ident List.list > joint_internal_function > (__ > __ > 2454 __ > __ > __ > __ > 'a1) > 'a1 **)2460 __ > __ > __ > __ > __ > 'a1) > 'a1 **) 2455 2461 let good_if_inv_rect_Type1 x1 x2 x3 h1 = 2456 2462 let hcut = good_if_rect_Type1 x1 x2 x3 h1 in hcut __ … … 2458 2464 (** val good_if_inv_rect_Type0 : 2459 2465 params > AST.ident List.list > joint_internal_function > (__ > __ > 2460 __ > __ > __ > __ > 'a1) > 'a1 **)2466 __ > __ > __ > __ > __ > 'a1) > 'a1 **) 2461 2467 let good_if_inv_rect_Type0 x1 x2 x3 h1 = 2462 2468 let hcut = good_if_rect_Type0 x1 x2 x3 h1 in hcut __ 2463 2464 (** val good_if_discr :2465 params > AST.ident List.list > joint_internal_function > __ **)2466 let good_if_discr a1 a2 a3 =2467 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH > dH __ __ __ __ __)) __2468 2469 2469 2470 (** val good_if_jmdiscr : 2470 2471 params > AST.ident List.list > joint_internal_function > __ **) 2471 2472 let good_if_jmdiscr a1 a2 a3 = 2472 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH > dH __ __ __ __ __ )) __2473 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH > dH __ __ __ __ __ __)) __ 2473 2474 2474 2475 type joint_closed_internal_function = joint_internal_function Types.sig0
Note: See TracChangeset
for help on using the changeset viewer.