source: src/ERTL/uses.ma @ 1249

Last change on this file since 1249 was 1249, checked in by mulligan, 9 years ago

changes to get everything to typecheck again

File size: 2.1 KB
Line 
1include "ERTL/ERTL.ma".
2
3include "utilities/adt/table_adt.ma".
4
5definition 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
11  ].
12
13definition count: register → table register nat → ? ≝
14  λr: register.
15  λuses: table register nat.
16    tbl_insert … r ((lookup uses r) + 1) uses.
17 
18definition 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(*
63definition examine_internal ≝
64  λglobals: list ident.
65  λint_fun: ertl_internal_function globals.
66  let graph ≝ recover_graph globals int_fun in
67  let uses ≝ tbl_fold ?? (examine_statement globals) (joint_if_graph … int_fun) (tbl_empty …) in
68      lookup uses.
69*)
Note: See TracBrowser for help on using the repository browser.