 Timestamp:
 Sep 23, 2011, 4:40:54 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLtoERTL.ma
r1259 r1262 369 369 ) start_lbl dest_lbl def. 370 370 371 definition translate_stmt ≝ 371 axiom translate_stmt : 372 ∀globals: list ident. label → rtl_statement → ertl_internal_function globals → ertl_internal_function globals. 373 (* 374 ≝ 372 375 λglobals. 373 376 λlbl. … … 408 411 ]. 409 412 cases not_implemented 410 qed. 413 qed.*) 411 414 412 415 (* hack with empty graphs used here *) 413 416 definition translate_funct_internal ≝ 414 λ def.417 λglobals,def. 415 418 let nb_params ≝ rtl_if_params def in 416 419 let added_stacksize ≝ max 0 (nb_params  RegisterParams) in … … 418 421 let entry' ≝ rtl_if_entry def in 419 422 let exit' ≝ rtl_if_exit def in 420 let graph' ≝ add ? ? (empty_map ? ?) entry' ( ertl_st_skipentry') in421 let graph' ≝ add ? ? graph' exit' ( ertl_st_skipexit') in423 let graph' ≝ add ? ? (empty_map ? ?) entry' (joint_st_goto … entry') in 424 let graph' ≝ add ? ? graph' exit' (joint_st_goto … exit') in 422 425 let def' ≝ 423 mk_ ertl_internal_function424 (rtl_if_luniverse def) (rtl_if_runiverse def)425 nb_params new_locals ((rtl_if_stacksize def) + added_stacksize)426 mk_joint_internal_function globals (ertl_params globals) 427 (rtl_if_luniverse def) (rtl_if_runiverse … def) it 428 nb_params new_locals ((rtl_if_stacksize … def) + added_stacksize) 426 429 graph' ? ? in 427 let def' ≝ foldi ? ? ? translate_stmt(rtl_if_graph def) def' in428 let def' ≝ add_pro_and_epilogue (rtl_if_params def) (rtl_if_result def) def' in430 let def' ≝ foldi ? ? ? (translate_stmt globals) (rtl_if_graph def) def' in 431 let def' ≝ add_pro_and_epilogue … (rtl_if_params def) (rtl_if_result def) def' in 429 432 def'. 430 [1: % 431 [1: @entry' 432 2: normalize nodelta 433 @graph_add_lookup 434 @graph_add 435 ] 436 2: % 437 [1: @exit' 438 2: normalize nodelta 439 @graph_add 440 ] 441 ] 442 qed. 443 444 definition translate_funct ≝ 445 λid_def: ident × ?. 446 let 〈id, def〉 ≝ id_def in 447 let def' ≝ 448 match def with 449 [ Internal def ⇒ Internal ? (translate_funct_internal def) 450  External def ⇒ External ? def 451 ] in 452 〈id, def'〉. 433 whd in match ertl_params (* CSC: Matita's bug here; not enough/too much reduction 434 makes the next application fail. Why? *) 435 % 436 [ @entry'  @graph_add_lookup @graph_add 437  @exit'  @graph_add ] 438 qed. 453 439 454 440 definition generate ≝ 441 λglobals. 455 442 λstmt. 456 443 λdef. 457 let 〈entry, nuniv〉 ≝ fresh_label def in 458 let graph ≝ add ? ? (ertl_if_graph def) entry stmt in 459 mk_ertl_internal_function 460 nuniv (ertl_if_runiverse def) (ertl_if_params def) 461 (ertl_if_locals def) (ertl_if_stacksize def) graph 462 ? ?. 463 [1: % 464 [1: @entry 465 2: normalize nodelta; 466 @graph_add 467 ] 468 2: generalize in match (ertl_if_exit def) 469 #HYP 470 cases HYP 471 #LBL #LBL_PRF 472 % 473 [1: @LBL 474 2: normalize nodelta; 475 @graph_add_lookup 476 @LBL_PRF 477 ] 478 ] 479 qed. 480 481 let rec find_and_remove_first_cost_label_internal 482 (def: ertl_internal_function) (lbl: label) (num_nodes: nat) 444 let 〈entry, nuniv〉 ≝ fresh_label … def in 445 let graph ≝ add ? ? (joint_if_code … def) entry stmt in 446 mk_joint_internal_function ? (ertl_params globals) 447 nuniv (joint_if_runiverse … def) it (joint_if_params … def) 448 (joint_if_locals … def) (joint_if_stacksize … def) graph 449 ? ?. 450 [ % [ @entry  @graph_add ] 451  cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL  @graph_add_lookup @LBL_PRF ] 452 qed. 453 454 let rec find_and_remove_first_cost_label_internal (globals: list ident) 455 (def: ertl_internal_function globals) (lbl: label) (num_nodes: nat) 483 456 on num_nodes ≝ 484 457 match num_nodes with 485 458 [ O ⇒ 〈None ?, def〉 486 459  S num_nodes' ⇒ 487 match lookup ? ? (ertl_if_graphdef) lbl with460 match lookup … (joint_if_code … def) lbl with 488 461 [ None ⇒ 〈None ?, def〉 489  Some stmt ⇒ 462  Some stmt ⇒ 490 463 match stmt with 491 [ ertl_st_cost cost_lbl next_lbl ⇒ 492 〈Some ? cost_lbl, add_graph lbl (ertl_st_skip next_lbl) def〉 493  ertl_st_cond _ _ _ ⇒ 〈None ?, def〉 494  ertl_st_return ⇒ 〈None ?, def〉 495  ertl_st_skip lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 496  ertl_st_comment _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 497  ertl_st_get_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 498  ertl_st_set_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 499  ertl_st_hdw_to_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 500  ertl_st_pop _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 501  ertl_st_push _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 502  ertl_st_addr _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 503  ertl_st_int _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 504  ertl_st_move _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 505  ertl_st_opaccs _ _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 506  ertl_st_op1 _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 507  ertl_st_op2 _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 508  ertl_st_clear_carry lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 509  ertl_st_set_carry lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 510  ertl_st_load _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 511  ertl_st_store _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 512  ertl_st_call_id _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 513  ertl_st_new_frame lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 514  ertl_st_del_frame lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 515  ertl_st_frame_size _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 516 ] 517 ] 518 ]. 464 [ joint_st_sequential inst lbl ⇒ 465 match inst with 466 [ joint_instr_cost_label cost_lbl ⇒ 467 〈Some … cost_lbl, add_graph ertl_params_ globals lbl (joint_st_goto … lbl) def〉 468  _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ] 469  joint_st_return ⇒ 〈None …, def〉 470  joint_st_goto lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' 471 ]]]. 519 472 520 473 definition find_and_remove_first_cost_label ≝ 521 λ def.522 find_and_remove_first_cost_label_internal def (ertl_if_entry def) (graph_num_nodes ? (ertl_if_graphdef)).474 λglobals,def. 475 find_and_remove_first_cost_label_internal globals def (joint_if_entry … def) (graph_num_nodes ? (joint_if_code … def)). 523 476 524 477 definition move_first_cost_label_up_internal ≝ 525 λ def.526 let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label def in478 λglobals,def. 479 let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label … def in 527 480 match cost_label with 528 481 [ None ⇒ def 529  Some cost_label ⇒ generate (ertl_st_cost cost_label (ertl_if_entry def)) def 530 ]. 531 482  Some cost_label ⇒ generate … (joint_st_sequential ertl_params_ globals (joint_instr_cost_label … cost_label) (joint_if_entry … def)) def 483 ]. 484 485 definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)). 486 487 (* 532 488 definition move_first_cost_label_up ≝ 489 λglobals. 533 490 λA: Type[0]. 534 491 λid_def: A × ?. … … 536 493 let def' ≝ 537 494 match def with 538 [ Internal int_fun ⇒ Internal ? (move_first_cost_label_up_internal int_fun)539  External ext ⇒ def495 [ Internal int_fun ⇒ Internal ? (move_first_cost_label_up_internal … (translate_funct_internal globals int_fun)) 496  External ext ⇒ External … ext 540 497 ] 541 498 in … … 545 502 λp. 546 503 let p ≝ tailcall_simplify p in (* tailcall simplification here *) 547 let f ≝ λfunct. move_first_cost_label_up ? (translate_funct funct)in504 let f ≝ λfunct. move_first_cost_label_up ? funct in 548 505 let vars ≝ map ? ? f (rtl_pr_functs p) in 549 506 mk_ertl_program (rtl_pr_vars p) vars (rtl_pr_main p). 507 *) 508 509 definition translate : rtl_program → ertl_program ≝ 510 λp. 511 let p ≝ tailcall_simplify p in (* tailcall simplification here *) 512 transform_program ??? p (transf_fundef ?? translate_funct).
Note: See TracChangeset
for help on using the changeset viewer.