Changeset 2293
 Timestamp:
 Aug 13, 2012, 12:21:28 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r2288 r2293 132 132 left. Functions are identified by their function pointer block because 133 133 this avoids introducing functions to map back pointers to function ids using 134 the global environment. (See the comment at the start of this file, too.) *) 134 the global environment. (See the comment at the start of this file, too.) 135 136 Calls also get the caller's instruction label (or None for the initial call) 137 so that we can distinguish different calls. This is used only for the 138 t.*_unrepeating property, which includes the pc for call states. 139 *) 135 140 136 141 inductive RTLabs_pc : Type[0] ≝ 137 142  rapc_state : block → label → RTLabs_pc 138  rapc_call : block → RTLabs_pc143  rapc_call : option label → block → RTLabs_pc 139 144  rapc_ret : option block → RTLabs_pc 140 145  rapc_fin : RTLabs_pc 141 146 . 142 147 148 (* TODO: move to pointers *) 149 unification hint 0 ≔ ; D ≟ block_eq 150 (**)⊢ 151 block ≡ carr D. 152 143 153 definition RTLabs_pc_eq : RTLabs_pc → RTLabs_pc → bool ≝ 144 154 λx,y. match x with 145 155 [ rapc_state b1 l1 ⇒ match y with [ rapc_state b2 l2 ⇒ eq_block b1 b2 ∧ eq_identifier … l1 l2  _ ⇒ false ] 146  rapc_call b1 ⇒ match y with [ rapc_call b2 ⇒ eq_block b1 b2  _ ⇒ false ] 147  rapc_ret b1 ⇒ match y with [ rapc_ret b2 ⇒ eq_option block_eq b1 b2  _ ⇒ false ] 156  rapc_call o1 b1 ⇒ match y with [ rapc_call o2 b2 ⇒ 157 eqb ? o1 o2 158 ∧ eq_block b1 b2 159  _ ⇒ false ] 160  rapc_ret b1 ⇒ match y with [ rapc_ret b2 ⇒ eqb ? b1 b2  _ ⇒ false ] 148 161  rapc_fin ⇒ match y with [ rapc_fin ⇒ true  _ ⇒ false ] 149 162 ]. 150 163 164 (* TODO: move *) 165 lemma eqb_elim : ∀D:DeqSet. ∀P:bool → Type[0]. ∀x,y:D. 166 (x = y → P true) → 167 (x ≠ y → P false) → 168 P (eqb D x y). 169 #D #P #x #y #T #F lapply (eqb_true D x y) cases (eqb D x y) * 170 [ #TT #_ @T @TT // 171  #_ #FF @F % #E destruct lapply (FF (refl ??)) #E destruct 172 ] qed. 173 151 174 definition RTLabs_deqset : DeqSet ≝ mk_DeqSet RTLabs_pc RTLabs_pc_eq ?. 152 whd in match RTLabs_pc_eq; whd in match eq_option; whd in match block_eq;153 * [ #b1 #l1  #b 1  * [2: #b1 ] ]154 * [ 1,5,9,13 ,17: #b2 #l2  2,6,10,14,18: #b2  3,7,11,15,19: * [2,4,6,8,10: #b2] *: ]175 whd in match RTLabs_pc_eq; 176 * [ #b1 #l1  #bl1 #b1  #ob1  ] 177 * [ 1,5,9,13: #b2 #l2  2,6,10,14: #bl2 #b2  3,7,11,15: #ob2  *: ] 155 178 normalize nodelta 156 [ 1,7,13: @eq_block_elim [ 1,3,5: #E destruct  *: * #NE ] ] 157 [ 1,4: @eq_identifier_elim [ 1,3: #E destruct  *: * #NE ] ] 179 [ @eq_block_elim [ #E destruct  * #NE ] ] 180 [ @eq_identifier_elim [ #E destruct  *: * #NE ] ] 181 [ 8,13: @eqb_elim [ 1,3: #E destruct  *: * #NE ] ] 182 [ @eq_block_elim [ #E destruct  * #NE ] ] 158 183 normalize % #E destruct try (cases (NE (refl ??))) @refl 159 184 qed. … … 163 188 match s' return λs'. Ras_Fn_Match ? s' ? → ? with 164 189 [ State f fs m ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  cons b _ ⇒ λ_. rapc_state b (next … f) ] 165  Callstate _ _ _ _ _ ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  cons b _ ⇒ λ_. rapc_callb ]190  Callstate _ _ _ fs _ ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  cons b _ ⇒ λ_. rapc_call (match fs with [ nil ⇒ None ?  cons f _ ⇒ Some ? (next f) ]) b ] 166 191  Returnstate _ _ _ _ ⇒ match stk with [ nil ⇒ λ_. rapc_ret (None ?)  cons b _ ⇒ λ_. rapc_ret (Some ? b) ] 167 192  Finalstate _ ⇒ λmtc. rapc_fin
Note: See TracChangeset
for help on using the changeset viewer.