Changeset 1241 for src/ERTL/uses.ma


Ignore:
Timestamp:
Sep 21, 2011, 5:28:06 PM (9 years ago)
Author:
mulligan
Message:

changes for claudio

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/uses.ma

    r1188 r1241  
    11include "ERTL/ERTL.ma".
    22
    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
     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
    1411  ].
    15      
    16 definition lookup ≝
    17   λuses.
    18   λr.
    19     assoc_list_find register nat (eq_identifier ?) uses 0 r.
     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
     62definition 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.