Changeset 1280 for src/LTL/LTL.ma


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/LTL/LTL.ma

    r1271 r1280  
    22
    33definition ltl_params_: params_ ≝
    4  mk_params_ (mk_params__ unit unit unit unit registers_move Register nat unit False unit unit unit) label.
     4 label_params__of_params__
     5  (mk_params__ unit unit unit unit registers_move Register nat unit False unit
     6    unit unit).
    57
    68definition ltl_statement ≝ joint_statement ltl_params_.
Note: See TracChangeset for help on using the changeset viewer.