source: src/LIN/LIN.ma @ 1281

Last change on this file since 1281 was 1281, checked in by sacerdot, 8 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 
1include "joint/Joint.ma".
2include "utilities/lists.ma".
3
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.
9
10definition pre_lin_statement ≝ joint_statement lin_params_.
11
12definition 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
22definition lin_statement ≝ λglobals.(option label) × (pre_lin_statement globals).
23
24definition 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
31definition lin_function ≝ λglobals. joint_function … (lin_params globals).
32
33definition lin_program ≝ joint_program lin_params.
Note: See TracBrowser for help on using the repository browser.