1 | (**************************************************************************) |
---|
2 | (* ___ *) |
---|
3 | (* ||M|| *) |
---|
4 | (* ||A|| A project by Andrea Asperti *) |
---|
5 | (* ||T|| *) |
---|
6 | (* ||I|| Developers: *) |
---|
7 | (* ||T|| The HELM team. *) |
---|
8 | (* ||A|| http://helm.cs.unibo.it *) |
---|
9 | (* \ / *) |
---|
10 | (* \ / This file is distributed under the terms of the *) |
---|
11 | (* v GNU General Public License Version 2 *) |
---|
12 | (* *) |
---|
13 | (**************************************************************************) |
---|
14 | |
---|
15 | include "joint/linearise.ma". |
---|
16 | include "common/StatusSimulation.ma". |
---|
17 | include "joint/Traces.ma". |
---|
18 | include "joint/SemanticUtils.ma". |
---|
19 | |
---|
20 | definition graph_abstract_status: |
---|
21 | ∀p:unserialized_params. |
---|
22 | (∀F.more_sem_unserialized_params p F) → |
---|
23 | joint_program (mk_graph_params p) → |
---|
24 | abstract_status |
---|
25 | ≝ |
---|
26 | λp,p',prog. |
---|
27 | joint_abstract_status |
---|
28 | (mk_prog_params |
---|
29 | (make_sem_graph_params (mk_graph_params p) (p' ?)) |
---|
30 | prog ⊥). |
---|
31 | @daemon (* I/O, TODO *) |
---|
32 | qed. |
---|
33 | |
---|
34 | definition lin_abstract_status: |
---|
35 | ∀p:unserialized_params. |
---|
36 | (∀F.more_sem_unserialized_params p F) → |
---|
37 | joint_program (mk_lin_params p) → |
---|
38 | abstract_status |
---|
39 | ≝ |
---|
40 | λp,p',prog. |
---|
41 | joint_abstract_status |
---|
42 | (mk_prog_params |
---|
43 | (make_sem_lin_params (mk_lin_params p) (p' ?)) |
---|
44 | prog ⊥). |
---|
45 | @daemon (* I/O, TODO *) |
---|
46 | qed. |
---|
47 | |
---|
48 | definition linearise_status_rel: |
---|
49 | ∀p,p',graph_prog. |
---|
50 | let lin_prog ≝ linearise ? graph_prog in |
---|
51 | status_rel |
---|
52 | (graph_abstract_status p p' graph_prog) |
---|
53 | (lin_abstract_status p p' lin_prog). |
---|
54 | cases daemon |
---|
55 | qed. |
---|
56 | |
---|
57 | lemma linearise_ok: |
---|
58 | ∀p,p',graph_prog. |
---|
59 | let lin_prog ≝ linearise ? graph_prog in |
---|
60 | status_simulation |
---|
61 | (graph_abstract_status p p' graph_prog) |
---|
62 | (lin_abstract_status p p' lin_prog) ≝ |
---|
63 | λp,p',graph_prog. mk_status_simulation … (linearise_status_rel p p' graph_prog) …. |
---|
64 | cases daemon |
---|
65 | qed. |
---|