Changeset 1270 for src/RTL/RTL.ma


Ignore:
Timestamp:
Sep 26, 2011, 3:59:28 PM (9 years ago)
Author:
sacerdot
Message:

Making RTL syntax an instance of Joint.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL.ma

    r1239 r1270  
    1 include "basics/list.ma".
    2 include "common/Registers.ma".
    3 include "common/AST.ma".
    4 include "common/Graphs.ma".
    5 include "common/CostLabel.ma".
     1include "joint/Joint.ma".
    62
    7 definition registers ≝ list register.
     3(*CSC: XXX PROBLEM HERE. Tailcalls are not instructions, but statements since they
     4  are not sequential. Thus there is a dummy label at the moment in the code.
     5  To be fixed once we understand exactly what to do with tail calls. *)
     6inductive rtl_statement_extension: Type[0] ≝
     7  | rtl_st_ext_call_ptr: register → register → list register → list register → rtl_statement_extension
     8  | rtl_st_ext_tailcall_id: ident → list register → rtl_statement_extension
     9  | rtl_st_ext_tailcall_ptr: register → register → list register → rtl_statement_extension.
    810
    9 inductive rtl_statement: Type[0] ≝
    10   | rtl_st_skip: label → rtl_statement
    11   | rtl_st_cost: costlabel → label → rtl_statement
    12                 (* ldest, hdest, symbol, next *)
    13   | rtl_st_addr: register → register → ident → label → rtl_statement
    14                 (* ldest, hdest, next *)
    15   | rtl_st_stack_addr: register → register → label → rtl_statement
    16   | rtl_st_int: register → Byte → label → rtl_statement
    17                 (* dest, src, next *)
    18   | rtl_st_move: register → register → label → rtl_statement
    19   | rtl_st_clear_carry: label → rtl_statement
    20                 (* op, acc dest, bacc dest, acc src, bacc src, next *)
    21   | rtl_st_opaccs: OpAccs → register → register → register → register → label → rtl_statement
    22                 (* op, dest, src, next *)
    23   | rtl_st_op1: Op1 → register → register → label → rtl_statement
    24                 (* op, dest, src1, src2, next *)
    25   | rtl_st_op2: Op2 → register → register → register → label → rtl_statement
    26   | rtl_st_load: register → register → register → label → rtl_statement
    27   | rtl_st_store: register → register → register → label → rtl_statement
    28   | rtl_st_call_id: ident → registers → registers → label → rtl_statement
    29   | rtl_st_call_ptr: register → register → registers → registers → label → rtl_statement
    30   | rtl_st_tailcall_id: ident → registers → rtl_statement
    31   | rtl_st_tailcall_ptr: register → register → registers → rtl_statement
    32   | rtl_st_cond: register → label → label → rtl_statement
    33   | rtl_st_set_carry: label → rtl_statement
    34   | rtl_st_return: rtl_statement.
    35  
    36 definition rtl_statement_graph ≝ graph rtl_statement.
     11definition rtl_params_: params_ ≝
     12 mk_params_
     13  (mk_params__ register register register register
     14    (register × register) register (list register) (list register)
     15      rtl_statement_extension unit (list register) (list register)) label.
    3716
    38 record rtl_internal_function: Type[0] ≝
    39 {
    40   rtl_if_luniverse: universe LabelTag;
    41   rtl_if_runiverse: universe RegisterTag;
    42 (*  rtl_if_sig: signature;  -- dropped in front end *)
    43   rtl_if_result   : registers;
    44   rtl_if_params   : registers;
    45   rtl_if_locals   : registers;
    46   rtl_if_stacksize: nat;
    47   rtl_if_graph    : rtl_statement_graph;
    48   rtl_if_entry    : Σl: label. lookup ? ? rtl_if_graph l ≠ None ?;
    49   rtl_if_exit     : Σl: label. lookup ? ? rtl_if_graph l ≠ None ?
    50 }.
     17definition rtl_statement ≝ joint_statement rtl_params_.
    5118
    52 definition rtl_function_definition ≝ fundef rtl_internal_function.
     19definition rtl_params: ∀globals. params globals ≝ graph_params rtl_params_.
    5320
    54 definition rtl_program: Type[0] ≝ program (λ_.rtl_function_definition) nat.
     21definition rtl_internal_function ≝
     22  λglobals.
     23    joint_internal_function globals (rtl_params globals).
     24
     25definition rtl_program ≝ joint_program rtl_params.
Note: See TracChangeset for help on using the changeset viewer.