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 | |
---|
1 | include "joint/Joint.ma". |
---|
2 | |
---|
3 | definition lin_params: params ≝ |
---|
4 | mk_params (mk_params_ unit unit unit unit registers_move Register False unit unit unit) unit. |
---|
5 | |
---|
6 | definition lin_statement ≝ joint_statement lin_params. |
---|
7 | |
---|
8 | definition 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 | (* |
---|
19 | definition 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 *) |
---|
23 | cases daemon |
---|
24 | qed. |
---|
25 | *) |
---|
26 | |
---|
27 | definition lin_program ≝ joint_program lin_params. |
---|
Note: See
TracBrowser
for help on using the repository browser.