Changeset 1241 for src/ERTL/ERTL.ma


Ignore:
Timestamp:
Sep 21, 2011, 5:28:06 PM (9 years ago)
Author:
mulligan
Message:

changes for claudio

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1223 r1241  
    1313  | ertl_st_ext_frame_size: register → label → ertl_statement_extension.
    1414
     15definition ertl_params_: params_ ≝
     16  mk_params_ register register register register
     17    (move_registers × move_registers) register
     18      ertl_statement_extension unit (list register) nat.
     19
    1520definition ertl_params: params ≝
    16  mk_params
    17    register register register register
    18      (move_registers × move_registers) register
    19        ertl_statement_extension unit (list register) nat.
     21  mk_params ertl_params_ label.
    2022
    2123definition ertl_statement ≝ joint_statement ertl_params.
    2224
     25(*
    2326definition ertl_sem_params_ : ∀globals. sem_params_ ertl_params globals ≝
    2427 λglobals.
    2528  mk_sem_params_ ertl_params globals (graph (ertl_statement globals)) (lookup …).
     29*)
    2630
    2731definition ertl_internal_function ≝
    28   λglobals. joint_internal_function globals … (ertl_sem_params_ globals).
     32  joint_internal_function ertl_params.
    2933
    30 definition ertl_program ≝ λglobals. joint_program globals … (ertl_sem_params_ globals).
     34definition ertl_program ≝ joint_program ertl_params.
Note: See TracChangeset for help on using the changeset viewer.