Changeset 2571 for src/RTLabs/abstract.ma
 Timestamp:
 Jan 8, 2013, 5:46:04 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/abstract.ma
r2511 r2571 201 201 *) 202 202 203 definition RTLabs_after_return : ∀ge. (Σs:RTLabs_ext_state ge. RTLabs_classify s =cl_call) → RTLabs_ext_state ge → Prop ≝203 definition RTLabs_after_return : ∀ge. (Σs:RTLabs_ext_state ge. Some ? (RTLabs_classify s) = Some ? cl_call) → RTLabs_ext_state ge → Prop ≝ 204 204 λge,s,s'. 205 205 match s with 206 206 [ mk_Sig s p ⇒ 207 match s return λs. RTLabs_classify s =cl_call → ? with207 match s return λs. Some ? (RTLabs_classify s) = Some ? cl_call → ? with 208 208 [ Callstate fd args dst stk m ⇒ 209 209 λ_. match s' with … … 219 219 ] p 220 220 ]. 221 [ whd in H:(?? %?);221 [ whd in H:(??(??%)?); 222 222 cases (next_instruction f) in H; 223 223 normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct … … 226 226 ] qed. 227 227 228 definition RTLabs_call_ident : ∀ge. (Σs:RTLabs_ext_state ge. RTLabs_classify s =cl_call) → ident ≝228 definition RTLabs_call_ident : ∀ge. (Σs:RTLabs_ext_state ge. Some ? (RTLabs_classify s) = Some ? cl_call) → ident ≝ 229 229 λge,s. 230 230 match s with 231 231 [ mk_Sig s p ⇒ 232 match s return λs':RTLabs_ext_state ge. RTLabs_classify s' =cl_call → ident with232 match s return λs':RTLabs_ext_state ge. Some ? (RTLabs_classify s') = Some ? cl_call → ident with 233 233 [ mk_RTLabs_ext_state s' stk mtc0 ⇒ 234 match s' return λs'. Ras_Fn_Match ? s' ? → RTLabs_classify s' =cl_call → ident with234 match s' return λs'. Ras_Fn_Match ? s' ? → Some ? (RTLabs_classify s') = Some ? cl_call → ident with 235 235 [ Callstate fd _ _ _ _ ⇒ 236 236 match stk return λstk. Ras_Fn_Match ?? stk → ? → ident with … … 243 243 ] p 244 244 ]. 245 [ whd in H:(?? %?);245 [ whd in H:(??(??%)?); 246 246 cases (next_instruction f) in H; 247 247 normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct … … 251 251 ] qed. 252 252 253 lemma RTLabs_notail : ∀s. 254 RTLabs_classify s = cl_tailcall → 255 False. 256 * [ #f #fs #m whd in ⊢ (??%? → ?); cases (next_instruction f) ] 257 normalize 258 #a try #b try #c try #d try #e try #g try #h try #i try #j destruct 259 qed. 260 261 (* Roughly corresponding to as_classifier *) 262 lemma RTLabs_notail' : ∀s. 263 Some ? (RTLabs_classify s) = Some ? cl_tailcall → 264 False. 265 #s #E @(RTLabs_notail … s) 266 generalize in match (RTLabs_classify s) in E ⊢ %; 267 #c #E' destruct % 268 qed. 253 269 254 270 definition RTLabs_status : genv → abstract_status ≝ … … 259 275 RTLabs_deqset 260 276 (RTLabs_ext_state_to_pc ge) 261 RTLabs_classify277 (λs. Some ? (RTLabs_classify s)) 262 278 (RTLabs_pc_to_cost_label ge) 263 279 (RTLabs_after_return ge) 264 280 (λs. RTLabs_is_final s ≠ None ?) 265 (RTLabs_call_ident ge). 266 267 281 (RTLabs_call_ident ge) 282 (λs. ⊥). 283 (* No tailcalls here for now. *) 284 cases s @RTLabs_notail' 285 qed. 268 286 269 287 (* Allow us to move between the different notions of when a state is cost
Note: See TracChangeset
for help on using the changeset viewer.