Changeset 1280 for src/RTL/RTL.ma


Ignore:
Timestamp:
Sep 28, 2011, 2:43:37 AM (9 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/RTL/RTL.ma

    r1278 r1280  
    1010  | rtl_st_ext_tailcall_ptr: register → register → list register → rtl_statement_extension.
    1111
    12 definition rtl_params_: params_ ≝
    13  mk_params_
    14   (mk_params__ register register register register
    15     (register × register) register (list register) (list register)
    16       rtl_statement_extension (list register) (list register) (list register)) label.
     12definition rtl_params__: params__ ≝
     13 mk_params__ register register register register (register × register) register
     14  (list register) (list register) rtl_statement_extension.
     15definition rtl_params_: params_ ≝ graph_params_ rtl_params__.
     16definition rtl_params0: params0 ≝ mk_params0 rtl_params__ (list register) (list register).
     17definition rtl_params1: params1 ≝ rtl_ertl_params1 rtl_params0.
     18definition rtl_params: ∀globals. params globals ≝ rtl_ertl_params rtl_params0.
    1719
    1820definition rtl_statement ≝ joint_statement rtl_params_.
    1921
    20 definition rtl_params: ∀globals. params globals ≝ graph_params rtl_params_.
    21 
    2222definition rtl_internal_function ≝
    23   λglobals.
    24     joint_internal_function globals (rtl_params globals).
     23  λglobals. joint_internal_function … (rtl_params globals).
    2524
    2625definition rtl_program ≝ joint_program rtl_params.
     
    3534  | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension.
    3635
    37 definition rtlntc_params_: params_ ≝
    38  mk_params_
    39   (mk_params__ register register register register
    40     (register × register) register (list register) (list register)
    41       rtlntc_statement_extension (list register) (list register) (list register)) label.
     36definition rtlntc_params__: params__ ≝
     37 mk_params__ register register register register (register × register) register
     38  (list register) (list register) rtlntc_statement_extension.
     39definition rtlntc_params_: params_ ≝ graph_params_ rtlntc_params__.
     40definition rtlntc_params0: params0 ≝ mk_params0 rtlntc_params__ (list register) (list register).
     41definition rtlntc_params1: params1 ≝ rtl_ertl_params1 rtlntc_params0.
     42definition rtlntc_params: ∀globals. params globals ≝ rtl_ertl_params rtlntc_params0.
    4243
    4344definition rtlntc_statement ≝ joint_statement rtlntc_params_.
    4445
    45 definition rtlntc_params: ∀globals. params globals ≝ graph_params rtlntc_params_.
    46 
    4746definition rtlntc_internal_function ≝
    48   λglobals.
    49     joint_internal_function globals (rtlntc_params globals).
     47  λglobals. joint_internal_function … (rtlntc_params globals).
    5048
    5149definition rtlntc_program ≝ joint_program rtlntc_params.
Note: See TracChangeset for help on using the changeset viewer.