Changeset 1246 for src/LTL/LTL.ma


Ignore:
Timestamp:
Sep 22, 2011, 2:50:44 AM (8 years ago)
Author:
sacerdot
Message:

Yet another change to Joint.ma to accomodate all passes.
The concrete memory representation for the code of internal functions is
back, at the price of more complexity in the definition of the parameters.

Note: I do not understand any more the well_formed_P invariant for LIN code.
Moreover, the invariant does not seem to hold for code produced using LTLToLin.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTL.ma

    r1233 r1246  
    11include "joint/Joint.ma".
    2 include "common/Graphs.ma".
     2include alias "common/Graphs.ma".
    33
    4 definition ltl_params: params
    5  mk_params (mk_params_ unit unit unit unit registers_move Register False unit unit unit) label.
     4definition ltl_params_: params_
     5 mk_params_ (mk_params__ unit unit unit unit registers_move Register False unit unit unit) label.
    66
    7 definition ltl_statement ≝ joint_statement ltl_params.
     7definition ltl_statement ≝ joint_statement ltl_params_.
    88
    9 (*definition ltl_sem_params_: ∀globals. sem_params_ ltl_params globals ≝
    10  λglobals.
    11   mk_sem_params_ ltl_params globals (graph (ltl_statement globals)) (lookup …).*)
     9definition ltl_params: ∀globals. params globals ≝
     10 λglobals. mk_params globals ltl_params_ (graph (ltl_statement globals)) (lookup …).
    1211
    1312definition ltl_program ≝ joint_program ltl_params.
Note: See TracChangeset for help on using the changeset viewer.