source: src/LIN/LIN.ma @ 1363

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: 1.2 KB
RevLine 
[1168]1include "joint/Joint.ma".
[1246]2include "utilities/lists.ma".
[491]3
[1281]4definition lin_params__: params__ ≝
5 mk_params__ unit unit unit unit registers_move Register nat unit False.
6definition lin_params_ : params_ ≝ mk_params_ lin_params__ unit.
7definition lin_params0 : params0 ≝ mk_params0 lin_params__ unit unit.
8definition lin_params1 : params1 ≝ mk_params1 lin_params0 unit.
[1168]9
[1246]10definition pre_lin_statement ≝ joint_statement lin_params_.
[1168]11
[757]12definition well_formed_P ≝
[723]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
[1233]20      | None ⇒ True]].
[1224]21
[1246]22definition lin_statement ≝ λglobals.(option label) × (pre_lin_statement globals).
23
24definition lin_params: ∀globals. params globals ≝
[1224]25 λglobals.
[1281]26  mk_params globals unit lin_params1 (Σcode:list (lin_statement globals). well_formed_P … code)
[1246]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).
[1224]30
[1264]31definition lin_function ≝ λglobals. joint_function … (lin_params globals).
32
[1281]33definition lin_program ≝ joint_program lin_params.
Note: See TracBrowser for help on using the repository browser.