 Timestamp:
 Apr 18, 2011, 5:32:46 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLtoERTL.ma
r756 r759 1 1 include "RTL/RTL.ma". 2 include "ERTL/ERTL.ma". 2 3 3 4 definition change_exit_label ≝ 4 5 λ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'. 20 17 21 18 definition change_entry_label ≝ 22 19 λ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 32 definition 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'. 38 46 39 47 definition fresh_label ≝ 40 48 λdef. 41 fresh LabelTag ( rtl_if_luniverse def).49 fresh LabelTag (ertl_if_luniverse def). 42 50 43 51 definition 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 81 let 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 100 let 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 120 definition fresh_register ≝ 121 λdef. 122
Note: See TracChangeset
for help on using the changeset viewer.