Changeset 2882 for extracted/joint_semantics.ml
 Timestamp:
 Mar 15, 2013, 5:52:58 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/joint_semantics.ml
r2873 r2882 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_ 25710=143 let rec genv_gen_rect_Type4 globals h_mk_genv_gen x_3 = 144 144 let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label = 145 get_pc_from_label0 } = x_ 25710145 get_pc_from_label0 } = x_3 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_ 25712=153 let rec genv_gen_rect_Type5 globals h_mk_genv_gen x_5 = 154 154 let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label = 155 get_pc_from_label0 } = x_ 25712155 get_pc_from_label0 } = x_5 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_ 25714=163 let rec genv_gen_rect_Type3 globals h_mk_genv_gen x_7 = 164 164 let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label = 165 get_pc_from_label0 } = x_ 25714165 get_pc_from_label0 } = x_7 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_ 25716=173 let rec genv_gen_rect_Type2 globals h_mk_genv_gen x_9 = 174 174 let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label = 175 get_pc_from_label0 } = x_ 25716175 get_pc_from_label0 } = x_9 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_ 25718=183 let rec genv_gen_rect_Type1 globals h_mk_genv_gen x_11 = 184 184 let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label = 185 get_pc_from_label0 } = x_ 25718185 get_pc_from_label0 } = x_11 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_ 25720=193 let rec genv_gen_rect_Type0 globals h_mk_genv_gen x_13 = 194 194 let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label = 195 get_pc_from_label0 } = x_ 25720195 get_pc_from_label0 } = x_13 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_ 25740=343 let rec sem_state_params_rect_Type4 h_mk_sem_state_params x_33 = 344 344 let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp = 345 load_sp0; save_sp = save_sp0 } = x_ 25740345 load_sp0; save_sp = save_sp0 } = x_33 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_ 25742=353 let rec sem_state_params_rect_Type5 h_mk_sem_state_params x_35 = 354 354 let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp = 355 load_sp0; save_sp = save_sp0 } = x_ 25742355 load_sp0; save_sp = save_sp0 } = x_35 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_ 25744=363 let rec sem_state_params_rect_Type3 h_mk_sem_state_params x_37 = 364 364 let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp = 365 load_sp0; save_sp = save_sp0 } = x_ 25744365 load_sp0; save_sp = save_sp0 } = x_37 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_ 25746=373 let rec sem_state_params_rect_Type2 h_mk_sem_state_params x_39 = 374 374 let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp = 375 load_sp0; save_sp = save_sp0 } = x_ 25746375 load_sp0; save_sp = save_sp0 } = x_39 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_ 25748=383 let rec sem_state_params_rect_Type1 h_mk_sem_state_params x_41 = 384 384 let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp = 385 load_sp0; save_sp = save_sp0 } = x_ 25748385 load_sp0; save_sp = save_sp0 } = x_41 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_ 25750=393 let rec sem_state_params_rect_Type0 h_mk_sem_state_params x_43 = 394 394 let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp = 395 load_sp0; save_sp = save_sp0 } = x_ 25750395 load_sp0; save_sp = save_sp0 } = x_43 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_ 25776 > h_one_is x_25776475  Both_is (x_ 25778, x_25777) > h_both_is x_25778 x_25777474  One_is x_69 > h_one_is x_69 475  Both_is (x_71, x_70) > h_both_is x_71 x_70 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_ 25783 > h_one_is x_25783483  Both_is (x_ 25785, x_25784) > h_both_is x_25785 x_25784482  One_is x_76 > h_one_is x_76 483  Both_is (x_78, x_77) > h_both_is x_78 x_77 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_ 25790 > h_one_is x_25790491  Both_is (x_ 25792, x_25791) > h_both_is x_25792 x_25791490  One_is x_83 > h_one_is x_83 491  Both_is (x_85, x_84) > h_both_is x_85 x_84 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_ 25797 > h_one_is x_25797499  Both_is (x_ 25799, x_25798) > h_both_is x_25799 x_25798498  One_is x_90 > h_one_is x_90 499  Both_is (x_92, x_91) > h_both_is x_92 x_91 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_ 25804 > h_one_is x_25804507  Both_is (x_ 25806, x_25805) > h_both_is x_25806 x_25805506  One_is x_97 > h_one_is x_97 507  Both_is (x_99, x_98) > h_both_is x_99 x_98 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_ 25811 > h_one_is x_25811515  Both_is (x_ 25813, x_25812) > h_both_is x_25813 x_25812514  One_is x_104 > h_one_is x_104 515  Both_is (x_106, x_105) > h_both_is x_106 x_105 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_ 25861=598 let rec state_rect_Type4 semp h_mk_state x_154 = 599 599 let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0; 600 m = m0 } = x_ 25861600 m = m0 } = x_154 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_ 25863=607 let rec state_rect_Type5 semp h_mk_state x_156 = 608 608 let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0; 609 m = m0 } = x_ 25863609 m = m0 } = x_156 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_ 25865=616 let rec state_rect_Type3 semp h_mk_state x_158 = 617 617 let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0; 618 m = m0 } = x_ 25865618 m = m0 } = x_158 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_ 25867=625 let rec state_rect_Type2 semp h_mk_state x_160 = 626 626 let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0; 627 m = m0 } = x_ 25867627 m = m0 } = x_160 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_ 25869=634 let rec state_rect_Type1 semp h_mk_state x_162 = 635 635 let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0; 636 m = m0 } = x_ 25869636 m = m0 } = x_162 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_ 25871=643 let rec state_rect_Type0 semp h_mk_state x_164 = 644 644 let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0; 645 m = m0 } = x_ 25871645 m = m0 } = x_164 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_ 25887=722 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_ 25887in721 let rec state_pc_rect_Type4 semp h_mk_state_pc x_180 = 722 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_180 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_ 25889=729 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_ 25889in728 let rec state_pc_rect_Type5 semp h_mk_state_pc x_182 = 729 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_182 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_ 25891=736 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_ 25891in735 let rec state_pc_rect_Type3 semp h_mk_state_pc x_184 = 736 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_184 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_ 25893=743 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_ 25893in742 let rec state_pc_rect_Type2 semp h_mk_state_pc x_186 = 743 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_186 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_ 25895=750 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_ 25895in749 let rec state_pc_rect_Type1 semp h_mk_state_pc x_188 = 750 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_188 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_ 25897=757 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_ 25897in756 let rec state_pc_rect_Type0 semp h_mk_state_pc x_190 = 757 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_190 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_2 5952=1096 let rec sem_unserialized_params_rect_Type4 uns_pars h_mk_sem_unserialized_params x_245 = 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_2 59521108 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_245 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_2 5954=1137 let rec sem_unserialized_params_rect_Type5 uns_pars h_mk_sem_unserialized_params x_247 = 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_2 59541149 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_247 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_2 5956=1178 let rec sem_unserialized_params_rect_Type3 uns_pars h_mk_sem_unserialized_params x_249 = 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_2 59561190 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_249 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 958=1219 let rec sem_unserialized_params_rect_Type2 uns_pars h_mk_sem_unserialized_params x_251 = 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 9581231 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_251 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 960=1260 let rec sem_unserialized_params_rect_Type1 uns_pars h_mk_sem_unserialized_params x_253 = 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 9601272 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_253 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 962=1301 let rec sem_unserialized_params_rect_Type0 uns_pars h_mk_sem_unserialized_params x_255 = 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 9621313 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_255 1314 1314 in 1315 1315 h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0 … … 1746 1746 Monad.m_bind0 (Monad.max_def Errors.res0) 1747 1747 (Obj.magic 1748 (ByteValues.pc_of_bevals (List.Cons (addr h, (List.Cons (addrl,1748 (ByteValues.pc_of_bevals (List.Cons (addrl, (List.Cons (addrh, 1749 1749 List.Nil)))))) (fun pr > 1750 1750 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = st''; … … 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_ 26032=1763 let rec sem_params_rect_Type4 h_mk_sem_params x_325 = 1764 1764 let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0; 1765 point_of_offset = point_of_offset0 } = x_ 260321765 point_of_offset = point_of_offset0 } = x_325 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_ 26034=1773 let rec sem_params_rect_Type5 h_mk_sem_params x_327 = 1774 1774 let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0; 1775 point_of_offset = point_of_offset0 } = x_ 260341775 point_of_offset = point_of_offset0 } = x_327 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_ 26036=1783 let rec sem_params_rect_Type3 h_mk_sem_params x_329 = 1784 1784 let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0; 1785 point_of_offset = point_of_offset0 } = x_ 260361785 point_of_offset = point_of_offset0 } = x_329 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_ 26038=1793 let rec sem_params_rect_Type2 h_mk_sem_params x_331 = 1794 1794 let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0; 1795 point_of_offset = point_of_offset0 } = x_ 260381795 point_of_offset = point_of_offset0 } = x_331 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_ 26040=1803 let rec sem_params_rect_Type1 h_mk_sem_params x_333 = 1804 1804 let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0; 1805 point_of_offset = point_of_offset0 } = x_ 260401805 point_of_offset = point_of_offset0 } = x_333 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_ 26042=1813 let rec sem_params_rect_Type0 h_mk_sem_params x_335 = 1814 1814 let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0; 1815 point_of_offset = point_of_offset0 } = x_ 260421815 point_of_offset = point_of_offset0 } = x_335 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.