Changeset 3031 for src/RTLabs/RTLabs_abstract.ma
 Timestamp:
 Mar 29, 2013, 12:38:41 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLabs_abstract.ma
r2895 r3031 323 323 #ge #s #E % #C >(proj2 … (RTLabs_costed ??)) in E; // #E destruct 324 324 qed. 325 326 (* Build a fullexec for the extended semantics, so that we can go on to make 327 a preclassified system later. *) 328 329 330 definition eval_ext_statement : ∀ge. RTLabs_ext_state ge → IO io_out io_in (trace × (RTLabs_ext_state ge)) ≝ 331 λge,s. 332 match eval_statement ge s return λx. (∀s',t. x = Value ??? 〈t,s'〉 → RTLabs_ext_state ge) → ? with 333 [ Value ts ⇒ λnext. Value ??? 〈\fst ts, next (\snd ts) (\fst ts) ?〉 334  Wrong m ⇒ λ_. Wrong ??? m 335  Interact o k ⇒ λ_. Wrong … (msg UnexpectedIO) 336 ] (next_state ge s). 337 // 338 qed. 339 340 lemma drop_exec_ext : ∀ge,s,tr,s'. 341 eval_ext_statement ge s = return 〈tr,s'〉 → 342 eval_statement ge s = return 〈tr,Ras_state … s'〉. 343 #ge #s #tr #s' 344 whd in ⊢ (??%? → ?); 345 letin f ≝ (next_state ge s) (* Is there a more natural way to generalize partial applications? *) 346 cut (∀s',t,EV. Ras_state … (f s' t EV) = s') 347 [ // ] 348 generalize in match f; f 349 cases (eval_statement ge s) 350 [ #o #k #n #N #E whd in E:(??%%); destruct 351  * #tr' #s'' #next #NEXT #E whd in E:(??%%); destruct >NEXT // 352  #m #n #N #E whd in E:(??%%); destruct 353 ] qed. 354 355 lemma as_eval_ext_statement : ∀ge,s,tr,s'. 356 eval_ext_statement ge s = Value … 〈tr,s'〉 → 357 as_execute (RTLabs_status ge) s s'. 358 #ge #s #tr #s' #EX 359 whd %{tr} %{(drop_exec_ext … EX)} 360 whd in EX:(??%?); 361 letin ns ≝ (next_state ge s) in EX; #EX 362 change with (ns s' tr ?) in match (next_state ge s s' tr ?); 363 generalize in match (drop_exec_ext ?????); 364 #EX' 365 generalize in match ns in EX ⊢ %; ns >EX' #ns whd in ⊢ (??%? → %); 366 #E destruct @e1 367 qed. 368 369 definition RTLabs_ext_exec : trans_system io_out io_in ≝ 370 mk_trans_system io_out io_in ? RTLabs_ext_state (λ_.RTLabs_is_final) eval_ext_statement. 371 372 definition make_ext_initial_state : ∀p:RTLabs_program. res (RTLabs_ext_state (make_global p)) ≝ 373 λp. 374 let ge ≝ make_global p in 375 do m ← init_mem … (λx.x) p; 376 let main ≝ prog_main ?? p in 377 do b as Eb ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main); 378 do f as Ef ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr … ge b); 379 let s ≝ Callstate main f (nil ?) (None ?) (nil ?) m in 380 return (mk_RTLabs_ext_state (make_global p) s [b] ?). 381 % [ % assumption  % ] 382 qed. 383 384 lemma initial_states_OK : ∀p,s. 385 make_ext_initial_state p = return s → 386 make_initial_state p = return (Ras_state … s). 387 #p #s #E 388 cases (bind_inversion ????? E) E #m * #E1 #E 389 cases (bind_as_inversion ????? E) E #b * #Eb #E 390 cases (bind_as_inversion ????? E) E #f * #Ef #E 391 whd in ⊢ (??%?); >E1 392 whd in ⊢ (??%?); >Eb 393 whd in ⊢ (??%?); >Ef 394 whd in E:(??%%) ⊢ (??%?); destruct 395 % 396 qed. 397 398 lemma initial_states_OK' : ∀p,s. 399 make_initial_state p = return s → 400 ∃S,M. make_ext_initial_state p = return (mk_RTLabs_ext_state (make_global p) s S M). 401 #p #s #E 402 cases (bind_inversion ????? E) E #m * #E1 #E 403 cases (bind_inversion ????? E) E #b * #Eb #E 404 cases (bind_inversion ????? E) E #f * #Ef #E 405 whd in E:(??%%); destruct 406 %{[b]} % [ % [ % assumption  % ] ] 407 whd in ⊢ (??%?); >E1 408 whd in ⊢ (??%?); generalize in match (refl ??); 409 >Eb in ⊢ (???% → ??(match % with [_⇒?_⇒?]?)?); #Eb' 410 whd in ⊢ (??%?); generalize in match (refl ??); 411 >Ef in ⊢ (???% → ??(match % with [_⇒?_⇒?]?)?); #Ef' % 412 qed. 413 414 415 definition RTLabs_ext_fullexec : fullexec io_out io_in ≝ 416 mk_fullexec … RTLabs_ext_exec make_global make_ext_initial_state. 417
Note: See TracChangeset
for help on using the changeset viewer.