source: src/LIN/LIN.ma @ 1171

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

changes made on claudio's request: changed order of nesting in the joint-ertl statements to make the semantics easier to write. big changes required...

File size: 1002 bytes
Line 
1include "joint/Joint.ma".
2
3definition lin_params: params ≝
4 mk_params unit unit unit unit registers_move Register.
5
6definition pre_lin_statement ≝
7 λglobals: list ident. joint_statement unit unit lin_params globals.
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.