source: src/LIN/LIN.ma @ 1224

Last change on this file since 1224 was 1224, checked in by sacerdot, 8 years ago

Type of programs in common/AST made more dependent.
In particular, the type of internal functions is now dependent on the
list of global variables. This is already used in the back-end to rule
out from the syntax programs that have free variables.

Note: only the test Clight/test/search.c.ma has been ported to the new type.
The porting requires two very minor changes.

File size: 1.3 KB
Line 
1include "joint/Joint.ma".
2
3definition lin_params: params ≝
4 mk_params
5   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
27definition lin_sem_params_: ∀globals. sem_params_ lin_params globals ≝
28 λglobals.
29  mk_sem_params_ lin_params globals (Σcode:list (lin_statement globals). well_formed_P … code) ?.
30(*CSC: lookup function to be implemented *)
31cases daemon
32qed.
33
34definition ltl_program ≝ λglobals. joint_program globals … (lin_sem_params_ globals).
35
36inductive lin_function_definition (globals: list ident): Type[0] ≝
37  lin_fu_internal: ∀code: list (lin_statement globals). well_formed_P ? ? code → lin_function_definition globals
38| lin_fu_external: external_function → lin_function_definition globals.
39
40record lin_program: Type[0] ≝
41{
42  lin_pr_vars: list (ident × nat);
43  lin_pr_funcs: list (ident × (lin_function_definition (map ? ? (fst ? ?) lin_pr_vars)));
44  lin_pr_main: option ident
45}.
Note: See TracBrowser for help on using the repository browser.