source: src/ERTL/uses.ma @ 1260

Last change on this file since 1260 was 1260, checked in by mulligan, 8 years ago

commit for csc

File size: 2.1 KB
Line 
1include "ERTL/ERTL.ma".
2include "utilities/adt/table_adt.ma".
3
4definition lookup: table register nat → register → nat ≝
5  λuses.
6  λr: register.
7  match tbl_find … r uses with
8  [ None      ⇒ 0
9  | Some uses ⇒ uses
10  ].
11
12definition count: register → table register nat → ? ≝
13  λr: register.
14  λuses: table register nat.
15    tbl_insert … r ((lookup uses r) + 1) uses.
16 
17definition examine_statement ≝
18  λglobals: list ident.
19  λstmt: ertl_statement globals.
20  λuses: table register nat.
21  match stmt with
22  [ joint_st_sequential seq l ⇒
23    match seq with
24    [ joint_instr_comment c ⇒ uses
25    | joint_instr_cost_label c ⇒ uses
26    | joint_instr_move pair_regs ⇒
27      let reg1 ≝ \fst pair_regs in
28      let reg2 ≝ \snd pair_regs in
29      match reg1 with
30      [ pseudo p ⇒ count p uses
31      | hardware h1 ⇒
32        match reg2 with
33        [ pseudo p ⇒ count p uses
34        | hardware h2 ⇒ uses]]
35    | joint_instr_clear_carry ⇒ uses
36    | joint_instr_set_carry ⇒ uses
37    | joint_instr_call_id _ _ ⇒ uses
38    | joint_instr_pop r ⇒ count r uses
39    | joint_instr_push r ⇒ count r uses
40    | joint_instr_int r _ ⇒ count r uses
41    | joint_instr_address lbl prf r1 r2 ⇒ count r1 (count r2 uses)
42    | joint_instr_opaccs opaccs acc_a acc_b ⇒ count acc_a (count acc_b uses)
43    | joint_instr_op1 op1 r1 r2 ⇒ count r1 (count r2 uses)
44    | joint_instr_op2 op2 r1 r2 r3 ⇒ count r1 (count r2 (count r3 uses))
45    | joint_instr_load destr r1 r2 ⇒ count r1 (count r2 (count destr uses))
46    | joint_instr_store srcr r1 r2 ⇒ count r1 (count r2 (count srcr uses))
47    | joint_instr_cond srcr l2 ⇒ count srcr uses
48    | joint_instr_extension ext ⇒
49      match ext with
50      [ ertl_st_ext_new_frame ⇒ uses
51      | ertl_st_ext_del_frame ⇒ uses
52      | ertl_st_ext_frame_size r ⇒ count r uses]]
53  | joint_st_return ⇒ uses
54  | joint_st_goto l ⇒ uses
55  ].
56
57definition examine_internal ≝
58  λglobals: list ident.
59  λint_fun: ertl_internal_function globals.
60  let uses ≝ graph_fold ?? (λ_. examine_statement globals) (joint_if_code … int_fun) (tbl_empty …) in
61    lookup uses.
Note: See TracBrowser for help on using the repository browser.