Last change
on this file since 1183 was
1183,
checked in by mulligan, 10 years ago
|
removed parameterised label types in the three lowest level languages
|
File size:
1020 bytes
|
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 | inductive 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 | |
---|
31 | record 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.