|
Last change
on this file since 1224 was
1224,
checked in by sacerdot, 10 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 | |
|---|
| 1 | include "joint/Joint.ma". |
|---|
| 2 | |
|---|
| 3 | definition lin_params: params ≝ |
|---|
| 4 | mk_params |
|---|
| 5 | unit unit unit unit registers_move Register |
|---|
| 6 | unit unit unit unit. |
|---|
| 7 | |
|---|
| 8 | definition pre_lin_statement ≝ |
|---|
| 9 | λglobals: list ident. joint_statement lin_params globals. |
|---|
| 10 | |
|---|
| 11 | definition lin_statement ≝ |
|---|
| 12 | λglobals. |
|---|
| 13 | option ident × (pre_lin_statement globals). |
|---|
| 14 | |
|---|
| 15 | definition 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 | |
|---|
| 27 | definition 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 *) |
|---|
| 31 | cases daemon |
|---|
| 32 | qed. |
|---|
| 33 | |
|---|
| 34 | definition ltl_program ≝ λglobals. joint_program globals … (lin_sem_params_ globals). |
|---|
| 35 | |
|---|
| 36 | inductive 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 | |
|---|
| 40 | record 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.
