source: src/LIN/LIN.ma @ 1179

Last change on this file since 1179 was 1179, checked in by mulligan, 10 years ago

changes to ertl, ltl and lin to use new notion of joint params. ertl to ltl pass in process of being changed

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