Changeset 1280 for src/ERTL


Ignore:
Timestamp:
Sep 28, 2011, 2:43:37 AM (8 years ago)
Author:
sacerdot
Message:

Some progress in the porting of RTLAbstoRTL to the joint syntax:

1) common code with RTLtoERTL factorized out in joint/TranslateUtils.ma
2) this required yet another refactoring of the parameters in Joint.ma
3) RTLtoERTL ported to the new parameters; LTLtoLIN and LINtoASM are

probably broken but easily fixable a.t.m. RTLAbstoRTL still in progress,
but the difficult part is almost done.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1270 r1280  
    1010  | ertl_st_ext_frame_size: register → ertl_statement_extension.
    1111
    12 definition ertl_params_: params_ ≝
    13  mk_params_
    14   (mk_params__ register register register register
    15     (move_registers × move_registers) register nat unit
    16       ertl_statement_extension unit (list register) nat) label.
     12definition ertl_params__: params__ ≝
     13 mk_params__ register register register register (move_registers × move_registers)
     14  register nat unit ertl_statement_extension.
     15definition ertl_params_: params_ ≝ graph_params_ ertl_params__.
     16definition ertl_params0: params0 ≝ mk_params0 ertl_params__ unit nat.
     17definition ertl_params1: params1 ≝ rtl_ertl_params1 ertl_params0.
     18definition ertl_params: ∀globals. params globals ≝ rtl_ertl_params ertl_params0.
    1719
    1820definition ertl_statement ≝ joint_statement ertl_params_.
    1921
    20 definition ertl_params: ∀globals. params globals ≝ graph_params ertl_params_.
    21 
    2222definition ertl_internal_function ≝
    23   λglobals.
    24     joint_internal_function globals (ertl_params globals).
     23  λglobals.joint_internal_function … (ertl_params globals).
    2524
    2625definition ertl_program ≝ joint_program ertl_params.
Note: See TracChangeset for help on using the changeset viewer.