source: src/LIN/LIN.ma @ 1110

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

changes to get ltl to lin pass to work properly

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