source: src/LIN/LIN.ma @ 733

Last change on this file since 733 was 723, checked in by mulligan, 9 years ago

Added dependent type internalising the invariant that LIN function bodies are non-empty and do not start with a label.

File size: 1.1 KB
Line 
1include "LIN/JointLTLLIN.ma".
2 
3definition PreLINStatement ≝ JointStatement unit.
4
5definition LINStatement ≝
6  λglobals.
7    option Identifier × (PreLINStatement globals).
8
9definition WellFormedP ≝
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      ]
19    ].
20   
21inductive LINFunctionDefinition (globals: list Identifier): Type[0] ≝
22  LIN_Fu_Internal: ∀code: list (LINStatement globals). WellFormedP ? ? code → LINFunctionDefinition globals
23| LIN_Fu_External: ExternalFunction → LINFunctionDefinition globals.
24
25record LINProgram: Type[0] ≝
26{
27  LIN_Pr_vars: list (Identifier × nat);
28  LIN_Pr_funs: list (Identifier × (LINFunctionDefinition (map ? ? (fst ? ?) LIN_Pr_vars)));
29  LIN_Pr_main: option Identifier
30}.
31
32definition LIN_Pr_vars:
33    LINProgram → list (Identifier × nat).
34  # r
35  cases r
36  # H1 # H2 #H3
37  @ H1
38qed.
39
40definition LIN_Pr_funs:
41  ∀p: LINProgram.
42    list (Identifier × (LINFunctionDefinition (map ? ? (fst ? ?) (LIN_Pr_vars p)))).
43  # r
44  cases r
45  # H1 # H2 #H3
46  @ H2
47qed.
Note: See TracBrowser for help on using the repository browser.