|
Last change
on this file since 1246 was
1246,
checked in by sacerdot, 9 years ago
|
|
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 size:
451 bytes
|
| Line | |
|---|
| 1 | include "joint/Joint.ma". |
|---|
| 2 | include alias "common/Graphs.ma". |
|---|
| 3 | |
|---|
| 4 | definition ltl_params_: params_ ≝ |
|---|
| 5 | mk_params_ (mk_params__ unit unit unit unit registers_move Register False unit unit unit) label. |
|---|
| 6 | |
|---|
| 7 | definition ltl_statement ≝ joint_statement ltl_params_. |
|---|
| 8 | |
|---|
| 9 | definition ltl_params: ∀globals. params globals ≝ |
|---|
| 10 | λglobals. mk_params globals ltl_params_ (graph (ltl_statement globals)) (lookup …). |
|---|
| 11 | |
|---|
| 12 | definition ltl_program ≝ joint_program ltl_params. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
