Changeset 759 for src/RTL


Ignore:
Timestamp:
Apr 18, 2011, 5:32:46 PM (10 years ago)
Author:
mulligan
Message:

More work on the RTL to ERTL pass.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLtoERTL.ma

    r756 r759  
    11include "RTL/RTL.ma".
     2include "ERTL/ERTL.ma".
    23
    34definition change_exit_label ≝
    45  λl: label.
    5   λp: rtl_internal_function.
    6   let rtl_if_luniverse' ≝ rtl_if_luniverse p in
    7   let rtl_if_runiverse' ≝ rtl_if_runiverse p in
    8   let rtl_if_sig' ≝ rtl_if_sig p in
    9   let rtl_if_result' ≝ rtl_if_result p in
    10   let rtl_if_params' ≝ rtl_if_params p in
    11   let rtl_if_locals' ≝ rtl_if_locals p in
    12   let rtl_if_stacksize' ≝ rtl_if_stacksize p in
    13   let rtl_if_graph' ≝ rtl_if_graph p in
    14   let rtl_if_entry' ≝ rtl_if_entry p in
    15   let rtl_if_exit' ≝ l in
    16     mk_rtl_internal_function rtl_if_luniverse' rtl_if_runiverse'
    17                              rtl_if_sig' rtl_if_result' rtl_if_params'
    18                              rtl_if_locals' rtl_if_stacksize'
    19                              rtl_if_graph' rtl_if_entry' rtl_if_exit'.
     6  λp: ertl_internal_function.
     7  let ertl_if_luniverse' ≝ ertl_if_luniverse p in
     8  let ertl_if_runiverse' ≝ ertl_if_runiverse p in
     9  let ertl_if_params' ≝ ertl_if_params p in
     10  let ertl_if_locals' ≝ ertl_if_locals p in
     11  let ertl_if_graph' ≝ ertl_if_graph p in
     12  let ertl_if_entry' ≝ ertl_if_entry p in
     13  let ertl_if_exit' ≝ l in
     14    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
     15                              ertl_if_params' ertl_if_locals'
     16                              ertl_if_graph' ertl_if_entry' ertl_if_exit'.
    2017
    2118definition change_entry_label ≝
    2219  λl: label.
    23   λp: rtl_internal_function.
    24   let rtl_if_luniverse' ≝ rtl_if_luniverse p in
    25   let rtl_if_runiverse' ≝ rtl_if_runiverse p in
    26   let rtl_if_sig' ≝ rtl_if_sig p in
    27   let rtl_if_result' ≝ rtl_if_result p in
    28   let rtl_if_params' ≝ rtl_if_params p in
    29   let rtl_if_locals' ≝ rtl_if_locals p in
    30   let rtl_if_stacksize' ≝ rtl_if_stacksize p in
    31   let rtl_if_graph' ≝ rtl_if_graph p in
    32   let rtl_if_entry' ≝ l in
    33   let rtl_if_exit' ≝ rtl_if_exit p in
    34     mk_rtl_internal_function rtl_if_luniverse' rtl_if_runiverse'
    35                              rtl_if_sig' rtl_if_result' rtl_if_params'
    36                              rtl_if_locals' rtl_if_stacksize'
    37                              rtl_if_graph' rtl_if_entry' rtl_if_exit'.
     20  λp: ertl_internal_function.
     21  let ertl_if_luniverse' ≝ ertl_if_luniverse p in
     22  let ertl_if_runiverse' ≝ ertl_if_runiverse p in
     23  let ertl_if_params' ≝ ertl_if_params p in
     24  let ertl_if_locals' ≝ ertl_if_locals p in
     25  let ertl_if_graph' ≝ ertl_if_graph p in
     26  let ertl_if_entry' ≝ l in
     27  let ertl_if_exit' ≝ ertl_if_exit p in
     28    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
     29                              ertl_if_params' ertl_if_locals'
     30                              ertl_if_graph' ertl_if_entry' ertl_if_exit'.
     31                             
     32definition add_graph ≝
     33  λl: label.
     34  λstmt.
     35  λp.
     36  let ertl_if_luniverse' ≝ ertl_if_luniverse p in
     37  let ertl_if_runiverse' ≝ ertl_if_runiverse p in
     38  let ertl_if_params' ≝ ertl_if_params p in
     39  let ertl_if_locals' ≝ ertl_if_locals p in
     40  let ertl_if_graph' ≝ add ? ? (ertl_if_graph p) l stmt in
     41  let ertl_if_entry' ≝ ertl_if_entry p in
     42  let ertl_if_exit' ≝ ertl_if_exit p in
     43    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
     44                              ertl_if_params' ertl_if_locals'
     45                              ertl_if_graph' ertl_if_entry' ertl_if_exit'.
    3846                             
    3947definition fresh_label ≝
    4048  λdef.
    41     fresh LabelTag (rtl_if_luniverse def).
     49    fresh LabelTag (ertl_if_luniverse def).
    4250   
    4351definition change_label ≝
    44   λ
     52  λl.
     53  λe: ertl_statement.
     54  match e with
     55  [ ertl_st_skip _ ⇒ ertl_st_skip l
     56  | ertl_st_comment s _ ⇒ ertl_st_comment s l
     57  | ertl_st_cost c _ ⇒ ertl_st_cost c l
     58  | ertl_st_get_hdw r1 r2 _ ⇒ ertl_st_get_hdw r1 r2 l
     59  | ertl_st_set_hdw r1 r2 _ ⇒ ertl_st_set_hdw r1 r2 l
     60  | ertl_st_hdw_to_hdw r1 r2 _ ⇒ ertl_st_hdw_to_hdw r1 r2 l
     61  | ertl_st_new_frame _ ⇒ ertl_st_new_frame l
     62  | ertl_st_del_frame _ ⇒ ertl_st_del_frame l
     63  | ertl_st_frame_size r _ ⇒ ertl_st_frame_size r l
     64  | ertl_st_pop r _ ⇒ ertl_st_pop r l
     65  | ertl_st_push r _ ⇒ ertl_st_push r l
     66  | ertl_st_addr_h r id _ ⇒ ertl_st_addr_h r id l
     67  | ertl_st_addr_l r id _ ⇒ ertl_st_addr_l r id l
     68  | ertl_st_int r i _ ⇒ ertl_st_int r i l
     69  | ertl_st_move r1 r2 _ ⇒ ertl_st_move r1 r2 l
     70  | ertl_st_opaccs opaccs d s1 s2 _ ⇒ ertl_st_opaccs opaccs d s1 s2 l
     71  | ertl_st_op1 op1 d s1 _ ⇒ ertl_st_op1 op1 d s1 l
     72  | ertl_st_op2 op2 d s1 s2 _ ⇒ ertl_st_op2 op2 d s1 s2 l
     73  | ertl_st_clear_carry _ ⇒ ertl_st_clear_carry l
     74  | ertl_st_load d a1 a2 _ ⇒ ertl_st_load d a1 a2 l
     75  | ertl_st_store a1 a2 s _ ⇒ ertl_st_store a1 a2 s l
     76  | ertl_st_call_id f args _ ⇒ ertl_st_call_id f args l
     77  | ertl_st_cond_acc a i1 i2 ⇒ ertl_st_cond_acc a i1 i2
     78  | ertl_st_return a ⇒ ertl_st_return a
     79  ].
     80 
     81let rec adds_graph (stmt_list: list ertl_statement) (start_lbl: label) (dest_lbl: label) (def: ertl_internal_function): option ertl_internal_function ≝
     82  match stmt_list with
     83  [ nil ⇒ Some ? def
     84  | cons hd tl ⇒
     85    match tl with
     86    [ nil ⇒ Some ? (add_graph start_lbl (change_label dest_lbl hd) def)
     87    | _ ⇒
     88      let tmp_lbl ≝ fresh_label def in
     89      match tmp_lbl with
     90      [ OK o ⇒
     91        let 〈lbl, univ〉 ≝ o in
     92        let stmt ≝ change_label lbl hd in
     93        let def ≝ add_graph start_lbl hd def in
     94          adds_graph tl lbl dest_lbl def
     95      | Error ⇒ None ?
     96      ]
     97    ]
     98  ].
     99
     100let rec add_translates (translate_list: list (label → label → ertl_internal_function → ertl_internal_function))
     101                       (start_lbl: label) (dest_lbl: label)
     102                       (def: ertl_internal_function): option ertl_internal_function ≝
     103  match translate_list with
     104  [ nil ⇒ Some ? def
     105  | cons hd tl ⇒
     106    match tl with
     107    [ nil ⇒ Some ? (hd start_lbl dest_lbl def)
     108    | _ ⇒
     109      let tmp_lbl ≝ fresh_label def in
     110      match tmp_lbl with
     111      [ OK o ⇒
     112        let 〈lbl, univ〉 ≝ o in
     113        let def ≝ hd start_lbl lbl def in
     114          add_translates tl lbl dest_lbl def
     115      | Error ⇒ None ?
     116      ]
     117    ]
     118  ].
     119 
     120definition fresh_register ≝
     121  λdef.
     122   
Note: See TracChangeset for help on using the changeset viewer.