 Timestamp:
 Mar 15, 2013, 5:52:58 PM (8 years ago)
 Location:
 extracted
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

extracted/blocks.ml
r2797 r2882 145 145 Joint.params > AST.ident List.list > Joint.joint_seq List.list > 146 146 step_block **) 147 let ensure_step_block p g l = 148 match split_on_last l with 149  Types.None > 150 { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x > 151 Joint.Step_seq 152 (Joint.nOOP (Joint.stmt_pars__o__uns_pars__o__u_pars p) g)) }; 153 Types.snd = List.Nil } 154  Types.Some pr > 155 { Types.fst = { Types.fst = (add_dummy_variance pr.Types.fst); 156 Types.snd = (fun x > Joint.Step_seq pr.Types.snd) }; Types.snd = 157 List.Nil } 147 let ensure_step_block p g = function 148  List.Nil > 149 { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x > Joint.Step_seq 150 (Joint.nOOP (Joint.stmt_pars__o__uns_pars__o__u_pars p) g)) }; 151 Types.snd = List.Nil } 152  List.Cons (hd, tl) > 153 { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x > Joint.Step_seq 154 hd) }; Types.snd = tl } 158 155 159 156 (** val map_eval : ('a1 > 'a2) List.list > 'a1 > 'a2 List.list **) 
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 __ __ 
extracted/rTLToERTL.ml
r2867 r2882 246 246 Types.snd = pr.Types.snd }) sregs)) 247 247 (List.append (List.Cons ((Joint.PUSH 248 (Obj.magic (Joint.psd_argument_from_reg sra h))), (List.Cons249 ((Joint.PUSH (Obj.magic (Joint.psd_argument_from_reg sra l))),248 (Obj.magic (Joint.psd_argument_from_reg sral))), (List.Cons 249 ((Joint.PUSH (Obj.magic (Joint.psd_argument_from_reg srah))), 250 250 (List.Cons 251 251 ((ERTL.ertl_seq_joint globals (Obj.magic ERTL.Ertl_del_frame)), … … 263 263 ((let x = ERTL.ertl_seq_joint globals (Obj.magic ERTL.Ertl_new_frame) 264 264 in 265 x), (List.Cons ((Joint.POP (Obj.magic sra l)), (List.Cons ((Joint.POP266 (Obj.magic sra h)), List.Nil))))))265 x), (List.Cons ((Joint.POP (Obj.magic srah)), (List.Cons ((Joint.POP 266 (Obj.magic sral)), List.Nil)))))) 267 267 (List.append (save_hdws globals sregs) 268 268 (get_params globals tmpr addr1 addr2 params)) 
extracted/toCminor.ml
r2827 r2882 198 198 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 199 199 let rec var_type_rect_Type4 h_Global h_Stack h_Local = function 200  Global x_ 13042 > h_Global x_13042201  Stack x_ 13043 > h_Stack x_13043200  Global x_634 > h_Global x_634 201  Stack x_635 > h_Stack x_635 202 202  Local > h_Local 203 203 … … 205 205 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 206 206 let rec var_type_rect_Type5 h_Global h_Stack h_Local = function 207  Global x_ 13048 > h_Global x_13048208  Stack x_ 13049 > h_Stack x_13049207  Global x_640 > h_Global x_640 208  Stack x_641 > h_Stack x_641 209 209  Local > h_Local 210 210 … … 212 212 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 213 213 let rec var_type_rect_Type3 h_Global h_Stack h_Local = function 214  Global x_ 13054 > h_Global x_13054215  Stack x_ 13055 > h_Stack x_13055214  Global x_646 > h_Global x_646 215  Stack x_647 > h_Stack x_647 216 216  Local > h_Local 217 217 … … 219 219 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 220 220 let rec var_type_rect_Type2 h_Global h_Stack h_Local = function 221  Global x_ 13060 > h_Global x_13060222  Stack x_ 13061 > h_Stack x_13061221  Global x_652 > h_Global x_652 222  Stack x_653 > h_Stack x_653 223 223  Local > h_Local 224 224 … … 226 226 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 227 227 let rec var_type_rect_Type1 h_Global h_Stack h_Local = function 228  Global x_ 13066 > h_Global x_13066229  Stack x_ 13067 > h_Stack x_13067228  Global x_658 > h_Global x_658 229  Stack x_659 > h_Stack x_659 230 230  Local > h_Local 231 231 … … 233 233 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 234 234 let rec var_type_rect_Type0 h_Global h_Stack h_Local = function 235  Global x_ 13072 > h_Global x_13072236  Stack x_ 13073 > h_Stack x_13073235  Global x_664 > h_Global x_664 236  Stack x_665 > h_Stack x_665 237 237  Local > h_Local 238 238 … … 1221 1221 let rec destination_rect_Type4 vars h_IdDest h_MemDest = function 1222 1222  IdDest (id, ty) > h_IdDest id ty __ 1223  MemDest x_ 14528 > h_MemDest x_145281223  MemDest x_712 > h_MemDest x_712 1224 1224 1225 1225 (** val destination_rect_Type5 : … … 1228 1228 let rec destination_rect_Type5 vars h_IdDest h_MemDest = function 1229 1229  IdDest (id, ty) > h_IdDest id ty __ 1230  MemDest x_ 14533 > h_MemDest x_145331230  MemDest x_717 > h_MemDest x_717 1231 1231 1232 1232 (** val destination_rect_Type3 : … … 1235 1235 let rec destination_rect_Type3 vars h_IdDest h_MemDest = function 1236 1236  IdDest (id, ty) > h_IdDest id ty __ 1237  MemDest x_ 14538 > h_MemDest x_145381237  MemDest x_722 > h_MemDest x_722 1238 1238 1239 1239 (** val destination_rect_Type2 : … … 1242 1242 let rec destination_rect_Type2 vars h_IdDest h_MemDest = function 1243 1243  IdDest (id, ty) > h_IdDest id ty __ 1244  MemDest x_ 14543 > h_MemDest x_145431244  MemDest x_727 > h_MemDest x_727 1245 1245 1246 1246 (** val destination_rect_Type1 : … … 1249 1249 let rec destination_rect_Type1 vars h_IdDest h_MemDest = function 1250 1250  IdDest (id, ty) > h_IdDest id ty __ 1251  MemDest x_ 14548 > h_MemDest x_145481251  MemDest x_732 > h_MemDest x_732 1252 1252 1253 1253 (** val destination_rect_Type0 : … … 1256 1256 let rec destination_rect_Type0 vars h_IdDest h_MemDest = function 1257 1257  IdDest (id, ty) > h_IdDest id ty __ 1258  MemDest x_ 14553 > h_MemDest x_145531258  MemDest x_737 > h_MemDest x_737 1259 1259 1260 1260 (** val destination_inv_rect_Type4 : … … 1382 1382 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1383 1383 'a1) > labgen > 'a1 **) 1384 let rec labgen_rect_Type4 h_mk_labgen x_14588 = 1385 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1386 x_14588 1384 let rec labgen_rect_Type4 h_mk_labgen x_772 = 1385 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_772 1387 1386 in 1388 1387 h_mk_labgen labuniverse0 label_genlist0 __ … … 1391 1390 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1392 1391 'a1) > labgen > 'a1 **) 1393 let rec labgen_rect_Type5 h_mk_labgen x_14590 = 1394 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1395 x_14590 1392 let rec labgen_rect_Type5 h_mk_labgen x_774 = 1393 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_774 1396 1394 in 1397 1395 h_mk_labgen labuniverse0 label_genlist0 __ … … 1400 1398 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1401 1399 'a1) > labgen > 'a1 **) 1402 let rec labgen_rect_Type3 h_mk_labgen x_14592 = 1403 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1404 x_14592 1400 let rec labgen_rect_Type3 h_mk_labgen x_776 = 1401 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_776 1405 1402 in 1406 1403 h_mk_labgen labuniverse0 label_genlist0 __ … … 1409 1406 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1410 1407 'a1) > labgen > 'a1 **) 1411 let rec labgen_rect_Type2 h_mk_labgen x_14594 = 1412 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1413 x_14594 1408 let rec labgen_rect_Type2 h_mk_labgen x_778 = 1409 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_778 1414 1410 in 1415 1411 h_mk_labgen labuniverse0 label_genlist0 __ … … 1418 1414 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1419 1415 'a1) > labgen > 'a1 **) 1420 let rec labgen_rect_Type1 h_mk_labgen x_14596 = 1421 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1422 x_14596 1416 let rec labgen_rect_Type1 h_mk_labgen x_780 = 1417 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_780 1423 1418 in 1424 1419 h_mk_labgen labuniverse0 label_genlist0 __ … … 1427 1422 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1428 1423 'a1) > labgen > 'a1 **) 1429 let rec labgen_rect_Type0 h_mk_labgen x_14598 = 1430 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1431 x_14598 1424 let rec labgen_rect_Type0 h_mk_labgen x_782 = 1425 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_782 1432 1426 in 1433 1427 h_mk_labgen labuniverse0 label_genlist0 __ … … 1554 1548 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1555 1549 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1556 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_ 14614=1557 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 14614in1550 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_798 = 1551 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_798 in 1558 1552 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1559 1553 … … 1561 1555 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1562 1556 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1563 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_ 14616=1564 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 14616in1557 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_800 = 1558 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_800 in 1565 1559 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1566 1560 … … 1568 1562 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1569 1563 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1570 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_ 14618=1571 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 14618in1564 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_802 = 1565 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_802 in 1572 1566 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1573 1567 … … 1575 1569 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1576 1570 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1577 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_ 14620=1578 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 14620in1571 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_804 = 1572 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_804 in 1579 1573 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1580 1574 … … 1582 1576 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1583 1577 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1584 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_ 14622=1585 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 14622in1578 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_806 = 1579 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_806 in 1586 1580 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1587 1581 … … 1589 1583 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1590 1584 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1591 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_ 14624=1592 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 14624in1585 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_808 = 1586 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_808 in 1593 1587 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1594 1588 … … 1674 1668 let rec convert_flag_rect_Type4 h_DoNotConvert h_ConvertTo = function 1675 1669  DoNotConvert > h_DoNotConvert 1676  ConvertTo (x_ 14646, x_14645) > h_ConvertTo x_14646 x_146451670  ConvertTo (x_830, x_829) > h_ConvertTo x_830 x_829 1677 1671 1678 1672 (** val convert_flag_rect_Type5 : … … 1681 1675 let rec convert_flag_rect_Type5 h_DoNotConvert h_ConvertTo = function 1682 1676  DoNotConvert > h_DoNotConvert 1683  ConvertTo (x_ 14651, x_14650) > h_ConvertTo x_14651 x_146501677  ConvertTo (x_835, x_834) > h_ConvertTo x_835 x_834 1684 1678 1685 1679 (** val convert_flag_rect_Type3 : … … 1688 1682 let rec convert_flag_rect_Type3 h_DoNotConvert h_ConvertTo = function 1689 1683  DoNotConvert > h_DoNotConvert 1690  ConvertTo (x_ 14656, x_14655) > h_ConvertTo x_14656 x_146551684  ConvertTo (x_840, x_839) > h_ConvertTo x_840 x_839 1691 1685 1692 1686 (** val convert_flag_rect_Type2 : … … 1695 1689 let rec convert_flag_rect_Type2 h_DoNotConvert h_ConvertTo = function 1696 1690  DoNotConvert > h_DoNotConvert 1697  ConvertTo (x_ 14661, x_14660) > h_ConvertTo x_14661 x_146601691  ConvertTo (x_845, x_844) > h_ConvertTo x_845 x_844 1698 1692 1699 1693 (** val convert_flag_rect_Type1 : … … 1702 1696 let rec convert_flag_rect_Type1 h_DoNotConvert h_ConvertTo = function 1703 1697  DoNotConvert > h_DoNotConvert 1704  ConvertTo (x_ 14666, x_14665) > h_ConvertTo x_14666 x_146651698  ConvertTo (x_850, x_849) > h_ConvertTo x_850 x_849 1705 1699 1706 1700 (** val convert_flag_rect_Type0 : … … 1709 1703 let rec convert_flag_rect_Type0 h_DoNotConvert h_ConvertTo = function 1710 1704  DoNotConvert > h_DoNotConvert 1711  ConvertTo (x_ 14671, x_14670) > h_ConvertTo x_14671 x_146701705  ConvertTo (x_855, x_854) > h_ConvertTo x_855 x_854 1712 1706 1713 1707 (** val convert_flag_inv_rect_Type4 : … … 1832 1826 Obj.magic (Errors.OK { Types.fst = { Types.fst = uv2; 1833 1827 Types.snd = ul }; Types.snd = (Cminor_syntax.St_seq 1834 ((Cminor_syntax.St_store (AST.ASTptr, (Cminor_syntax.Id 1835 (AST.ASTptr, tmp2)), (Types.pi1 e1'))), 1836 (Cminor_syntax.St_seq ((Cminor_syntax.St_call ((Types.Some 1837 { Types.fst = tmp; Types.snd = 1838 (Csyntax.typ_of_type (Csyntax.typeof e1)) }), 1828 ((Cminor_syntax.St_assign (AST.ASTptr, tmp2, 1829 (Types.pi1 e1'))), (Cminor_syntax.St_seq 1830 ((Cminor_syntax.St_call ((Types.Some { Types.fst = tmp; 1831 Types.snd = (Csyntax.typ_of_type (Csyntax.typeof e1)) }), 1839 1832 (Types.pi1 ef'0), (Types.pi1 args'))), 1840 1833 (Cminor_syntax.St_store 1841 1834 ((Csyntax.typ_of_type (Csyntax.typeof e1)), 1842 ( Types.pi1 e1'), (Cminor_syntax.Id1835 (Cminor_syntax.Id (AST.ASTptr, tmp2)), (Cminor_syntax.Id 1843 1836 ((Csyntax.typ_of_type (Csyntax.typeof e1)), tmp)))))))) }))) 1844 1837 __)) __))))) … … 2044 2037 Obj.magic 2045 2038 (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su) 2046 (fun eta24 36>2047 let result = eta24 36in2039 (fun eta244 > 2040 let result = eta244 in 2048 2041 (let { Types.fst = fgens1; Types.snd = s0 } = result in 2049 2042 (fun _ >
Note: See TracChangeset
for help on using the changeset viewer.