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
RevLine 
[1168]1include "joint/Joint.ma".
[491]2
[1168]3definition lin_params: params ≝
[1233]4 mk_params (mk_params_ unit unit unit unit registers_move Register False unit unit unit) unit.
[1168]5
[1233]6definition lin_statement ≝ joint_statement lin_params.
[1168]7
[757]8definition well_formed_P ≝
[723]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
[1233]16      | None ⇒ True]].
[1224]17
[1233]18(*
[1224]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.
[1233]25*)
[1224]26
[1236]27definition lin_program ≝ joint_program lin_params.
Note: See TracBrowser for help on using the repository browser.