source: src/LIN/LIN.ma @ 1168

Last change on this file since 1168 was 1168, checked in by sacerdot, 9 years ago

Joint statements parameterized over a record.

File size: 997 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 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.