Changeset 1806 for src/common/StructuredTraces.ma
- Timestamp:
- Mar 5, 2012, 12:38:26 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/StructuredTraces.ma
r1783 r1806 95 95 trace_any_label S end_flag status_pre status_end. 96 96 97 coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝ 98 | tld_step: 99 ∀status_initial: S. 100 ∀status_labelled: S. 101 trace_label_label S doesnt_end_with_ret status_initial status_labelled → 102 trace_label_diverges S status_labelled → 103 trace_label_diverges S status_initial 104 | tld_base: 105 ∀status_initial: S. 106 ∀status_pre_fun_call: S. 107 ∀status_start_fun_call: S. 108 trace_label_call S status_initial status_pre_fun_call → 109 as_execute S status_pre_fun_call status_start_fun_call → 110 ∀H:as_classifier S status_pre_fun_call cl_call. 111 trace_label_diverges S status_start_fun_call → 112 trace_label_diverges S status_initial 113 114 with trace_label_call: S → S → Type[0] ≝ 115 | tlc_base: 116 ∀start_status: S. 117 ∀end_status: S. 118 trace_any_call S start_status end_status → 119 as_costed S start_status → 120 trace_label_call S start_status end_status 121 122 with trace_any_call: S → S → Type[0] ≝ 97 inductive trace_any_call (S:abstract_status) : S → S → Type[0] ≝ 123 98 | tac_base: 124 99 ∀status: S. … … 147 122 trace_any_call S status_pre status_end. 148 123 124 125 coinductive 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 142 with 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 149 151 let rec trace_any_label_label S s s' f 150 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 ] ≝ … … 164 166 qed. 165 167 168 lemma 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 // 171 qed.
Note: See TracChangeset
for help on using the changeset viewer.