source: src/LIN/LIN.ma @ 1378

Last change on this file since 1378 was 1378, checked in by sacerdot, 9 years ago

New file LIN/joint_LTL_LIN.ma to factorize out the syntactic parameters shared
by LTL and LIN.

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