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

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/joint_semantics.ml
r2867 r2873 141 141 (AST.ident > Nat.nat Types.option) > (AST.ident > Graphs.label > 142 142 ByteValues.program_counter Errors.res) > 'a2) > 'a1 genv_gen > 'a2 **) 143 let rec genv_gen_rect_Type4 globals h_mk_genv_gen x_25 541=143 let rec genv_gen_rect_Type4 globals h_mk_genv_gen x_25710 = 144 144 let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label = 145 get_pc_from_label0 } = x_25 541145 get_pc_from_label0 } = x_25710 146 146 in 147 147 h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0 … … 151 151 (AST.ident > Nat.nat Types.option) > (AST.ident > Graphs.label > 152 152 ByteValues.program_counter Errors.res) > 'a2) > 'a1 genv_gen > 'a2 **) 153 let rec genv_gen_rect_Type5 globals h_mk_genv_gen x_25 543=153 let rec genv_gen_rect_Type5 globals h_mk_genv_gen x_25712 = 154 154 let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label = 155 get_pc_from_label0 } = x_25 543155 get_pc_from_label0 } = x_25712 156 156 in 157 157 h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0 … … 161 161 (AST.ident > Nat.nat Types.option) > (AST.ident > Graphs.label > 162 162 ByteValues.program_counter Errors.res) > 'a2) > 'a1 genv_gen > 'a2 **) 163 let rec genv_gen_rect_Type3 globals h_mk_genv_gen x_25 545=163 let rec genv_gen_rect_Type3 globals h_mk_genv_gen x_25714 = 164 164 let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label = 165 get_pc_from_label0 } = x_25 545165 get_pc_from_label0 } = x_25714 166 166 in 167 167 h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0 … … 171 171 (AST.ident > Nat.nat Types.option) > (AST.ident > Graphs.label > 172 172 ByteValues.program_counter Errors.res) > 'a2) > 'a1 genv_gen > 'a2 **) 173 let rec genv_gen_rect_Type2 globals h_mk_genv_gen x_25 547=173 let rec genv_gen_rect_Type2 globals h_mk_genv_gen x_25716 = 174 174 let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label = 175 get_pc_from_label0 } = x_25 547175 get_pc_from_label0 } = x_25716 176 176 in 177 177 h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0 … … 181 181 (AST.ident > Nat.nat Types.option) > (AST.ident > Graphs.label > 182 182 ByteValues.program_counter Errors.res) > 'a2) > 'a1 genv_gen > 'a2 **) 183 let rec genv_gen_rect_Type1 globals h_mk_genv_gen x_25 549=183 let rec genv_gen_rect_Type1 globals h_mk_genv_gen x_25718 = 184 184 let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label = 185 get_pc_from_label0 } = x_25 549185 get_pc_from_label0 } = x_25718 186 186 in 187 187 h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0 … … 191 191 (AST.ident > Nat.nat Types.option) > (AST.ident > Graphs.label > 192 192 ByteValues.program_counter Errors.res) > 'a2) > 'a1 genv_gen > 'a2 **) 193 let rec genv_gen_rect_Type0 globals h_mk_genv_gen x_25 551=193 let rec genv_gen_rect_Type0 globals h_mk_genv_gen x_25720 = 194 194 let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label = 195 get_pc_from_label0 } = x_25 551195 get_pc_from_label0 } = x_25720 196 196 in 197 197 h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0 … … 341 341 ByteValues.xpointer Errors.res) > (__ > ByteValues.xpointer > __) > 342 342 'a1) > sem_state_params > 'a1 **) 343 let rec sem_state_params_rect_Type4 h_mk_sem_state_params x_25 571=343 let rec sem_state_params_rect_Type4 h_mk_sem_state_params x_25740 = 344 344 let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp = 345 load_sp0; save_sp = save_sp0 } = x_25 571345 load_sp0; save_sp = save_sp0 } = x_25740 346 346 in 347 347 h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0 … … 351 351 ByteValues.xpointer Errors.res) > (__ > ByteValues.xpointer > __) > 352 352 'a1) > sem_state_params > 'a1 **) 353 let rec sem_state_params_rect_Type5 h_mk_sem_state_params x_25 573=353 let rec sem_state_params_rect_Type5 h_mk_sem_state_params x_25742 = 354 354 let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp = 355 load_sp0; save_sp = save_sp0 } = x_25 573355 load_sp0; save_sp = save_sp0 } = x_25742 356 356 in 357 357 h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0 … … 361 361 ByteValues.xpointer Errors.res) > (__ > ByteValues.xpointer > __) > 362 362 'a1) > sem_state_params > 'a1 **) 363 let rec sem_state_params_rect_Type3 h_mk_sem_state_params x_25 575=363 let rec sem_state_params_rect_Type3 h_mk_sem_state_params x_25744 = 364 364 let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp = 365 load_sp0; save_sp = save_sp0 } = x_25 575365 load_sp0; save_sp = save_sp0 } = x_25744 366 366 in 367 367 h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0 … … 371 371 ByteValues.xpointer Errors.res) > (__ > ByteValues.xpointer > __) > 372 372 'a1) > sem_state_params > 'a1 **) 373 let rec sem_state_params_rect_Type2 h_mk_sem_state_params x_25 577=373 let rec sem_state_params_rect_Type2 h_mk_sem_state_params x_25746 = 374 374 let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp = 375 load_sp0; save_sp = save_sp0 } = x_25 577375 load_sp0; save_sp = save_sp0 } = x_25746 376 376 in 377 377 h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0 … … 381 381 ByteValues.xpointer Errors.res) > (__ > ByteValues.xpointer > __) > 382 382 'a1) > sem_state_params > 'a1 **) 383 let rec sem_state_params_rect_Type1 h_mk_sem_state_params x_25 579=383 let rec sem_state_params_rect_Type1 h_mk_sem_state_params x_25748 = 384 384 let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp = 385 load_sp0; save_sp = save_sp0 } = x_25 579385 load_sp0; save_sp = save_sp0 } = x_25748 386 386 in 387 387 h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0 … … 391 391 ByteValues.xpointer Errors.res) > (__ > ByteValues.xpointer > __) > 392 392 'a1) > sem_state_params > 'a1 **) 393 let rec sem_state_params_rect_Type0 h_mk_sem_state_params x_25 581=393 let rec sem_state_params_rect_Type0 h_mk_sem_state_params x_25750 = 394 394 let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp = 395 load_sp0; save_sp = save_sp0 } = x_25 581395 load_sp0; save_sp = save_sp0 } = x_25750 396 396 in 397 397 h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0 … … 472 472 let rec internal_stack_rect_Type4 h_empty_is h_one_is h_both_is = function 473 473  Empty_is > h_empty_is 474  One_is x_25 607 > h_one_is x_25607475  Both_is (x_25 609, x_25608) > h_both_is x_25609 x_25608474  One_is x_25776 > h_one_is x_25776 475  Both_is (x_25778, x_25777) > h_both_is x_25778 x_25777 476 476 477 477 (** val internal_stack_rect_Type5 : … … 480 480 let rec internal_stack_rect_Type5 h_empty_is h_one_is h_both_is = function 481 481  Empty_is > h_empty_is 482  One_is x_25 614 > h_one_is x_25614483  Both_is (x_25 616, x_25615) > h_both_is x_25616 x_25615482  One_is x_25783 > h_one_is x_25783 483  Both_is (x_25785, x_25784) > h_both_is x_25785 x_25784 484 484 485 485 (** val internal_stack_rect_Type3 : … … 488 488 let rec internal_stack_rect_Type3 h_empty_is h_one_is h_both_is = function 489 489  Empty_is > h_empty_is 490  One_is x_25 621 > h_one_is x_25621491  Both_is (x_25 623, x_25622) > h_both_is x_25623 x_25622490  One_is x_25790 > h_one_is x_25790 491  Both_is (x_25792, x_25791) > h_both_is x_25792 x_25791 492 492 493 493 (** val internal_stack_rect_Type2 : … … 496 496 let rec internal_stack_rect_Type2 h_empty_is h_one_is h_both_is = function 497 497  Empty_is > h_empty_is 498  One_is x_25 628 > h_one_is x_25628499  Both_is (x_25 630, x_25629) > h_both_is x_25630 x_25629498  One_is x_25797 > h_one_is x_25797 499  Both_is (x_25799, x_25798) > h_both_is x_25799 x_25798 500 500 501 501 (** val internal_stack_rect_Type1 : … … 504 504 let rec internal_stack_rect_Type1 h_empty_is h_one_is h_both_is = function 505 505  Empty_is > h_empty_is 506  One_is x_25 635 > h_one_is x_25635507  Both_is (x_25 637, x_25636) > h_both_is x_25637 x_25636506  One_is x_25804 > h_one_is x_25804 507  Both_is (x_25806, x_25805) > h_both_is x_25806 x_25805 508 508 509 509 (** val internal_stack_rect_Type0 : … … 512 512 let rec internal_stack_rect_Type0 h_empty_is h_one_is h_both_is = function 513 513  Empty_is > h_empty_is 514  One_is x_25 642 > h_one_is x_25642515  Both_is (x_25 644, x_25643) > h_both_is x_25644 x_25643514  One_is x_25811 > h_one_is x_25811 515  Both_is (x_25813, x_25812) > h_both_is x_25813 x_25812 516 516 517 517 (** val internal_stack_inv_rect_Type4 : … … 596 596 sem_state_params > (__ Types.option > internal_stack > 597 597 ByteValues.bebit > __ > BEMem.bemem > 'a1) > state > 'a1 **) 598 let rec state_rect_Type4 semp h_mk_state x_25 692=598 let rec state_rect_Type4 semp h_mk_state x_25861 = 599 599 let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0; 600 m = m0 } = x_25 692600 m = m0 } = x_25861 601 601 in 602 602 h_mk_state st_frms0 istack0 carry0 regs0 m0 … … 605 605 sem_state_params > (__ Types.option > internal_stack > 606 606 ByteValues.bebit > __ > BEMem.bemem > 'a1) > state > 'a1 **) 607 let rec state_rect_Type5 semp h_mk_state x_25 694=607 let rec state_rect_Type5 semp h_mk_state x_25863 = 608 608 let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0; 609 m = m0 } = x_25 694609 m = m0 } = x_25863 610 610 in 611 611 h_mk_state st_frms0 istack0 carry0 regs0 m0 … … 614 614 sem_state_params > (__ Types.option > internal_stack > 615 615 ByteValues.bebit > __ > BEMem.bemem > 'a1) > state > 'a1 **) 616 let rec state_rect_Type3 semp h_mk_state x_25 696=616 let rec state_rect_Type3 semp h_mk_state x_25865 = 617 617 let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0; 618 m = m0 } = x_25 696618 m = m0 } = x_25865 619 619 in 620 620 h_mk_state st_frms0 istack0 carry0 regs0 m0 … … 623 623 sem_state_params > (__ Types.option > internal_stack > 624 624 ByteValues.bebit > __ > BEMem.bemem > 'a1) > state > 'a1 **) 625 let rec state_rect_Type2 semp h_mk_state x_25 698=625 let rec state_rect_Type2 semp h_mk_state x_25867 = 626 626 let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0; 627 m = m0 } = x_25 698627 m = m0 } = x_25867 628 628 in 629 629 h_mk_state st_frms0 istack0 carry0 regs0 m0 … … 632 632 sem_state_params > (__ Types.option > internal_stack > 633 633 ByteValues.bebit > __ > BEMem.bemem > 'a1) > state > 'a1 **) 634 let rec state_rect_Type1 semp h_mk_state x_25 700=634 let rec state_rect_Type1 semp h_mk_state x_25869 = 635 635 let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0; 636 m = m0 } = x_25 700636 m = m0 } = x_25869 637 637 in 638 638 h_mk_state st_frms0 istack0 carry0 regs0 m0 … … 641 641 sem_state_params > (__ Types.option > internal_stack > 642 642 ByteValues.bebit > __ > BEMem.bemem > 'a1) > state > 'a1 **) 643 let rec state_rect_Type0 semp h_mk_state x_25 702=643 let rec state_rect_Type0 semp h_mk_state x_25871 = 644 644 let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0; 645 m = m0 } = x_25 702645 m = m0 } = x_25871 646 646 in 647 647 h_mk_state st_frms0 istack0 carry0 regs0 m0 … … 719 719 sem_state_params > (state > ByteValues.program_counter > 720 720 ByteValues.program_counter > 'a1) > state_pc > 'a1 **) 721 let rec state_pc_rect_Type4 semp h_mk_state_pc x_25 718=722 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25 718in721 let rec state_pc_rect_Type4 semp h_mk_state_pc x_25887 = 722 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25887 in 723 723 h_mk_state_pc st_no_pc0 pc0 last_pop0 724 724 … … 726 726 sem_state_params > (state > ByteValues.program_counter > 727 727 ByteValues.program_counter > 'a1) > state_pc > 'a1 **) 728 let rec state_pc_rect_Type5 semp h_mk_state_pc x_25 720=729 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25 720in728 let rec state_pc_rect_Type5 semp h_mk_state_pc x_25889 = 729 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25889 in 730 730 h_mk_state_pc st_no_pc0 pc0 last_pop0 731 731 … … 733 733 sem_state_params > (state > ByteValues.program_counter > 734 734 ByteValues.program_counter > 'a1) > state_pc > 'a1 **) 735 let rec state_pc_rect_Type3 semp h_mk_state_pc x_25 722=736 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25 722in735 let rec state_pc_rect_Type3 semp h_mk_state_pc x_25891 = 736 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25891 in 737 737 h_mk_state_pc st_no_pc0 pc0 last_pop0 738 738 … … 740 740 sem_state_params > (state > ByteValues.program_counter > 741 741 ByteValues.program_counter > 'a1) > state_pc > 'a1 **) 742 let rec state_pc_rect_Type2 semp h_mk_state_pc x_25 724=743 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25 724in742 let rec state_pc_rect_Type2 semp h_mk_state_pc x_25893 = 743 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25893 in 744 744 h_mk_state_pc st_no_pc0 pc0 last_pop0 745 745 … … 747 747 sem_state_params > (state > ByteValues.program_counter > 748 748 ByteValues.program_counter > 'a1) > state_pc > 'a1 **) 749 let rec state_pc_rect_Type1 semp h_mk_state_pc x_25 726=750 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25 726in749 let rec state_pc_rect_Type1 semp h_mk_state_pc x_25895 = 750 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25895 in 751 751 h_mk_state_pc st_no_pc0 pc0 last_pop0 752 752 … … 754 754 sem_state_params > (state > ByteValues.program_counter > 755 755 ByteValues.program_counter > 'a1) > state_pc > 'a1 **) 756 let rec state_pc_rect_Type0 semp h_mk_state_pc x_25 728=757 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25 728in756 let rec state_pc_rect_Type0 semp h_mk_state_pc x_25897 = 757 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25897 in 758 758 h_mk_state_pc st_no_pc0 pc0 last_pop0 759 759 … … 1094 1094 state > (state, ByteValues.program_counter) Types.prod Errors.res) > 1095 1095 'a2) > 'a1 sem_unserialized_params > 'a2 **) 1096 let rec sem_unserialized_params_rect_Type4 uns_pars h_mk_sem_unserialized_params x_25 783=1096 let rec sem_unserialized_params_rect_Type4 uns_pars h_mk_sem_unserialized_params x_25952 = 1097 1097 let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ = 1098 1098 acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ = … … 1106 1106 set_result0; call_args_for_main = call_args_for_main0; 1107 1107 call_dest_for_main = call_dest_for_main0; read_result = read_result0; 1108 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_25 7831108 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_25952 1109 1109 in 1110 1110 h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0 … … 1135 1135 state > (state, ByteValues.program_counter) Types.prod Errors.res) > 1136 1136 'a2) > 'a1 sem_unserialized_params > 'a2 **) 1137 let rec sem_unserialized_params_rect_Type5 uns_pars h_mk_sem_unserialized_params x_25 785=1137 let rec sem_unserialized_params_rect_Type5 uns_pars h_mk_sem_unserialized_params x_25954 = 1138 1138 let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ = 1139 1139 acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ = … … 1147 1147 set_result0; call_args_for_main = call_args_for_main0; 1148 1148 call_dest_for_main = call_dest_for_main0; read_result = read_result0; 1149 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_25 7851149 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_25954 1150 1150 in 1151 1151 h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0 … … 1176 1176 state > (state, ByteValues.program_counter) Types.prod Errors.res) > 1177 1177 'a2) > 'a1 sem_unserialized_params > 'a2 **) 1178 let rec sem_unserialized_params_rect_Type3 uns_pars h_mk_sem_unserialized_params x_25 787=1178 let rec sem_unserialized_params_rect_Type3 uns_pars h_mk_sem_unserialized_params x_25956 = 1179 1179 let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ = 1180 1180 acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ = … … 1188 1188 set_result0; call_args_for_main = call_args_for_main0; 1189 1189 call_dest_for_main = call_dest_for_main0; read_result = read_result0; 1190 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_25 7871190 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_25956 1191 1191 in 1192 1192 h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0 … … 1217 1217 state > (state, ByteValues.program_counter) Types.prod Errors.res) > 1218 1218 'a2) > 'a1 sem_unserialized_params > 'a2 **) 1219 let rec sem_unserialized_params_rect_Type2 uns_pars h_mk_sem_unserialized_params x_25 789=1219 let rec sem_unserialized_params_rect_Type2 uns_pars h_mk_sem_unserialized_params x_25958 = 1220 1220 let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ = 1221 1221 acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ = … … 1229 1229 set_result0; call_args_for_main = call_args_for_main0; 1230 1230 call_dest_for_main = call_dest_for_main0; read_result = read_result0; 1231 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_25 7891231 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_25958 1232 1232 in 1233 1233 h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0 … … 1258 1258 state > (state, ByteValues.program_counter) Types.prod Errors.res) > 1259 1259 'a2) > 'a1 sem_unserialized_params > 'a2 **) 1260 let rec sem_unserialized_params_rect_Type1 uns_pars h_mk_sem_unserialized_params x_25 791=1260 let rec sem_unserialized_params_rect_Type1 uns_pars h_mk_sem_unserialized_params x_25960 = 1261 1261 let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ = 1262 1262 acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ = … … 1270 1270 set_result0; call_args_for_main = call_args_for_main0; 1271 1271 call_dest_for_main = call_dest_for_main0; read_result = read_result0; 1272 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_25 7911272 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_25960 1273 1273 in 1274 1274 h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0 … … 1299 1299 state > (state, ByteValues.program_counter) Types.prod Errors.res) > 1300 1300 'a2) > 'a1 sem_unserialized_params > 'a2 **) 1301 let rec sem_unserialized_params_rect_Type0 uns_pars h_mk_sem_unserialized_params x_25 793=1301 let rec sem_unserialized_params_rect_Type0 uns_pars h_mk_sem_unserialized_params x_25962 = 1302 1302 let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ = 1303 1303 acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ = … … 1311 1311 set_result0; call_args_for_main = call_args_for_main0; 1312 1312 call_dest_for_main = call_dest_for_main0; read_result = read_result0; 1313 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_25 7931313 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_25962 1314 1314 in 1315 1315 h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0 … … 1761 1761 sem_unserialized_params > (__ > Positive.pos) > (Positive.pos > __) 1762 1762 > __ > __ > 'a1) > sem_params > 'a1 **) 1763 let rec sem_params_rect_Type4 h_mk_sem_params x_2 5863=1763 let rec sem_params_rect_Type4 h_mk_sem_params x_26032 = 1764 1764 let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0; 1765 point_of_offset = point_of_offset0 } = x_2 58631765 point_of_offset = point_of_offset0 } = x_26032 1766 1766 in 1767 1767 h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __ … … 1771 1771 sem_unserialized_params > (__ > Positive.pos) > (Positive.pos > __) 1772 1772 > __ > __ > 'a1) > sem_params > 'a1 **) 1773 let rec sem_params_rect_Type5 h_mk_sem_params x_2 5865=1773 let rec sem_params_rect_Type5 h_mk_sem_params x_26034 = 1774 1774 let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0; 1775 point_of_offset = point_of_offset0 } = x_2 58651775 point_of_offset = point_of_offset0 } = x_26034 1776 1776 in 1777 1777 h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __ … … 1781 1781 sem_unserialized_params > (__ > Positive.pos) > (Positive.pos > __) 1782 1782 > __ > __ > 'a1) > sem_params > 'a1 **) 1783 let rec sem_params_rect_Type3 h_mk_sem_params x_2 5867=1783 let rec sem_params_rect_Type3 h_mk_sem_params x_26036 = 1784 1784 let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0; 1785 point_of_offset = point_of_offset0 } = x_2 58671785 point_of_offset = point_of_offset0 } = x_26036 1786 1786 in 1787 1787 h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __ … … 1791 1791 sem_unserialized_params > (__ > Positive.pos) > (Positive.pos > __) 1792 1792 > __ > __ > 'a1) > sem_params > 'a1 **) 1793 let rec sem_params_rect_Type2 h_mk_sem_params x_2 5869=1793 let rec sem_params_rect_Type2 h_mk_sem_params x_26038 = 1794 1794 let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0; 1795 point_of_offset = point_of_offset0 } = x_2 58691795 point_of_offset = point_of_offset0 } = x_26038 1796 1796 in 1797 1797 h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __ … … 1801 1801 sem_unserialized_params > (__ > Positive.pos) > (Positive.pos > __) 1802 1802 > __ > __ > 'a1) > sem_params > 'a1 **) 1803 let rec sem_params_rect_Type1 h_mk_sem_params x_2 5871=1803 let rec sem_params_rect_Type1 h_mk_sem_params x_26040 = 1804 1804 let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0; 1805 point_of_offset = point_of_offset0 } = x_2 58711805 point_of_offset = point_of_offset0 } = x_26040 1806 1806 in 1807 1807 h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __ … … 1811 1811 sem_unserialized_params > (__ > Positive.pos) > (Positive.pos > __) 1812 1812 > __ > __ > 'a1) > sem_params > 'a1 **) 1813 let rec sem_params_rect_Type0 h_mk_sem_params x_2 5873=1813 let rec sem_params_rect_Type0 h_mk_sem_params x_26042 = 1814 1814 let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0; 1815 point_of_offset = point_of_offset0 } = x_2 58731815 point_of_offset = point_of_offset0 } = x_26042 1816 1816 in 1817 1817 h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __
Note: See TracChangeset
for help on using the changeset viewer.