Changeset 756 for src/ERTL/Uses.ma


Ignore:
Timestamp:
Apr 15, 2011, 5:47:32 PM (10 years ago)
Author:
mulligan
Message:

Made a start on RTL. Renaming in ERTL and below to move closer to Brian's naming convention and datatypes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/Uses.ma

    r746 r756  
    33include "ASM/Arithmetic.ma".
    44include "ASM/I8051.ma".
     5include "common/Registers.ma".
    56
    67definition count ≝
    7   λregister.
     8  λr: register.
    89  λuses.
    910    let l ≝ increment ? (lookup ? ? register uses (zero 16)) in
     
    1112     
    1213definition examine_statement ≝
    13   λstatement: ERTLStatement.
     14  λstatement: ertl_statement.
    1415  λuses.
    1516  match statement with
    16   [ ERTL_St_Skip _ ⇒ uses
    17   | ERTL_St_Comment _ _ ⇒ uses
    18   | ERTL_St_Cost _ _ ⇒ uses
    19   | ERTL_St_Hdw_To_Hdw _ _ _ ⇒ uses
    20   | ERTL_St_NewFrame _ ⇒ uses
    21   | ERTL_St_DelFrame _ ⇒ uses
    22   | ERTL_St_ClearCarry _ ⇒ uses
    23   | ERTL_St_Call_Id _ _ _ ⇒ uses
    24   | ERTL_St_Return _ ⇒ uses
    25   | ERTL_St_Get_Hdw r _ _ ⇒ count (word_of_register r) uses
    26   | ERTL_St_Set_Hdw _ r _ ⇒ count (word_of_register r) uses
    27   | ERTL_St_FrameSize ar _ ⇒
     17  [ ertl_st_skip _ ⇒ uses
     18  | ertl_st_comment _ _ ⇒ uses
     19  | ertl_st_cost _ _ ⇒ uses
     20  | ertl_st_hdw_to_hdw _ _ _ ⇒ uses
     21  | ertl_st_new_frame _ ⇒ uses
     22  | ertl_st_del_frame _ ⇒ uses
     23  | ertl_st_clear_carry _ ⇒ uses
     24  | ertl_st_call_id _ _ _ ⇒ uses
     25  | ertl_st_return _ ⇒ uses
     26  | ertl_st_get_hdw r _ _ ⇒ count (word_of_register r) uses
     27  | ertl_st_set_hdw _ r _ ⇒ count (word_of_register r) uses
     28  | ertl_st_frame_size ar _ ⇒
    2829    match ar with [
    29       mkAbstractRegister r ⇒
     30      mk_abstract_register r ⇒
    3031        (* dpm: shift the abstract registers above the physical registers *)
    3132        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    3233          count offset uses
    3334    ]
    34   | ERTL_St_Pop ar _ ⇒
     35  | ertl_st_pop ar _ ⇒
    3536    match ar with [
    36       mkAbstractRegister r ⇒
     37      mk_abstract_register r ⇒
    3738        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    3839          count offset uses
    3940    ]
    40   | ERTL_St_Push ar _ ⇒
     41  | ertl_st_push ar _ ⇒
    4142    match ar with [
    42       mkAbstractRegister r ⇒
     43      mk_abstract_register r ⇒
    4344        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    4445          count offset uses
    4546    ]
    46   | ERTL_St_Int ar _ _ ⇒
     47  | ertl_st_int ar _ _ ⇒
    4748    match ar with [
    48       mkAbstractRegister r ⇒
     49      mk_abstract_register r ⇒
    4950        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    5051          count offset uses
    5152    ]
    52   | ERTL_St_AddrH ar _ _ ⇒
     53  | ertl_st_addr_h ar _ _ ⇒
    5354    match ar with [
    54       mkAbstractRegister r ⇒
     55      mk_abstract_register r ⇒
    5556        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    5657          count offset uses
    5758    ]
    58   | ERTL_St_AddrL ar _ _ ⇒
     59  | ertl_st_addr_l ar _ _ ⇒
    5960    match ar with [
    60       mkAbstractRegister r ⇒
     61      mk_abstract_register r ⇒
    6162        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    6263          count offset uses
    6364    ]
    64   | ERTL_St_CondAcc ar _ _ ⇒
     65  | ertl_st_cond_acc ar _ _ ⇒
    6566    match ar with [
    66       mkAbstractRegister r ⇒
     67      mk_abstract_register r ⇒
    6768        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    6869          count offset uses
    6970    ]
    70   | ERTL_St_Move ar1 ar2 _ ⇒
     71  | ertl_st_move ar1 ar2 _ ⇒
    7172    match ar1 with [
    72       mkAbstractRegister r1 ⇒
     73      mk_abstract_register r1 ⇒
    7374      match ar2 with [
    74         mkAbstractRegister r2 ⇒
     75        mk_abstract_register r2 ⇒
    7576          let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
    7677          let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
     
    7879      ]
    7980    ]
    80   | ERTL_St_Op1 op1 ar1 ar2 _ ⇒
     81  | ertl_st_op1 op1 ar1 ar2 _ ⇒
    8182    match ar1 with [
    82       mkAbstractRegister r1 ⇒
     83      mk_abstract_register r1 ⇒
    8384      match ar2 with [
    84         mkAbstractRegister r2 ⇒
     85        mk_abstract_register r2 ⇒
    8586          let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
    8687          let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
     
    8889      ]
    8990    ]
    90   | ERTL_St_Op2 op2 ar1 ar2 ar3 _ ⇒
     91  | ertl_st_op2 op2 ar1 ar2 ar3 _ ⇒
    9192    match ar1 with [
    92       mkAbstractRegister r1 ⇒
     93      mk_abstract_register r1 ⇒
    9394      match ar2 with [
    94         mkAbstractRegister r2 ⇒
     95        mk_abstract_register r2 ⇒
    9596        match ar3 with [
    96           mkAbstractRegister r3 ⇒
     97          mk_abstract_register r3 ⇒
    9798          let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
    9899          let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
     
    102103      ]
    103104    ]
    104   | ERTL_St_Opaccs opaccs ar1 ar2 ar3 _ ⇒
     105  | ertl_st_opaccs opaccs ar1 ar2 ar3 _ ⇒
    105106    match ar1 with [
    106       mkAbstractRegister r1 ⇒
     107      mk_abstract_register r1 ⇒
    107108      match ar2 with [
    108         mkAbstractRegister r2 ⇒
     109        mk_abstract_register r2 ⇒
    109110        match ar3 with [
    110           mkAbstractRegister r3 ⇒
     111          mk_abstract_register r3 ⇒
    111112          let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
    112113          let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
     
    116117      ]
    117118    ]
    118   | ERTL_St_Load ar1 ar2 ar3 _ ⇒
     119  | ertl_st_load ar1 ar2 ar3 _ ⇒
    119120    match ar1 with [
    120       mkAbstractRegister r1 ⇒
     121      mk_abstract_register r1 ⇒
    121122      match ar2 with [
    122         mkAbstractRegister r2 ⇒
     123        mk_abstract_register r2 ⇒
    123124        match ar3 with [
    124           mkAbstractRegister r3 ⇒
     125          mk_abstract_register r3 ⇒
    125126          let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
    126127          let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
     
    130131      ]
    131132    ]
    132   | ERTL_St_Store ar1 ar2 ar3 _ ⇒
     133  | ertl_st_store ar1 ar2 ar3 _ ⇒
    133134    match ar1 with [
    134       mkAbstractRegister r1 ⇒
     135      mk_abstract_register r1 ⇒
    135136      match ar2 with [
    136         mkAbstractRegister r2 ⇒
     137        mk_abstract_register r2 ⇒
    137138        match ar3 with [
    138           mkAbstractRegister r3 ⇒
     139          mk_abstract_register r3 ⇒
    139140          let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
    140141          let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
Note: See TracChangeset for help on using the changeset viewer.