Changeset 783 for src


Ignore:
Timestamp:
Apr 29, 2011, 1:36:35 PM (10 years ago)
Author:
mulligan
Message:

rtl to ertl pass complete (modulo some straightforward axioms that need filling in) and refactoring to get rid of all the option types.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r782 r783  
    7171  ertl_pr_vars: list (ident × nat);
    7272  ertl_pr_funcs: list (ident × ertl_function);
    73   ertl_pr_main: option label
     73  ertl_pr_main: option ident
    7474}.
    7575
  • src/RTL/RTL.ma

    r782 r783  
    6161  rtl_pr_main: option ident
    6262}.
     63
     64definition rtl_pr_vars: rtl_program → list (ident × nat).
     65  # P
     66  cases P
     67  # H1 # H2 # H3
     68  @ H1
     69qed.
  • src/RTL/RTLtoERTL.ma

    r782 r783  
    11include "RTL/RTL.ma".
     2include "RTL/RTLTailcall.ma".
    23include "ERTL/ERTL.ma".
    34include "utilities/RegisterSet.ma".
     
    489490  | rtl_st_tailcall_ptr r1 r2 regs ⇒ None ? (* dpm: impossible *)
    490491  ].
    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   
     493definition translate_funct_internal ≝
    501494  λdef.
    502495  let nb_params ≝ length ? (rtl_if_params def) in
     
    518511    match def with
    519512    [ rtl_f_internal def ⇒
    520       match translate_internal def with
     513      match translate_funct_internal def with
    521514      [ None ⇒ None ?
    522515      | Some internal_def ⇒ Some ? (ertl_f_internal internal_def)
     
    537530  ].
    538531 
     532let 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 
     592axiom num_entries:
     593  ∀A: Type[0].
     594  ∀g: graph A.
     595    nat.
     596 
     597definition 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
     601definition 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 
     614definition 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 
     633definition 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
     641let 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 
     651definition 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.