source: src/common/StructuredTraces.ma @ 1536

Last change on this file since 1536 was 1536, checked in by campbell, 8 years ago

Use predicates throughout the structured traces.

File size: 5.1 KB
Line 
1include "basics/types.ma".
2include "basics/bool.ma".
3
4inductive status_class : Type[0] ≝
5| cl_return : status_class
6| cl_call   : status_class
7| cl_cost   : status_class
8| cl_nocost : status_class
9.
10
11record abstract_status : Type[1] ≝ {
12  as_status :> Type[0];
13  as_execute : as_status → as_status → Prop;
14  as_classifier : as_status → status_class → Prop;
15  as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
16}.
17
18inductive trace_ends_with_ret: Type[0] ≝
19  | ends_with_ret: trace_ends_with_ret
20  | doesnt_end_with_ret: trace_ends_with_ret.
21
22inductive trace_label_return (S:abstract_status) : S → S → Type[0] ≝
23  | tlr_base:
24      ∀status_before: S.
25      ∀status_after: S.
26        trace_label_label S ends_with_ret status_before status_after →
27        trace_label_return S status_before status_after
28  | tlr_step:
29      ∀status_initial: S.
30      ∀status_labelled: S.
31      ∀status_final: S.
32        trace_label_label S doesnt_end_with_ret status_initial status_labelled →
33        trace_label_return S status_labelled status_final →
34          trace_label_return S status_initial status_final
35with trace_label_label: trace_ends_with_ret → S → S → Type[0] ≝
36  | tll_base:
37      ∀ends_flag: trace_ends_with_ret.
38      ∀start_status: S.
39      ∀end_status: S.
40        trace_any_label S ends_flag start_status end_status →
41        as_classifier S start_status cl_cost →
42          trace_label_label S ends_flag start_status end_status
43with trace_any_label: trace_ends_with_ret → S → S → Type[0] ≝
44  | tal_base_not_return:
45      ∀start_status: S.
46      ∀final_status: S.
47        as_execute S start_status final_status →
48        ¬ as_classifier S start_status cl_return →
49        as_classifier S final_status cl_cost →
50          trace_any_label S doesnt_end_with_ret start_status final_status
51  | tal_base_return:
52      ∀start_status: S.
53      ∀final_status: S.
54        as_execute S start_status final_status →
55        as_classifier S start_status cl_return →
56          trace_any_label S ends_with_ret start_status final_status
57  | tal_step_call:
58      ∀end_flag: trace_ends_with_ret.
59      ∀status_pre_fun_call: S.
60      ∀status_after_fun_call: S.
61      ∀status_final: S.
62      ∀status_start_fun_call: S.
63        as_execute S status_pre_fun_call status_start_fun_call →
64        ∀H:as_classifier S status_pre_fun_call cl_call.
65          as_after_return S (dp ?? status_pre_fun_call H) status_after_fun_call →
66          trace_label_return S status_start_fun_call status_after_fun_call →
67          trace_any_label S end_flag status_after_fun_call status_final →
68            trace_any_label S end_flag status_pre_fun_call status_final
69  | tal_step_default:
70      ∀end_flag: trace_ends_with_ret.
71      ∀status_pre: S.
72      ∀status_end: S.
73      ∀status_init: S.
74        as_execute S status_pre status_init →
75        trace_any_label S end_flag status_init status_end →
76        as_classifier S status_pre cl_nocost →
77          trace_any_label S end_flag status_pre status_end.
78
79
80coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝
81  | tld_step:
82      ∀status_initial: S.
83      ∀status_labelled: S.
84          trace_label_label S doesnt_end_with_ret status_initial status_labelled →
85          trace_label_diverges S status_labelled →
86            trace_label_diverges S status_initial
87  | tld_base:
88      ∀status_initial: S.
89      ∀status_pre_fun_call: S.
90      ∀status_after_fun_call: S.
91      ∀status_start_fun_call: S.
92        trace_label_call S status_initial status_pre_fun_call →
93        as_execute S status_pre_fun_call status_start_fun_call →
94        ∀H:as_classifier S status_pre_fun_call cl_call.
95          trace_label_diverges S status_start_fun_call →
96            trace_label_diverges S status_initial
97             
98with trace_label_call: S → S → Type[0] ≝
99  | tlc_base:
100      ∀start_status: S.
101      ∀end_status: S.
102        trace_any_call S start_status end_status →
103        as_classifier S start_status cl_cost →
104        trace_label_call S start_status end_status
105       
106with trace_any_call: S → S → Type[0] ≝
107  | tac_base:
108      ∀status: S.
109        as_classifier S status cl_call →
110          trace_any_call S status status
111  | tac_step_call:
112      ∀status_pre_fun_call: S.
113      ∀status_after_fun_call: S.
114      ∀status_final: S.
115      ∀status_start_fun_call: S.
116        as_execute S status_pre_fun_call status_start_fun_call →
117        ∀H:as_classifier S status_pre_fun_call cl_call.
118          as_after_return S (dp ?? status_pre_fun_call H) status_after_fun_call →
119          trace_label_return S status_start_fun_call status_after_fun_call →
120          trace_any_call S status_after_fun_call status_final →
121            trace_any_call S status_pre_fun_call status_final
122  | tac_step_default:
123      ∀status_pre: S.
124      ∀status_end: S.
125      ∀status_init: S.
126        as_execute S status_pre status_init →
127        trace_any_call S status_init status_end →
128        as_classifier S status_pre cl_nocost →
129          trace_any_call S status_pre status_end.
130
Note: See TracBrowser for help on using the repository browser.