|
Last change
on this file since 1298 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:
1.2 KB
|
| Line | |
|---|
| 1 | include "joint/Joint.ma". |
|---|
| 2 | include "utilities/lists.ma". |
|---|
| 3 | |
|---|
| 4 | definition lin_params__: params__ ≝ |
|---|
| 5 | mk_params__ unit unit unit unit registers_move Register nat unit False. |
|---|
| 6 | definition lin_params_ : params_ ≝ mk_params_ lin_params__ unit. |
|---|
| 7 | definition lin_params0 : params0 ≝ mk_params0 lin_params__ unit unit. |
|---|
| 8 | definition lin_params1 : params1 ≝ mk_params1 lin_params0 unit. |
|---|
| 9 | |
|---|
| 10 | definition pre_lin_statement ≝ joint_statement lin_params_. |
|---|
| 11 | |
|---|
| 12 | definition well_formed_P ≝ |
|---|
| 13 | λA, B: Type[0]. |
|---|
| 14 | λcode: list (option A × B). |
|---|
| 15 | match code with |
|---|
| 16 | [ nil ⇒ False |
|---|
| 17 | | cons hd tl ⇒ |
|---|
| 18 | match \fst hd with |
|---|
| 19 | [ Some lbl ⇒ False |
|---|
| 20 | | None ⇒ True]]. |
|---|
| 21 | |
|---|
| 22 | definition lin_statement ≝ λglobals.(option label) × (pre_lin_statement globals). |
|---|
| 23 | |
|---|
| 24 | definition lin_params: ∀globals. params globals ≝ |
|---|
| 25 | λglobals. |
|---|
| 26 | mk_params globals unit lin_params1 (Σcode:list (lin_statement globals). well_formed_P … code) |
|---|
| 27 | (λcode:Σcode.?. λl. |
|---|
| 28 | find ?? (λs. let 〈l',x〉 ≝ s in |
|---|
| 29 | match l' with [ None ⇒ None … | Some l'' ⇒ if eq_identifier … l l'' then Some … x else None ?]) code). |
|---|
| 30 | |
|---|
| 31 | definition lin_function ≝ λglobals. joint_function … (lin_params globals). |
|---|
| 32 | |
|---|
| 33 | definition lin_program ≝ joint_program lin_params. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
