Ignore:
Timestamp:
Mar 29, 2013, 12:38:41 PM (7 years ago)
Author:
campbell
Message:

Tidy up RTLabs preclassified_system definitions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs_abstract.ma

    r2895 r3031  
    323323#ge #s #E % #C >(proj2 … (RTLabs_costed ??)) in E; // #E destruct
    324324qed.
     325
     326(* Build a fullexec for the extended semantics, so that we can go on to make
     327   a preclassified system later. *)
     328
     329
     330definition eval_ext_statement : ∀ge. RTLabs_ext_state ge → IO io_out io_in (trace × (RTLabs_ext_state ge)) ≝
     331λge,s.
     332match 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//
     338qed.
     339
     340lemma 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'
     344whd in ⊢ (??%? → ?);
     345letin f ≝ (next_state ge s) (* Is there a more natural way to generalize partial applications? *)
     346cut (∀s',t,EV. Ras_state … (f s' t EV) = s')
     347[ // ]
     348generalize in match f; -f
     349cases (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
     355lemma 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
     359whd %{tr} %{(drop_exec_ext … EX)}
     360whd in EX:(??%?);
     361letin ns ≝ (next_state ge s) in EX; #EX
     362change with (ns s' tr ?) in match (next_state ge s s' tr ?);
     363generalize in match (drop_exec_ext ?????);
     364#EX'
     365generalize in match ns in EX ⊢ %; -ns >EX' #ns whd in ⊢ (??%? → %);
     366#E destruct @e1
     367qed.
     368
     369definition 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
     372definition 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 | % ]
     382qed.
     383
     384lemma 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
     388cases (bind_inversion ????? E) -E #m * #E1 #E
     389cases (bind_as_inversion ????? E) -E #b * #Eb #E
     390cases (bind_as_inversion ????? E) -E #f * #Ef #E
     391whd in ⊢ (??%?); >E1
     392whd in ⊢ (??%?); >Eb
     393whd in ⊢ (??%?); >Ef
     394whd in E:(??%%) ⊢ (??%?); destruct
     395%
     396qed.
     397
     398lemma 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
     402cases (bind_inversion ????? E) -E #m * #E1 #E
     403cases (bind_inversion ????? E) -E #b * #Eb #E
     404cases (bind_inversion ????? E) -E #f * #Ef #E
     405whd in E:(??%%); destruct
     406%{[b]} % [ % [ % assumption | % ] ]
     407whd in ⊢ (??%?); >E1
     408whd in ⊢ (??%?); generalize in match (refl ??);
     409>Eb in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?); #Eb'
     410whd in ⊢ (??%?); generalize in match (refl ??);
     411>Ef in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?); #Ef' %
     412qed.
     413
     414
     415definition 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.