source: src/LIN/LIN.ma @ 1132

Last change on this file since 1132 was 1132, checked in by mulligan, 10 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.