Changeset 777 for src/ERTL/ERTL.ma


Ignore:
Timestamp:
Apr 27, 2011, 5:25:26 PM (10 years ago)
Author:
mulligan
Message:

Lots of work on RTL to ERTL pass from today.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r759 r777  
    66include "common/Registers.ma".
    77
    8 inductive abstract_register: Type[0] ≝
    9   mk_abstract_register: Word → abstract_register.
    10 
    11 definition abstract_registers ≝ list abstract_register.
    12 
     8definition hardware_register ≝ Register.
    139definition registers ≝ list register.
    1410
     
    1713  | ertl_st_comment: String → label → ertl_statement
    1814  | ertl_st_cost: costlabel → label → ertl_statement
    19   | ertl_st_get_hdw: register → abstract_register → label → ertl_statement
    20   | ertl_st_set_hdw: abstract_register → register → label → ertl_statement
    21   | ertl_st_hdw_to_hdw: register → register → label → ertl_statement
     15  | ertl_st_get_hdw: register → hardware_register → label → ertl_statement
     16  | ertl_st_set_hdw: hardware_register → register → label → ertl_statement
     17  | ertl_st_hdw_to_hdw: hardware_register → hardware_register → label → ertl_statement
    2218  | ertl_st_new_frame: label → ertl_statement
    2319  | ertl_st_del_frame: label → ertl_statement
    24   | ertl_st_frame_size: abstract_register → label → ertl_statement
    25   | ertl_st_pop: abstract_register → label → ertl_statement
    26   | ertl_st_push: abstract_register → label → ertl_statement
    27   | ertl_st_addr_h: abstract_register → label → label → ertl_statement
    28   | ertl_st_addr_l: abstract_register → label → label → ertl_statement
    29   | ertl_st_int: abstract_register → Byte → label → ertl_statement
    30   | ertl_st_move: abstract_register → abstract_register → label → ertl_statement
    31   | ertl_st_opaccs: OpAccs → abstract_register → abstract_register → abstract_register → label → ertl_statement
    32   | ertl_st_op1: Op1 → abstract_register → abstract_register → label → ertl_statement
    33   | ertl_st_op2: Op2 → abstract_register → abstract_register → abstract_register → label → ertl_statement
     20  | ertl_st_frame_size: register → label → ertl_statement
     21  | ertl_st_pop: register → label → ertl_statement
     22  | ertl_st_push: register → label → ertl_statement
     23  | ertl_st_addr_h: register → label → label → ertl_statement
     24  | ertl_st_addr_l: register → label → label → ertl_statement
     25  | ertl_st_int: register → Byte → label → ertl_statement
     26  | ertl_st_move: register → register → label → ertl_statement
     27  | ertl_st_opaccs: OpAccs → register → register → register → label → ertl_statement
     28  | ertl_st_op1: Op1 → register → register → label → ertl_statement
     29  | ertl_st_op2: Op2 → register → register → register → label → ertl_statement
    3430  | ertl_st_clear_carry: label → ertl_statement
    35   | ertl_st_load: abstract_register → abstract_register → abstract_register → label → ertl_statement
    36   | ertl_st_store: abstract_register → abstract_register → abstract_register → label → ertl_statement
     31  | ertl_st_load: register → register → register → label → ertl_statement
     32  | ertl_st_store: register → register → register → label → ertl_statement
    3733  | ertl_st_call_id: label → Byte → label → ertl_statement
    38   | ertl_st_cond_acc: abstract_register → label → label → ertl_statement
    39   | ertl_st_return: abstract_registers → ertl_statement.
     34  | ertl_st_cond_acc: register → label → label → ertl_statement
     35  | ertl_st_return: registers → ertl_statement.
    4036
    4137definition ertl_statement_graph ≝ graph ertl_statement.
Note: See TracChangeset for help on using the changeset viewer.