|
Last change
on this file since 1363 was
1281,
checked in by sacerdot, 9 years ago
|
|
Porting of all transformation to the joint syntax practically completed.
Some functions remain to be ported in RTLAbstoRTL, but it is just repetitive
coding.
|
|
File size:
635 bytes
|
| Line | |
|---|
| 1 | include "joint/Joint.ma". |
|---|
| 2 | |
|---|
| 3 | definition ltl_params__: params__ ≝ |
|---|
| 4 | (mk_params__ unit unit unit unit registers_move Register nat unit False). |
|---|
| 5 | definition ltl_params_ : params_ ≝ graph_params_ ltl_params__. |
|---|
| 6 | definition ltl_params0 : params0 ≝ mk_params0 ltl_params__ unit unit. |
|---|
| 7 | definition ltl_params1 : params1 ≝ mk_params1 ltl_params0 unit. |
|---|
| 8 | definition ltl_params: ∀globals. params globals ≝ graph_params ltl_params1. |
|---|
| 9 | |
|---|
| 10 | definition ltl_statement ≝ joint_statement ltl_params_. |
|---|
| 11 | |
|---|
| 12 | definition ltl_program ≝ joint_program ltl_params. |
|---|
| 13 | |
|---|
| 14 | definition ltl_internal_function ≝ |
|---|
| 15 | λglobals. joint_internal_function … (ltl_params globals). |
|---|
Note: See
TracBrowser
for help on using the repository browser.
