source: src/LIN/LIN.ma @ 757

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

Lots more fixing to get both front and backends using same conventions and types.

File size: 1.1 KB
Line 
1include "LIN/JointLTLLIN.ma".
2 
3definition pre_lin_statement ≝ joint_statement unit.
4
5definition lin_statement ≝
6  λglobals.
7    option ident × (pre_lin_statement globals).
8
9definition well_formed_P ≝
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 lin_function_definition (globals: list ident): Type[0] ≝
22  lin_fu_internal: ∀code: list (lin_statement globals). well_formed_P ? ? code → lin_function_definition globals
23| lin_fu_external: external_function → lin_function_definition globals.
24
25record lin_program: Type[0] ≝
26{
27  lin_pr_vars: list (ident × nat);
28  lin_pr_funcs: list (ident × (lin_function_definition (map ? ? (fst ? ?) lin_pr_vars)));
29  lin_pr_main: option ident
30}.
31
32definition lin_pr_vars:
33    lin_program → list (ident × nat).
34  # r
35  cases r
36  # H1 # H2 #H3
37  @ H1
38qed.
39
40definition lin_pr_funcs:
41  ∀p: lin_program.
42    list (ident × (lin_function_definition (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.