source: src/LIN/LIN.ma @ 1163

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

even more streamlining and fixes to get things type checking

File size: 996 bytes
Line 
1include "LIN/JointLTLLIN.ma".
2 
3definition pre_lin_statement ≝
4  λglobals.
5  joint_statement unit globals Register Register
6                  Register Register Register
7                  (Register × Register).
8
9definition lin_statement ≝
10  λglobals.
11    option ident × (pre_lin_statement globals).
12
13definition well_formed_P ≝
14  λA, B: Type[0].
15  λcode: list (option A × B).
16    match code with
17    [ nil ⇒ False
18    | cons hd tl ⇒
19      match \fst hd with
20      [ Some lbl ⇒ False
21      | None ⇒ True
22      ]
23    ].
24   
25inductive lin_function_definition (globals: list ident): Type[0] ≝
26  lin_fu_internal: ∀code: list (lin_statement globals). well_formed_P ? ? code → lin_function_definition globals
27| lin_fu_external: external_function → lin_function_definition globals.
28
29record lin_program: Type[0] ≝
30{
31  lin_pr_vars: list (ident × nat);
32  lin_pr_funcs: list (ident × (lin_function_definition (map ? ? (fst ? ?) lin_pr_vars)));
33  lin_pr_main: option ident
34}.
Note: See TracBrowser for help on using the repository browser.