Changeset 487 for Deliverables/D3.1/Csemantics/Events.ma
 Timestamp:
 Feb 9, 2011, 11:49:17 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/Events.ma
r478 r487 22 22 (*include "Floats.ma".*) 23 23 include "Values.ma". 24 include " datatypes/list.ma".24 include "basics/list.ma". 25 25 include "extralib.ma". 26 26 include "CostLabel.ma". … … 37 37 world. *) 38 38 39 ninductive eventval: Type:=39 inductive eventval: Type[0] := 40 40  EVint: int > eventval 41 41  EVfloat: float > eventval. 42 42 43 ninductive event : Type≝43 inductive event : Type[0] ≝ 44 44  EVcost: costlabel → event 45 45  EVextcall: ∀ev_name: ident. ∀ev_args: list eventval. ∀ev_res: eventval. event. … … 48 48 Traces are of two kinds: finite (type [trace]) or infinite (type [traceinf]). *) 49 49 50 ndefinition trace := list event.51 52 ndefinition E0 : trace := nil ?.53 54 ndefinition Echarge : costlabel → trace ≝50 definition trace := list event. 51 52 definition E0 : trace := nil ?. 53 54 definition Echarge : costlabel → trace ≝ 55 55 λlabel. EVcost label :: (nil ?). 56 56 57 ndefinition Eextcall : ident → list eventval → eventval → trace ≝57 definition Eextcall : ident → list eventval → eventval → trace ≝ 58 58 λname: ident. λargs: list eventval. λres: eventval. 59 59 EVextcall name args res :: (nil ?). 60 60 61 ndefinition Eapp : trace → trace → trace ≝ λt1,t2. t1 @ t2.62 63 ncoinductive traceinf : Type:=61 definition Eapp : trace → trace → trace ≝ λt1,t2. t1 @ t2. 62 63 coinductive traceinf : Type[0] := 64 64  Econsinf: event > traceinf > traceinf. 65 65 66 nlet rec Eappinf (t: trace) (T: traceinf) on t : traceinf :=66 let rec Eappinf (t: trace) (T: traceinf) on t : traceinf := 67 67 match t with 68 68 [ nil => T … … 87 87 Infix "***" := Eappinf (at level 60, right associativity). 88 88 *) 89 nlemma E0_left: ∀t. E0 ⧺ t = t.90 //; nqed.91 92 nlemma E0_right: ∀t. t ⧺ E0 = t.93 napply append_nil; nqed.94 95 nlemma Eapp_assoc: ∀t1,t2,t3. (t1 ⧺ t2) ⧺ t3 = t1 ⧺ (t2 ⧺ t3).96 napply associative_append; nqed.97 98 nlemma Eapp_E0_inv: ∀t1,t2. t1 ⧺ t2 = E0 → t1 = E0 ∧ t2 = E0.99 napply nil_append_nil_both; nqed.89 lemma E0_left: ∀t. E0 ⧺ t = t. 90 //; qed. 91 92 lemma E0_right: ∀t. t ⧺ E0 = t. 93 @append_nil qed. 94 95 lemma Eapp_assoc: ∀t1,t2,t3. (t1 ⧺ t2) ⧺ t3 = t1 ⧺ (t2 ⧺ t3). 96 @associative_append qed. 97 98 lemma Eapp_E0_inv: ∀t1,t2. t1 ⧺ t2 = E0 → t1 = E0 ∧ t2 = E0. 99 @nil_append_nil_both qed. 100 100 101 nlemma E0_left_inf: ∀T. E0 ⧻ T = T.102 //; nqed.103 104 nlemma Eappinf_assoc: ∀t1,t2,T. (t1 ⧺ t2) ⧻ T = t1 ⧻ (t2 ⧻ T).105 #t1 ; nelim t1; #t2 T; nnormalize; //; nqed.101 lemma E0_left_inf: ∀T. E0 ⧻ T = T. 102 //; qed. 103 104 lemma Eappinf_assoc: ∀t1,t2,T. (t1 ⧺ t2) ⧻ T = t1 ⧻ (t2 ⧻ T). 105 #t1 elim t1; #t2 #T normalize; //; qed. 106 106 107 107 (* … … 137 137 infinite concatenations of nonempty finite traces. *) 138 138 139 ncoinductive traceinf': Type≝139 coinductive traceinf': Type[0] ≝ 140 140  Econsinf': ∀t: trace. ∀T: traceinf'. t ≠ E0 → traceinf'. 141 141 142 ndefinition split_traceinf' : ∀t:trace. traceinf' → t ≠ E0 → event × traceinf' ≝142 definition split_traceinf' : ∀t:trace. traceinf' → t ≠ E0 → event × traceinf' ≝ 143 143 λt,T. 144 144 match t return λt0.t0 ≠ E0 → ? with … … 150 150 ]) (refl ? t') 151 151 ]. 152 ##[ *; #NE; napply False_rect_Type0; napply NE; napply refl; 153 ## @; #E'; nrewrite > E' in E; #E; nwhd in E:(??%%); ndestruct (E);154 ##] nqed.155 156 nlet corec traceinf_of_traceinf' (T': traceinf') : traceinf ≝152 [ *; #NE @False_rect_Type0 @NE @refl 153  % #E' >E' in E #E whd in E:(??%%); destruct (E); 154 ] qed. 155 156 let corec traceinf_of_traceinf' (T': traceinf') : traceinf ≝ 157 157 match T' with 158 158 [ Econsinf' t T'' NOTEMPTY ⇒ 159 match split_traceinf' t T'' NOTEMPTY with [ mk_pair e tl ⇒159 match split_traceinf' t T'' NOTEMPTY with [ pair e tl ⇒ 160 160 Econsinf e (traceinf_of_traceinf' tl) ] 161 161 ]. 162 162 163 nremarkunroll_traceinf':163 lemma unroll_traceinf': 164 164 ∀T. T = match T with [ Econsinf' t T' NE ⇒ Econsinf' t T' NE ]. 165 #T ; ncases T; //; nqed.166 167 nremarkunroll_traceinf:165 #T cases T; //; qed. 166 167 lemma unroll_traceinf: 168 168 ∀T. T = match T with [ Econsinf t T' ⇒ Econsinf t T' ]. 169 #T ; ncases T; //;170 nqed.171 172 nlemma traceinf_traceinfp_app:169 #T cases T #ev #tr @refl (* XXX //; *) 170 qed. 171 172 lemma traceinf_traceinfp_app: 173 173 ∀t,T,NE. 174 174 traceinf_of_traceinf' (Econsinf' t T NE) = t ⧻ traceinf_of_traceinf' T. 175 #t ; nelim t;176 ##[ #T NE; ncases NE; #NE'; napply False_ind; napply NE'; napply refl; 177 ## #h t'; ncases t'; ##[ ##2: #h' t''; ##] #IH T NE; 178 nrewrite > (unroll_traceinf (traceinf_of_traceinf' ?));179 nwhd in ⊢ (??%?); //; nrewrite > (IH …); napply refl;180 ##] nqed.175 #t elim t; 176 [ #T #NE cases NE; #NE' @False_ind @NE' @refl 177  #h #t' cases t'; [ 2: #h' #t'' ] #IH #T #NE 178 >(unroll_traceinf (traceinf_of_traceinf' ?)) 179 whd in ⊢ (??%?); //; >(IH …) @refl 180 ] qed. 181 181 182 182 (* <<< *) … … 187 187 from the operating system. *) 188 188 189 ninductive eventval_match: eventval > typ > val > Prop :=189 inductive eventval_match: eventval > typ > val > Prop := 190 190  ev_match_int: 191 191 ∀i. eventval_match (EVint i) ASTint (Vint i) … … 193 193 ∀f. eventval_match (EVfloat f) ASTfloat (Vfloat f). 194 194 195 ninductive eventval_list_match: list eventval > list typ > list val > Prop :=195 inductive eventval_list_match: list eventval > list typ > list val > Prop := 196 196  evl_match_nil: 197 197 eventval_list_match (nil ?) (nil ?) (nil ?) … … 202 202 eventval_list_match (ev1::evl) (ty1::tyl) (v1::vl). 203 203 204 ninductive event_match:204 inductive event_match: 205 205 external_function > list val > trace > val > Prop := 206 206 event_match_intro:
Note: See TracChangeset
for help on using the changeset viewer.