 Timestamp:
 Apr 29, 2011, 1:36:35 PM (10 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTL.ma
r782 r783 71 71 ertl_pr_vars: list (ident × nat); 72 72 ertl_pr_funcs: list (ident × ertl_function); 73 ertl_pr_main: option label73 ertl_pr_main: option ident 74 74 }. 75 75 
src/RTL/RTL.ma
r782 r783 61 61 rtl_pr_main: option ident 62 62 }. 63 64 definition rtl_pr_vars: rtl_program → list (ident × nat). 65 # P 66 cases P 67 # H1 # H2 # H3 68 @ H1 69 qed. 
src/RTL/RTLtoERTL.ma
r782 r783 1 1 include "RTL/RTL.ma". 2 include "RTL/RTLTailcall.ma". 2 3 include "ERTL/ERTL.ma". 3 4 include "utilities/RegisterSet.ma". … … 489 490  rtl_st_tailcall_ptr r1 r2 regs ⇒ None ? (* dpm: impossible *) 490 491 ]. 491 492 (* dpm: this should not be option, fix *) 493 axiom map_fold: 494 ∀A, B: Type[0]. 495 ∀f: label → A → B → option B. 496 ∀m: rtl_statement_graph. 497 ∀b: B. 498 B. 499 500 definition translate_internal ≝ 492 493 definition translate_funct_internal ≝ 501 494 λdef. 502 495 let nb_params ≝ length ? (rtl_if_params def) in … … 518 511 match def with 519 512 [ rtl_f_internal def ⇒ 520 match translate_ internal def with513 match translate_funct_internal def with 521 514 [ None ⇒ None ? 522 515  Some internal_def ⇒ Some ? (ertl_f_internal internal_def) … … 537 530 ]. 538 531 532 let rec find_and_remove_first_cost_label_internal (def: ertl_internal_function) 533 (lbl: label) (n: nat) on n ≝ 534 match n with 535 [ O ⇒ None ? 536  S n' ⇒ 537 let statement_at_label ≝ lookup ? ? (ertl_if_graph def) lbl in 538 match statement_at_label with 539 [ None ⇒ None ? 540  Some statement ⇒ 541 match statement with 542 [ ertl_st_cost cost_lbl next_lbl ⇒ 543 let def' ≝ add_graph lbl (ertl_st_skip next_lbl) def in 544 Some ? 〈Some ? cost_lbl, def'〉 545  ertl_st_cond_acc _ _ _ ⇒ Some ? 〈None ?, def〉 546  ertl_st_return _⇒ Some ? 〈None ?, def〉 547  ertl_st_skip lbl' ⇒ find_and_remove_first_cost_label_internal def lbl' n' 548  ertl_st_comment _ lbl' ⇒ 549 find_and_remove_first_cost_label_internal def lbl' n' 550  ertl_st_get_hdw _ _ lbl' ⇒ 551 find_and_remove_first_cost_label_internal def lbl' n' 552  ertl_st_set_hdw _ _ lbl' ⇒ 553 find_and_remove_first_cost_label_internal def lbl' n' 554  ertl_st_hdw_to_hdw _ _ lbl' ⇒ 555 find_and_remove_first_cost_label_internal def lbl' n' 556  ertl_st_pop _ lbl' ⇒ 557 find_and_remove_first_cost_label_internal def lbl' n' 558  ertl_st_push _ lbl' ⇒ 559 find_and_remove_first_cost_label_internal def lbl' n' 560  ertl_st_addr_h _ _ lbl' ⇒ 561 find_and_remove_first_cost_label_internal def lbl' n' 562  ertl_st_addr_l _ _ lbl' ⇒ 563 find_and_remove_first_cost_label_internal def lbl' n' 564  ertl_st_int _ _ lbl' ⇒ 565 find_and_remove_first_cost_label_internal def lbl' n' 566  ertl_st_move _ _ lbl' ⇒ 567 find_and_remove_first_cost_label_internal def lbl' n' 568  ertl_st_opaccs _ _ _ _ lbl' ⇒ 569 find_and_remove_first_cost_label_internal def lbl' n' 570  ertl_st_op2 _ _ _ _ lbl' ⇒ 571 find_and_remove_first_cost_label_internal def lbl' n' 572  ertl_st_op1 _ _ _ lbl' ⇒ 573 find_and_remove_first_cost_label_internal def lbl' n' 574  ertl_st_clear_carry lbl' ⇒ 575 find_and_remove_first_cost_label_internal def lbl' n' 576  ertl_st_load _ _ _ lbl' ⇒ 577 find_and_remove_first_cost_label_internal def lbl' n' 578  ertl_st_store _ _ _ lbl' ⇒ 579 find_and_remove_first_cost_label_internal def lbl' n' 580  ertl_st_call_id _ _ lbl' ⇒ 581 find_and_remove_first_cost_label_internal def lbl' n' 582  ertl_st_new_frame lbl' ⇒ 583 find_and_remove_first_cost_label_internal def lbl' n' 584  ertl_st_del_frame lbl' ⇒ 585 find_and_remove_first_cost_label_internal def lbl' n' 586  ertl_st_frame_size _ lbl' ⇒ 587 find_and_remove_first_cost_label_internal def lbl' n' 588 ] 589 ] 590 ]. 591 592 axiom num_entries: 593 ∀A: Type[0]. 594 ∀g: graph A. 595 nat. 596 597 definition find_and_remove_first_cost_label ≝ 598 λdef. 599 find_and_remove_first_cost_label_internal def (ertl_if_entry def) (num_entries ? (ertl_if_graph def)). 600 601 definition move_first_cost_label_up_internal ≝ 602 λdef. 603 let cost_label_def ≝ find_and_remove_first_cost_label def in 604 match cost_label_def with 605 [ None ⇒ None ? 606  Some cost_label_def ⇒ 607 let 〈cost_label, def〉 ≝ cost_label_def in 608 match cost_label with 609 [ None ⇒ Some ? def 610  Some cost_label ⇒ generate (ertl_st_cost cost_label (ertl_if_entry def)) def 611 ] 612 ]. 613 614 definition move_first_cost_label_up ≝ 615 λid_def: ident × ?. 616 let 〈id, def〉 ≝ id_def in 617 let def' ≝ 618 match def with 619 [ ertl_f_internal int_fun ⇒ 620 let cost_label_def ≝ move_first_cost_label_up_internal int_fun in 621 match cost_label_def with 622 [ None ⇒ None ? 623  Some cost_label_def ⇒ 624 Some ? (ertl_f_internal cost_label_def) 625 ] 626  ertl_f_external _ ⇒ Some ? def 627 ] in 628 match def' with 629 [ None ⇒ None ? 630  Some def' ⇒ Some ? 〈id, def'〉 631 ]. 632 633 definition translate_internal ≝ 634 λfunct. 635 let 〈id, funct〉 ≝ translate_funct funct in 636 match funct with 637 [ None ⇒ None ? 638  Some funct ⇒ move_first_cost_label_up 〈id, funct〉 639 ]. 640 641 let rec strip_none (A: Type[0]) (l: list (option A)) on l: list A ≝ 642 match l with 643 [ nil ⇒ nil ? 644  cons hd tl ⇒ 645 match hd with 646 [ None ⇒ strip_none A tl 647  Some hd ⇒ hd :: strip_none A tl 648 ] 649 ]. 650 651 definition translate: rtl_program → ertl_program ≝ 652 λp. 653 let p ≝ tailcall_simplify p in 654 let rtl_pr_vars' ≝ rtl_pr_vars p in 655 let rtl_pr_functs' ≝ map … translate_internal (rtl_pr_functs p) in 656 let rtl_pr_functs_filtered ≝ strip_none ? rtl_pr_functs' in 657 let rtl_pr_main' ≝ rtl_pr_main p in 658 mk_ertl_program rtl_pr_vars' rtl_pr_functs_filtered rtl_pr_main'.
Note: See TracChangeset
for help on using the changeset viewer.