Changeset 756 for src/ERTL/ERTL.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/ERTL.ma

    r753 r756  
    33include "utilities/IdentifierTools.ma".
    44include "common/Graphs.ma".
     5include "common/CostLabel.ma".
     6include "common/Registers.ma".
    57
    6 inductive AbstractRegister: Type[0] ≝
    7   mkAbstractRegister: Word → AbstractRegister.
     8inductive abstract_register: Type[0] ≝
     9  mk_abstract_register: Word → abstract_register.
    810
    9 definition AbstractRegisters ≝ list AbstractRegister.
     11definition abstract_registers ≝ list abstract_register.
    1012
    11 inductive ERTLStatement: Type[0] ≝
    12   | ERTL_St_Skip: Identifier → ERTLStatement
    13   | ERTL_St_Comment: String → Identifier → ERTLStatement
    14   | ERTL_St_Cost: Identifier → Identifier → ERTLStatement
    15   | ERTL_St_Get_Hdw: Register → AbstractRegister → Identifier → ERTLStatement
    16   | ERTL_St_Set_Hdw: AbstractRegister → Register → Identifier → ERTLStatement
    17   | ERTL_St_Hdw_To_Hdw: Register → Register → Identifier → ERTLStatement
    18   | ERTL_St_NewFrame: Identifier → ERTLStatement
    19   | ERTL_St_DelFrame: Identifier → ERTLStatement
    20   | ERTL_St_FrameSize: AbstractRegister → Identifier → ERTLStatement
    21   | ERTL_St_Pop: AbstractRegister → Identifier → ERTLStatement
    22   | ERTL_St_Push: AbstractRegister → Identifier → ERTLStatement
    23   | ERTL_St_AddrH: AbstractRegister → Identifier → Identifier → ERTLStatement
    24   | ERTL_St_AddrL: AbstractRegister → Identifier → Identifier → ERTLStatement
    25   | ERTL_St_Int: AbstractRegister → Byte → Identifier → ERTLStatement
    26   | ERTL_St_Move: AbstractRegister → AbstractRegister → Identifier → ERTLStatement
    27   | ERTL_St_Opaccs: OpAccs → AbstractRegister → AbstractRegister → AbstractRegister → Identifier → ERTLStatement
    28   | ERTL_St_Op1: Op1 → AbstractRegister → AbstractRegister → Identifier → ERTLStatement
    29   | ERTL_St_Op2: Op2 → AbstractRegister → AbstractRegister → AbstractRegister → Identifier → ERTLStatement
    30   | ERTL_St_ClearCarry: Identifier → ERTLStatement
    31   | ERTL_St_Load: AbstractRegister → AbstractRegister → AbstractRegister → Identifier → ERTLStatement
    32   | ERTL_St_Store: AbstractRegister → AbstractRegister → AbstractRegister → Identifier → ERTLStatement
    33   | ERTL_St_Call_Id: Identifier → Byte → Identifier → ERTLStatement
    34   | ERTL_St_CondAcc: AbstractRegister → Identifier → Identifier → ERTLStatement
    35   | ERTL_St_Return: AbstractRegisters → ERTLStatement.
     13definition registers ≝ list register.
    3614
    37 definition ERTLStatementGraph ≝ graph ERTLStatement.
     15inductive ertl_statement: Type[0] ≝
     16  | ertl_st_skip: ident → ertl_statement
     17  | ertl_st_comment: String → ident → ertl_statement
     18  | ertl_st_cost: costlabel → ident → ertl_statement
     19  | ertl_st_get_hdw: register → abstract_register → ident → ertl_statement
     20  | ertl_st_set_hdw: abstract_register → register → ident → ertl_statement
     21  | ertl_st_hdw_to_hdw: register → register → ident → ertl_statement
     22  | ertl_st_new_frame: ident → ertl_statement
     23  | ertl_st_del_frame: ident → ertl_statement
     24  | ertl_st_frame_size: abstract_register → ident → ertl_statement
     25  | ertl_st_pop: abstract_register → ident → ertl_statement
     26  | ertl_st_push: abstract_register → ident → ertl_statement
     27  | ertl_st_addr_h: abstract_register → ident → ident → ertl_statement
     28  | ertl_st_addr_l: abstract_register → ident → ident → ertl_statement
     29  | ertl_st_int: abstract_register → Byte → ident → ertl_statement
     30  | ertl_st_move: abstract_register → abstract_register → ident → ertl_statement
     31  | ertl_st_opaccs: OpAccs → abstract_register → abstract_register → abstract_register → ident → ertl_statement
     32  | ertl_st_op1: Op1 → abstract_register → abstract_register → ident → ertl_statement
     33  | ertl_st_op2: Op2 → abstract_register → abstract_register → abstract_register → ident → ertl_statement
     34  | ertl_st_clear_carry: ident → ertl_statement
     35  | ertl_st_load: abstract_register → abstract_register → abstract_register → ident → ertl_statement
     36  | ertl_st_store: abstract_register → abstract_register → abstract_register → ident → ertl_statement
     37  | ertl_st_call_id: ident → Byte → ident → ertl_statement
     38  | ertl_st_cond_acc: abstract_register → ident → ident → ertl_statement
     39  | ertl_st_return: abstract_registers → ertl_statement.
    3840
    39 record ERTLInternalFunction: Type[0] ≝
     41definition ertl_statement_graph ≝ graph ertl_statement.
     42
     43record ertl_internal_function: Type[0] ≝
    4044{
    41   ERTL_IF_LUniverse: Universe;
    42   ERTL_IF_RUniverse: Universe;
    43   ERTL_IF_Params: Byte;
    44   ERTL_IF_Locals: BitVectorTrieSet 16;
    45   ERTL_IF_Graph: ERTLStatementGraph;
    46   ERTL_IF_Entry: Identifier;
    47   ERTL_IF_Exit: Identifier
     45  ertl_if_luniverse: universe LabelTag;
     46  ertl_if_runiverse: universe RegisterTag;
     47  ertl_if_params: nat;
     48  ertl_if_locals: registers;
     49  ertl_if_graph: ertl_statement_graph;
     50  ertl_if_entry: ident;
     51  ertl_if_exit: ident
    4852}.
    4953
    50 inductive ERTLFunction: Type[0] ≝
    51   | ERTL_Fu_Internal: ERTLInternalFunction → ERTLFunction
    52   | ERTL_Fu_External: ExternalFunction → ERTLFunction.
     54inductive ertl_function: Type[0] ≝
     55  | ertl_fu_internal: ertl_internal_function → ertl_function
     56  | ertl_fu_external: external_function → ertl_function.
    5357 
    54 record ERTLProgram: Type[0] ≝
     58record ertl_program: Type[0] ≝
    5559{
    56   ERTL_Pr_Vars: list (Identifier × nat);
    57   ERTL_Pr_Funcs: list (Identifier × ERTLFunction);
    58   ERTL_Pr_Main: option Identifier
     60  ertl_pr_vars: list (ident × nat);
     61  ertl_pr_funcs: list (ident × ertl_function);
     62  ertl_pr_main: option ident
    5963}.
    6064
    61 definition ERTL_Pr_Vars: ERTLProgram → list (Identifier × nat).
     65definition ertl_pr_vars: ertl_program → list (ident × nat).
    6266  # E
    6367  cases E
Note: See TracChangeset for help on using the changeset viewer.