Changeset 1241 for src/ERTL/uses.ma
 Timestamp:
 Sep 21, 2011, 5:28:06 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/uses.ma
r1188 r1241 1 1 include "ERTL/ERTL.ma". 2 2 3 let rec assoc_list_find 4 (A: Type[0]) (B: Type[0]) (eq_a: A → A → bool) (to_find: A) 5 (def: B) (l: list (A × B)) 6 on l ≝ 7 match l with 8 [ nil ⇒ def 9  cons hd tl ⇒ 10 if eq_a (\fst hd) to_find then 11 \snd hd 12 else 13 assoc_list_find A B eq_a to_find def tl 3 include "utilities/adt/table_adt.ma". 4 5 definition lookup: table register nat → register → nat ≝ 6 λuses. 7 λr: register. 8 match tbl_find … r uses with 9 [ None ⇒ 0 10  Some uses ⇒ uses 14 11 ]. 15 16 definition lookup ≝ 17 λuses. 18 λr. 19 assoc_list_find register nat (eq_identifier ?) uses 0 r. 12 13 definition count: register → table register nat → ? ≝ 14 λr: register. 15 λuses: table register nat. 16 tbl_insert … r ((lookup uses r) + 1) uses. 17 18 definition examine_statement ≝ 19 λglobals: list ident. 20 λstmt: ertl_statement globals. 21 λuses: table register nat. 22 match stmt with 23 [ joint_st_sequential seq l ⇒ 24 match seq with 25 [ joint_instr_comment c ⇒ uses 26  joint_instr_cost_label c ⇒ uses 27  joint_instr_move pair_regs ⇒ 28 let reg1 ≝ \fst pair_regs in 29 let reg2 ≝ \snd pair_regs in 30 match reg1 with 31 [ pseudo p ⇒ count p uses 32  hardware h1 ⇒ 33 match reg2 with 34 [ pseudo p ⇒ count p uses 35  hardware h2 ⇒ uses 36 ] 37 ] 38  joint_instr_clear_carry ⇒ uses 39  joint_instr_set_carry ⇒ uses 40  joint_instr_call_id _ _ ⇒ uses 41  joint_instr_pop r ⇒ count r uses 42  joint_instr_push r ⇒ count r uses 43  joint_instr_int r _ ⇒ count r uses 44  joint_instr_address lbl prf r1 r2 ⇒ count r1 (count r2 uses) 45  joint_instr_opaccs opaccs acc_a acc_b ⇒ count acc_a (count acc_b uses) 46  joint_instr_op1 op1 r1 ⇒ count r1 uses 47  joint_instr_op2 op2 r1 r2 ⇒ count r1 (count r2 uses) 48  joint_instr_load destr r1 r2 ⇒ count r1 (count r2 (count destr uses)) 49  joint_instr_store srcr r1 r2 ⇒ count r1 (count r2 (count srcr uses)) 50  joint_instr_cond srcr l2 ⇒ count srcr uses 51 ] 52  joint_st_return ⇒ uses 53  joint_st_goto l ⇒ uses 54  joint_st_extension ext ⇒ 55 match ext with 56 [ ertl_st_ext_new_frame l ⇒ uses 57  ertl_st_ext_del_frame l ⇒ uses 58  ertl_st_ext_frame_size r l ⇒ count r uses 59 ] 60 ]. 61 62 definition examine_internal ≝ 63 λglobals: list ident. 64 λint_fun: ertl_internal_function globals. 65 let uses ≝ tbl_fold ?? (examine_statement globals) (joint_if_graph … int_fun) (tbl_empty …) in 66 lookup uses.
Note: See TracChangeset
for help on using the changeset viewer.