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

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/translateUtils.ml
r2873 r2951 1 1 open Preamble 2 3 open Extra_bool 4 5 open Coqlib 6 7 open Values 8 9 open FrontEndVal 10 11 open GenMem 12 13 open FrontEndMem 14 15 open Globalenvs 2 16 3 17 open String … … 268 282 > (Graphs.label > Joint.joint_fin_step > Blocks.bind_fin_block) > __ 269 283 > __ > __ > __ > 'a1) > b_graph_translate_data > 'a1 **) 270 let rec b_graph_translate_data_rect_Type4 src dst globals h_mk_b_graph_translate_data x_ 21201=284 let rec b_graph_translate_data_rect_Type4 src dst globals h_mk_b_graph_translate_data x_18305 = 271 285 let { init_ret = init_ret0; init_params = init_params0; init_stack_size = 272 286 init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0; 273 f_step = f_step0; f_fin = f_fin0 } = x_ 21201287 f_step = f_step0; f_fin = f_fin0 } = x_18305 274 288 in 275 289 h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0 … … 282 296 > (Graphs.label > Joint.joint_fin_step > Blocks.bind_fin_block) > __ 283 297 > __ > __ > __ > 'a1) > b_graph_translate_data > 'a1 **) 284 let rec b_graph_translate_data_rect_Type5 src dst globals h_mk_b_graph_translate_data x_ 21203=298 let rec b_graph_translate_data_rect_Type5 src dst globals h_mk_b_graph_translate_data x_18307 = 285 299 let { init_ret = init_ret0; init_params = init_params0; init_stack_size = 286 300 init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0; 287 f_step = f_step0; f_fin = f_fin0 } = x_ 21203301 f_step = f_step0; f_fin = f_fin0 } = x_18307 288 302 in 289 303 h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0 … … 296 310 > (Graphs.label > Joint.joint_fin_step > Blocks.bind_fin_block) > __ 297 311 > __ > __ > __ > 'a1) > b_graph_translate_data > 'a1 **) 298 let rec b_graph_translate_data_rect_Type3 src dst globals h_mk_b_graph_translate_data x_ 21205=312 let rec b_graph_translate_data_rect_Type3 src dst globals h_mk_b_graph_translate_data x_18309 = 299 313 let { init_ret = init_ret0; init_params = init_params0; init_stack_size = 300 314 init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0; 301 f_step = f_step0; f_fin = f_fin0 } = x_ 21205315 f_step = f_step0; f_fin = f_fin0 } = x_18309 302 316 in 303 317 h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0 … … 310 324 > (Graphs.label > Joint.joint_fin_step > Blocks.bind_fin_block) > __ 311 325 > __ > __ > __ > 'a1) > b_graph_translate_data > 'a1 **) 312 let rec b_graph_translate_data_rect_Type2 src dst globals h_mk_b_graph_translate_data x_ 21207=326 let rec b_graph_translate_data_rect_Type2 src dst globals h_mk_b_graph_translate_data x_18311 = 313 327 let { init_ret = init_ret0; init_params = init_params0; init_stack_size = 314 328 init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0; 315 f_step = f_step0; f_fin = f_fin0 } = x_ 21207329 f_step = f_step0; f_fin = f_fin0 } = x_18311 316 330 in 317 331 h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0 … … 324 338 > (Graphs.label > Joint.joint_fin_step > Blocks.bind_fin_block) > __ 325 339 > __ > __ > __ > 'a1) > b_graph_translate_data > 'a1 **) 326 let rec b_graph_translate_data_rect_Type1 src dst globals h_mk_b_graph_translate_data x_ 21209=340 let rec b_graph_translate_data_rect_Type1 src dst globals h_mk_b_graph_translate_data x_18313 = 327 341 let { init_ret = init_ret0; init_params = init_params0; init_stack_size = 328 342 init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0; 329 f_step = f_step0; f_fin = f_fin0 } = x_ 21209343 f_step = f_step0; f_fin = f_fin0 } = x_18313 330 344 in 331 345 h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0 … … 338 352 > (Graphs.label > Joint.joint_fin_step > Blocks.bind_fin_block) > __ 339 353 > __ > __ > __ > 'a1) > b_graph_translate_data > 'a1 **) 340 let rec b_graph_translate_data_rect_Type0 src dst globals h_mk_b_graph_translate_data x_ 21211=354 let rec b_graph_translate_data_rect_Type0 src dst globals h_mk_b_graph_translate_data x_18315 = 341 355 let { init_ret = init_ret0; init_params = init_params0; init_stack_size = 342 356 init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0; 343 f_step = f_step0; f_fin = f_fin0 } = x_ 21211357 f_step = f_step0; f_fin = f_fin0 } = x_18315 344 358 in 345 359 h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0 … … 652 666 Joint.joint_program > Joint.joint_program **) 653 667 let b_graph_transform_program src dst init p = 654 AST.transform_program p (fun varnames > 655 AST.transf_fundef (fun def_in > 656 Types.pi1 657 (b_graph_translate src dst varnames (init varnames def_in) def_in))) 668 { Joint.joint_prog = 669 (AST.transform_program p.Joint.joint_prog (fun varnames > 670 AST.transf_fundef (fun def_in > 671 Types.pi1 672 (b_graph_translate src dst varnames (init varnames def_in) def_in)))); 673 Joint.init_cost_label = p.Joint.init_cost_label } 658 674 659 675 (** val added_registers :
Note: See TracChangeset
for help on using the changeset viewer.