source: src/LIN/LIN.ma @ 1236

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

LTLToLin.ma completed (up to a couple of daemons used to provide dead code/data
that will be removed from the joint status later)

File size: 744 bytes
Line 
1include "joint/Joint.ma".
2
3definition lin_params: params ≝
4 mk_params (mk_params_ unit unit unit unit registers_move Register False unit unit unit) unit.
5
6definition 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
18(*
19definition lin_sem_params_: ∀globals. sem_params_ lin_params globals ≝
20 λglobals.
21  mk_sem_params_ lin_params globals (Σcode:list (lin_statement globals). well_formed_P … code) ?.
22(*CSC: lookup function to be implemented *)
23cases daemon
24qed.
25*)
26
27definition lin_program ≝ joint_program lin_params.
Note: See TracBrowser for help on using the repository browser.