source: src/common/StructuredTraces.ma @ 1806

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

Show that we could construct RTLabs non-terminating structured traces
if it weren't for Prop/Type?/coinduction issue.
Separate out the inductive part of the coinductive structured traces so
that we get an induction principle.

File size: 7.0 KB
Line 
1include "basics/types.ma".
2include "basics/bool.ma".
3include "basics/jmeq.ma".
4
5inductive status_class : Type[0] ≝
6| cl_return : status_class
7| cl_jump   : status_class
8| cl_call   : status_class
9| cl_other : status_class.
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_costed : as_status → Prop;
16  as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
17}.
18
19inductive trace_ends_with_ret: Type[0] ≝
20  | ends_with_ret: trace_ends_with_ret
21  | doesnt_end_with_ret: trace_ends_with_ret.
22
23inductive trace_label_return (S:abstract_status) : S → S → Type[0] ≝
24  | tlr_base:
25      ∀status_before: S.
26      ∀status_after: S.
27        trace_label_label S ends_with_ret status_before status_after →
28        trace_label_return S status_before status_after
29  | tlr_step:
30      ∀status_initial: S.
31      ∀status_labelled: S.
32      ∀status_final: S.
33        trace_label_label S doesnt_end_with_ret status_initial status_labelled →
34        trace_label_return S status_labelled status_final →
35          trace_label_return S status_initial status_final
36with trace_label_label: trace_ends_with_ret → S → S → Type[0] ≝
37  | tll_base:
38      ∀ends_flag: trace_ends_with_ret.
39      ∀start_status: S.
40      ∀end_status: S.
41        trace_any_label S ends_flag start_status end_status →
42        as_costed S start_status →
43          trace_label_label S ends_flag start_status end_status
44with trace_any_label: trace_ends_with_ret → S → S → Type[0] ≝
45  (* Single steps within a function which reach a label.
46     Note that this is the only case applicable for a jump. *)
47  | tal_base_not_return:
48      ∀start_status: S.
49      ∀final_status: S.
50        as_execute S start_status final_status →
51        (as_classifier S start_status cl_jump ∨
52         as_classifier S start_status cl_other) →
53        as_costed S final_status →
54          trace_any_label S doesnt_end_with_ret start_status final_status
55  | tal_base_return:
56      ∀start_status: S.
57      ∀final_status: S.
58        as_execute S start_status final_status →
59        as_classifier S start_status cl_return →
60          trace_any_label S ends_with_ret start_status final_status
61  (* A call followed by a label on return. *)
62  | tal_base_call:
63      ∀status_pre_fun_call: S.
64      ∀status_start_fun_call: S.
65      ∀status_final: S.
66        as_execute S status_pre_fun_call status_start_fun_call →
67        ∀H:as_classifier S status_pre_fun_call cl_call.
68          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_final →
69          trace_label_return S status_start_fun_call status_final →
70          as_costed S status_final →
71            trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
72  (* A call followed by a non-empty trace. *)
73  | tal_step_call:
74      ∀end_flag: trace_ends_with_ret.
75      ∀status_pre_fun_call: S.
76      ∀status_start_fun_call: S.
77      ∀status_after_fun_call: S.
78      ∀status_final: S.
79        as_execute S status_pre_fun_call status_start_fun_call →
80        ∀H:as_classifier S status_pre_fun_call cl_call.
81          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call →
82          trace_label_return S status_start_fun_call status_after_fun_call →
83          ¬ as_costed S status_after_fun_call →
84          trace_any_label S end_flag status_after_fun_call status_final →
85            trace_any_label S end_flag status_pre_fun_call status_final
86  | tal_step_default:
87      ∀end_flag: trace_ends_with_ret.
88      ∀status_pre: S.
89      ∀status_init: S.
90      ∀status_end: S.
91        as_execute S status_pre status_init →
92        trace_any_label S end_flag status_init status_end →
93        as_classifier S status_pre cl_other →
94        ¬ (as_costed S status_init) →
95          trace_any_label S end_flag status_pre status_end.
96
97inductive trace_any_call (S:abstract_status) : S → S → Type[0] ≝
98  | tac_base:
99      ∀status: S.
100        as_classifier S status cl_call →
101          trace_any_call S status status
102  | tac_step_call:
103      ∀status_pre_fun_call: S.
104      ∀status_after_fun_call: S.
105      ∀status_final: S.
106      ∀status_start_fun_call: S.
107        as_execute S status_pre_fun_call status_start_fun_call →
108        ∀H:as_classifier S status_pre_fun_call cl_call.
109          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call →
110          trace_label_return S status_start_fun_call status_after_fun_call →
111          ¬ as_costed S status_after_fun_call →
112          trace_any_call S status_after_fun_call status_final →
113            trace_any_call S status_pre_fun_call status_final
114  | tac_step_default:
115      ∀status_pre: S.
116      ∀status_end: S.
117      ∀status_init: S.
118        as_execute S status_pre status_init →
119        trace_any_call S status_init status_end →
120        as_classifier S status_pre cl_other →
121        ¬ (as_costed S status_init) →
122          trace_any_call S status_pre status_end.
123
124
125coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝
126  | tld_step:
127      ∀status_initial: S.
128      ∀status_labelled: S.
129          trace_label_label S doesnt_end_with_ret status_initial status_labelled →
130          trace_label_diverges S status_labelled →
131            trace_label_diverges S status_initial
132  | tld_base:
133      ∀status_initial: S.
134      ∀status_pre_fun_call: S.
135      ∀status_start_fun_call: S.
136        trace_label_call S status_initial status_pre_fun_call →
137        as_execute S status_pre_fun_call status_start_fun_call →
138        ∀H:as_classifier S status_pre_fun_call cl_call.
139          trace_label_diverges S status_start_fun_call →
140            trace_label_diverges S status_initial
141             
142with trace_label_call: S → S → Type[0] ≝
143  | tlc_base:
144      ∀start_status: S.
145      ∀end_status: S.
146        trace_any_call S start_status end_status →
147        as_costed S start_status →
148        trace_label_call S start_status end_status
149.       
150
151let rec trace_any_label_label S s s' f
152  (tr:trace_any_label S f s s') on tr : match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ] ≝
153match tr return λf,s,s',tr. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ] with
154[ tal_base_not_return start final _ _ C ⇒ C
155| tal_base_return _ _  _ _ ⇒ I
156| tal_base_call _ _ _ _ _ _ _ C ⇒ C
157| tal_step_call f pre start after final X C RET LR C' tr' ⇒ trace_any_label_label … tr'
158| tal_step_default f pre init end X tr' C C' ⇒ trace_any_label_label … tr'
159].
160
161lemma trace_label_label_label : ∀S,s,s',f.
162  ∀tr:trace_label_label S f s s'. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ].
163#S #s #s' #f #tr
164cases tr
165#f #start #end #tr' #C @(trace_any_label_label … tr')
166qed.
167
168lemma trace_any_call_call : ∀S,s,s'.
169  trace_any_call S s s' → as_classifier S s' cl_call.
170#S #s #s' #T elim T //
171qed.
Note: See TracBrowser for help on using the repository browser.