Last change
on this file since 1264 was
1264,
checked in by sacerdot, 10 years ago
|
Almost ported to new Joint syntax.
|
File size:
1.0 KB
|
Line | |
---|
1 | include "joint/Joint.ma". |
---|
2 | include "utilities/lists.ma". |
---|
3 | |
---|
4 | definition lin_params_: params_ ≝ |
---|
5 | mk_params_ (mk_params__ unit unit unit unit registers_move Register False unit unit unit) unit. |
---|
6 | |
---|
7 | definition pre_lin_statement ≝ joint_statement lin_params_. |
---|
8 | |
---|
9 | definition well_formed_P ≝ |
---|
10 | λA, B: Type[0]. |
---|
11 | λcode: list (option A × B). |
---|
12 | match code with |
---|
13 | [ nil ⇒ False |
---|
14 | | cons hd tl ⇒ |
---|
15 | match \fst hd with |
---|
16 | [ Some lbl ⇒ False |
---|
17 | | None ⇒ True]]. |
---|
18 | |
---|
19 | definition lin_statement ≝ λglobals.(option label) × (pre_lin_statement globals). |
---|
20 | |
---|
21 | definition lin_params: ∀globals. params globals ≝ |
---|
22 | λglobals. |
---|
23 | mk_params globals lin_params_ (Σcode:list (lin_statement globals). well_formed_P … code) |
---|
24 | (λcode:Σcode.?. λl. |
---|
25 | find ?? (λs. let 〈l',x〉 ≝ s in |
---|
26 | match l' with [ None ⇒ None … | Some l'' ⇒ if eq_identifier … l l'' then Some … x else None ?]) code). |
---|
27 | |
---|
28 | definition lin_function ≝ λglobals. joint_function … (lin_params globals). |
---|
29 | |
---|
30 | definition lin_program ≝ joint_program lin_params. |
---|
Note: See
TracBrowser
for help on using the repository browser.