source: src/LIN/LIN.ma @ 1132

Last change on this file since 1132 was 1132, checked in by mulligan, 8 years ago

reunified ltl and lin instruction type, removing lifting in ltl and lin and simplifying the ertl > ertl passes

File size: 869 bytes
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}.
Note: See TracBrowser for help on using the repository browser.