source: src/LIN/LIN.ma @ 1281

Last change on this file since 1281 was 1281, checked in by sacerdot, 10 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.