Changeset 1171 for src/ERTL/ERTL.ma


Ignore:
Timestamp:
Sep 2, 2011, 2:51:20 PM (9 years ago)
Author:
mulligan
Message:

changes made on claudio's request: changed order of nesting in the joint-ertl statements to make the semantics easier to write. big changes required...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1168 r1171  
    1515definition ertl_params: params ≝
    1616 mk_params register register register register (move_registers × move_registers) register.
     17                 
     18inductive ertl_statement_extension: Type[0] ≝
     19  | ertl_st_ext_new_frame: label → ertl_statement_extension
     20  | ertl_st_ext_del_frame: label → ertl_statement_extension
     21  | ertl_st_ext_frame_size: register → label → ertl_statement_extension.
    1722
    18 definition pre_ertl_statement ≝ joint_statement label ertl_params.
    19                  
    20 inductive ertl_statement (globals: list ident): Type[0] ≝
    21   | ertl_st_lift_pre: pre_ertl_statement globals → ertl_statement globals
    22   | ertl_st_new_frame: label → ertl_statement globals
    23   | ertl_st_del_frame: label → ertl_statement globals
    24   | ertl_st_frame_size: register → label → ertl_statement globals.
     23definition ertl_statement ≝ joint_statement label ertl_statement_extension ertl_params.
    2524
    2625definition ertl_statement_graph ≝ λglobals. graph (ertl_statement globals).
Note: See TracChangeset for help on using the changeset viewer.