Changeset 1242


Ignore:
Timestamp:
Sep 21, 2011, 5:35:54 PM (8 years ago)
Author:
sacerdot
Message:

Some clean-up.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1241 r1242  
    11include "joint/Joint.ma".
    2 include "common/Graphs.ma".
    3 
    4 definition registers ≝ list register.
    52
    63inductive move_registers: Type[0] ≝
     
    1310  | ertl_st_ext_frame_size: register → label → ertl_statement_extension.
    1411
    15 definition ertl_params_: params_ ≝
    16   mk_params_ register register register register
     12definition ertl_params: params ≝
     13 mk_params
     14  (mk_params_ register register register register
    1715    (move_registers × move_registers) register
    18       ertl_statement_extension unit (list register) nat.
    19 
    20 definition ertl_params: params ≝
    21   mk_params ertl_params_ label.
     16      ertl_statement_extension unit (list register) nat) label.
    2217
    2318definition ertl_statement ≝ joint_statement ertl_params.
    2419
    25 (*
    26 definition ertl_sem_params_ : ∀globals. sem_params_ ertl_params globals ≝
    27  λglobals.
    28   mk_sem_params_ ertl_params globals (graph (ertl_statement globals)) (lookup …).
    29 *)
    30 
    31 definition ertl_internal_function ≝
    32   joint_internal_function ertl_params.
     20definition ertl_internal_function ≝ joint_internal_function ertl_params.
    3321
    3422definition ertl_program ≝ joint_program ertl_params.
Note: See TracChangeset for help on using the changeset viewer.