source: src/LIN/LIN.ma @ 1270

Last change on this file since 1270 was 1270, checked in by sacerdot, 8 years ago

Making RTL syntax an instance of Joint.

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